Upgrade VOQC to work with 8.18

inQWIRE · Jan 30, 2024 · 2e0a612 · 2e0a612
1 parent d7c4abd
commit 2e0a612
Show file tree

Hide file tree

Showing 3 changed files with 20 additions and 4 deletions.
diff --git 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
@@ -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
@@ -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,