fix for Coq v8.18 compatibility

.github/workflows/coq-action.yml

@@ -1,6 +1,7 @@
 name: CI
 
 on:
+  workflow_dispatch:
   push:
     branches: ['main']
   pull_request:
@@ -18,6 +19,7 @@ jobs:
           - '8.15'
           - '8.16'
           - '8.17'
+          - '8.18'
           - 'dev'
         ocaml_version:
           - 'default'
@@ -29,4 +31,3 @@ jobs:
           opam_file: 'coq-quantumlib.opam'
           coq_version: ${{ matrix.coq_version }}
           ocaml_version: ${{ matrix.ocaml_version }}
-

DiscreteProb.v

@@ -102,7 +102,7 @@
 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.
+  rewrite <- 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,14 +1498,16 @@
     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 (Nat.add_comm (2 ^ k) (2 ^ n * 2 ^ k - 2 ^ k)) in H0.
+    rewrite Nat.sub_add 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.
+    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.
+    apply (pow_positive 2 n) in H3.
     lia.
   - rewrite big_sum_0_bounded.
     rewrite Rmult_0_l; easy. 

Eigenvectors.v

@@ -6,7 +6,6 @@ Require Export Complex.
 Require Export Quantum. 
 Require Import FTA.
 
-
 (****************************)
 (** * Proving some indentities *)
 (****************************)
@@ -40,7 +39,8 @@ Lemma XH_eq_HZ : σx × hadamard = hadamard × σz. Proof. lma'. Qed.
 Lemma SX_eq_YS : Sgate × σx = σy × Sgate. Proof. lma'; unfold Mmult;
                                                    simpl; rewrite Cexp_PI2; lca. Qed.
 Lemma SZ_eq_ZS : Sgate × σz = σz × Sgate. Proof. lma'; unfold Mmult;
-                                                   simpl; rewrite Cexp_PI2; lca. Qed.
+                                              simpl; rewrite Cexp_PI2; lca. Qed.
+
 Lemma cnotX1 : cnot × (σx ⊗ I 2) = (σx ⊗ σx) × cnot. Proof. lma'. Qed.
 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.
@@ -258,8 +258,8 @@ Proof. induction n as [| n'].
              assert (H1 := (IHn' (reduce A 0 0))).
              rewrite p in H1; easy. }
            rewrite H', Pplus_comm, Pplus_degree2; auto. 
-           rewrite H1. 
-           apply le_lt_n_Sm.
+           rewrite H1.
+           rewrite Nat.lt_succ_r.
            apply Psum_degree; intros. 
            assert (H2 : prep_mat A (S i) 0 = [A (S i) 0]).
            { unfold prep_mat. 
@@ -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,9 @@ 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 (Nat.add_comm (m * (b / m)) (a - m * (b / m))) in H.
+       rewrite (Nat.add_comm (m * (b / m)) (b - m * (b / m))) in H.
+       rewrite ! Nat.sub_add in H.
        apply H.
        apply Nat.mul_div_le; apply H0.
        rewrite <- Hdiv; apply Nat.mul_div_le; apply H0.

Matrix.v

@@ -306,8 +306,8 @@
   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,10 +543,12 @@
   let y := fresh "y" in
   let H := fresh "H" in
   intros x y [H | H];
-  apply le_plus_minus in H; rewrite H;
+  apply Nat.sub_add in H;
+  rewrite Nat.add_comm in H;
+  rewrite <- H;
   cbv;
   destruct_m_eq;
-  try lca.
+  try lca.                                        
 
 (* Create HintDb wf_db. *)
 #[export] Hint Resolve WF_Zero WF_I WF_I1 WF_mult WF_plus WF_scale WF_transpose
@@ -1191,9 +1193,9 @@
   + repeat rewrite <- beq_nat_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). 
       2: specialize (Nat.mod_upper_bound y (S n)); intros; lia. 
       rewrite Cmult_1_r.
@@ -1209,13 +1211,13 @@
         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.
@@ -1227,7 +1229,6 @@
     rewrite H, H0; reflexivity.
 Qed.
 
-
 Local Open Scope nat_scope.
 
 Lemma div_mod : forall (x y z : nat), (x / y) mod z = (x mod (y * z)) / y.
@@ -1253,7 +1254,8 @@
     (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 (Nat.sub_add (y * z) x H) as G.
+  rewrite Nat.add_comm in 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 +1279,8 @@
   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 +1314,7 @@
   prep_matrix_equality.
   destruct q.
   + simpl.
-    rewrite mult_0_r.
+    rewrite Nat.mul_0_r.
     simpl.
     rewrite Cmult_0_r.
     reflexivity. 
@@ -2622,7 +2624,7 @@
        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 *)
@@ -2637,13 +2639,16 @@
        assert (H' : (big_sum (fun x : nat => (as' x 0 .* get_vec x T) i 0) (S m) = 
                      (@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. 
+         replace (S m) with (col + (S (m - col))) by lia; rewrite big_sum_sum.
+         rewrite <- (Nat.sub_add col m);
+           try rewrite (Nat.add_comm (m - col) col);
+           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 (Nat.add_comm col (m - col)).
+         rewrite (Nat.sub_add col m), <- 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 +2851,8 @@
        prep_matrix_equality. 
        unfold Mmult. 
        bdestruct (x <? m); try lia.
-       rewrite (le_plus_minus x m); try lia.
+       rewrite <- (Nat.sub_add x m);
+         try rewrite (Nat.add_comm (m - x) x); try lia.
        do 2 rewrite big_sum_sum. 
        apply Cplus_simplify. 
        apply big_sum_eq_bounded.
@@ -2858,7 +2864,9 @@
        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 <- (Nat.sub_add (y - x - 1) x');
+         try rewrite (Nat.add_comm (x' - (y - x - 1)) (y - x - 1));
+         try lia. 
        do 2 rewrite big_sum_sum.
        do 2 rewrite <- Cplus_assoc.
        apply Cplus_simplify. 
@@ -2915,7 +2923,9 @@
        prep_matrix_equality. 
        unfold Mmult.   
        bdestruct (x <? m); try lia.
-       rewrite (le_plus_minus x m); try lia.       
+       rewrite <- (Nat.sub_add x m);
+         try rewrite (Nat.add_comm (m - x) x);
+         try lia.
        do 2 rewrite big_sum_sum.
        apply Cplus_simplify. 
        apply big_sum_eq_bounded.
@@ -2927,7 +2937,9 @@
        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 <- (Nat.sub_add (y - x - 1) x');
+         try rewrite (Nat.add_comm (x' - (y - x - 1)) (y - x - 1));
+         try lia. 
        do 2 rewrite big_sum_sum.
        do 2 rewrite <- Cplus_assoc.
        apply Cplus_simplify. 
@@ -3242,7 +3254,7 @@
        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.
 
@@ -4347,7 +4359,7 @@
   | R : _ < _ |- _           => let d := fresh "d" in
                               destruct (lt_ex_diff_r _ _ R);
                               clear R; subst
-  | H : _ = _ |- _           => rewrite <- plus_assoc in H
+  | H : _ = _ |- _           => rewrite <- Nat.add_assoc in H
   | H : ?a + _ = ?a + _ |- _ => apply Nat.add_cancel_l in H; subst
   | H : ?a + _ = ?b + _ |- _ => destruct (lt_eq_lt_dec a b) as [[?|?]|?]; subst
   end; try lia.
@@ -4375,7 +4387,7 @@
   restore_dims; distribute_plus;
   repeat rewrite Nat.pow_add_r;
   repeat rewrite <- id_kron; simpl;
-  repeat rewrite mult_assoc;
+  repeat rewrite Nat.mul_assoc;
   restore_dims; repeat rewrite <- kron_assoc by auto_wf;
   restore_dims; repeat rewrite kron_mixed_product;
   (* simplify *)

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,8 @@ 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 (Nat.add_comm n (o - n)).
+    rewrite Nat.sub_add 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 +346,8 @@ 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 (Nat.add_comm o (n - o)).
+  rewrite Nat.sub_add 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.

Quantum.v

@@ -898,7 +898,8 @@ Proof.
         ++ apply functional_extensionality. intros x.
            bdestructΩ (n + x <? n).
            bdestructΩ (n <=? n + x).
-           rewrite minus_plus.
+           rewrite (Nat.add_comm n x).
+           rewrite Nat.add_sub.
            easy.
         ++ intros x L.
            bdestructΩ (y =? x).
@@ -955,7 +956,8 @@ Proof.
         ++ apply functional_extensionality. intros z.
            bdestructΩ (n + z <? n).
            bdestructΩ (n <=? n + z).
-           rewrite minus_plus.
+           rewrite (Nat.add_comm n z).
+           rewrite Nat.add_sub.
            easy.
         ++ rewrite big_sum_0. easy.
            intros z.