Update QuantumLib for compatibility with Coq v8.16-8.19

.github/workflows/coq-action.yml

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

.gitignore

@@ -49,7 +49,10 @@ time-of-build-pretty.log
 .CoqMakefile.d
 CoqMakefile*
 Makefile.coq*
+Makefile.conf
 
 _build
 
-docs
+docs
+/.vscode
+.DS_Store

CITATION.cff

@@ -4,7 +4,7 @@ title: "INQWIRE QuantumLib"
 abstract: "QuantumLib is a Coq library for reasoning about quantum programs."
 authors:
   - name: "The INQWIRE Developers"
-version: 1.0.0
+version: 1.3.0
 date-released: 2022-01-06
 license: MIT
 repository-code: "https://github.com/inQWIRE/QuantumLib"

Complex.v

@@ -624,6 +624,7 @@ Proof.  intros.
         rewrite <- H' in H2. easy.
 Qed.
 
+
 Lemma Cinv_mult_distr : forall c1 c2 : C, c1 <> 0 -> c2 <> 0 -> / (c1 * c2) = / c1 * / c2.
 Proof.
   intros.
@@ -634,7 +635,7 @@ Proof.
     rewrite Rmult_div.
     rewrite Rmult_opp_opp.
     unfold Rminus.
-    rewrite <- RIneq.Ropp_div.
+    rewrite <- Ropp_div.
     rewrite <- Rdiv_plus_distr.
     rewrite Rmult_plus_distr_r.
     rewrite Rmult_plus_distr_l.
@@ -1397,7 +1398,7 @@ Proof.
   lca.
 Qed.
 
-Hint Rewrite Cexp_0 Cexp_PI Cexp_PI2 Cexp_2PI Cexp_3PI2 Cexp_PI4 Cexp_PIm4
+#[global] Hint Rewrite Cexp_0 Cexp_PI Cexp_PI2 Cexp_2PI Cexp_3PI2 Cexp_PI4 Cexp_PIm4
   Cexp_1PI4 Cexp_2PI4 Cexp_3PI4 Cexp_4PI4 Cexp_5PI4 Cexp_6PI4 Cexp_7PI4 Cexp_8PI4
   Cexp_add Cexp_neg Cexp_plus_PI Cexp_minus_PI : Cexp_db.
 
@@ -1442,28 +1443,28 @@ Ltac nonzero :=
   | |- Rle _ _ => lra
   end.
 
-Hint Rewrite Cminus_unfold Cdiv_unfold Ci2 Cconj_R Cconj_opp Cconj_rad2 
+#[global] Hint Rewrite Cminus_unfold Cdiv_unfold Ci2 Cconj_R Cconj_opp Cconj_rad2 
      Cinv_sqrt2_sqrt Cplus_div2
      Cplus_0_l Cplus_0_r Cplus_opp_r Cplus_opp_l Copp_0  Copp_involutive
      Cmult_0_l Cmult_0_r Cmult_1_l Cmult_1_r : C_db.
 
-Hint Rewrite <- Copp_mult_distr_l Copp_mult_distr_r Cdouble : C_db.
-Hint Rewrite Csqrt_sqrt using Psatz.lra : C_db.
-Hint Rewrite Cinv_l Cinv_r using nonzero : C_db.
+#[global] Hint Rewrite <- Copp_mult_distr_l Copp_mult_distr_r Cdouble : C_db.
+#[global] Hint Rewrite Csqrt_sqrt using Psatz.lra : C_db.
+#[global] Hint Rewrite Cinv_l Cinv_r using nonzero : C_db.
 (* Previously in the other direction *)
-Hint Rewrite Cinv_mult_distr using nonzero : C_db.
+#[global] Hint Rewrite Cinv_mult_distr using nonzero : C_db.
 
 (* Light rewriting db *)
-Hint Rewrite Cplus_0_l Cplus_0_r Cmult_0_l Cmult_0_r Copp_0 
+#[global] Hint Rewrite Cplus_0_l Cplus_0_r Cmult_0_l Cmult_0_r Copp_0 
              Cconj_R Cmult_1_l Cmult_1_r : C_db_light.
 
 (* Distributing db *)
-Hint Rewrite Cmult_plus_distr_l Cmult_plus_distr_r Copp_plus_distr Copp_mult_distr_l 
+#[global] Hint Rewrite Cmult_plus_distr_l Cmult_plus_distr_r Copp_plus_distr Copp_mult_distr_l 
               Copp_involutive : Cdist_db.
 
-Hint Rewrite RtoC_opp RtoC_mult RtoC_minus RtoC_plus : RtoC_db.
-Hint Rewrite RtoC_inv using nonzero : RtoC_db.
-Hint Rewrite RtoC_pow : RtoC_db.
+#[global] Hint Rewrite RtoC_opp RtoC_mult RtoC_minus RtoC_plus : RtoC_db.
+#[global] Hint Rewrite RtoC_inv using nonzero : RtoC_db.
+#[global] Hint Rewrite RtoC_pow : RtoC_db.
 
 Ltac Csimpl := 
   repeat match goal with

DiscreteProb.v

@@ -102,7 +102,7 @@ Lemma sample_ub_lt :  forall l r,
 Proof.
   induction l; intros. unfold sum_over_list in H. simpl in H. lra.
   simpl. destruct (Rlt_le_dec r a). lia.
-  apply lt_n_S. apply IHl. rewrite sum_over_list_cons in H. lra.
+  apply -> Nat.succ_lt_mono. apply IHl. rewrite sum_over_list_cons in H. lra.
 Qed.
 
 Lemma sample_lb : forall l r, (0 <= sample l r)%nat.
@@ -1472,6 +1472,10 @@ Proof.
   assumption.
 Qed.
 
+(* This was removed from std lib without replacement in 8.19 *)
+Lemma mult_O_le_stt : forall n m : nat, (m = 0 \/ n <= m * n)%nat.
+Proof. intros. induction m. auto. right. lia. Qed.
+
 Lemma rewrite_pr_outcome_sum : forall n k (u : Square (2 ^ (n + k))) f,
   WF_Matrix u ->
   pr_outcome_sum (apply_u u) (fun x => f (fst k x)) 
@@ -1498,12 +1502,12 @@ Proof.
     replace (2 ^ (n + k))%nat with (2 ^ n * 2 ^ k)%nat by unify_pows_two.
     apply (Nat.mul_le_mono_r _ _ (2^k)%nat) in H0.
     rewrite Nat.mul_sub_distr_r in H0.
-    rewrite mult_1_l in H0.
+    rewrite Nat.mul_1_l in H0.
     apply (Nat.add_lt_le_mono x0 (2^k)%nat) in H0; auto.
-    rewrite <- le_plus_minus in H0.
-    rewrite plus_comm in H0.
+    rewrite <- le_plus_minus' in H0.
+    rewrite Nat.add_comm in H0.
     assumption.
-    destruct (mult_O_le (2^k) (2^n))%nat; auto.
+    destruct (mult_O_le_stt (2^k) (2^n))%nat; auto.
     assert (2 <> 0)%nat by lia.
     apply (pow_positive 2 n) in H2.
     lia.

Eigenvectors.v

@@ -25,15 +25,15 @@ Lemma Y_eq_iXZ : σy = Ci .* σx × σz. Proof. lma'. Qed.
 Lemma H_eq_Hadjoint : hadamard† = hadamard. Proof. lma'. Qed.
 
 
-Hint Rewrite Y_eq_iXZ H_eq_Hadjoint : Q_db.
+#[global] Hint Rewrite Y_eq_iXZ H_eq_Hadjoint : Q_db.
 
 Lemma ItimesIid : I 2 × I 2 = I 2. Proof. lma'. Qed.      
 Lemma XtimesXid : σx × σx = I 2. Proof. lma'. Qed.      
 Lemma YtimesYid : σy × σy = I 2. Proof. lma'. Qed.
 Lemma ZtimesZid : σz × σz = I 2. Proof. lma'. Qed.
 Lemma HtimesHid : hadamard × hadamard = I 2. Proof. lma'; Hhelper. Qed.
 
-Hint Rewrite ItimesIid XtimesXid YtimesYid ZtimesZid HtimesHid : Q_db.
+#[global] Hint Rewrite ItimesIid XtimesXid YtimesYid ZtimesZid HtimesHid : Q_db.
 
 Lemma ZH_eq_HX : σz × hadamard = hadamard × σx. Proof. lma'. Qed.
 Lemma XH_eq_HZ : σx × hadamard = hadamard × σz. Proof. lma'. Qed.
@@ -46,7 +46,7 @@ Lemma cnotX2 : cnot × (I 2 ⊗ σx) = (I 2 ⊗ σx) × cnot. Proof. lma'. Qed.
 Lemma cnotZ1 : cnot × (σz ⊗ I 2) = (σz ⊗ I 2) × cnot. Proof. lma'. Qed.
 Lemma cnotZ2 : cnot × (I 2 ⊗ σz) = (σz ⊗ σz) × cnot. Proof. lma'. Qed.
 
-Hint Rewrite ZH_eq_HX XH_eq_HZ SX_eq_YS SZ_eq_ZS cnotX1 cnotX2 cnotZ1 cnotZ2 : Q_db.
+#[global] Hint Rewrite ZH_eq_HX XH_eq_HZ SX_eq_YS SZ_eq_ZS cnotX1 cnotX2 cnotZ1 cnotZ2 : Q_db.
 
 
 (*******************************)
@@ -259,7 +259,7 @@ Proof. induction n as [| n'].
              rewrite p in H1; easy. }
            rewrite H', Pplus_comm, Pplus_degree2; auto. 
            rewrite H1. 
-           apply le_lt_n_Sm.
+           apply Nat.lt_succ_r.
            apply Psum_degree; intros. 
            assert (H2 : prep_mat A (S i) 0 = [A (S i) 0]).
            { unfold prep_mat. 
@@ -356,7 +356,7 @@ Proof. intros.
        prep_matrix_equality.
        unfold get_vec, form_basis.
        bdestruct (y =? 0).
-       rewrite <- beq_nat_refl, H0; easy.
+       rewrite Nat.eqb_refl, H0; easy.
        unfold WF_Matrix in H.
        rewrite H; try easy.
        right. 
@@ -885,7 +885,7 @@ Proof. induction m2 as [| m2'].
          exists Zero.
          split. easy.
          rewrite smash_zero; try easy.
-         rewrite plus_0_r.
+         rewrite Nat.add_0_r.
          apply H2.
        - intros. 
          rewrite (split_col T2) in *.
@@ -1180,8 +1180,8 @@ Proof. intros a b m H0 Hdiv Hmod.
        rewrite Hdiv in Hmod.
        assert (H : m * (b / m) + (a - m * (b / m)) = m * (b / m) + (b - m * (b / m))).
        { rewrite Hmod. reflexivity. }
-       rewrite <- (le_plus_minus  (m * (b / m)) a) in H.
-       rewrite <- (le_plus_minus  (m * (b / m)) b) in H.
+       rewrite <- (le_plus_minus'  (m * (b / m)) a) in H.
+       rewrite <- (le_plus_minus'  (m * (b / m)) b) in H.
        apply H.
        apply Nat.mul_div_le; apply H0.
        rewrite <- Hdiv; apply Nat.mul_div_le; apply H0.

FiniteGroups.v

@@ -16,7 +16,7 @@ Global Program Instance list_is_monoid {X} : Monoid (list X) :=
   { Gzero := []
   ; Gplus := @app X
   }.
-Next Obligation. rewrite app_nil_end; easy. Qed.
+Next Obligation. rewrite <- app_nil_r; easy. Qed.
 Next Obligation. rewrite app_assoc; easy. Qed.
 
 

GenMatrix.v

@@ -316,8 +316,8 @@ Ltac by_cell :=
   let Hi := fresh "Hi" in 
   let Hj := fresh "Hj" in 
   intros i j Hi Hj; try solve_end;
-  repeat (destruct i as [|i]; simpl; [|apply Nat.succ_lt_mono in Hi]; try solve_end); clear Hi;
-  repeat (destruct j as [|j]; simpl; [|apply Nat.succ_lt_mono in Hj]; try solve_end); clear Hj.
+  repeat (destruct i as [|i]; simpl; [|apply <- Nat.succ_lt_mono in Hi]; try solve_end); clear Hi;
+  repeat (destruct j as [|j]; simpl; [|apply <- Nat.succ_lt_mono in Hj]; try solve_end); clear Hj.
 
 Ltac lgma' :=
   apply genmat_equiv_eq;
@@ -3639,7 +3639,7 @@ Proof. intros.
        simpl.  
        autorewrite with R_db.
        rewrite Rmult_comm.
-       rewrite Rinv_mult_distr; try easy. 
+       rewrite Rinv_mult; try easy. 
        rewrite <- Rmult_comm.
        rewrite <- Rmult_assoc.
        rewrite Rinv_r; try easy.
@@ -3648,7 +3648,7 @@ Proof. intros.
        unfold Cinv.
        simpl. 
        autorewrite with R_db.
-       rewrite Rinv_mult_distr; try easy. 
+       rewrite Rinv_mult; try easy. 
        rewrite <- Rmult_assoc.
        rewrite Rinv_r; try easy.
        autorewrite with R_db.