Update Coq version support

.github/workflows/coq-action.yml

@@ -12,13 +12,9 @@ jobs:
     strategy:
       matrix:
         coq_version:
-          - '8.12'
-          - '8.13'
-          - '8.14'
-          - '8.15'
           - '8.16'
           - '8.17'
-          - 'dev'
+          - '8.18'
         ocaml_version:
           - 'default'
       fail-fast: false # don't stop jobs if one fails
@@ -34,13 +30,9 @@ jobs:
     strategy:
       matrix:
         coq_version:
-          - '8.12'
-          - '8.13'
-          - '8.14'
-          - '8.15'
           - '8.16'
           - '8.17'
-          - 'dev'
+          - '8.18'
         ocaml_version:
           - 'default'
       fail-fast: false # don't stop jobs if one fails

README.md

@@ -67,7 +67,7 @@ Our proofs are resource intensive so expect `make all` to take a little while. I
 ## Using With Other Projects
 
 To install SQIR, run 
-```opam pin coq-sqir htts://github.com/inQWIRE/SQIR.git```
+```opam pin coq-sqir https://github.com/inQWIRE/SQIR.git```
 
 To pull subsequent updates, run `opam install coq-sqir`. 
 

SQIR/Equivalences.v

@@ -1,5 +1,6 @@
 Require Export QuantumLib.VectorStates.
 Require Export UnitaryOps.
+Require Export SQIR.
 
 Local Open Scope ucom_scope.
 Local Close Scope C_scope.

SQIR/GateDecompositions.v

@@ -68,7 +68,7 @@ Definition C4X {dim} (a b c d e : nat) : base_ucom dim :=
   invert (RC3X a b c d) ;
   C3SQRTX a b c e.
 
-Hint Rewrite <- RtoC_minus : RtoC_db.
+#[export] Hint Rewrite <- RtoC_minus : RtoC_db.
 
 Local Transparent H U3.
 Lemma CH_is_control_H : forall dim a b, @CH dim a b ≡ control a (H b).
@@ -97,6 +97,13 @@ Proof.
                   Ci * Ci * cos (PI / 2 / 2 / 2) * cos (PI / 2 / 2 / 2))
          with (- (cos (PI / 2 / 2 / 2) * cos (PI / 2 / 2 / 2) - 
                  sin (PI / 2 / 2 / 2) * sin (PI / 2 / 2 / 2))) by lca.
+    all: autorewrite with RtoC_db; apply c_proj_eq; simpl; autorewrite with R_db;
+    try rewrite <- Rminus_unfold; try rewrite <- cos_2a; try rewrite <- sin_2a;
+    replace (2 * (PI * / 4 * / 2))%R with (PI * / 4)%R by lra;
+    replace (2 * (PI * / 2 * / 2 * / 2))%R with (PI * / 4)%R by lra;
+    try symmetry; try apply sin_cos_PI4; try reflexivity; 
+    try rewrite Ropp_eq_compat with (cos (PI * / 4)) (sin (PI * / 4));
+    try reflexivity; try symmetry; try apply sin_cos_PI4; try reflexivity.
     all: autorewrite with RtoC_db; rewrite <- sin_2a; rewrite <- cos_2a;
          replace (2 * (PI / 4 / 2))%R with (PI / 4)%R by lra;
          replace (2 * (PI / 2 / 2 / 2))%R with (PI / 4)%R by lra;
@@ -107,12 +114,8 @@ Proof.
   { assert (aux: forall x, (x * x = x²)%R) by (unfold Rsqr; reflexivity).
     solve_matrix; repeat rewrite RIneq.Ropp_div; autorewrite with Cexp_db trig_db; 
       repeat rewrite RtoC_opp; field_simplify_eq; try nonzero; 
-      autorewrite with RtoC_db; repeat rewrite aux.
-    rewrite 2 (Rplus_comm ((cos _)²)).
-    rewrite 2 sin2_cos2.
-    reflexivity.
-    rewrite 2 sin2_cos2.
-    reflexivity. }
+    autorewrite with RtoC_db; repeat rewrite aux;
+    replace (PI / 2 / 2 / 2)%R with (PI / 4 / 2)%R by lra; reflexivity. }
   intros dim a b.
   unfold H, CH, uc_equiv.
   simpl.

SQIR/NDSem.v

@@ -108,15 +108,21 @@ Proof.
     + contradict H0.
       rewrite <- Mmult_assoc.
       rewrite proj_twice_neq by easy.
-      unfold norm. 
-      Msimpl; simpl.
-      apply sqrt_0.
+      try Msimpl.
+      try (
+        unfold norm; 
+        Msimpl; simpl;
+        apply sqrt_0
+      ).
+      try apply norm_zero_iff_zero. try apply WF_Zero. try easy.
     + contradict H0. 
       rewrite <- Mmult_assoc.
       rewrite proj_twice_neq by easy.
       unfold norm. 
       Msimpl; simpl.
-      apply sqrt_0.
+      try apply sqrt_0.
+      try apply norm_zero_iff_zero. try apply WF_Zero.
+      try easy.
     + rewrite <- Mmult_assoc in H0, H1.
       rewrite proj_twice_eq in H0, H1.
       apply nd_meas_f; assumption.

SQIR/UnitaryOps.v

@@ -52,7 +52,7 @@
 
 (* A few common inverses *)
 
-Hint Rewrite sin_neg cos_neg : trig_db.
+#[export] Hint Rewrite sin_neg cos_neg : trig_db.
 
 Lemma invert_CNOT : forall dim m n, invert (@CNOT dim m n) ≡ CNOT m n.
 Proof. intros. reflexivity. Qed.
@@ -66,7 +66,7 @@
   gridify.
   do 2 (apply f_equal2; try reflexivity).
   unfold rotation. 
   solve_matrix; try rewrite Ropp_div; autorewrite with Cexp_db trig_db; lca.
 Qed.
 Local Opaque X.
 
@@ -79,7 +79,7 @@
   gridify.
   do 2 (apply f_equal2; try reflexivity).
   unfold rotation. 
   solve_matrix; try rewrite Ropp_div; autorewrite with Cexp_db trig_db; lca.
 Qed.
 Local Opaque H.
 
@@ -387,15 +387,15 @@
 Lemma bra1_phase : forall ϕ, bra 1 × phase_shift ϕ = Cexp ϕ .* bra 1.
 Proof. intros; solve_matrix. Qed.
 
-Hint Rewrite bra0_phase bra1_phase : bra_db.
+#[export] Hint Rewrite bra0_phase bra1_phase : bra_db.
 
 Lemma braketbra_same : forall x y, bra x × (ket x × bra y) = bra y. 
 Proof. intros. destruct x; destruct y; solve_matrix. Qed.
 
 Lemma braketbra_diff : forall x y z, (x + y = 1)%nat -> bra x × (ket y × bra z) = Zero. 
 Proof. intros. destruct x; destruct y; try lia; solve_matrix. Qed.
 
-Hint Rewrite braketbra_same braketbra_diff using lia : bra_db.
+#[export] Hint Rewrite braketbra_same braketbra_diff using lia : bra_db.
 
 (* Auxiliary proofs about the semantics of CU and TOFF *)
 Lemma CU_correct : forall (dim : nat) θ ϕ λ c t,
@@ -415,11 +415,25 @@
      goal #1 = goal #3 and goal #2 = goal #4 *)
   - solve_matrix; autorewrite with R_db C_db RtoC_db Cexp_db trig_db;
       try lca; field_simplify_eq; try nonzero; group_Cexp.
-    + simpl. rewrite Rplus_comm; setoid_rewrite sin2_cos2; easy.
-    + rewrite Copp_mult_distr_l, Copp_mult_distr_r. 
-      repeat rewrite <- Cmult_assoc; rewrite <- Cmult_plus_distr_l.  
-      autorewrite with RtoC_db. rewrite Ropp_involutive.
-      setoid_rewrite sin2_cos2. rewrite Cmult_1_r.
+    + simpl. try (rewrite Rplus_comm; setoid_rewrite sin2_cos2; easy).
+    try (
+      rewrite Cplus_comm; unfold Cplus, Cmult;
+      autorewrite with R_db; simpl;
+      setoid_rewrite sin2_cos2; easy
+    ).
+    + try (simpl; rewrite Copp_mult_distr_l, Copp_mult_distr_r; 
+      repeat rewrite <- Cmult_assoc; rewrite <- Cmult_plus_distr_l;  
+      autorewrite with RtoC_db; rewrite Ropp_involutive;
+      setoid_rewrite sin2_cos2; rewrite Cmult_1_r;
+      apply f_equal; lra).
+      try (
+      simpl; repeat rewrite <- Cmult_assoc; simpl;
+      rewrite <- Cmult_plus_distr_l; 
+      unfold Cplus, Cmult;
+      autorewrite with R_db; simpl;
+      setoid_rewrite sin2_cos2; autorewrite with R_db;
+      unfold Cexp; apply f_equal2; [apply f_equal; lra|]
+      ).
       apply f_equal; lra.
   - rewrite <- Mscale_kron_dist_l.
     repeat rewrite <- Mscale_kron_dist_r.
@@ -433,9 +447,12 @@
     + unfold Cminus.
       rewrite Copp_mult_distr_r, <- Cmult_plus_distr_l. 
       apply f_equal2; [apply f_equal; lra|].
-      autorewrite with RtoC_db.
+      try (autorewrite with RtoC_db).
+      try (rewrite <- Cminus_unfold;
+      unfold Cminus, Cmult; simpl; autorewrite with R_db;
+      apply c_proj_eq; simpl; autorewrite with R_db).
       rewrite <- Rminus_unfold, <- cos_plus.
-      apply f_equal. apply f_equal. lra.
+      apply f_equal. try apply f_equal. try lra. lra.
     + apply f_equal2; [apply f_equal; lra|].
       apply c_proj_eq; simpl; try lra.
       R_field_simplify.
@@ -453,16 +470,35 @@
     + rewrite Copp_mult_distr_r.
       rewrite <- Cmult_plus_distr_l.
       apply f_equal2; [apply f_equal; lra|].
-      autorewrite with RtoC_db.      
-      rewrite Rplus_comm; rewrite <- Rminus_unfold, <- cos_plus.
-      apply f_equal; apply f_equal; lra.
+      try (autorewrite with RtoC_db;
+      rewrite Rplus_comm; rewrite <- Rminus_unfold, <- cos_plus;
+      apply f_equal; apply f_equal; lra).
+      try (
+        rewrite Cplus_comm; apply c_proj_eq; simpl; try lra;
+      autorewrite with R_db; rewrite <- Rminus_unfold;
+      rewrite <- cos_plus; apply f_equal; lra
+      ).
   - solve_matrix; autorewrite with R_db C_db RtoC_db Cexp_db trig_db; try lca;
       field_simplify_eq; try nonzero; group_Cexp.
-    + rewrite Rplus_comm; setoid_rewrite sin2_cos2; easy.
-    + rewrite Copp_mult_distr_l, Copp_mult_distr_r. 
-      repeat rewrite <- Cmult_assoc; rewrite <- Cmult_plus_distr_l.  
-      autorewrite with RtoC_db. rewrite Ropp_involutive.
-      setoid_rewrite sin2_cos2. rewrite Cmult_1_r.
+    + try (rewrite Rplus_comm; setoid_rewrite sin2_cos2; easy).
+      try (
+        simpl; rewrite Cplus_comm; unfold Cplus, Cmult;
+      autorewrite with R_db; simpl;
+      setoid_rewrite sin2_cos2; easy
+      ).
+    + try (rewrite Copp_mult_distr_l, Copp_mult_distr_r; 
+      repeat rewrite <- Cmult_assoc; rewrite <- Cmult_plus_distr_l; 
+      autorewrite with RtoC_db; rewrite Ropp_involutive;
+      setoid_rewrite sin2_cos2; rewrite Cmult_1_r).
+      try (
+      simpl;
+      repeat rewrite <- Cmult_assoc; simpl;
+      rewrite <- Cmult_plus_distr_l; 
+      unfold Cplus, Cmult;
+      autorewrite with R_db; simpl;
+      setoid_rewrite sin2_cos2; autorewrite with R_db;
+      unfold Cexp; apply f_equal2; [apply f_equal; lra|] 
+      ).
       apply f_equal; lra.
   - rewrite <- 3 Mscale_kron_dist_l.
     repeat rewrite <- Mscale_kron_dist_r.
@@ -474,9 +510,15 @@
     + unfold Cminus.
       rewrite Copp_mult_distr_r, <- Cmult_plus_distr_l. 
       apply f_equal2; [apply f_equal; lra|].
-      autorewrite with RtoC_db.
+      try (autorewrite with RtoC_db).
+      try (
+        repeat rewrite <- Cmult_assoc; simpl;
+      unfold Cplus, Cmult;
+      autorewrite with R_db; simpl;
+      apply c_proj_eq; simpl; try lra
+      ).
       rewrite <- Rminus_unfold, <- cos_plus.
-      apply f_equal. apply f_equal. lra.
+      apply f_equal. try apply f_equal. lra.
     + apply f_equal2; [apply f_equal; lra|].
       apply c_proj_eq; simpl; try lra.
       R_field_simplify.
@@ -494,9 +536,15 @@
     + rewrite Copp_mult_distr_r.
       rewrite <- Cmult_plus_distr_l.
       apply f_equal2; [apply f_equal; lra|].
-      autorewrite with RtoC_db.      
-      rewrite Rplus_comm; rewrite <- Rminus_unfold, <- cos_plus.
-      apply f_equal; apply f_equal; lra.
+      try (autorewrite with RtoC_db;    
+      rewrite Rplus_comm; rewrite <- Rminus_unfold, <- cos_plus;
+      apply f_equal; apply f_equal; lra);
+      try (
+      apply c_proj_eq; simpl; try lra;
+      rewrite Rplus_comm; autorewrite with R_db;
+      rewrite <- Rminus_unfold, <- cos_plus;
+      apply f_equal; lra
+      ).
 Qed.
 
 Lemma UR_not_WT : forall (dim a b : nat) r r0 r1,
@@ -583,7 +631,7 @@
    intros. rewrite denote_H. apply f_to_vec_hadamard; auto.
 Qed.
 
-Hint Rewrite f_to_vec_CNOT f_to_vec_Rz f_to_vec_X using lia : f_to_vec_db.
+#[export] Hint Rewrite f_to_vec_CNOT f_to_vec_Rz f_to_vec_X using lia : f_to_vec_db.
 
 Ltac f_to_vec_simpl_body :=
   autorewrite with f_to_vec_db;

SQIR/UnitarySem.v

@@ -564,9 +564,9 @@ Lemma unfold_ueval_swap : forall dim m n,
       Zero.
 Proof. easy. Qed.
 
-Hint Rewrite denote_H denote_X denote_Y denote_Z denote_ID denote_SKIP 
+#[export] Hint Rewrite denote_H denote_X denote_Y denote_Z denote_ID denote_SKIP 
              denote_Rx denote_Ry denote_Rz denote_cnot denote_swap : eval_db.
-Hint Rewrite unfold_ueval_r unfold_ueval_cnot unfold_ueval_swap unfold_pad unfold_pad_u : eval_db.
+#[export] Hint Rewrite unfold_ueval_r unfold_ueval_cnot unfold_ueval_swap unfold_pad unfold_pad_u : eval_db.
 
 Global Opaque H X Y Z ID Rx Ry Rz CNOT SWAP.
 

VOQC/ChangeRotationBasis.v

@@ -336,7 +336,7 @@
 
 Lemma Cexp_PI2_minus : Cexp (- PI / 2) = (- Ci)%C.
 Proof.
   rewrite Ropp_div.
   unfold Cexp.
   rewrite cos_neg, sin_neg.  
   rewrite cos_PI2, sin_PI2.
@@ -404,7 +404,7 @@
   rewrite sqrt_Rsqr.
   field_simplify_eq; nonzero.
   left.
   rewrite Ropp_inv_permute by lra.
   apply Rinv_0_lt_compat.
   lra.
   unfold Rsqr.
@@ -417,7 +417,7 @@
   rewrite sqrt_Rsqr.
   field_simplify_eq; nonzero.
   left.
   rewrite Ropp_inv_permute by lra.
   apply Rinv_0_lt_compat.
   lra.
   unfold Rsqr.
@@ -505,7 +505,7 @@
 Proof.
   intros. unfold atan2.
   destruct_Rltb. 
   rewrite Ropp_div.
   autorewrite with Cexp_db.
   lca.
 Qed.
@@ -852,7 +852,7 @@
   (m00_R θ1 ξ θ2 / √ k1 θ1 ξ θ2)² + (m00_I θ1 ξ θ2 / √ k1 θ1 ξ θ2)² = 1.
 Proof.
   intros θ1 ξ θ2 H.
   repeat rewrite Rsqr_div; try nonzero.
   rewrite Rsqr_sqrt by lra.
   field_simplify_eq; try nonzero.
   rewrite k1_rewrite.
@@ -920,7 +920,21 @@
        rewrite sqrt_Rsqr by lra.
        rewrite <- Rsqr_pow2.
        rewrite Rsqr_sqrt by lra.
-       lra. }
+       repeat rewrite Rmult_assoc.
+       autorewrite with R_db.
+       replace (-2) with (-(2)) by lra.
+       rewrite Ropp_mult_distr_l_reverse.
+       repeat rewrite Rmult_assoc.
+       rewrite <- Ropp_eq_compat with (k2 θ1 ξ θ2 * (√ k1 θ1 ξ θ2 ^ 4 * 2 ^ 2)) (2 * (k1 θ1 ξ θ2 * (k2 θ1 ξ θ2 * (√ k1 θ1 ξ θ2 ^ 2 * 2)))).
+       reflexivity.
+       simpl.
+       repeat rewrite Rmult_1_r.
+       rewrite Rmult_comm.
+       autorewrite with R_db.
+       repeat rewrite <- Rmult_assoc.
+       rewrite sqrt_def.
+       lra. apply Rlt_le; easy.
+       }
   unfold rm02, rm12.
   replace θ1 with (2 * (θ1 / 2)) by lra.
   replace θ2 with (2 * (θ2 / 2)) by lra.
@@ -1215,7 +1229,7 @@
     repeat rewrite <- Cmult_assoc.
     rewrite (Cmult_assoc (√ _)).
     autorewrite with RtoC_db.
-    rewrite sqrt_def by lra.
+    rewrite Csqrt_sqrt by lra.
     apply m01_rewrite_alt_aux2; assumption.
   - rewrite Cexp_PI2_minus.
     autorewrite with C_db.
@@ -1239,7 +1253,7 @@
     repeat rewrite <- Cmult_assoc.
     rewrite (Cmult_assoc (√ _)).
     autorewrite with RtoC_db.
-    rewrite sqrt_def by lra.
+    rewrite Csqrt_sqrt by lra.
     apply m01_rewrite_alt_aux2; assumption.
   - (* rm12 = 0 and rm02 = 0 forces k2 = 0, which is a contradiction *)
     assert (H: k2 θ1 ξ θ2 = 0). 
@@ -1380,7 +1394,7 @@
   rewrite <- (Cmult_assoc (m00 _ _ _) (√ k2 _ _ _)).
   rewrite <- (Cmult_assoc (m00 _ _ _) (√ k1 _ _ _)).
   autorewrite with RtoC_db.
-  rewrite 2 sqrt_def by lra.
+  rewrite 2 Csqrt_sqrt by lra.
   lca.
   repeat split; try assumption; nonzero.
 Qed.
@@ -1402,8 +1416,8 @@
 Proof. lra. Qed.
 Lemma one_plus_minus_1 : 1 + -1 = 0.
 Proof. lra. Qed.
-Hint Rewrite minus_1_plus_1 one_plus_minus_1 : R_db.
-Hint Rewrite atan_0 atan_opp : trig_db.
+#[export] Hint Rewrite minus_1_plus_1 one_plus_minus_1 : R_db.
+#[export] Hint Rewrite atan_0 atan_opp : trig_db.
 
 (* The proof is split into 3 main cases, each with various subcases, depending 
    on the values of θ1 ξ θ2. In general, different parameters lead to different

VOQC/ConnectivityGraph.v

@@ -249,8 +249,8 @@
   | H : _ && _ = true |- _ => apply andb_prop in H as [? ?]
   | H : _ || _ = true |- _ => apply orb_prop in H
   | H : _ <? _ = true |- _ => apply Nat.ltb_lt in H
-  | H : _ =? _ = false |- _ => apply beq_nat_false in H 
-  | H : _ =? _ = true |- _ => apply beq_nat_true in H 
+  | H : _ =? _ = false |- _ => apply Nat.eqb_neq in H 
+  | H : _ =? _ = true |- _ => apply Nat.eqb_eq in H 
   | H : negb _ = true |- _ => apply negb_true_iff in H
   end.
 
@@ -998,7 +998,7 @@
     left.
     unfold is_in_graph.
     bdestruct_all; reflexivity.
     rewrite plus_assoc.
     apply IHdist; lia.
 Qed.
 
@@ -1158,7 +1158,7 @@
       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. }
       remember (numCols * (n1 / numCols)) as x.
       remember (numCols * (n2 / numCols)) as y.
       clear - Haux1 Haux2 H1 H2.
@@ -1183,7 +1183,7 @@
       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. }
       remember (numCols * (n1 / numCols)) as x.
       remember (numCols * (n2 / numCols)) as y.
       clear - Haux1 Haux2 H2 H3.
@@ -1202,7 +1202,7 @@
       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. }
       remember (numCols * (n1 / numCols)) as x.
       remember (numCols * (n2 / numCols)) as y.
       clear - Haux1 Haux2 H1 H4.
@@ -1223,7 +1223,7 @@
       (* 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 
            |  remember (numCols * (n1 / numCols)) as x;
               remember (numCols * (n2 / numCols)) as y;
               clear - Haux1 Haux2 H0 H1;

VOQC/FullGateSet.v

@@ -296,8 +296,18 @@ Proof.
   try rewrite Cexp_add;
   try rewrite Cexp_minus_PI;
   replace (PI / 2 / 2) with (PI / 4) by lra;
-  autorewrite with trig_db RtoC_db;
-  lca.
+  autorewrite with eval_db. rewrite cos_PI4.
+  apply c_proj_eq; simpl; try R_field_simplify; try easy;
+  try apply sqrt2_neq_0.
+  rewrite sin_PI4.
+  apply c_proj_eq; simpl; try R_field_simplify; try easy;
+  try apply sqrt2_neq_0.
+  rewrite sin_PI4.
+  apply c_proj_eq; simpl; try R_field_simplify; try easy;
+  try apply sqrt2_neq_0.
+  rewrite cos_PI4.
+  apply c_proj_eq; simpl; try R_field_simplify; try easy; 
+  try apply sqrt2_neq_0.
 Qed.
 
 Lemma rx_to_rz : forall dim a q,

VOQC/NonUnitaryListRepresentation.v

@@ -176,7 +176,7 @@ Proof.
   - induction l2; try rewrite IHl2; reflexivity.
 Qed.
 Global Opaque instr_to_com.
-Hint Rewrite instr_to_com_UC instr_to_com_Meas.
+#[export] Hint Rewrite instr_to_com_UC instr_to_com_Meas.
 
 Lemma list_to_com_append : forall {dim} (l1 l2 : com_list G.U dim),
   list_to_com (l1 ++ l2) ≡ list_to_com l1 ; list_to_com l2.