Support for Coq 8.20 (#63)

Author: wjbs

.github/workflows/coq-action.yml

@@ -15,6 +15,8 @@ jobs:
           - '8.16'
           - '8.17'
           - '8.18'
+          - '8.19'
+          - '8.20'
         ocaml_version:
           - 'default'
       fail-fast: false # don't stop jobs if one fails
@@ -33,6 +35,8 @@ jobs:
           - '8.16'
           - '8.17'
           - '8.18'
+          - '8.19'
+          - '8.20'
         ocaml_version:
           - 'default'
       fail-fast: false # don't stop jobs if one fails

README.md

@@ -28,7 +28,7 @@ If you are interested in learning more about formal verification of quantum prog
 
 ## Setup
 
-To compile SQIR and VOQC, you will need [Coq](https://coq.inria.fr/) and [QuantumLib](https://github.com/inQWIRE/QuantumLib) (version 1.1.0). In order to build the Shor proof, you will also need the [Coq Interval package](http://coq-interval.gforge.inria.fr/) and the [coq-euler](https://github.com/taorunz/euler) library. We strongly recommend using [opam](https://opam.ocaml.org/doc/Install.html) to install Coq and `opam switch` to manage Coq versions. We currently support Coq **versions 8.12-8.16**. If you run into errors when compiling our proofs, first check your version of Coq (`coqc -v`).
+To compile SQIR and VOQC, you will need [Coq](https://coq.inria.fr/) and [QuantumLib](https://github.com/inQWIRE/QuantumLib) (version 1.7.0). In order to build the Shor proof, you will also need the [Coq Interval package](http://coq-interval.gforge.inria.fr/) and the [coq-euler](https://github.com/taorunz/euler) library. We strongly recommend using [opam](https://opam.ocaml.org/doc/Install.html) to install Coq and `opam switch` to manage Coq versions. We currently support Coq **versions 8.16-8.20**. If you run into errors when compiling our proofs, first check your version of Coq (`coqc -v`).
 
 Assuming you have opam installed (following the instructions in the link above), follow the steps below to set up your environment.
 ```
@@ -46,7 +46,7 @@ opam install coq
 # install the QuantumLib library
 opam repo add coq-released https://coq.inria.fr/opam/released
 opam update
-opam install coq-quantumlib.1.1.0
+opam install coq-quantumlib.1.7.0
 
 # Optional, if you want to compile the proofs in examples/shor
 opam install coq-interval
@@ -55,7 +55,7 @@ opam pin coq-euler https://github.com/taorunz/euler.git
 
 *Notes*:
 * Depending on your system, you may need to replace 4.13.1 in the instructions above with something like "ocaml-base-compiler.4.13.1". Any recent version of OCaml should be fine.
-* We require Coq version >= 8.12.
+* We require Coq version >= 8.16.
 * opam error messages and warnings are typically informative, so if you run into trouble then make sure you read the console output.
 
 ## Compilation

VOQC/ConnectivityGraph.v

@@ -1158,7 +1158,7 @@ Proof.
       rewrite (Nat.mul_comm (n1 / numCols)).
       rewrite (Nat.mul_comm (n2 / numCols)).
       assert (numCols * (n1 / numCols) < numCols * (n2 / numCols)).
-      { apply mult_lt_compat_l; assumption. }
+      { nia. }
       remember (numCols * (n1 / numCols)) as x.
       remember (numCols * (n2 / numCols)) as y.
       clear - Haux1 Haux2 H1 H2.
@@ -1183,7 +1183,7 @@ Proof.
       rewrite (Nat.mul_comm (n1 / numCols)).
       rewrite (Nat.mul_comm (n2 / numCols)).
       assert (numCols * (n1 / numCols) <= numCols * (n2 / numCols)).
-      { apply mult_le_compat_l; lia. }
+      { nia. }
       remember (numCols * (n1 / numCols)) as x.
       remember (numCols * (n2 / numCols)) as y.
       clear - Haux1 Haux2 H2 H3.
@@ -1202,7 +1202,7 @@ Proof.
       rewrite (Nat.mul_comm (n1 / numCols)).
       rewrite (Nat.mul_comm (n2 / numCols)).
       assert (numCols * (n1 / numCols) < numCols * (n2 / numCols)).
-      { apply mult_lt_compat_l; assumption. }
+      { nia. }
       remember (numCols * (n1 / numCols)) as x.
       remember (numCols * (n2 / numCols)) as y.
       clear - Haux1 Haux2 H1 H4.
@@ -1223,7 +1223,7 @@ Proof.
       (* In Coq v8.10, the goal is solved by the previous line. *)
       try (rewrite Nat.add_sub_assoc; try assumption; 
            assert (numCols * (n2 / numCols) < numCols * (n1 / numCols));
-           [ apply mult_lt_compat_l; assumption 
+           [ nia 
            |  remember (numCols * (n1 / numCols)) as x;
               remember (numCols * (n2 / numCols)) as y;
               clear - Haux1 Haux2 H0 H1;
@@ -1270,7 +1270,7 @@ Proof.
       rewrite (Nat.mul_comm (n1 / numCols)).
       rewrite (Nat.mul_comm (n2 / numCols)).
       assert (numCols * (n2 / numCols) <= numCols * (n1 / numCols)).
-      { apply mult_le_compat_l; lia. }
+      { nia. }
       remember (numCols * (n1 / numCols)) as x.
       remember (numCols * (n2 / numCols)) as y.
       clear - Haux1 Haux2 H1 H2.

VOQC/Main.v

@@ -997,6 +997,13 @@ Proof.
   contradiction.
 Qed.
 
+Section with_permutations. 
+
+Import Permutations. 
+
+Local Hint Resolve get_phys_perm get_log_perm : perm_db.
+
+
 Lemma check_swap_equivalence_correct : forall dim (c1 c2 : circ dim) (lay1 lay2 : layout),
   uc_well_typed_l c1 ->
   uc_well_typed_l c2 ->
@@ -1013,21 +1020,23 @@ Proof.
     (fun n : nat => MappingGateSet.match_gate match_gate)) eqn:mv.
   assert (mvWF:=mv).
   destruct p.
-  2: inversion H.
-  apply MVP.check_swap_equivalence_implies_equivalence in mv; 
-    auto using full_to_map_WT.
-  apply MVP.check_swap_equivalence_layouts_WF in mvWF as [? ?]; 
-    auto using full_to_map_WT.
+  2: { inversion H. }
+  apply MVP.check_swap_equivalence_implies_equivalence in mv;
+    [|solve [auto using full_to_map_WT]..].
+  apply MVP.check_swap_equivalence_layouts_WF in mvWF as [? ?];
+    [|solve [auto using full_to_map_WT]..].
   unfold MVP.SRP.uc_equiv_perm_ex in mv.
   exists (get_phys lay1 ∘ get_log lay2)%prg.
   exists (get_phys l0 ∘ get_log l)%prg.
-  repeat split; [auto with perm_db..|].
+  repeat split; [PermutationAutomation.auto_perm..|].
   unfold eval.
   unfold MVP.SRP.MapList.eval in mv.
   rewrite <- 2 list_to_ucom_full_to_map in mv.
   apply mv.
 Qed.
 
+End with_permutations.
+
 Lemma check_constraints_correct : forall dim (c : circ dim) (cg : c_graph),
   check_constraints c cg = true ->
   respects_constraints_directed (is_in_graph cg) MappingGateSet.UMap_CNOT (full_to_map c).

VOQC/MappingValidation.v

@@ -114,6 +114,8 @@ Module MappingValidationProofs (G : GateSet).
 Module SRP := SwapRouteProofs G.
 Import SRP.
 
+Local Hint Resolve get_phys_perm get_log_perm : perm_db.
+
 Lemma remove_swaps'_sound : forall {dim} (l l' : ucom_l dim) m m' acc,
   uc_well_typed_l l ->
   layout_bijective dim m ->
@@ -165,7 +167,7 @@ Proof.
         constructor.
         apply uc_well_typed_l_implies_dim_nonzero in WT.
         assumption.
-      * apply IHl in H; auto with perm_db.
+      * apply IHl in H; [|solve [auto using swap_log_preserves_bij with perm_db]..].
         destruct H as [l0 [? ?]].
         exists l0. subst. split; auto.
         rewrite (cons_to_app _ l).
@@ -183,7 +185,8 @@ Proof.
         repeat rewrite Mmult_assoc.
         rewrite f_to_vec_SWAP by assumption.
         Msimpl.
-        rewrite perm_to_matrix_permutes_qubits by auto with perm_db.
+        rewrite perm_to_matrix_permutes_qubits 
+          by auto using swap_log_preserves_bij with perm_db.
         apply f_to_vec_eq.        
         intros x Hx.
         rewrite fswap_swap_log with (dim:=dim) by assumption.
@@ -256,6 +259,7 @@ Proof.
   apply remove_swaps_WF in rs2; auto.
 Qed.
 
+
 (** If check_swap_equivalence returns Some then l1 and l2 are equivalent programs 
     wrt to layouts m1 and m2. *)
 Lemma check_swap_equivalence_implies_equivalence : forall {dim} (l1 l2 : ucom_l dim) m1 m2 m1' m2',
@@ -275,22 +279,23 @@ Proof.
   apply remove_swaps'_bijective in rs1'; auto.
   apply remove_swaps'_bijective in rs2'; auto.
   destruct (equalb m m0 (fun n : nat => MapG.match_gate)) eqn:eq.
-  inversion H; subst.
-  apply MapList.equalb_correct in eq.
-  unfold uc_equiv_perm_ex, MapList.eval in *.
-  unfold MapList.uc_equiv_l, uc_equiv in *.
-  rewrite rs1, rs2, eq.
-  rewrite <- 2 perm_to_matrix_Mmult by auto with perm_db.
-  repeat rewrite Mmult_assoc.
-  apply f_equal2; try reflexivity.
-  repeat rewrite <- Mmult_assoc.
-  apply f_equal2; try reflexivity.
-  rewrite perm_to_matrix_Mmult by auto with perm_db.
-  repeat rewrite Mmult_assoc.
-  rewrite perm_to_matrix_Mmult by auto with perm_db.
-  rewrite 2 perm_to_matrix_I by eauto with perm_inv_db.
-  Msimpl. reflexivity.
-  inversion H.
+  - inversion H; subst.
+    apply MapList.equalb_correct in eq.
+    unfold uc_equiv_perm_ex, MapList.eval in *.
+    unfold MapList.uc_equiv_l, uc_equiv in *.
+    rewrite rs1, rs2, eq.
+    rewrite 2 perm_to_matrix_compose by auto_perm.
+    repeat rewrite Mmult_assoc.
+    apply f_equal2; try reflexivity.
+    repeat rewrite <- Mmult_assoc.
+    apply f_equal2; try reflexivity.
+    rewrite <- perm_to_matrix_compose by auto_perm.
+    repeat rewrite Mmult_assoc.
+    rewrite <- perm_to_matrix_compose by auto_perm.
+    rewrite 2 perm_to_matrix_I by 
+      (intros; apply get_log_phys_inv with (n:=dim); auto).
+    Msimpl. reflexivity.
+  - inversion H.
 Qed.
 
 Lemma check_constraints_implies_respect_constraints : forall {dim} (l : ucom_l dim) is_in_graph,

VOQC/SwapRoute.v

@@ -170,7 +170,7 @@ Proof.
   - apply equal_on_basis_states_implies_equal; auto with wf_db.
     intro f.
     repeat rewrite Mmult_assoc.
-    rewrite perm_to_matrix_permutes_qubits by auto with perm_bounded_db.
+    rewrite perm_to_matrix_permutes_qubits by auto_perm.
     assert (p2 n < dim).
     { destruct H1 as [? H1].
       specialize (H1 n H5).
@@ -196,7 +196,7 @@ Proof.
         with (f_to_vec (dim - (n + 1)) (shift f0 (n + 1))).
       replace (dim - (n + 1)) with (dim - 1 - n) by lia.
       rewrite <- f_to_vec_split by auto.
-      rewrite perm_to_matrix_permutes_qubits by auto with perm_bounded_db.
+      rewrite perm_to_matrix_permutes_qubits by auto_perm.
       remember (update (fun x : nat => f (p1 x)) (p2 n) false) as f0'.
       replace (f_to_vec dim (fun x : nat => f0 (p1 x))) with (f_to_vec dim f0').
       rewrite (f_to_vec_split 0 dim (p2 n)) by auto.
@@ -223,7 +223,7 @@ Proof.
         with (f_to_vec (dim - (n + 1)) (shift f1 (n + 1))).
       replace (dim - (n + 1)) with (dim - 1 - n) by lia.
       rewrite <- f_to_vec_split by auto.
-      rewrite perm_to_matrix_permutes_qubits by auto with perm_bounded_db.
+      rewrite perm_to_matrix_permutes_qubits by auto_perm.
       remember (update (fun x : nat => f (p1 x)) (p2 n) true) as f1'.
       replace (f_to_vec dim (fun x : nat => f1 (p1 x))) with (f_to_vec dim f1').
       rewrite (f_to_vec_split 0 dim (p2 n)) by auto.
@@ -246,10 +246,10 @@ Proof.
   - apply equal_on_basis_states_implies_equal; auto with wf_db.
     intro f.
     repeat rewrite Mmult_assoc.
-    rewrite perm_to_matrix_permutes_qubits by auto with perm_bounded_db.
+    rewrite perm_to_matrix_permutes_qubits by auto_perm.
     replace (ueval_cnot dim n n0) with (uc_eval (@SQIR.CNOT dim n n0)) by reflexivity.
     rewrite f_to_vec_CNOT by assumption.
-    rewrite perm_to_matrix_permutes_qubits by auto with perm_bounded_db.
+    rewrite perm_to_matrix_permutes_qubits by auto_perm.
     replace (ueval_cnot dim (p2 n) (p2 n0)) 
       with (uc_eval (@SQIR.CNOT dim (p2 n) (p2 n0))) by reflexivity.
     assert (p2 n < dim).
@@ -303,7 +303,7 @@ Proof.
   unfold eval; simpl.
   rewrite denote_SKIP by assumption.
   Msimpl.
-  rewrite perm_to_matrix_Mmult, perm_to_matrix_I; auto.
+  rewrite <- perm_to_matrix_compose, perm_to_matrix_I; auto_perm.
 Qed.
 
 Lemma SWAP_well_typed : forall dim a b,
@@ -505,7 +505,7 @@ Proof.
   rewrite (perm_to_matrix_I _ (p1inv ∘ p1)%prg).
   Msimpl.
   reflexivity.
-  auto.
+  unfold eval; auto with wf_db.
 Qed.
 
 Lemma uc_equiv_perm_ex_app2 : forall {dim} (l1 l2 : ucom_l dim) (g : gate_app (Map_Unitary (G.U 1)) dim) p1 p2 p3,

VOQC/UnitaryListRepresentation.v

@@ -1321,15 +1321,12 @@ Proof.
   exists (perm_inv dim p2).
   repeat split; auto with perm_db.
   rewrite H.
-  rewrite <- !perm_to_matrix_transpose_eq by easy.
-  rewrite !Mmult_assoc.
-  restore_dims.
-  rewrite 2!perm_to_matrix_transpose_eq, 
-    <- perm_to_matrix_compose by auto with perm_bounded_db.
-  rewrite <- !Mmult_assoc.
-  rewrite <- perm_to_matrix_compose by auto with perm_bounded_db.
-  rewrite 2!perm_to_matrix_I by (intros; cleanup_perm_inv).
-  now Msimpl.
+  repeat rewrite Mmult_assoc.
+  rewrite <- perm_to_matrix_compose by auto_perm.  
+  repeat rewrite <- Mmult_assoc.
+  rewrite <- perm_to_matrix_compose by auto_perm.
+  rewrite 2 perm_to_matrix_I by (intros; cleanup_perm_inv).
+  unfold eval. Msimpl. reflexivity.
 Qed.
 
 Lemma uc_equiv_perm_trans : forall {dim} (l1 l2 l3 : gate_list G.U dim), 
@@ -1342,10 +1339,8 @@ Proof.
   rewrite H1, H2.
   exists (p1 ∘ p3)%prg.
   exists (p4 ∘ p2)%prg.
-  repeat split.
-  apply permutation_compose; auto.
-  apply permutation_compose; auto.
-  rewrite <- 2 perm_to_matrix_Mmult; auto with perm_bounded_db.
+  repeat split; [solve [auto using permutation_compose]..|].
+  rewrite 2 perm_to_matrix_compose; auto using permutation_is_bounded.
   repeat rewrite Mmult_assoc.
   reflexivity.
 Qed.

dune-project

@@ -1,6 +1,6 @@
 (lang dune 3.8)
 (name coq-sqirvoqc)
-(version 1.3.1)
+(version 1.4.0)
 (using coq 0.7)
 (generate_opam_files true)
 
@@ -17,7 +17,7 @@
  )
  (depends
    (coq-interval (>= 4.9.0))
-   (coq-quantumlib (>= 1.5.0))
+   (coq-quantumlib (>= 1.7.0))
    (coq (>= 8.16))))
 
 (package
@@ -28,6 +28,6 @@
  )
  (depends
    (coq-interval (>= 4.9.0))
-   (coq-quantumlib (>= 1.5.0))
-   (coq-sqir (>= 1.3.0))
+   (coq-quantumlib (>= 1.7.0))
+   (coq-sqir (>= 1.4.0))
    (coq (>= 8.16))))