Update SQIR for QuantumLib >= 1.5.0, VOQC for >= 1.1.0

SQIR/UnitaryOps.v

@@ -1,5 +1,5 @@
 Require Export UnitarySem.
-Require Export QuantumLib.VectorStates.
+Require Export QuantumLib.VectorStates QuantumLib.Bits.
 
 (* This file contains useful operations over unitary programs including:
    - inversion
@@ -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.
 

VOQC/RemoveZRotationBeforeMeasure.v

@@ -81,6 +81,9 @@ Proof.
   repeat rewrite Mmult_assoc.
   Msimpl.
   repeat (restore_dims; rewrite <- Mmult_assoc).
+  (* This line is extraneous with the patch to 
+     Qsimpl / Q_db in QuantumLib > 1.5.0 *)
+  replace (σx †) with σx by (symmetry; apply σx_hermitian).
   Qsimpl.
   rewrite Mplus_comm; reflexivity.
   rewrite Mplus_comm; reflexivity.

coq-sqir.opam

@@ -1,6 +1,6 @@
 # This file is generated by dune, edit dune-project instead
 opam-version: "2.0"
-version: "1.3.0"
+version: "1.3.1"
 synopsis: "Coq library for reasoning about quantum circuits"
 description: """
 inQWIRE's SQIR is a Coq library for reasoning
@@ -14,7 +14,7 @@ bug-reports: "https://github.com/inQWIRE/SQIR/issues"
 depends: [
   "dune" {>= "3.8"}
   "coq-interval" {>= "4.9.0"}
-  "coq-quantumlib" {= "1.3.0"}
+  "coq-quantumlib" {>= "1.5.0"}
   "coq" {>= "8.16"}
   "odoc" {with-doc}
 ]

coq-voqc.opam

@@ -1,6 +1,6 @@
 # This file is generated by dune, edit dune-project instead
 opam-version: "2.0"
-version: "1.3.0"
+version: "1.3.1"
 synopsis: "A verified optimizer for quantum compilation"
 description: """
 inQWIRE's VOQC is a Coq library for verified
@@ -14,7 +14,7 @@ bug-reports: "https://github.com/inQWIRE/SQIR/issues"
 depends: [
   "dune" {>= "2.8"}
   "coq-interval" {>= "4.6.1"}
-  "coq-quantumlib" {>= "1.1.0" < "1.4.0"}
+  "coq-quantumlib" {>= "1.1.0"}
   "coq-sqir" {>= "1.3.0"}
   "coq" {>= "8.12"}
   "odoc" {with-doc}

dune-project

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