diff --git a/.github/workflows/coq-action.yml b/.github/workflows/coq-action.yml index 5a4c355..547daf9 100644 --- a/.github/workflows/coq-action.yml +++ b/.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 diff --git a/Bits.v b/Bits.v index acd17b6..37ae4ec 100644 --- a/Bits.v +++ b/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. diff --git a/CauchySchwarz.v b/CauchySchwarz.v index cd2a25a..d8031e1 100644 --- a/CauchySchwarz.v +++ b/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. diff --git a/Complex.v b/Complex.v index 51f5a35..44816e7 100644 --- a/Complex.v +++ b/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. diff --git a/Ctopology.v b/Ctopology.v index 25d1ab2..29f12d8 100644 --- a/Ctopology.v +++ b/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. diff --git a/DiscreteProb.v b/DiscreteProb.v index 9b61a22..384060d 100644 --- a/DiscreteProb.v +++ b/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. diff --git a/Eigenvectors.v b/Eigenvectors.v index 851e9f4..cf909ad 100644 --- a/Eigenvectors.v +++ b/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 *) diff --git a/FTA.v b/FTA.v index c42cca6..13824e7 100644 --- a/FTA.v +++ b/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). diff --git a/FiniteGroups.v b/FiniteGroups.v index 29eb619..d7cbb87 100644 --- a/FiniteGroups.v +++ b/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 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. diff --git a/GenMatrix.v b/GenMatrix.v index ac4c20e..ae49757 100644 --- a/GenMatrix.v +++ b/GenMatrix.v @@ -1,12 +1,12 @@ (** In this file, we define matrices and prove many basic facts from linear algebra *) -Require Import Psatz. -Require Import String. -Require Import Program. -Require Import List. +From Stdlib Require Import Psatz. +From Stdlib Require Import String. +From Stdlib Require Import Program. +From Stdlib Require Import List. Require Export Summation. -Require Import Setoid. +From Stdlib Require Import Setoid. Require Import Modulus. @@ -1871,8 +1871,8 @@ Proof. bdestruct (x mod n =? y mod n); simpl; dumb_lRa. destruct n; simpl; dumb_lRa. contradict Eq. - rewrite (Nat.div_mod x (S n)) by lia. - rewrite (Nat.div_mod y (S n)) by lia. + rewrite (Nat.Div0.div_mod x (S n)) by lia. + rewrite (Nat.Div0.div_mod y (S n)) by lia. rewrite H, H0; reflexivity. Qed. @@ -1997,7 +1997,7 @@ Proof. induction l1. - intros. simpl. rewrite IHl1. rewrite kron_assoc. do 2 (rewrite <- Nat.pow_add_r). - rewrite app_length. + rewrite length_app. reflexivity. assert (H' := H 0); simpl in H'; easy. all : try apply (WF_big_kron _ _ _ (@Zero n m)); try easy. @@ -2363,8 +2363,8 @@ Proof. rewrite make_WF_equiv. intros i j Hi Hj. unfold list2D_to_genmatrix. - rewrite (map_nth_small Zero) by now rewrite map_length, seq_length. - rewrite (map_nth_small 0) by now rewrite seq_length. + rewrite (map_nth_small Zero) by now rewrite length_map, length_seq. + rewrite (map_nth_small 0) by now rewrite length_seq. rewrite nth_vec_to_list by easy. now rewrite seq_nth by easy. Qed. diff --git a/GenRowColOps.v b/GenRowColOps.v index ece55e9..5afcc23 100644 --- a/GenRowColOps.v +++ b/GenRowColOps.v @@ -1,5 +1,5 @@ -Require Import Psatz. -Require Import Reals. +From Stdlib Require Import Psatz. +From Stdlib Require Import Reals. Require Export GenMatrix. @@ -442,14 +442,6 @@ Proof. unfold WF_GenMatrix in *. bdestruct (x WF_GenMatrix T2 -> WF_GenMatrix (smash T1 T2). Proof. unfold WF_GenMatrix, smash in *. @@ -532,7 +524,7 @@ Qed. #[export] Hint Resolve WF_get_col WF_get_row WF_reduce_row WF_reduce_col WF_reduce_vecn WF_get_minor : wf_db. -#[export] Hint Resolve WF_row_append WF_col_append WF_row_wedge WF_col_wedge WF_smash : wf_db. +#[export] Hint Resolve WF_row_wedge WF_col_wedge WF_smash : wf_db. #[export] Hint Resolve WF_col_swap WF_row_swap WF_col_scale WF_row_scale WF_col_add WF_row_add : wf_db. #[export] Hint Resolve WF_gen_new_col WF_gen_new_row WF_col_add_many WF_row_add_many : wf_db. #[export] Hint Resolve WF_col_scale_many WF_row_scale_many WF_col_add_each WF_row_add_each : wf_db. diff --git a/GenSubspaces.v b/GenSubspaces.v index a5e6ae8..9b3add7 100644 --- a/GenSubspaces.v +++ b/GenSubspaces.v @@ -1,4 +1,6 @@ -Require Import Permutation. +From Stdlib Require Import Permutation. +From Stdlib Require Import Logic. +From Stdlib Require Import Vectors.FinFun. Require Export Summation. Require Export GenVecSet. @@ -372,8 +374,8 @@ Proof. intros n m A H0. + rewrite nth_overflow. * rewrite H0; trivial. lia. - * rewrite map_length. - rewrite seq_length. + * rewrite length_map. + rewrite length_seq. assumption. - bdestruct (y if (y =? 0)%nat then M x1 i0 else 0) (S m)). - 2 : rewrite map_length; - rewrite seq_length; + 2 : rewrite length_map; + rewrite length_seq; assumption. rewrite map_nth with (d := S m). bdestruct_all. @@ -431,7 +433,7 @@ Proof. intros n m P M a H0 H1 H2. bdestruct_all. rewrite Gmult_0_r, Gplus_0_r. f_equal. - 2 : symmetry; apply seq_length. + 2 : symmetry; apply length_seq. apply functional_extensionality; intros. assert ((x1 >= S m)%nat \/ (x0 >= 1)%nat). { right. assumption. } specialize (H0' x1 x0 H5). @@ -448,10 +450,10 @@ Proof. intros n m P M a H0 H1 H2. unfold subspace in H1. destruct H1 as [WFP [PZero [Psum Pscale]]]. apply Psum. - + rewrite ! seq_length. + + rewrite ! length_seq. apply IHm. * pose (WF_GenMatrix_vector_row_choose_indices_list (List.seq 0 m) a). - rewrite ! seq_length in w; auto. + rewrite ! length_seq in w; auto. * intros i0 H1. assert (get_col (matrix_column_choose (List.seq 0 m) M) i0 = get_col M i0). { unfold matrix_column_choose, list_vector_to_matrix. @@ -460,8 +462,8 @@ Proof. intros n m P M a H0 H1 H2. bdestruct_all; trivial. subst. rewrite nth_indep with (d' := (fun i1 x0 y : nat => if (y =? 0)%nat then M x0 i1 else 0) (S m)). - 2 : rewrite map_length; - rewrite seq_length; + 2 : rewrite length_map; + rewrite length_seq; assumption. rewrite map_nth with (d := S m). bdestruct_all. @@ -718,7 +720,7 @@ Proof. intros A d l H0. apply nth_In. rewrite H0. rewrite removelast_last. - rewrite app_length. + rewrite length_app. simpl. lia. Qed. @@ -946,15 +948,14 @@ Proof. intros n m M H0 H1 H2. (if x1 M x y * u y x0) m @@ -1004,19 +1005,19 @@ Proof. intros n m M H0 H1 H2. bdestruct_all. - rewrite <- nth_firstn with (n := i); try lia. rewrite firstn_app. - rewrite seq_length. + rewrite length_seq. replace (i - i)%nat with 0%nat by lia. simpl. rewrite app_nil_r. replace i with (length (List.seq 0 i)) at 1 - by (rewrite seq_length; reflexivity). + by (rewrite length_seq; reflexivity). rewrite firstn_all. rewrite seq_nth; try lia. simpl. ring. - subst. rewrite app_assoc. replace (m - 1)%nat with (length (List.seq 0 i ++ List.seq (i + 1) (m - i - 1))) - by (rewrite app_length; rewrite ! seq_length; lia). + by (rewrite length_app; rewrite ! length_seq; lia). rewrite nth_middle. reflexivity. - bdestruct (x1 M x z * u z x0). - 2: rewrite seq_length; lia. + 2: rewrite length_seq; lia. replace (List.seq 0 m) with (List.seq 0 i ++ List.seq i (m - i)) by (rewrite <- seq_app; f_equal; lia). apply Permutation_app. @@ -1180,7 +1181,6 @@ Proof. intros n m M H0 H1. apply Cplus_inv_r with (c := (M x i * u i 0%nat)%C). replace (- (M x i * u i 0%nat) + M x i * u i 0%nat)%C with C0 by lca. rewrite <- H4 at 1. - Search big_sum. assert (Σ (fun x1 : nat => @@ -1196,15 +1196,14 @@ Proof. intros n m M H0 H1. (if x1 M x y * u y x0) m @@ -1254,19 +1253,19 @@ Proof. intros n m M H0 H1. bdestruct_all. - rewrite <- nth_firstn with (n := i); try lia. rewrite firstn_app. - rewrite seq_length. + rewrite length_seq. replace (i - i)%nat with 0%nat by lia. simpl. rewrite app_nil_r. replace i with (length (List.seq 0 i)) at 1 - by (rewrite seq_length; reflexivity). + by (rewrite length_seq; reflexivity). rewrite firstn_all. rewrite seq_nth; try lia. lca. - subst. rewrite app_assoc. replace (m - 1)%nat with (length (List.seq 0 i ++ List.seq (i + 1) (m - i - 1))) - by (rewrite app_length; rewrite ! seq_length; lia). + by (rewrite length_app; rewrite ! length_seq; lia). rewrite nth_middle. reflexivity. - bdestruct (x1 M x z * u z x0). - 2: rewrite seq_length; lia. + 2: rewrite length_seq; lia. replace (List.seq 0 m) with (List.seq 0 i ++ List.seq i (m - i)) by (rewrite <- seq_app; f_equal; lia). apply Permutation_app. @@ -1343,12 +1342,12 @@ Proof. intros n m M H0 H1. rewrite seq_nth; try lia. rewrite <- nth_firstn with (n := i); try lia. rewrite firstn_app. - rewrite seq_length. + rewrite length_seq. replace (i - i)%nat with 0%nat by lia. simpl. rewrite app_nil_r. replace i with (length (List.seq 0 i)) at 1 - by (rewrite seq_length; reflexivity). + by (rewrite length_seq; reflexivity). rewrite firstn_all. rewrite seq_nth; lia. ---- rewrite in_seq in H13. @@ -1358,27 +1357,27 @@ Proof. intros n m M H0 H1. *** f_equal. ---- rewrite map_ext_nth. assert (length (List.seq (i + 1) (m - i - 1)) = length (List.seq i (m - i - 1))). - { rewrite ! seq_length. + { rewrite ! length_seq. reflexivity. } split; try assumption. intros n0 H14. - rewrite seq_length in H14. + rewrite length_seq in H14. f_equal. ++++ f_equal. rewrite ! seq_nth; try lia. **** rewrite <- nth_firstn with (n := (i + n0 + 1)%nat). ----- rewrite <- Nat.add_assoc with (n := i) (m := n0) (p := 1%nat). replace i with (length (List.seq 0 i)) at 3 - by (rewrite seq_length; reflexivity). + by (rewrite length_seq; reflexivity). rewrite firstn_app_2. rewrite app_nth2 with (n := (i + n0)%nat); - try (rewrite seq_length; lia). - rewrite seq_length. + try (rewrite length_seq; lia). + rewrite length_seq. replace (i + n0 - i)%nat with n0 by lia. rewrite nth_firstn; try lia. rewrite <- nth_firstn with (n := (m - i - 1)%nat); try lia. rewrite firstn_app. - rewrite seq_length. + rewrite length_seq. replace (m - i - 1 - (m - i - 1))%nat with 0%nat by lia. simpl. rewrite app_nil_r. @@ -1401,8 +1400,8 @@ Proof. intros n m M H0 H1. +++++ f_equal. rewrite seq_nth; try lia. assert (length (List.seq 0 i ++ List.seq (i + 1) (m - i - 1)) + 0 = m - 1)%nat. - { rewrite app_length. - rewrite ! seq_length. + { rewrite length_app. + rewrite ! length_seq. lia. } rewrite <- H15. rewrite app_assoc. @@ -1695,7 +1694,7 @@ Proof. intros. - rewrite nth_overflow. + unfold WF_GenMatrix in H. rewrite H; auto. - + rewrite seq_length; trivial. + + rewrite length_seq; trivial. Qed. Lemma WF_GenMatrix_submatrix_column : forall {n m} (k : nat) (M : GenMatrix n m), @@ -1731,7 +1730,6 @@ Proof. intros n m M H H0 H1. induction m. - exists 0%nat. intros. - Search Zero. unfold linearly_dependent in H1. destruct H1 as [a [H1 [H2 H3]]]. contradict H2. @@ -2440,24 +2438,24 @@ Proof. intros n m k indices_list A H H0. unfold get_col. bdestruct_all. f_equal. - rewrite ! app_nth1; trivial; rewrite firstn_length; lia. + rewrite ! app_nth1; trivial; rewrite length_firstn; lia. - rewrite H1. rewrite ! map_nth with (d := m). unfold get_col. bdestruct_all. f_equal. rewrite app_nth2. - + rewrite firstn_length. + + rewrite length_firstn. replace (Init.Nat.min k (length indices_list)) with k by lia. rewrite <- firstn_skipn with (n := (k + 1)%nat) at 1. rewrite app_nth2. - * rewrite firstn_length. + * rewrite length_firstn. replace (Init.Nat.min (k + 1) (length indices_list)) with (k + 1)%nat by lia. f_equal. lia. - * rewrite firstn_length. + * rewrite length_firstn. lia. - + rewrite firstn_length. + + rewrite length_firstn. lia. Qed. @@ -2465,9 +2463,9 @@ Lemma length_delete_nth : forall {A : Type} (l : list A) (k : nat), (k < length l)%nat -> length (delete_nth l k) = ((length l) - 1)%nat. Proof. intros A l k H0. unfold delete_nth. - rewrite app_length. - rewrite firstn_length. - rewrite skipn_length. + rewrite length_app. + rewrite length_firstn. + rewrite length_skipn. lia. Qed. @@ -2583,7 +2581,7 @@ Proof. intros n m o P M A H0 H1 H2 H3 H4 nonzero_col_M nonzero_col_A j H5. - right. exists (List.seq 0 m). split. - + rewrite seq_length. lia. + + rewrite length_seq. lia. + split. * unfold incl. intros a H6. @@ -2602,7 +2600,7 @@ Proof. intros n m o P M A H0 H1 H2 H3 H4 nonzero_col_M nonzero_col_A j H5. bdestruct_all. replace (y - 0)%nat with y by lia. reflexivity. } - rewrite seq_length. + rewrite length_seq. rewrite H9. split; auto. - assert (H6 : (j <= m)%nat). { lia. } @@ -3076,24 +3074,13 @@ Lemma permutation_repeat_nth : forall {A : Type} {a : A} {l : list A}, Permutation l (repeat a (length l)) <-> (forall i, nth i l a = a). Proof. intros A a l. split; intros. - - rewrite Permutation_nth in H. - destruct H as [H [f [H0 [H1 H2]]]]. - remember H1 as H3. clear HeqH3. - rewrite FinFun.bInjective_bSurjective in H3; auto. - destruct (FinFun.bSurjective_bBijective H0 H3) as [g [H4 H5]]. - bdestruct (i a i0 0%nat) (List.seq 1 (length l))) = (map (fun i : nat => a (i + 1)%nat 0%nat) (List.seq 0 (length l)))). { apply nth_ext with (d := 0%G) (d' := 0%G). - - rewrite ! map_length, ! seq_length; reflexivity. + - rewrite ! length_map, ! length_seq; reflexivity. - intros n0 H2. rewrite nth_indep with (d' := a 0%nat 0%nat); auto. rewrite map_nth with (f := (fun i0 : nat => a i0 0%nat)) (d := 0%nat). @@ -3158,8 +3145,8 @@ Proof. intros n l1 l2 H a H0. f_equal. rewrite ! seq_nth. lia. - all : try rewrite map_length, seq_length; - rewrite map_length, seq_length in H2; + all : try rewrite length_map, length_seq; + rewrite length_map, length_seq in H2; auto. } rewrite H2. assert ((map @@ -3167,9 +3154,9 @@ Proof. intros n l1 l2 H a H0. (List.seq 1 (length l'))) = (map (fun i : nat => b i 0%nat) (List.seq 0 (length l')))). { apply nth_ext with (d := 0%G) (d' := 0%G). - - rewrite ! map_length, ! seq_length; reflexivity. + - rewrite ! length_map, ! length_seq; reflexivity. - intros n0 H3. - rewrite map_length, seq_length in H3. + rewrite length_map, length_seq in H3. rewrite nth_indep with (d' := (fun i0 : nat => if (i0 =? 0)%nat then a 0%nat 0%nat else b (i0 - 1)%nat 0%nat) 0%nat); auto. @@ -3181,8 +3168,8 @@ Proof. intros n l1 l2 H a H0. + rewrite seq_nth in H4; auto; lia. + do 2 f_equal. rewrite ! seq_nth; auto; lia. - + rewrite map_length, seq_length; easy. - + rewrite map_length, seq_length; easy. } + + rewrite length_map, length_seq; easy. + + rewrite length_map, length_seq; easy. } rewrite H3. auto. - exists (fun r c => if (r =? 0)%nat then a 1%nat c else @@ -3209,9 +3196,9 @@ Proof. intros n l1 l2 H a H0. (List.seq 2 (length l)) = map (fun i0 : nat => a i0 0%nat) (List.seq 2 (length l))). { apply nth_ext with (d := 0%G) (d' := 0%G). - - rewrite ! map_length; reflexivity. + - rewrite ! length_map; reflexivity. - intros n0 H. - rewrite ! map_length, seq_length in H. + rewrite ! length_map, length_seq in H. rewrite nth_indep with (d' := (fun i0 : nat => if (i0 =? 0)%nat then a 1%nat 0%nat @@ -3225,8 +3212,8 @@ Proof. intros n l1 l2 H a H0. bdestruct_all; auto. + rewrite seq_nth in H1; auto; lia. + rewrite seq_nth in H2; auto; lia. - + rewrite map_length, seq_length; auto. - + rewrite map_length, seq_length; auto. } + + rewrite length_map, length_seq; auto. + + rewrite length_map, length_seq; auto. } rewrite H. apply perm_swap. - destruct (IHPermutation1 a H0) as [b [H2 [H3 H4]]]. @@ -3251,10 +3238,10 @@ Proof. intros n l1 l2 H0 H1. rewrite H1 in H6. unfold Zero in H6. rewrite map_const_repeat in H6. - rewrite seq_length in H6. + rewrite length_seq in H6. rewrite <- (Permutation_length H0) in H6. assert (H7 : forall i, nth i (map (fun i : nat => a i 0%nat) (List.seq 0 (length l2))) 0%G = 0%G) - by (rewrite <- permutation_repeat_nth, map_length, seq_length; auto). + by (rewrite <- permutation_repeat_nth, length_map, length_seq; auto). assert (H8 : forall i, (i < length l2)%nat -> a i 0%nat = 0%G). { intros i0 H8. assert (H9 : a (length l2) 0%nat = 0%G) by (rewrite H2; auto). @@ -3305,8 +3292,8 @@ Proof. intros n l1 l2 P H0 H1 H2 i0 H3. rewrite Permutation_nth in H4. destruct H4 as [H4 [f [H5 [H6 H7]]]]. remember H6 as H8. clear HeqH8. - rewrite (FinFun.bInjective_bSurjective H5) in H8. - destruct (FinFun.bSurjective_bBijective H5 H8) as [g [H9 H10]]. + rewrite (bInjective_bSurjective H5) in H8. + destruct (bSurjective_bBijective H5 H8) as [g [H9 H10]]. rewrite H4 in *. rewrite H7; auto. Qed. @@ -3328,9 +3315,9 @@ Proof. intros n m indices_list1 indices_list2 M H0. rewrite Permutation_nth in H0. destruct H0 as [eq_len [f [bFunf [bInjf eq_nth]]]]. rewrite Permutation_nth. - split; try rewrite ! map_length, eq_len; auto. + split; try rewrite ! length_map, eq_len; auto. exists f. - repeat split; try rewrite map_length; auto. + repeat split; try rewrite length_map; auto. intros x H0. setoid_rewrite map_nth with (f := (fun i0 : nat => get_col M i0)). f_equal. @@ -3347,29 +3334,29 @@ Proof. intros n m indices_list1 indices_list2 P M H0 H1 H2. unfold basis, matrix_column_choose. split; intros H3; destruct H3 as [H4 [H5 [H6 H7]]]; repeat (split; intros; auto). - pose (permutation_preserves_subspace_containment H4 p). - rewrite ! map_length in p0. + rewrite ! length_map in p0. specialize (p0 H5). apply p0; auto. - pose (permutation_preserves_span p). - rewrite ! map_length in s. + rewrite ! length_map in s. specialize (s v). apply s; auto. - pose (permutation_preserves_linearly_indep p). - rewrite ! map_length in l. + rewrite ! length_map in l. specialize (l H7); auto. - apply Permutation_sym in p. pose (permutation_preserves_subspace_containment H4 p). - rewrite ! map_length in p0. + rewrite ! length_map in p0. specialize (p0 H5). apply p0; auto. - apply Permutation_sym in p. pose (permutation_preserves_span p). - rewrite ! map_length in s. + rewrite ! length_map in s. specialize (s v). apply s; auto. - apply Permutation_sym in p. pose (permutation_preserves_linearly_indep p). - rewrite ! map_length in l. + rewrite ! length_map in l. specialize (l H7); auto. Qed. @@ -3483,7 +3470,7 @@ Proof. intros n m P M H H0 H1 H2 H3 H4. reflexivity. } rewrite ! H16. destruct basis_P as [subspaceP [in_P [spans_P lin_ind]]]. - rewrite ! map_length. + rewrite ! length_map. repeat (split; auto). -- apply not_lindep_implies_linindep in H15. exists (delete_nth (List.seq 0 (S (S m))) i). @@ -3502,17 +3489,17 @@ Proof. intros n m P M H H0 H1 H2 H3 H4. { setoid_rewrite nth_helper with (x := 0%nat) at 2. replace (S i) with (i + 1)%nat by lia. rewrite seq_nth. - all : try rewrite seq_length; auto. } + all : try rewrite length_seq; auto. } rewrite H16. rewrite firstn_skipn. apply seq_NoDup. ** unfold basis. rewrite <- ! reduce_col_matrix_column_choose_delete; auto. - 2: rewrite seq_length; assumption. + 2: rewrite length_seq; assumption. rewrite ! matrix_column_choose_original; auto. rewrite ! length_delete_nth. - 2: rewrite seq_length; assumption. - rewrite ! seq_length. + 2: rewrite length_seq; assumption. + rewrite ! length_seq. replace ((S (S m)) - 1)%nat with (S m) by lia. repeat (split; auto). - apply not_lindep_implies_linindep in H5. @@ -3523,7 +3510,7 @@ Proof. intros n m P M H H0 H1 H2 H3 H4. * apply seq_NoDup. * unfold basis. rewrite matrix_column_choose_original; auto. - rewrite ! seq_length. + rewrite ! length_seq. repeat (split; try assumption). Qed. @@ -4129,13 +4116,13 @@ Proof. intros n d P A H H0 H1 H2 H3. exists (matrix_column_choose indices_list A). split; auto with wf_db. } pose (unique_dimension H9 H1'). - rewrite seq_length, e; auto. } + rewrite length_seq, e; auto. } pose (NoDup_Permutation_bis NoDuplist H9 incl_list) as p. rewrite (permutation_preserves_basis H subspaceP p) in basisP. unfold basis in basisP. destruct basisP as [subspaceP' [AinP [AspansP linindepA]]]. rewrite matrix_column_choose_original in *; auto. - rewrite ! seq_length in *; auto. + rewrite ! length_seq in *; auto. Qed. Lemma equal_dimension_span_basis : forall {n d : nat} {P : GenVector n -> Prop} {A : GenMatrix n d}, @@ -4430,7 +4417,7 @@ Proof. intros n m d M WFM H. pose (basis_equal_number WFB H1 basisB' basis_subset) as e. rewrite e. pose (NoDup_incl_length NoDup_indices incl_indices) as l. - rewrite seq_length in l. auto. + rewrite length_seq in l. auto. Qed. Lemma zerospace_is_subspace : forall {n : nat}, subspace (fun v : GenVector n => v = Zero). @@ -4558,7 +4545,7 @@ Proof. intros n m M H. bdestruct_all. bdestruct (y nth c list_vector (@Zero n 1%nat) r 0%nat) (length list_vector)). { prep_genmatrix_equality. @@ -4601,8 +4588,8 @@ Proof. intros m n2 n1 A1 A2. apply nth_ext with (d := (fun i x y : nat => if y =? 0 then if i if y =? 0 then A2 x i else 0) 0%nat). - + rewrite ! map_length. rewrite ! seq_length. auto. - + intros n H. rewrite ! map_length in H. rewrite ! seq_length in H. + + rewrite ! length_map. rewrite ! length_seq. auto. + + intros n H. rewrite ! length_map in H. rewrite ! length_seq in H. rewrite ! map_nth with (d := 0%nat). prep_genmatrix_equality. bdestruct_all; auto. @@ -4621,12 +4608,12 @@ Proof. intros m n2 n1 A1 A2 H H0 H1. rewrite <- matrix_to_list_vector_to_matrix; auto with wf_db. pose (permutation_preserves_linearly_indep H2) as l. assert ((@length (GenVector m) (@matrix_to_list_vector m (n2 + n1) (smash A2 A1))) = - n2 + n1). { unfold matrix_to_list_vector. rewrite map_length, seq_length. auto. } + n2 + n1). { unfold matrix_to_list_vector. rewrite length_map, length_seq. auto. } rewrite H3 in l. apply l. rewrite matrix_to_list_vector_to_matrix; auto with wf_db. assert ((@length (GenVector m) (@matrix_to_list_vector m (n1 + n2) (smash A1 A2))) = - n1 + n2). { unfold matrix_to_list_vector. rewrite map_length, seq_length. auto. } + n1 + n2). { unfold matrix_to_list_vector. rewrite length_map, length_seq. auto. } rewrite H4. auto. Qed. @@ -4650,8 +4637,8 @@ Proof. intros. rewrite <- matrix_to_list_vector_to_matrix; auto with wf_db. assert (length (matrix_to_list_vector (smash A2 A1)) = (n2 + n1)%nat). { unfold matrix_to_list_vector. - rewrite map_length. - rewrite seq_length. auto. } + rewrite length_map. + rewrite length_seq. auto. } pose (@permutation_preserves_span m (matrix_to_list_vector (smash A1 A2)) (matrix_to_list_vector (smash A2 A1)) H2) as e. @@ -4660,8 +4647,8 @@ Proof. intros. rewrite matrix_to_list_vector_to_matrix; auto with wf_db. assert (length (matrix_to_list_vector (smash A1 A2)) = (n1 + n2)%nat). { unfold matrix_to_list_vector. - rewrite map_length. - rewrite seq_length. auto. } + rewrite length_map. + rewrite length_seq. auto. } rewrite H4. apply H1; auto. Qed. diff --git a/GenVecSet.v b/GenVecSet.v index 3cbdbcd..c8bbf4d 100644 --- a/GenVecSet.v +++ b/GenVecSet.v @@ -3,8 +3,8 @@ (** In this file, we define more advanced linear algebra concepts such as bases, linear independence, etc... *) -Require Import Psatz. -Require Import Reals. +From Stdlib Require Import Psatz. +From Stdlib Require Import Reals. Require Export GenRowColOps. diff --git a/Kronecker.v b/Kronecker.v index 91083fb..db22692 100644 --- a/Kronecker.v +++ b/Kronecker.v @@ -172,7 +172,7 @@ Proof. unfold mx_to_vec; auto with wf_db. Qed. #[export] Hint Resolve WF_mx_to_vec : wf_db. (* Compute vec_to_list (mx_to_vec (Matrix.I 2)). *) -From Coq Require Import ZArith. +From Stdlib Require Import ZArith. Ltac Zify.zify_post_hook ::= PreOmega.Z.div_mod_to_equations. Lemma kron_comm_mx_to_vec_helper : forall i p q, (i < p * q)%nat -> diff --git a/Matrix.v b/Matrix.v index 02737f4..101a856 100644 --- a/Matrix.v +++ b/Matrix.v @@ -1,12 +1,12 @@ (** In this file, we define matrices and prove many basic facts from linear algebra *) -Require Import Psatz. -Require Import String. -Require Import Program. +From Stdlib Require Import Psatz. +From Stdlib Require Import String. +From Stdlib Require Import Program. Require Export Complex. -Require Import List. -Require Import Setoid. +From Stdlib Require Import List. +From Stdlib Require Import Setoid. Require Import Modulus. @@ -1789,8 +1789,8 @@ Proof. bdestruct (x mod n =? y mod n); simpl; try lca. destruct n; try lca. contradict Eq. - rewrite (Nat.div_mod x (S n)) by lia. - rewrite (Nat.div_mod y (S n)) by lia. + rewrite (Nat.Div0.div_mod x (S n)) by lia. + rewrite (Nat.Div0.div_mod y (S n)) by lia. rewrite H, H0; reflexivity. Qed. @@ -1912,7 +1912,7 @@ Proof. induction l1. - intros. simpl. rewrite IHl1. rewrite kron_assoc. do 2 (rewrite <- Nat.pow_add_r). - rewrite app_length. + rewrite length_app. reflexivity. assert (H' := H 0); simpl in H'; easy. all : try apply (WF_big_kron _ _ _ (@Zero n m)); try easy. @@ -2256,8 +2256,8 @@ Proof. rewrite make_WF_equiv. intros i j Hi Hj. unfold list2D_to_matrix. - rewrite (map_nth_small Zero) by now rewrite map_length, seq_length. - rewrite (map_nth_small 0) by now rewrite seq_length. + rewrite (map_nth_small Zero) by now rewrite length_map, length_seq. + rewrite (map_nth_small 0) by now rewrite length_seq. rewrite nth_vec_to_list by easy. now rewrite seq_nth by easy. Qed. diff --git a/Modulus.v b/Modulus.v index b8f63f5..e3888ee 100644 --- a/Modulus.v +++ b/Modulus.v @@ -485,19 +485,19 @@ Proof. lia. Qed. Lemma div0_div_le_mono : forall a b c : nat, a <= b -> a / c <= b / c. Proof. intros a b []; [easy|]. - apply Nat.div_le_mono; easy. + apply Nat.Div0.div_le_mono; easy. Qed. Lemma div0_div_lt_upper_bound : forall a b c : nat, a < b * c -> a / b < c. Proof. - intros a b c H; apply Nat.div_lt_upper_bound; lia. + intros a b c H; apply Nat.Div0.div_lt_upper_bound; lia. Qed. Lemma div0_div_div : forall a b c, a / b / c = a / (b * c). Proof. intros a [] []; [rewrite ?Nat.mul_0_r; easy..|]. - now apply Nat.div_div. + now apply Nat.Div0.div_div. Qed. Lemma nat_mod_0_r : forall a, a mod 0 = a. @@ -506,13 +506,13 @@ Proof. easy. Qed. Lemma div0_mod_0_l : forall a, 0 mod a = 0. Proof. intros []; [easy|]; - now apply Nat.mod_0_l. + now apply Nat.Div0.mod_0_l. Qed. Lemma div0_mod_add : forall a b c, (a + b * c) mod c = a mod c. Proof. intros a b []; [f_equal; lia|]; - now apply Nat.mod_add. + now apply Nat.Div0.mod_add. Qed. Lemma div0_mod_mul_r : forall a b c, @@ -520,37 +520,37 @@ Lemma div0_mod_mul_r : forall a b c, Proof. intros a [] []; rewrite ?Nat.mul_0_r, ?Nat.mul_0_l, ?nat_mod_0_r; [lia..| pose proof (Nat.div_mod_eq a (S n)); lia |]. - now apply Nat.mod_mul_r. + now apply Nat.Div0.mod_mul_r. Qed. Lemma div0_mod_mod : forall a n, (a mod n) mod n = a mod n. Proof. - intros a []; [easy|]; now apply Nat.mod_mod. + intros a []; [easy|]; now apply Nat.Div0.mod_mod. Qed. Lemma div0_mod_mul : forall a b, (a * b) mod b = 0. Proof. intros a []; [cbn;lia|]; - now apply Nat.mod_mul. + now apply Nat.Div0.mod_mul. Qed. Lemma div0_add_mod_idemp_l : forall a b n : nat, (a mod n + b) mod n = (a + b) mod n. Proof. - intros a b []; [easy|]; now apply Nat.add_mod_idemp_l. + intros a b []; [easy|]; now apply Nat.Div0.add_mod_idemp_l. Qed. Lemma div0_add_mod : forall a b n, (a + b) mod n = (a mod n + b mod n) mod n. Proof. intros a b []; [easy|]; - now apply Nat.add_mod. + now apply Nat.Div0.add_mod. Qed. Lemma div0_mod_same : forall n, n mod n = 0. Proof. - intros []; [easy|]; now apply Nat.mod_same. + intros []; [easy|]; now apply Nat.Div0.mod_same. Qed. Lemma div0_div_0_l : forall n, 0 / n = 0. @@ -854,7 +854,7 @@ Lemma div_mul_not_exact a b : b <> 0 -> (a / b) * b = a - (a mod b). Proof. intros Hb. - rewrite (Nat.div_mod a b Hb) at 1 2. + rewrite (Nat.Div0.div_mod a b) at 1 2. rewrite Nat.add_sub. rewrite (Nat.mul_comm b (a/b)), Nat.add_comm, Nat.div_add by easy. rewrite Nat.div_small by (apply Nat.mod_upper_bound; easy). @@ -963,8 +963,8 @@ Proof. rewrite div_mul_not_exact by easy. rewrite 2!Nat.mul_sub_distr_r. rewrite div_mul_not_exact by easy. - pose proof (Nat.mod_le (b * c - a) c Hc). - pose proof (Nat.mod_le a c Hc). + pose proof (Nat.Div0.mod_le (b * c - a) c). + pose proof (Nat.Div0.mod_le a c). enough (a + (b * c - a) mod c = (a + c * Nat.b2n (¬ a mod c =? 0) - a mod c)) by lia. @@ -1177,7 +1177,7 @@ Proof. intros m n. destruct n. - cbn; lia. - - pose proof (Nat.div_mod m (S n)). + - pose proof (Nat.Div0.div_mod m (S n)). lia. Qed. @@ -1307,8 +1307,8 @@ Proof. easy. - intros Heq s Hs. rewrite 2!Nat.testbit_eqb. - rewrite (Nat.div_mod i (2^(S s)) ltac:(apply Nat.pow_nonzero; lia)). - rewrite (Nat.div_mod j (2^(S s)) ltac:(apply Nat.pow_nonzero; lia)). + rewrite (Nat.Div0.div_mod i (2^(S s))). + rewrite (Nat.Div0.div_mod j (2^(S s))). rewrite (mod_pow2_eq_closed_down i j (S s) n ltac:(lia) Heq). rewrite 2!(Nat.mul_comm (2^ S s)), 2!(Nat.add_comm (_*_)). rewrite Nat.pow_succ_r by lia. @@ -1331,7 +1331,7 @@ Proof. split; [|intros ->; easy]. intros H; apply bits_inj_upto in H. assert (H2n : 2^n <> 0) by (apply Nat.pow_nonzero; lia). - rewrite (Nat.div_mod i (2^n) H2n), (Nat.div_mod j (2^n) H2n). + rewrite (Nat.Div0.div_mod i (2^n)), (Nat.Div0.div_mod j (2^n)). rewrite 2!Nat.div_small, Nat.mul_0_r by lia. easy. Qed. diff --git a/Pad.v b/Pad.v index bb02e65..d5511a5 100644 --- a/Pad.v +++ b/Pad.v @@ -1,8 +1,8 @@ Require Export Complex. Require Export Quantum. -Require Export Init.Datatypes. -Require Export Coq.Sorting.Permutation. -Require Export Coq.Lists.List. +From Stdlib Require Export Init.Datatypes. +From Stdlib Require Export Sorting.Permutation. +From Stdlib Require Export Lists.List. (** This file provides padding functions to extend a matrix to a larger space. This is useful for describing the effect of 1- and 2-qubit gates on a larger quantum space. *) diff --git a/PermutationInstances.v b/PermutationInstances.v index 811a97e..d532a06 100644 --- a/PermutationInstances.v +++ b/PermutationInstances.v @@ -2054,8 +2054,8 @@ Proof. rewrite <- Nat.add_assoc. replace (n - m mod n + m) with (n - m mod n + (n * (m / n) + m mod n)) by - (rewrite <- (Nat.div_mod m n Hn0); easy). - pose proof (Nat.mod_upper_bound m n Hn0). + (rewrite <- (Nat.Div0.div_mod m n); easy). + pose proof (Nat.mod_upper_bound m n). replace (n - m mod n + (n * (m / n) + m mod n)) with (n * (1 + m / n)) by lia. rewrite Nat.mul_comm, Nat.Div0.mod_add. diff --git a/Polynomial.v b/Polynomial.v index bfbf089..46cb74e 100644 --- a/Polynomial.v +++ b/Polynomial.v @@ -1,8 +1,8 @@ -Require Import Psatz. -Require Import String. +From Stdlib Require Import Psatz. +From Stdlib Require Import String. Require Export Complex. -Require Import List. -Require Import Setoid. +From Stdlib Require Import List. +From Stdlib Require Import Setoid. Declare Scope poly_scope. Delimit Scope poly_scope with P. @@ -58,7 +58,7 @@ Proof. intros X p n H H0. rewrite (destruct_from_last n' x); auto. apply H0. apply IHn'. - rewrite firstn_length, H1. + rewrite length_firstn, H1. rewrite min_l; lia. Qed. @@ -165,7 +165,7 @@ Proof. induction p1 as [| a1]. apply f_equal_gen; try lca. apply f_equal_gen; try easy. unfold Peval. - rewrite map_length, (@big_sum_mult_l C _ _ _ C_is_ring). + rewrite length_map, (@big_sum_mult_l C _ _ _ C_is_ring). apply big_sum_eq_bounded; intros. replace C0 with (Cmult a1 C0) by lca. rewrite map_nth, Cmult_0_r. @@ -186,11 +186,11 @@ Lemma app_eval : forall (f g : Polynomial), Proof. intros. apply functional_extensionality; intros. unfold Peval. - rewrite app_length, big_sum_sum. + rewrite length_app, big_sum_sum. apply Cplus_simplify. apply big_sum_eq_bounded; intros. rewrite app_nth1; easy. - rewrite app_length, big_sum_sum. + rewrite length_app, big_sum_sum. rewrite repeat_length. assert (big_sum (fun i : nat => nth i (repeat C0 (Datatypes.length f) ++ g) C0 * x ^ i) (length f) = C0). @@ -222,7 +222,7 @@ Lemma mul_by_x_to_n : forall (f : Polynomial) (n : nat) (c : C), ((repeat C0 n) ++ f)[[c]] = f[[c]] * c^n. Proof. intros. unfold Peval. - rewrite app_length, big_sum_sum, <- Cplus_0_l. + rewrite length_app, big_sum_sum, <- Cplus_0_l. apply Cplus_simplify. apply (@big_sum_0_bounded C C_is_monoid); intros. rewrite app_nth1, nth_repeat; auto; lca. @@ -548,12 +548,13 @@ Proof. intros. left; apply (Rmin_pos δ1 δ2); auto. } destruct H5 as [b [H5 H6] ]. assert (H7 : Cmod (f b - L1) + Cmod (f b - L2) < Cmod (L1 - L2)). - rewrite (double_var (Cmod (L1 - L2))). - apply Rplus_lt_compat. - apply H2; auto. - assert (H' := (Rmin_l δ1 δ2)). lra. - apply H4; auto. - assert (H' := (Rmin_r δ1 δ2)). lra. + { rewrite <- (Rplus_half_diag (Cmod (L1 - L2))). + apply Rplus_lt_compat. + apply H2; auto. + assert (H' := (Rmin_l δ1 δ2)). lra. + apply H4; auto. + assert (H' := (Rmin_r δ1 δ2)). lra. + } assert (H8 : Cmod (L1 - (f b) + (f b - L2)) <= Cmod (L1 - f b) + Cmod (f b - L2)). { apply Cmod_triangle. } replace (L1 - f b + (f b - L2)) with (L1 - L2) in H8 by lca. @@ -758,7 +759,7 @@ Lemma power_x_eval : forall (n : nat) (a x : C), (repeat C0 n ++ [a]) [[x]] = a * x^n. Proof. intros. unfold Peval. - rewrite app_length; simpl. + rewrite length_app; simpl. rewrite Nat.add_1_r, <- big_sum_extend_r, <- (Nat.add_0_r (length (repeat C0 n))), app_nth2_plus, Nat.add_0_r, repeat_length; simpl. rewrite <- Cplus_0_l. @@ -991,7 +992,7 @@ Lemma last_C0_Peq_front : forall (p : Polynomial), Proof. intros. unfold Peq, Peval. apply functional_extensionality; intros. - rewrite app_length; simpl. + rewrite length_app; simpl. rewrite Nat.add_1_r, <- big_sum_extend_r. rewrite app_nth2, Nat.sub_diag; auto; simpl. rewrite Cmult_0_l, Cplus_0_r. @@ -1072,7 +1073,7 @@ Lemma compactify_length : forall (p : Polynomial), length (compactify p) <= length p. Proof. intros. unfold compactify. - rewrite rev_length, <- (rev_length p). + rewrite length_rev, <- (length_rev p). apply prune_length. Qed. @@ -1272,7 +1273,7 @@ Proof. induction p1 as [| h]. do 2 rewrite Pplus_0_r. rewrite map_app. split; try easy. - rewrite map_length; easy. + rewrite length_map; easy. - intros. simpl. destruct (IHp1 p2) as [p [H1 H2] ]. @@ -1280,8 +1281,8 @@ Proof. induction p1 as [| h]. split. rewrite H1, app_comm_cons. apply Pplus_lt_app. - rewrite map_length, app_length; simpl; lia. - rewrite Pplus_length1, map_length, app_length; simpl. + rewrite length_map, length_app; simpl; lia. + rewrite Pplus_length1, length_map, length_app; simpl. lia. Qed. @@ -1291,7 +1292,7 @@ Lemma Pmult_length_le : forall (p1 p2 : Polynomial), Proof. induction p1 as [| a1]. - intros; destruct p2; try easy; simpl; lia. - intros. destruct p2; try easy; simpl. - rewrite Pplus_length1, map_length. + rewrite Pplus_length1, length_map. destruct p2; try lia. Qed. @@ -1301,10 +1302,10 @@ Lemma Pmult_length_helper : forall (n : nat) (a1 a2 : C) (p1 p2 : Polynomial), Proof. induction n as [| n']. - intros. destruct p1; try easy; simpl. - rewrite Pplus_0_r, map_length. + rewrite Pplus_0_r, length_map. easy. - intros; simpl. - rewrite Pplus_length1, map_length; simpl. + rewrite Pplus_length1, length_map; simpl. destruct p1. + simpl; lia. + rewrite max_r, IHn'. @@ -1444,9 +1445,9 @@ Proof. intros. rewrite <- H; auto. apply f_equal_gen; auto. rewrite last_C0_Peq_front; easy. - + rewrite app_nonzero_compactify_reduce, app_length in *; auto. + + rewrite app_nonzero_compactify_reduce, length_app in *; auto. rewrite (p_Peq_compactify_p p1), Pplus_lt_app. - rewrite app_nonzero_compactify_reduce, app_length; auto. + rewrite app_nonzero_compactify_reduce, length_app; auto. do 2 (apply f_equal_gen; auto). rewrite Pplus_length2; auto. all : simpl in *; lia. @@ -1646,7 +1647,7 @@ Proof. intros. rewrite H0; simpl. rewrite <- poly_shift_const; easy. unfold poly_shift. - rewrite H0, app_length, Nat.add_1_r; simpl. + rewrite H0, length_app, Nat.add_1_r; simpl. assert (H1 : degree (p' ++ [a]) = degree (map (Cmult (nth (Datatypes.length p') (p' ++ [a]) C0)) @@ -1656,7 +1657,7 @@ Proof. intros. ([a] *, (Ppow [- m; C1] (Datatypes.length p'))) by easy. rewrite Pmult_degree, Ppow_degree. unfold degree. - rewrite <- H0, compactify_idempotent, H0, app_length; simpl. + rewrite <- H0, compactify_idempotent, H0, length_app; simpl. unfold compactify, prune; simpl. destruct (Ceq_dec a C0); try easy. assert (H' := C1_neq_C0). @@ -1672,7 +1673,7 @@ Proof. intros. rewrite Pplus_degree2; try easy. rewrite <- H1. replace (degree (p' ++ [a])) with (length p') by - (unfold degree; rewrite <- H0, compactify_idempotent, H0, app_length; simpl; lia). + (unfold degree; rewrite <- H0, compactify_idempotent, H0, length_app; simpl; lia). rewrite E1. apply Nat.lt_succ_r; apply Psum_degree; intros. replace (map (Cmult (nth i (p' ++ [a]) C0)) (Ppow [- m; C1] i) +, [C0]) with diff --git a/Prelim.v b/Prelim.v index d885a93..733e84c 100644 --- a/Prelim.v +++ b/Prelim.v @@ -2,12 +2,12 @@ (** This file contains basic utility, definitions, and proofs. *) -Require Export Bool. -Require Export Arith. -Require Export Reals. -Require Export Psatz. -Require Export Program. -Require Export List. +From Stdlib Require Export Bool. +From Stdlib Require Export Arith. +From Stdlib Require Export Reals. +From Stdlib Require Export Psatz. +From Stdlib Require Export Program. +From Stdlib Require Export List. Export ListNotations. @@ -121,7 +121,7 @@ Lemma map_nth_small [A B] (dnew : A) (f : A -> B) (l : list A) (d : B) i : nth i (map f l) d = f (nth i l dnew). Proof. intros Hi. - rewrite (nth_indep _ d (f dnew)) by (now rewrite map_length). + rewrite (nth_indep _ d (f dnew)) by (now rewrite length_map). apply map_nth. Qed. diff --git a/Quantum.v b/Quantum.v index 2cf8906..a4916a7 100644 --- a/Quantum.v +++ b/Quantum.v @@ -1,8 +1,8 @@ (** In this file, we define specific objects/concepts specific to quantum computing and we prove lemmas about thems. *) -Require Import Psatz. -Require Import Reals. +From Stdlib Require Import Psatz. +From Stdlib Require Import Reals. Require Export VecSet. Require Export CauchySchwarz. Require Import Kronecker. @@ -312,7 +312,7 @@ Lemma WF_bools_to_matrix : forall l, Proof. induction l; auto with wf_db. unfold bools_to_matrix in *; simpl. - apply WF_kron; try rewrite map_length; try lia. + apply WF_kron; try rewrite length_map; try lia. apply WF_bool_to_matrix. apply IHl. Qed. diff --git a/RealAux.v b/RealAux.v index c699476..21301d5 100644 --- a/RealAux.v +++ b/RealAux.v @@ -1,8 +1,8 @@ (** Supplement to Coq's axiomatized Reals *) -Require Export Reals. -Require Import Psatz. -Require Export Program. +From Stdlib Require Export Reals. +From Stdlib Require Import Psatz. +From Stdlib Require Export Program. Require Export Summation. (** * Basic lemmas *) @@ -398,12 +398,12 @@ Proof. intros. destruct (Z_plusminus_nat a) as [x [H0 | H0]]; subst. induction x; auto. replace (S x) with (1 + x)%nat by lia. - rewrite Nat2Z.inj_add, Z.pow_add_r, two_val_mult; try lia. + rewrite Znat.Nat2Z.inj_add, Z.pow_add_r, two_val_mult; try lia. rewrite IHx; auto; try lia. try (apply (Z.pow_nonzero 2 x); lia). induction x; auto. replace (S x) with (1 + x)%nat by lia. - rewrite Nat2Z.inj_add, Z.opp_add_distr, Z.pow_add_r, two_val_mult; try lia. + rewrite Znat.Nat2Z.inj_add, Z.opp_add_distr, Z.pow_add_r, two_val_mult; try lia. Qed. Lemma twoadic_nonzero : forall (a b : Z), @@ -441,7 +441,7 @@ Proof. intros. - replace (2 ^ S x * (2 * b + 1)) with (2 * (2 ^ x * (2 * b + 1))). rewrite odd_part_reduce, IHx; try lia. replace (S x) with (1 + x)%nat by lia. - rewrite Nat2Z.inj_add, Z.pow_add_r; try lia. + rewrite Znat.Nat2Z.inj_add, Z.pow_add_r; try lia. - destruct x; try easy. replace (2 ^ (- 0%nat) * (2 * b + 1)) with (2 * b + 1) by lia. destruct b; simpl; auto. diff --git a/Rings.v b/Rings.v index 4296697..848df53 100644 --- a/Rings.v +++ b/Rings.v @@ -1,5 +1,5 @@ -Require Import List. +From Stdlib Require Import List. Require Export Complex. (* @@ -320,7 +320,7 @@ Proof. intros. induction n; try easy. rewrite <- Cpow_int_cons in *. replace (S n) with (1 + n)%nat by lia. - rewrite Nat2Z.inj_add, Z.pow_add_r, Cpow_add_r; try lia. + rewrite Znat.Nat2Z.inj_add, Z.pow_add_r, Cpow_add_r; try lia. rewrite mult_IZR, <- IHn, RtoC_mult, RtoC_pow, pow_IZR. apply f_equal_gen; auto. Qed. @@ -524,7 +524,7 @@ Proof. rewrite H in H'; easy. - assert (H' := DtoC_neq_0 z z0). rewrite H in H'; easy. - - destruct (Ztrichotomy_inf z z1) as [[H0 | H0] | H0]. + - destruct (Zorder.Ztrichotomy_inf z z1) as [[H0 | H0] | H0]. + apply DtoC_inj_uneq_case in H; lia. + subst. apply move_power_2 in H. @@ -579,7 +579,7 @@ Definition Dplus (x y : Dyadic) : Dyadic := | (D0, _) => y | (_, D0) => x | (Dn n x', Dn m y') => - match Ztrichotomy_inf n m with + match Zorder.Ztrichotomy_inf n m with | inleft (left _) => (* x has lower power of 2 *) Dn n (2^(m-n-1) * (2*y'+1) + x') | inleft (right _) => (* equal power of 2 *) @@ -633,7 +633,7 @@ Infix "^," := Dpow (at level 30) : D_scope. Lemma DtoC_plus : forall d1 d2, DtoC (d1 +, d2) = (DtoC d1 + DtoC d2)%C. Proof. intros. destruct d1; destruct d2; simpl; try lca. - unfold Dplus; destruct (Ztrichotomy_inf z z1); try destruct s. + unfold Dplus; destruct (Zorder.Ztrichotomy_inf z z1); try destruct s. - unfold Dplus, DtoC. fastZtoC. rewrite (Cmult_plus_distr_l _ _ z0), (Cmult_assoc C2). @@ -1087,7 +1087,7 @@ Lemma DisZ_plus : forall (d1 d2 : Dyadic), Proof. intros. destruct d1; destruct d2; try easy. unfold Dplus, DisZ in *. - destruct (Ztrichotomy_inf z z1); try lia. + destruct (Zorder.Ztrichotomy_inf z z1); try lia. destruct s; try lia. destruct (odd_part (2 * z0 + 1 + (2 * z2 + 1))); auto; apply Z.le_ge; apply Z.add_nonneg_nonneg; try lia. @@ -1133,7 +1133,7 @@ Lemma DisZ_dec : forall (d : Dyadic), Proof. intros. destruct d; try (left; easy). simpl. - apply Z_ge_dec. + apply ZArith_dec.Z_ge_dec. Qed. diff --git a/RowColOps.v b/RowColOps.v index bc87f9c..604f8c3 100644 --- a/RowColOps.v +++ b/RowColOps.v @@ -1,5 +1,5 @@ -Require Import Psatz. -Require Import Reals. +From Stdlib Require Import Psatz. +From Stdlib Require Import Reals. Require Export Matrix. @@ -438,14 +438,6 @@ Proof. unfold WF_Matrix in *. bdestruct (x WF_Matrix T2 -> WF_Matrix (smash T1 T2). Proof. unfold WF_Matrix, smash in *. @@ -528,7 +520,7 @@ Qed. #[export] Hint Resolve WF_get_col WF_get_row WF_reduce_row WF_reduce_col WF_reduce_vecn WF_get_minor : wf_db. -#[export] Hint Resolve WF_row_append WF_col_append WF_row_wedge WF_col_wedge WF_smash : wf_db. +#[export] Hint Resolve WF_row_wedge WF_col_wedge WF_smash : wf_db. #[export] Hint Resolve WF_col_swap WF_row_swap WF_col_scale WF_row_scale WF_col_add WF_row_add : wf_db. #[export] Hint Resolve WF_gen_new_col WF_gen_new_row WF_col_add_many WF_row_add_many : wf_db. #[export] Hint Resolve WF_col_scale_many WF_row_scale_many WF_col_add_each WF_row_add_each : wf_db. diff --git a/Summation.v b/Summation.v index 499774f..f506dea 100644 --- a/Summation.v +++ b/Summation.v @@ -1,5 +1,5 @@ -Require Import List. -Require Export Prelim. +From Stdlib Require Import List. +Require Export Prelim. Declare Scope group_scope. Delimit Scope group_scope with G. @@ -651,8 +651,8 @@ Proof. rewrite Nat.div_add_l by assumption. rewrite Nat.div_small; trivial. rewrite Nat.add_0_r. - rewrite Nat.add_mod by assumption. - rewrite Nat.mod_mul by assumption. + rewrite Nat.Div0.add_mod by assumption. + rewrite Nat.Div0.mod_mul by assumption. rewrite Nat.add_0_l. repeat rewrite Nat.mod_small; trivial. } rewrite <- big_sum_sum. @@ -676,7 +676,7 @@ Proof. induction m as [| m']. rewrite Nat.mul_comm. rewrite Nat.div_add_l; try lia. rewrite (Nat.add_comm (m' * n)). - rewrite Nat.mod_add; try lia. + rewrite Nat.Div0.mod_add; try lia. destruct (Nat.mod_small_iff x n) as [_ HD]; try lia. destruct (Nat.div_small_iff x n) as [_ HA]; try lia. rewrite HD, HA; try lia. diff --git a/VecSet.v b/VecSet.v index 5c5f2f5..df68090 100644 --- a/VecSet.v +++ b/VecSet.v @@ -3,8 +3,8 @@ (** In this file, we define more advanced linear algebra concepts such as bases, linear independence, etc... *) -Require Import Psatz. -Require Import Reals. +From Stdlib Require Import Psatz. +From Stdlib Require Import Reals. Require Export RowColOps. diff --git a/VectorStates.v b/VectorStates.v index 6f4f871..9319094 100644 --- a/VectorStates.v +++ b/VectorStates.v @@ -431,8 +431,7 @@ Proof. - destruct H1. replace (y * r)%nat with (r * y)%nat by lia. rewrite <- H1, <- H2. - apply Nat.div_mod. - lia. + apply Nat.Div0.div_mod. Qed. Lemma split_basis_vector : forall m n x y, diff --git a/coq-quantumlib.opam b/coq-quantumlib.opam index 42134c1..276b05d 100644 --- a/coq-quantumlib.opam +++ b/coq-quantumlib.opam @@ -13,8 +13,8 @@ homepage: "https://github.com/inQWIRE/QuantumLib" doc: "https://inqwire.github.io/QuantumLib/toc.html" bug-reports: "https://github.com/inQWIRE/QuantumLib/issues" depends: [ - "dune" {>= "2.8"} - "coq" {>= "8.16" & < "8.21"} + "dune" {>= "3.11"} + "rocq-prover" {>= "9.0.0" & < "9.2"} "odoc" {with-doc} ] build: [ diff --git a/dune-project b/dune-project index 5d973dd..86cfcca 100644 --- a/dune-project +++ b/dune-project @@ -1,7 +1,8 @@ -(lang dune 2.8) +(lang dune 3.11) (name coq-quantumlib) (version 1.8.0) -(using coq 0.2) +(using coq 0.3) +(warnings (deprecated_coq_lang_lt_08 disabled)) (generate_opam_files true) @@ -18,4 +19,4 @@ "\| about quantum computation and quantum programs. ) (depends - (coq (and (>= 8.16) (< 8.21))))) + (rocq-prover (and (>= 9.0.0) (< 9.2)))))