Fixes for QuantumLib 1.6.0 and performance improvements (#61)

inQWIRE · Jan 21, 2025 · 9081860 · 9081860
1 parent cc932ab
commit 9081860
Show file tree

Hide file tree

Showing 12 changed files with 1,087 additions and 867 deletions.
diff --git a/SQIR/Equivalences.v b/SQIR/Equivalences.v
diff --git a/SQIR/ExtractionGateSet.v b/SQIR/ExtractionGateSet.v
@@ -294,22 +294,19 @@ Proof.
   unfold uc_eval. simpl.
   rewrite Ropp_0.
   apply f_equal.
-  unfold rotation.
-  solve_matrix; autorewrite with Cexp_db trig_db R_db; lca.
+  lma'; autorewrite with Cexp_db trig_db R_db; lca.
   (* U_U2 *)
   unfold uc_eval. simpl.
   apply f_equal.
-  unfold rotation.
-  solve_matrix; autorewrite with Cexp_db trig_db R_db; lca.
+  lma'; autorewrite with Cexp_db trig_db R_db; lca.
   (* U_CU1 *)
   rewrite invert_control.
   unfold uc_eval. simpl.
   apply control_cong.
   unfold uc_equiv. simpl.
   rewrite Ropp_0.
   apply f_equal.
-  unfold rotation.
-  solve_matrix; autorewrite with Cexp_db trig_db R_db; lca.
+  lma'; autorewrite with Cexp_db trig_db R_db; lca.
   split; intro; invert_is_fresh; repeat constructor; auto.
   (* U_CH *)
   rewrite invert_control.
@@ -333,8 +330,7 @@ Proof.
   unfold uc_equiv. simpl.
   rewrite Ropp_0.
   apply f_equal.
-  unfold rotation.
-  solve_matrix; autorewrite with Cexp_db trig_db R_db; lca.
+  lma'; autorewrite with Cexp_db trig_db R_db; lca.
   split; intro; invert_is_fresh; repeat constructor; auto.
   rewrite <- is_fresh_invert.
   rewrite <- 2 fresh_control.