Update/v9.0

.github/workflows/coq-action.yml

@@ -18,6 +18,8 @@ jobs:
           - '8.18'
           - '8.19'
           - '8.20'
+          - '9.0'
+          - '9.1'
         ocaml_version:
           - 'default'
       fail-fast: false # don't stop jobs if one fails

Bits.v

@@ -353,7 +353,7 @@ Lemma nat_to_binlist_length : forall len n,
 Proof.
   intros len n Hlen.
   unfold nat_to_binlist.
-  rewrite app_length, repeat_length. 
+  rewrite length_app, repeat_length. 
   bdestruct (n =? 0); subst; simpl. lia.
   apply nat_to_binlist_length' in Hlen.
   lia.
@@ -646,8 +646,7 @@ Proof.
     easy.
   - rewrite (funbool_to_nat_shift _ _ n0); [|lia].
     replace (n0 + S n1 - n0) with (S n1) by lia.
-    rewrite Nat.add_comm, Nat.mul_comm, Nat.mod_add;
-    [|apply Nat.pow_nonzero; easy].
+    rewrite Nat.add_comm, Nat.mul_comm, Nat.Div0.mod_add.
     rewrite Nat.mod_small; [|apply funbool_to_nat_bound].
     easy.
 Qed.

CauchySchwarz.v

@@ -1,5 +1,5 @@
-Require Import Psatz.  
-Require Import Reals.
+From Stdlib Require Import Psatz.
+From Stdlib Require Import Reals.
 
 Require Export VecSet.
 

Complex.v

@@ -874,7 +874,7 @@ Proof.
     rewrite Rmult_div.
     rewrite Rmult_opp_opp.
     unfold Rminus.
-    rewrite <- Ropp_div.
+  rewrite <- Rdiv_opp_l.
     rewrite <- Rdiv_plus_distr.
     rewrite Rmult_plus_distr_r.
     rewrite Rmult_plus_distr_l.
@@ -1724,7 +1724,7 @@ Qed.
 Lemma Cexp_PIm4 : Cexp (- PI / 4) = /√2 - /√2 * Ci.
 Proof.
   unfold Cexp. 
-  rewrite Ropp_div.
+  rewrite Rdiv_opp_l.
   rewrite sin_antisym.
   rewrite cos_neg.
   rewrite sin_PI4, cos_PI4.
@@ -1775,7 +1775,7 @@ Proof.
   replace (7 * PI / 4)%R with (- PI / 4 + 2 * INR 1 * PI)%R.
   2:{ R_field_simplify. rewrite Rmult_1_r. lra. }
   rewrite cos_period, sin_period.
-  rewrite Ropp_div.
+  rewrite Rdiv_opp_l.
   rewrite cos_neg, sin_neg.
   rewrite sin_PI4, cos_PI4.
   eapply c_proj_eq; simpl.
@@ -1866,8 +1866,8 @@ Proof.
 		rewrite Rmult_0_l.
 		left.
 		apply Cexp_0.
-	-	rewrite S_O_plus_INR.
-		rewrite Rmult_plus_distr_r.
+	- rewrite S_O_plus_INR_depr.
+    rewrite Rmult_plus_distr_r.
 		rewrite Rmult_1_l.
 		rewrite Rplus_comm.
 		rewrite Cexp_plus_PI.
@@ -1887,7 +1887,7 @@ Proof.
 	- rewrite S_INR.
 		rewrite 2 Rmult_plus_distr_r.
 		rewrite Rmult_1_l.
-		rewrite double.
+		rewrite <- Rplus_diag.
 		rewrite <- Rplus_assoc.
 		rewrite 2 Cexp_plus_PI.
 		rewrite IHa.

Ctopology.v

@@ -297,7 +297,7 @@ Proof. unfold subset, ϵ_disk, open_square; intros.
          rewrite <- sqrt_Rsqr; try lra. 
          apply sqrt_lt_1_alt. split. 
          apply Rplus_le_le_0_compat; apply pow2_ge_0.
-         rewrite double_var.
+         rewrite <- Rplus_half_diag.
          apply Rplus_lt_compat;
          unfold Rsqr in *; simpl; lra. 
 Qed.
@@ -328,7 +328,7 @@ Lemma square_contains_center : forall (cen : C) (s : R),
   s > 0 -> open_square cen s cen.
 Proof. intros. 
        unfold open_square.
-       do 2 rewrite Rminus_eq_0, Rabs_R0; easy.
+       do 2 rewrite Rminus_diag, Rabs_R0; easy.
 Qed.
 
 (** some lemmas about open/closed sets *)
@@ -1547,7 +1547,7 @@ Proof. intros.
          unfold subset, open_rect; intros. 
          destruct H4; destruct c; subst; simpl in *. 
          split.
-         rewrite Rminus_eq_0, Rabs_R0; auto.  
+         rewrite Rminus_diag, Rabs_R0; auto.  
          apply Rabs_def1; lra.
          unfold subset; intros. 
          destruct H4; simpl.

DiscreteProb.v

@@ -806,7 +806,7 @@ Lemma length_apply_u : forall n (u : Square (2 ^ n)),
 Proof.
   intros n u.
   unfold apply_u.
-  rewrite map_length.
+  rewrite length_map.
   rewrite vec_to_list_length.
   reflexivity.
 Qed.
@@ -847,7 +847,7 @@ Proof.
   assumption.
   apply basis_vector_WF.
   apply pow_positive. lia.
-  rewrite map_length.  
+  rewrite length_map.  
   rewrite vec_to_list_length.
   assumption.
 Qed.
@@ -920,7 +920,7 @@ Qed.
 
 Lemma length_uniform : forall l r, (l <= r)%nat -> (length (uniform l r) = r)%nat.
 Proof.
-  intros. unfold uniform. rewrite app_length, repeat_length, repeat_length. lia.
+  intros. unfold uniform. rewrite length_app, repeat_length, repeat_length. lia.
 Qed.
 
 
@@ -951,7 +951,7 @@ Definition join l1 l2 := join' l1 l2 (length l1).
 
 Lemma fst_0 : forall m, fst m 0 = O.
 Proof.
-  intros. unfold fst. apply Nat.div_0_l. apply Nat.pow_nonzero. lia. 
+  intros. unfold fst. apply Nat.Div0.div_0_l.
 Qed.
 
 Lemma fst_plus : forall m x, fst m (2 ^ m + x) = S (fst m x).
@@ -969,7 +969,7 @@ Proof. intros. unfold fst. apply Nat.div_small. auto. Qed.
 
 Lemma snd_0 : forall m, snd m 0 = O.
 Proof.
-  intros. unfold snd. apply Nat.mod_0_l. apply Nat.pow_nonzero. lia. 
+  intros. unfold snd. apply Nat.Div0.mod_0_l.
 Qed.
 
 Lemma snd_small : forall m x, (x < 2 ^ m)%nat -> snd m x = x.
@@ -981,8 +981,7 @@ Proof.
   unfold snd.
   rewrite Nat.add_comm.
   rewrite <- (Nat.mul_1_l (2 ^ m)) at 1. 
-  apply Nat.mod_add.
-  apply Nat.pow_nonzero. lia. 
+  apply Nat.Div0.mod_add.
 Qed.
 
 Lemma simplify_fst : forall n x y,
@@ -1005,11 +1004,9 @@ Proof.
   intros n x y Hy.
   unfold snd. 
   rewrite Nat.add_comm.
-  rewrite Nat.mod_add.
+  rewrite Nat.Div0.mod_add.
   apply Nat.mod_small. 
   assumption.
-  apply Nat.pow_nonzero.
-  lia.
 Qed.
 
 Lemma sum_over_list_scale : forall x l,
@@ -1334,7 +1331,7 @@ Lemma length_join' : forall x l1 l2 m,
 Proof.
   induction x; intros.
   - reflexivity.
-  - simpl. rewrite app_length. rewrite IHx with (m := m).
+  - simpl. rewrite length_app. rewrite IHx with (m := m).
     rewrite length_scale. rewrite H. lia. lia.
     intros. apply H. lia.
 Qed.
@@ -1366,7 +1363,9 @@ Proof.
   Local Opaque firstn.
   simpl length.
   rewrite <- big_sum_extend_r, Rplus_comm.
-  repeat rewrite firstn_length_le.
+  simpl in Hn.
+  repeat rewrite firstn_length_le by lia.
+
   assert (aux : forall a b c d, (a < 2 + d)%nat ->
             nth a (b :: c :: firstn d l) 0 = nth a (b :: c :: l) 0).
   { clear.
@@ -1379,16 +1378,18 @@ Proof.
     apply nth_firstn.
     lia. }
   apply f_equal2.
-  rewrite aux. reflexivity. lia.
+  { rewrite aux; auto. }
+
+
   rewrite <- big_sum_extend_r, Rplus_comm.
   apply f_equal2.
-  rewrite aux. reflexivity. lia.
+  { rewrite aux; auto. lia. }
+  rewrite firstn_length_le. 2:{ simpl. lia. }
+
   apply big_sum_eq_bounded.
   intros i Hi.
   rewrite aux by lia. 
-  rewrite nth_firstn. reflexivity. lia.
-  lia.
-  simpl in Hn. lia.
+  rewrite nth_firstn; auto.
 Qed.
 
 (** If the probability of f1 in distr1(=l1) is r1 and the probability of 
@@ -1518,7 +1519,7 @@ Proof.
     rewrite fx.
     reflexivity. 
   - unfold apply_u.
-    rewrite map_length.
+    rewrite length_map.
     rewrite vec_to_list_length.
     easy.
 Qed. 

Eigenvectors.v

@@ -2,7 +2,7 @@
 (** This file contains more concepts relevent to quantum computing, as well as some more general linear algebra concepts such as Gram-Schmidt and eigenvectors/eigenvalues. *)
 
 Require Import Permutations.
-Require Import List.        
+From Stdlib Require Import List.        
 Require Export Complex.
 Require Export CauchySchwarz.
 Require Export Quantum. 
@@ -270,16 +270,15 @@ Qed.
 Lemma div_mod_eq : forall (a b m : nat),
   m <> 0 -> (a / m = b / m) -> (a mod m = b mod m) -> a = b.
 Proof. intros a b m H0 Hdiv Hmod.
-       rewrite (Nat.mod_eq a m), (Nat.mod_eq b m) in Hmod.
+       rewrite (Nat.Div0.mod_eq a m), (Nat.Div0.mod_eq b m) in 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.
        apply H.
-       apply Nat.mul_div_le; apply H0.
-       rewrite <- Hdiv; apply Nat.mul_div_le; apply H0.
-       apply H0. apply H0.
+       apply Nat.Div0.mul_div_le; apply H0.
+       rewrite <- Hdiv; apply Nat.Div0.mul_div_le; apply H0.
 Qed.
 
 Lemma diag_kron : forall {n m : nat} (A : Square n) (B : Square m), 
@@ -1841,22 +1840,23 @@ Proof. intros.
        apply (@Gplus_cancel_l C _ C_is_group) in H1.
        symmetry in H1. 
        destruct i; try lia.
-       eapply big_sum_squeeze in H1. 
+       eapply big_sum_squeeze in H1.
+       2:{ 
+
+        intros.
+        rewrite Cmult_comm, <- Cmod_sqr.
+        simpl. autorewrite with R_db.  
+        replace (Cmod (T 0%nat (S x)) * Cmod (T 0%nat  (S x)))%R with (Rsqr (Cmod (T 0%nat (S x)))).
+        apply Rle_0_sqr.
+        unfold Rsqr; easy. 
+       } 
        replace (fst (T 0 (S i) * (T 0 (S i)) ^*)%C) with 
-                 ((Rsqr (fst (T O (S i))) + Rsqr (snd (T O (S i))))%R) in H1. 
-       apply c_proj_eq.
-       apply Rplus_sqr_eq_0_l in H1; auto.
-       rewrite Rplus_comm in H1.
-       apply Rplus_sqr_eq_0_l in H1; auto. 
-       unfold Rsqr; simpl. lra.
-       intros. 
-       rewrite Cmult_comm, <- Cmod_sqr.
-       simpl. autorewrite with R_db.  
-       replace (Cmod (T 0%nat (S x)) * Cmod (T 0%nat (S x)))%R with (Rsqr (Cmod (T 0%nat (S x)))).
-       apply Rle_0_sqr.
-       unfold Rsqr; easy. 
-       apply Nat.succ_lt_mono in H3.
-       easy.
+                 ((Rsqr (fst (T O (S i))) + Rsqr (snd (T O (S i))))%R) in H1.
+       2:{ unfold Rsqr; simpl. lra. }
+       2:{ lia. }
+
+       apply Rplus_sqr_eq_0 in H1; destruct H1.
+       apply c_proj_eq; auto.
 Qed.
 
 (* this is the crucial step of Schur for => spectral theorem *)

FTA.v

@@ -47,7 +47,7 @@ Proof. intros.
          destruct n as [n [a [p' [H H0] ] ] ].
          rewrite H0, app_C0_compactify_reduce, app_nonzero_compactify_reduce; auto.
          unfold poly_coef_norm.
-         rewrite app_length, big_sum_sum, <- (Rplus_0_r).
+         rewrite length_app, big_sum_sum, <- (Rplus_0_r).
          apply f_equal_gen. 
          apply f_equal_gen; auto.
          apply big_sum_eq_bounded; intros. 
@@ -119,7 +119,7 @@ Proof. intros.
        apply Rlt_minus_r.
        replace (Cmod z - Cmod z * / 2)%R with (Cmod z /2 + Cmod z /2 - Cmod z * / 2)%R.
        lra.
-       rewrite <- (double_var (Cmod z)); easy.
+       rewrite <- (Rplus_half_diag (Cmod z)). lra.
 Qed.
 
 Lemma leading_term_dom : forall (p : Polynomial) (a c : C),
@@ -333,7 +333,7 @@ Proof. intros.
                       (repeat C0 (k + 1)) ++ (C0 :: p)).
        { replace (C0 :: p) with ([C0] ++ p) by easy.
          rewrite app_assoc, <- repeat_cons; simpl. 
-         rewrite app_length, repeat_length; simpl; easy. }
+         rewrite length_app, repeat_length; simpl; easy. }
        rewrite H5, mul_by_x_to_n, Cpow_mul_l, (Cmult_comm (ϵ ^ (k + 1))), Cmult_assoc.
        repeat rewrite Cmod_mult.
        rewrite RtoC_pow, Cmod_R, Rabs_pos_eq; try (apply pow_le; lra).

FiniteGroups.v

@@ -1,9 +1,9 @@
-Require Import List.
+From Stdlib Require Import List.
 Require Import Prelim.
 Require Import Summation. 
-Require Import FinFun. 
-Require Import ListDec.
-Require Import Setoid.
+From Stdlib Require Import FinFun. 
+From Stdlib Require Import ListDec.
+From Stdlib Require Import Setoid.
 
 (* two important list functions used are NoDup and incl *)
 (* in the following sections, we expand on these list functions *)
@@ -27,7 +27,7 @@ Proof. induction l.
          destruct l'; easy.
        - intros.
          simpl in *; subst.
-         rewrite app_length, (IHl (G_big_plus l)); easy. 
+         rewrite length_app, (IHl (G_big_plus l)); easy. 
 Qed.
 
 Lemma length_big_sum_list : forall {X} (l : list (list X)),
@@ -182,9 +182,9 @@ Proof. induction l1; intros; inversion H.
          subst. 
          apply EMP_reduce in H.
          apply IHl1 in H.
-         rewrite app_length; simpl. 
+         rewrite length_app; simpl. 
          rewrite Nat.add_succ_r; apply eq_S. 
-         rewrite <- app_length.
+         rewrite <- length_app.
          easy. 
 Qed.
 
@@ -527,11 +527,11 @@ Proof. intros.
        unfold coset_rep_list_to_cosets.
        rewrite length_big_sum_list.
        rewrite (big_plus_constant _ (group_size H)).
-       rewrite times_n_nat, map_map, map_length; easy. 
+       rewrite times_n_nat, map_map, length_map; easy. 
        intros.
        rewrite map_map in H7.
        apply in_map_iff in H7; destruct H7 as [x [H7 H8]]; subst.
-       rewrite map_map, map_length; easy.
+       rewrite map_map, length_map; easy.
 Qed.
 
 
@@ -561,17 +561,17 @@ Lemma get_coset_rep_list2 : forall H G `{FiniteGroup H} `{FiniteGroup G} (f : H
   exists l, group_size H * length l >= group_size G /\ NoDup (coset_rep_list_to_cosets H G f l).
 Proof. intros. 
        destruct (get_coset_rep_list1 H G f (group_size G / group_size H)%nat) as [l [H7 H8]]; auto.
-       apply Nat.mul_div_le. 
-       assert (H' := group_size_gt_0 H). lia. 
+       apply Nat.Div0.mul_div_le.
+       assert (H' := group_size_gt_0 H).
        bdestruct (group_size H * length l <? group_size G).
        - destruct (extend_coset_rep_list H G f l) as [g H10]; auto.
          rewrite length_cosets; auto.
          exists (g :: l); split; auto.
          simpl; rewrite H7.
-         assert (H' := group_size_gt_0 H).
-         assert (H'' : group_size H <> 0). 
+         assert (H'' := group_size_gt_0 H).
+         assert (H''' : group_size H <> 0). 
          destruct (group_size H); try easy.
-         apply (Nat.mul_succ_div_gt (group_size G) (group_size H)) in H''.
+         apply (Nat.mul_succ_div_gt (group_size G) (group_size H)) in H'''.
          lia.
        - exists l; split; easy.
 Qed.