From a4963db6d23318e9931b02853a8dc0faa94bf2bd Mon Sep 17 00:00:00 2001
From: BHAKTISHAH <shahbhakti21@gmail.com>
Date: Fri, 14 Apr 2023 18:08:12 -0500
Subject: [PATCH 1/8] 8.17 compatibility for sqir

---
 SQIR/Equivalences.v       |  1 +
 SQIR/GateDecompositions.v | 17 ++++---
 SQIR/NDSem.v              | 14 ++++--
 SQIR/UnitaryOps.v         | 96 +++++++++++++++++++++++++++++----------
 SQIR/UnitarySem.v         |  4 +-
 5 files changed, 95 insertions(+), 37 deletions(-)

diff --git a/SQIR/Equivalences.v b/SQIR/Equivalences.v
index a23a2641..517bec37 100644
--- a/SQIR/Equivalences.v
+++ b/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.
diff --git a/SQIR/GateDecompositions.v b/SQIR/GateDecompositions.v
index 1a5ac8f9..26654cfa 100644
--- a/SQIR/GateDecompositions.v
+++ b/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.
diff --git a/SQIR/NDSem.v b/SQIR/NDSem.v
index eb21ccae..8ec9e1b1 100644
--- a/SQIR/NDSem.v
+++ b/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.
diff --git a/SQIR/UnitaryOps.v b/SQIR/UnitaryOps.v
index 8e1e8e48..5f5e84b6 100644
--- a/SQIR/UnitaryOps.v
+++ b/SQIR/UnitaryOps.v
@@ -52,7 +52,7 @@ Qed.
 
 (* 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.
@@ -387,7 +387,7 @@ Proof. intros; solve_matrix. Qed.
 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.
@@ -395,7 +395,7 @@ 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 @@ Proof.
      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 @@ Proof.
     + 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 @@ Proof.
     + 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 @@ Proof.
     + 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 @@ Proof.
     + 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 @@ Proof.
    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;
diff --git a/SQIR/UnitarySem.v b/SQIR/UnitarySem.v
index 19622382..5b119289 100644
--- a/SQIR/UnitarySem.v
+++ b/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.
 

From c620fa705151c1c9d27b0ecea0a2afe7b2e960a8 Mon Sep 17 00:00:00 2001
From: BHAKTISHAH <shahbhakti21@gmail.com>
Date: Sat, 15 Apr 2023 21:44:24 -0500
Subject: [PATCH 2/8] voqc compiling on 8.17

---
 VOQC/ChangeRotationBasis.v          | 26 ++++++++++++++++++++------
 VOQC/FullGateSet.v                  | 14 ++++++++++++--
 VOQC/NonUnitaryListRepresentation.v |  2 +-
 VOQC/RotationMerging.v              |  5 ++++-
 4 files changed, 37 insertions(+), 10 deletions(-)

diff --git a/VOQC/ChangeRotationBasis.v b/VOQC/ChangeRotationBasis.v
index e75a1a78..c9c69d76 100644
--- a/VOQC/ChangeRotationBasis.v
+++ b/VOQC/ChangeRotationBasis.v
@@ -920,7 +920,21 @@ Proof.
        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 @@ Proof.
     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 @@ Proof.
     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 @@ Proof.
   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 @@ Lemma minus_1_plus_1 : -1 + 1 = 0.
 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
diff --git a/VOQC/FullGateSet.v b/VOQC/FullGateSet.v
index 16a44790..8f478c6e 100644
--- a/VOQC/FullGateSet.v
+++ b/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,
diff --git a/VOQC/NonUnitaryListRepresentation.v b/VOQC/NonUnitaryListRepresentation.v
index 6364ff7d..26b77950 100644
--- a/VOQC/NonUnitaryListRepresentation.v
+++ b/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.
diff --git a/VOQC/RotationMerging.v b/VOQC/RotationMerging.v
index 3470a081..7a51a4e4 100644
--- a/VOQC/RotationMerging.v
+++ b/VOQC/RotationMerging.v
@@ -1158,7 +1158,10 @@ Proof.
   rewrite invert_alt.
   Local Transparent ID.
   induction l; simpl.
-  rewrite Ropp_0. reflexivity.
+  replace (uc_eval SKIP) with ((@uc_eval dim SKIP) †).
+  apply invert_correct.
+  autorewrite with eval_db.
+  apply id_adjoint_eq. easy.
   Local Opaque ID Z.sub. 
   destruct a as [u | u | u]; dependent destruction u; unfold invert; simpl.
   all: rewrite map_app, list_to_ucom_append; simpl.

From b35c50a9ed90379831b3602da041ddb68e63dea8 Mon Sep 17 00:00:00 2001
From: BHAKTISHAH <shahbhakti21@gmail.com>
Date: Sun, 16 Apr 2023 17:20:21 -0500
Subject: [PATCH 3/8] version bumps + dune changes

---
 dune-project | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

diff --git a/dune-project b/dune-project
index fe1cd2ae..8d633ac2 100644
--- a/dune-project
+++ b/dune-project
@@ -1,7 +1,7 @@
-(lang dune 2.8)
+(lang dune 3.7)
 (name coq-sqirvoqc)
-(version 1.1.0)
-(using coq 0.2)
+(version 1.2.0)
+(using coq 0.7)
 
 (generate_opam_files true)
 
@@ -18,8 +18,8 @@
  )
  (depends
    (coq-interval (>= 4.6.1))
-   (coq-quantumlib (>= 1.1.0))
-   (coq (>= 8.12))))
+   (coq-quantumlib (>= 1.2.0))
+   (coq (>= 8.17))))
 
 (package
  (name coq-voqc)
@@ -29,6 +29,6 @@
  )
  (depends
    (coq-interval (>= 4.6.1))
-   (coq-quantumlib (>= 1.1.0))
-   (coq-sqir (>= 1.1.0))
-   (coq (>= 8.12))))
+   (coq-quantumlib (>= 1.2.0))
+   (coq-sqir (>= 1.2.0))
+   (coq (>= 8.17))))

From 1f2db24aefbc18b1545332238e89b1b143fa318a Mon Sep 17 00:00:00 2001
From: BHAKTISHAH <shahbhakti21@gmail.com>
Date: Sun, 16 Apr 2023 17:25:21 -0500
Subject: [PATCH 4/8] version bump

---
 coq-sqir.opam | 2 +-
 coq-voqc.opam | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/coq-sqir.opam b/coq-sqir.opam
index 3c6c6cbd..d1c2bc09 100644
--- a/coq-sqir.opam
+++ b/coq-sqir.opam
@@ -1,6 +1,6 @@
 # This file is generated by dune, edit dune-project instead
 opam-version: "2.0"
-version: "1.1.0"
+version: "1.2.0"
 synopsis: "Coq library for reasoning about quantum circuits"
 description: """
 inQWIRE's VOQC is a Coq library for reasoning
diff --git a/coq-voqc.opam b/coq-voqc.opam
index ad4f8f3f..964e2b96 100644
--- a/coq-voqc.opam
+++ b/coq-voqc.opam
@@ -1,6 +1,6 @@
 # This file is generated by dune, edit dune-project instead
 opam-version: "2.0"
-version: "1.1.0"
+version: "1.2.0"
 synopsis: "A verified optimizer for quantum compilation"
 description: """
 inQWIRE's VOQC is a Coq tool for verified

From d632f9e0c11a5f3843904211ccf0fba041ef7130 Mon Sep 17 00:00:00 2001
From: Adrian Lehmann <info@adrianlehmann.net>
Date: Fri, 26 Jan 2024 13:09:40 -0600
Subject: [PATCH 5/8] Fix readme pin git url

---
 README.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/README.md b/README.md
index bfc5e12c..8a09f9e8 100644
--- a/README.md
+++ b/README.md
@@ -70,7 +70,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`. 
 

From aa72b66a7631e4cbc8dfca96409c7f19b5db4a53 Mon Sep 17 00:00:00 2001
From: Adrian Lehmann <info@adrianlehmann.net>
Date: Mon, 29 Jan 2024 16:37:44 -0600
Subject: [PATCH 6/8] Update build files to 1.3.0

---
 coq-sqir.opam | 9 +++++----
 coq-voqc.opam | 3 ++-
 dune-project  | 5 ++---
 3 files changed, 9 insertions(+), 8 deletions(-)

diff --git a/coq-sqir.opam b/coq-sqir.opam
index 46d8f123..c0a318ec 100644
--- a/coq-sqir.opam
+++ b/coq-sqir.opam
@@ -1,6 +1,6 @@
 # This file is generated by dune, edit dune-project instead
 opam-version: "2.0"
-version: "1.2.0"
+version: "1.3.0"
 synopsis: "Coq library for reasoning about quantum circuits"
 description: """
 inQWIRE's SQIR is a Coq library for reasoning
@@ -12,9 +12,10 @@ license: "MIT"
 homepage: "https://github.com/inQWIRE/SQIR"
 bug-reports: "https://github.com/inQWIRE/SQIR/issues"
 depends: [
-  "dune" {>= "2.8"}
-  "coq-quantumlib" {>= "1.1.0"}
-  "coq" {>= "8.12"}
+  "dune" {>= "3.8"}
+  "coq-interval" {>= "4.9.0"}
+  "coq-quantumlib" {>= "1.3.0"}
+  "coq" {>= "8.16"}
   "odoc" {with-doc}
 ]
 build: [
diff --git a/coq-voqc.opam b/coq-voqc.opam
index 88d6e2ba..a0c928cb 100644
--- a/coq-voqc.opam
+++ b/coq-voqc.opam
@@ -1,6 +1,6 @@
 # This file is generated by dune, edit dune-project instead
 opam-version: "2.0"
-version: "1.2.0"
+version: "1.3.0"
 synopsis: "A verified optimizer for quantum compilation"
 description: """
 inQWIRE's VOQC is a Coq library for verified
@@ -13,6 +13,7 @@ homepage: "https://github.com/inQWIRE/SQIR"
 bug-reports: "https://github.com/inQWIRE/SQIR/issues"
 depends: [
   "dune" {>= "2.8"}
+  "coq-interval" {>= "4.6.1"}
   "coq-quantumlib" {>= "1.1.0"}
   "coq-sqir" {>= "1.1.0"}
   "coq" {>= "8.12"}
diff --git a/dune-project b/dune-project
index 43dd51f5..84df1133 100644
--- a/dune-project
+++ b/dune-project
@@ -1,4 +1,4 @@
-(lang dune 3.7)
+(lang dune 3.8)
 (name coq-sqirvoqc)
 (version 1.3.0)
 (using coq 0.7)
@@ -18,7 +18,7 @@
  (depends
    (coq-interval (>= 4.9.0))
    (coq-quantumlib (>= 1.3.0))
-   (coq (>= 8.19))))
+   (coq (>= 8.16))))
 
 (package
  (name coq-voqc)
@@ -27,7 +27,6 @@
               "\|  optimization of quantum circuits
  )
  (depends
-<<<<<<< HEAD
    (coq-interval (>= 4.9.0))
    (coq-quantumlib (>= 1.3.0))
    (coq-sqir (>= 1.3.0))

From d7c4abd089e817f78665d938fb853d2daf3daf33 Mon Sep 17 00:00:00 2001
From: Adrian Lehmann <info@adrianlehmann.net>
Date: Tue, 30 Jan 2024 11:24:34 -0600
Subject: [PATCH 7/8] Update CI to 8.16-8.18

---
 .github/workflows/coq-action.yml | 12 ++----------
 1 file changed, 2 insertions(+), 10 deletions(-)

diff --git a/.github/workflows/coq-action.yml b/.github/workflows/coq-action.yml
index b85c3857..a1dec498 100644
--- a/.github/workflows/coq-action.yml
+++ b/.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

From 2e0a6123b97f1fb410ca722826af60e0be7f08e8 Mon Sep 17 00:00:00 2001
From: Adrian Lehmann <info@adrianlehmann.net>
Date: Tue, 30 Jan 2024 12:20:45 -0600
Subject: [PATCH 8/8] Upgrade VOQC to work with 8.18

---
 VOQC/ConnectivityGraph.v         |  4 ++--
 VOQC/RotationMerging.v           | 18 +++++++++++++++++-
 VOQC/UnitaryListRepresentation.v |  2 +-
 3 files changed, 20 insertions(+), 4 deletions(-)

diff --git a/VOQC/ConnectivityGraph.v b/VOQC/ConnectivityGraph.v
index 85ace7c6..5edecbb2 100644
--- a/VOQC/ConnectivityGraph.v
+++ b/VOQC/ConnectivityGraph.v
@@ -249,8 +249,8 @@ Ltac destruct_bool_goals :=
   | 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.
 
diff --git a/VOQC/RotationMerging.v b/VOQC/RotationMerging.v
index 7a51a4e4..c6386719 100644
--- a/VOQC/RotationMerging.v
+++ b/VOQC/RotationMerging.v
@@ -131,7 +131,7 @@ Proof.
         right. split; auto.
         intro contra; destruct contra as [contra1 contra2].
         apply H2 in contra1 as [contra1 | contra1]; auto. }
-      rewrite <- FSetProps.fold_equal in H; try apply H3; auto.
+      rewrite FSetProps.fold_equal in H; try apply H3; auto.
       rewrite (FSetProps.fold_2 _ _ Hcompat Htranspose H1 H2).
       rewrite xorb_assoc.
       rewrite <- H. 
@@ -141,6 +141,22 @@ Proof.
       intro contra; destruct contra as [[contra1 | contra1] contra2];
       contradict contra2; split; auto.
       apply H2; auto.
+      { unfold compat_op in *.
+      apply proper_sym_flip_2; try easy.
+      unfold Proper.
+      unfold respectful.
+      intros.
+      unfold flip in H5.
+      subst.
+      easy.
+      }
+      {
+        unfold transpose.
+        intros.
+        unfold flip.
+        rewrite <- xorb_assoc, (xorb_comm (f y)), xorb_assoc; auto.
+      }
+      easy.
     + assert (FSet.Equal (FSet.diff (FSet.union s1' s2) (FSet.inter s1' s2)) (FSet.add x (FSet.diff (FSet.union s1 s2) (FSet.inter s1 s2)))). 
       { clear - H0 H1 H2.
         unfold FSet.Equal.
diff --git a/VOQC/UnitaryListRepresentation.v b/VOQC/UnitaryListRepresentation.v
index aa698690..7b7796e0 100644
--- a/VOQC/UnitaryListRepresentation.v
+++ b/VOQC/UnitaryListRepresentation.v
@@ -442,7 +442,7 @@ Ltac simpl_dnr :=
   | H : _ && _ = true |- _ =>
       apply andb_true_iff in H as [? ?]
   | H : (_ =? _)%nat = false |- _ => 
-      apply beq_nat_false in H
+      apply Nat.eqb_neq in H
   end.
 
 Lemma does_not_reference_rev : forall {U dim} (l : gate_list U dim) q,