Remove deprecation issue for 8.16+

.github/workflows/coq-action.yml

@@ -12,12 +12,10 @@ jobs:
     strategy:
       matrix:
         coq_version:
-          - '8.12'
-          - '8.13'
-          - '8.14'
-          - '8.15'
           - '8.16'
           - '8.17'
+          - '8.18'
+          - '8.19'
           - 'dev'
         ocaml_version:
           - 'default'

.gitignore

@@ -49,8 +49,10 @@ time-of-build-pretty.log
 .CoqMakefile.d
 CoqMakefile*
 Makefile.coq*
+Makefile.conf
 
 _build
 
 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"

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.
@@ -1498,12 +1498,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 (Arith_prebase.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

@@ -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.

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.

Matrix.v

@@ -306,8 +306,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 lt_S_n in Hi]; try solve_end); clear Hi;
-  repeat (destruct j as [|j]; simpl; [|apply lt_S_n 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 lma' :=
   apply mat_equiv_eq;
@@ -543,7 +543,7 @@ Ltac show_wf :=
   let y := fresh "y" in
   let H := fresh "H" in
   intros x y [H | H];
-  apply le_plus_minus in H; rewrite H;
+  apply le_plus_minus' in H; rewrite H;
   cbv;
   destruct_m_eq;
   try lca.
@@ -1188,10 +1188,10 @@ Proof.
   unfold I, kron.
   prep_matrix_equality.
   bdestruct (x =? y); rename H into Eq; subst.
-  + repeat rewrite <- beq_nat_refl; simpl.
+  + repeat rewrite Nat.eqb_refl; simpl.
     destruct n.
     - simpl.
-      rewrite mult_0_r.
+      rewrite Nat.mul_0_r.
       bdestruct (y <? 0); try lia.
       autorewrite with C_db; reflexivity.
     - bdestruct (y mod S n <? S n). 
@@ -1209,13 +1209,13 @@ Proof.
         simpl. apply Nat.neq_succ_0. (* `lia` will solve in 8.11+ *)
         apply Nat.div_small in L1.
         rewrite Nat.div_div in L1; try lia.
-        rewrite mult_comm.
+        rewrite Nat.mul_comm.
         assumption.
       * apply Nat.ltb_nlt in L1. 
         apply Nat.ltb_lt in L2. 
         contradict L1. 
         apply Nat.div_lt_upper_bound. lia.
-        rewrite mult_comm.
+        rewrite Nat.mul_comm.
         assumption.
   + simpl.
     bdestruct (x / n =? y / n); simpl; try lca.
@@ -1253,7 +1253,7 @@ Lemma sub_mul_mod :
     (x - y * z) mod z = x mod z.
 Proof.
   intros. bdestruct (z =? 0). subst. simpl. lia.
-  specialize (le_plus_minus_r (y * z) x H) as G.
+  specialize (le_plus_minus_r' (y * z) x H) as G.
   remember (x - (y * z)) as r.
   rewrite <- G. rewrite <- Nat.add_mod_idemp_l by easy. rewrite Nat.mod_mul by easy.
   easy.
@@ -1277,8 +1277,8 @@ Proof.
   intros. intros i j Hi Hj.
   remember (A ⊗ B ⊗ C) as LHS.
   unfold kron.  
-  rewrite (mult_comm p r) at 1 2.
-  rewrite (mult_comm q s) at 1 2.
+  rewrite (Nat.mul_comm p r) at 1 2.
+  rewrite (Nat.mul_comm q s) at 1 2.
   assert (m * p * r <> 0) by lia.
   assert (n * q * s <> 0) by lia.
   apply Nat.neq_mul_0 in H as [Hmp Hr].
@@ -1312,7 +1312,7 @@ Proof.
   prep_matrix_equality.
   destruct q.
   + simpl.
-    rewrite mult_0_r.
+    rewrite Nat.mul_0_r.
     simpl.
     rewrite Cmult_0_r.
     reflexivity. 
@@ -2622,7 +2622,7 @@ Proof. intros.
        apply big_sum_eq_bounded; intros.
        bdestruct (e + S x0 =? e); try lia; easy.
        unfold get_vec. simpl. 
-       rewrite plus_0_r; easy.
+       rewrite Nat.add_0_r; easy.
 Qed.
 
 (* shows that we can eliminate a column in a matrix using col_add_many *)
@@ -2638,12 +2638,12 @@ Proof. intros.
                      (@Mmult n m 1 (reduce_col T col) (reduce_row as' col)) i 0)%C).
        { unfold Mmult.
          replace (S m) with (col + (S (m - col))) by lia; rewrite big_sum_sum. 
-         rewrite (le_plus_minus col m); try lia; rewrite big_sum_sum. 
+         rewrite (le_plus_minus' col m); try lia; rewrite big_sum_sum. 
          apply Cplus_simplify. 
          apply big_sum_eq_bounded; intros. 
          unfold get_vec, scale, reduce_col, reduce_row. 
          bdestruct (x <? col); simpl; try lia; lca.
-         rewrite <- le_plus_minus, <- big_sum_extend_l, plus_0_r, H0; try lia. 
+         rewrite <- le_plus_minus', <- big_sum_extend_l, Nat.add_0_r, H0; try lia. 
          unfold scale; rewrite Cmult_0_l, Cplus_0_l.
          apply big_sum_eq_bounded; intros. 
          unfold get_vec, scale, reduce_col, reduce_row. 
@@ -2846,7 +2846,7 @@ Proof. intros.
        prep_matrix_equality. 
        unfold Mmult. 
        bdestruct (x <? m); try lia.
-       rewrite (le_plus_minus x m); try lia.
+       rewrite (le_plus_minus' x m); try lia.
        do 2 rewrite big_sum_sum. 
        apply Cplus_simplify. 
        apply big_sum_eq_bounded.
@@ -2858,7 +2858,7 @@ Proof. intros.
        rewrite Cplus_comm.
        rewrite (Cplus_comm (col_swap A x y x0 (x + 0)%nat * row_swap B x y (x + 0)%nat y0)%C _).
        bdestruct ((y - x - 1) <? x'); try lia.  
-       rewrite (le_plus_minus (y - x - 1) x'); try lia. 
+       rewrite (le_plus_minus' (y - x - 1) x'); try lia. 
        do 2 rewrite big_sum_sum.
        do 2 rewrite <- Cplus_assoc.
        apply Cplus_simplify. 
@@ -2915,7 +2915,7 @@ Proof. intros.
        prep_matrix_equality. 
        unfold Mmult.   
        bdestruct (x <? m); try lia.
-       rewrite (le_plus_minus x m); try lia.       
+       rewrite (le_plus_minus' x m); try lia.       
        do 2 rewrite big_sum_sum.
        apply Cplus_simplify. 
        apply big_sum_eq_bounded.
@@ -2927,7 +2927,7 @@ Proof. intros.
        rewrite Cplus_comm. 
        rewrite (Cplus_comm (col_add A x y a x0 (x + 0)%nat * B (x + 0)%nat y0)%C _).
        bdestruct ((y - x - 1) <? x'); try lia.  
-       rewrite (le_plus_minus (y - x - 1) x'); try lia. 
+       rewrite (le_plus_minus' (y - x - 1) x'); try lia. 
        do 2 rewrite big_sum_sum.
        do 2 rewrite <- Cplus_assoc.
        apply Cplus_simplify. 
@@ -3242,7 +3242,7 @@ Proof. intros.
        prep_matrix_equality. 
        bdestruct (y =? m); bdestruct (y <? m); try lia; try easy.
        rewrite H1.
-       rewrite <- minus_diag_reverse; easy. 
+       rewrite Nat.sub_diag; easy. 
        rewrite H0, H; try lia; try easy.
 Qed.
 
@@ -3533,7 +3533,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.
@@ -3542,7 +3542,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.

Measurement.v

@@ -59,7 +59,7 @@ Proof.
   unfold prob_partial_meas.
   rewrite norm_squared.
   unfold inner_product, Mmult, adjoint.
-  rewrite (@big_sum_func_distr C R _ C_is_group _ R_is_group), mult_1_l.
+  rewrite (@big_sum_func_distr C R _ C_is_group _ R_is_group), Nat.mul_1_l.
   apply big_sum_eq_bounded; intros. 
   unfold probability_of_outcome.
   assert (H' : forall c, ((Cmod c)^2)%R = fst (c^* * c)).

Pad.v

@@ -219,29 +219,29 @@ Ltac rem_max_min :=
    unfold gt, ge, abs_diff in *;
   repeat match goal with 
   | [ H: (?a < ?b)%nat |- context[Nat.max (?a - ?b) (?b - ?a)] ] => 
-    rewrite (Max.max_r (a - b) (b - a)) by lia 
+    rewrite (Nat.max_r (a - b) (b - a)) by lia 
   | [ H: (?a < ?b)%nat |- context[Nat.max (?b - ?a) (?a - ?b)] ] => 
-    rewrite (Max.max_l (b - a) (a - b)) by lia 
+    rewrite (Nat.max_l (b - a) (a - b)) by lia 
   | [ H: (?a <= ?b)%nat |- context[Nat.max (?a - ?b) (?b - ?a)] ] => 
-    rewrite (Max.max_r (a - b) (b - a)) by lia 
+    rewrite (Nat.max_r (a - b) (b - a)) by lia 
   | [ H: (?a <= ?b)%nat |- context[Nat.max (?b - ?a) (?a - ?b)] ] => 
-    rewrite (Max.max_l (b - a) (a - b)) by lia   
+    rewrite (Nat.max_l (b - a) (a - b)) by lia   
   | [ H: (?a < ?b)%nat |- context[Nat.min ?a ?b] ] => 
-    rewrite Min.min_l by lia 
+    rewrite Nat.min_l by lia 
   | [ H: (?a < ?b)%nat |- context[Nat.max ?a ?b] ] => 
-    rewrite Max.max_r by lia 
+    rewrite Nat.max_r by lia 
   | [ H: (?a < ?b)%nat |- context[Nat.min ?b ?a] ] => 
-    rewrite Min.min_r by lia 
+    rewrite Nat.min_r by lia 
   | [ H: (?a < ?b)%nat |- context[Nat.max ?b ?a] ] => 
-    rewrite Max.max_l by lia 
+    rewrite Nat.max_l by lia 
   | [ H: (?a <= ?b)%nat |- context[Nat.min ?a ?b] ] => 
-    rewrite Min.min_l by lia 
+    rewrite Nat.min_l by lia 
   | [ H: (?a <= ?b)%nat |- context[Nat.max ?a ?b] ] => 
-    rewrite Max.max_r by lia 
+    rewrite Nat.max_r by lia 
   | [ H: (?a <= ?b)%nat |- context[Nat.min ?b ?a] ] => 
-    rewrite Min.min_r by lia 
+    rewrite Nat.min_r by lia 
   | [ H: (?a <= ?b)%nat |- context[Nat.max ?b ?a] ] => 
-    rewrite Max.max_l by lia 
+    rewrite Nat.max_l by lia 
   end.
 
 Definition pad2x2_u (dim n : nat) (u : Square 2) : Square (2^dim) := @embed dim [(u,n)].
@@ -336,7 +336,7 @@ Proof.
   intros. unfold pad2x2_u, pad2x2_ctrl, abs_diff. bdestruct_all; simpl; rem_max_min;
   Msimpl; trivial.
   + repeat rewrite Mmult_plus_distr_l; repeat rewrite Mmult_plus_distr_r.
-  rewrite le_plus_minus_r by (apply Nat.lt_le_incl; trivial).
+  rewrite le_plus_minus_r' by (apply Nat.lt_le_incl; trivial).
   repeat rewrite embed_mult; simpl.
   rewrite (embed_commutes dim [(A, m); (∣1⟩⟨1∣, n); (B, o)] [(∣1⟩⟨1∣, n); (B, o); (A, m)]).
   rewrite (embed_commutes dim [(A, m); (∣0⟩⟨0∣, n); (I 2, o)] [(∣0⟩⟨0∣, n); (I 2, o); (A, m)]).
@@ -345,7 +345,7 @@ Proof.
   all : rewrite perm_swap; apply perm_skip; apply perm_swap.
 
   + repeat rewrite Mmult_plus_distr_l; repeat rewrite Mmult_plus_distr_r.
-  rewrite le_plus_minus_r by trivial; repeat rewrite embed_mult; simpl.
+  rewrite le_plus_minus_r' by trivial; repeat rewrite embed_mult; simpl.
   rewrite (embed_commutes dim [(A, m); (B, o); (∣1⟩⟨1∣, n)] [(B, o); (∣1⟩⟨1∣, n); (A, m)]).
   rewrite (embed_commutes dim [(A, m); (I 2, o); (∣0⟩⟨0∣, n)] [(I 2, o); (∣0⟩⟨0∣, n); (A, m)]).
   trivial.

Permutations.v

@@ -162,7 +162,7 @@ Proof.
   bdestruct_all; simpl; try lca.
   subst.
   rewrite andb_true_r in H.
-  apply beq_nat_false in H.
+  apply Nat.eqb_neq in H.
   assert (pinv (p x) = pinv (p y)) by auto.
   destruct (Hp x) as [_ [_ [H5 _]]]; auto.
   destruct (Hp y) as [_ [_ [H6 _]]]; auto.
@@ -198,7 +198,7 @@ Proof.
   bdestruct_all; simpl; try lca.
   subst.
   rewrite 2 andb_true_r in H.
-  apply beq_nat_false in H.
+  apply Nat.eqb_neq in H.
   contradiction.
 Qed.
 
@@ -287,7 +287,7 @@ Proof.
   intros z.
   bdestruct_all; simpl; try lca.
   rewrite andb_true_r in H.
-  apply beq_nat_false in H.
+  apply Nat.eqb_neq in H.
   subst z.
   erewrite funbool_to_nat_eq in H2.
   2: { intros. rewrite funbool_to_nat_inverse. reflexivity.