From b38e663c1416a989dfde0d880f2bdc2d3f2a137b Mon Sep 17 00:00:00 2001 From: BHAKTISHAH Date: Fri, 31 Mar 2023 23:13:37 -0500 Subject: [PATCH 1/7] made changes to make quantumlib compile on 8.17 --- .gitignore | 3 ++- Complex.v | 22 +++++++++++----------- Eigenvectors.v | 6 +++--- Matrix.v | 22 +++++++++++----------- Polar.v | 7 +++---- Polynomial.v | 2 +- Quantum.v | 20 ++++++++++---------- RealAux.v | 10 +++++----- Rings.v | 6 +++--- Summation.v | 4 +--- VectorStates.v | 26 +++++++++++++------------- 11 files changed, 63 insertions(+), 65 deletions(-) diff --git a/.gitignore b/.gitignore index d70e3d6..6ddf536 100644 --- a/.gitignore +++ b/.gitignore @@ -52,4 +52,5 @@ Makefile.coq* _build -docs \ No newline at end of file +docs +/.vscode diff --git a/Complex.v b/Complex.v index e430eb3..3b09ebc 100644 --- a/Complex.v +++ b/Complex.v @@ -1397,7 +1397,7 @@ Proof. lca. Qed. -Hint Rewrite Cexp_0 Cexp_PI Cexp_PI2 Cexp_2PI Cexp_3PI2 Cexp_PI4 Cexp_PIm4 +#[global] Hint Rewrite Cexp_0 Cexp_PI Cexp_PI2 Cexp_2PI Cexp_3PI2 Cexp_PI4 Cexp_PIm4 Cexp_1PI4 Cexp_2PI4 Cexp_3PI4 Cexp_4PI4 Cexp_5PI4 Cexp_6PI4 Cexp_7PI4 Cexp_8PI4 Cexp_add Cexp_neg Cexp_plus_PI Cexp_minus_PI : Cexp_db. @@ -1442,28 +1442,28 @@ Ltac nonzero := | |- Rle _ _ => lra end. -Hint Rewrite Cminus_unfold Cdiv_unfold Ci2 Cconj_R Cconj_opp Cconj_rad2 +#[global] Hint Rewrite Cminus_unfold Cdiv_unfold Ci2 Cconj_R Cconj_opp Cconj_rad2 Cinv_sqrt2_sqrt Cplus_div2 Cplus_0_l Cplus_0_r Cplus_opp_r Cplus_opp_l Copp_0 Copp_involutive Cmult_0_l Cmult_0_r Cmult_1_l Cmult_1_r : C_db. -Hint Rewrite <- Copp_mult_distr_l Copp_mult_distr_r Cdouble : C_db. -Hint Rewrite Csqrt_sqrt using Psatz.lra : C_db. -Hint Rewrite Cinv_l Cinv_r using nonzero : C_db. +#[global] Hint Rewrite <- Copp_mult_distr_l Copp_mult_distr_r Cdouble : C_db. +#[global] Hint Rewrite Csqrt_sqrt using Psatz.lra : C_db. +#[global] Hint Rewrite Cinv_l Cinv_r using nonzero : C_db. (* Previously in the other direction *) -Hint Rewrite Cinv_mult_distr using nonzero : C_db. +#[global] Hint Rewrite Cinv_mult_distr using nonzero : C_db. (* Light rewriting db *) -Hint Rewrite Cplus_0_l Cplus_0_r Cmult_0_l Cmult_0_r Copp_0 +#[global] Hint Rewrite Cplus_0_l Cplus_0_r Cmult_0_l Cmult_0_r Copp_0 Cconj_R Cmult_1_l Cmult_1_r : C_db_light. (* Distributing db *) -Hint Rewrite Cmult_plus_distr_l Cmult_plus_distr_r Copp_plus_distr Copp_mult_distr_l +#[global] Hint Rewrite Cmult_plus_distr_l Cmult_plus_distr_r Copp_plus_distr Copp_mult_distr_l Copp_involutive : Cdist_db. -Hint Rewrite RtoC_opp RtoC_mult RtoC_minus RtoC_plus : RtoC_db. -Hint Rewrite RtoC_inv using nonzero : RtoC_db. -Hint Rewrite RtoC_pow : RtoC_db. +#[global] Hint Rewrite RtoC_opp RtoC_mult RtoC_minus RtoC_plus : RtoC_db. +#[global] Hint Rewrite RtoC_inv using nonzero : RtoC_db. +#[global] Hint Rewrite RtoC_pow : RtoC_db. Ltac Csimpl := repeat match goal with diff --git a/Eigenvectors.v b/Eigenvectors.v index d7f227b..33760ab 100644 --- a/Eigenvectors.v +++ b/Eigenvectors.v @@ -25,7 +25,7 @@ Lemma Y_eq_iXZ : σy = Ci .* σx × σz. Proof. lma'. Qed. Lemma H_eq_Hadjoint : hadamard† = hadamard. Proof. lma'. Qed. -Hint Rewrite Y_eq_iXZ H_eq_Hadjoint : Q_db. +#[global] Hint Rewrite Y_eq_iXZ H_eq_Hadjoint : Q_db. Lemma ItimesIid : I 2 × I 2 = I 2. Proof. lma'. Qed. Lemma XtimesXid : σx × σx = I 2. Proof. lma'. Qed. @@ -33,7 +33,7 @@ Lemma YtimesYid : σy × σy = I 2. Proof. lma'. Qed. Lemma ZtimesZid : σz × σz = I 2. Proof. lma'. Qed. Lemma HtimesHid : hadamard × hadamard = I 2. Proof. lma'; Hhelper. Qed. -Hint Rewrite ItimesIid XtimesXid YtimesYid ZtimesZid HtimesHid : Q_db. +#[global] Hint Rewrite ItimesIid XtimesXid YtimesYid ZtimesZid HtimesHid : Q_db. Lemma ZH_eq_HX : σz × hadamard = hadamard × σx. Proof. lma'. Qed. Lemma XH_eq_HZ : σx × hadamard = hadamard × σz. Proof. lma'. Qed. @@ -46,7 +46,7 @@ Lemma cnotX2 : cnot × (I 2 ⊗ σx) = (I 2 ⊗ σx) × cnot. Proof. lma'. Qed. Lemma cnotZ1 : cnot × (σz ⊗ I 2) = (σz ⊗ I 2) × cnot. Proof. lma'. Qed. Lemma cnotZ2 : cnot × (I 2 ⊗ σz) = (σz ⊗ σz) × cnot. Proof. lma'. Qed. -Hint Rewrite ZH_eq_HX XH_eq_HZ SX_eq_YS SZ_eq_ZS cnotX1 cnotX2 cnotZ1 cnotZ2 : Q_db. +#[global] Hint Rewrite ZH_eq_HX XH_eq_HZ SX_eq_YS SZ_eq_ZS cnotX1 cnotX2 cnotZ1 cnotZ2 : Q_db. (*******************************) diff --git a/Matrix.v b/Matrix.v index c9a657d..f1aa2e9 100644 --- a/Matrix.v +++ b/Matrix.v @@ -240,25 +240,25 @@ Fixpoint direct_sum_n n {m1 m2} (A : Matrix m1 m2) : Matrix (n*m1) (n*m2) := (** * Showing that M is a vector space *) -Program Instance M_is_monoid : forall n m, Monoid (Matrix n m) := +#[global] Program Instance M_is_monoid : forall n m, Monoid (Matrix n m) := { Gzero := @Zero n m ; Gplus := Mplus }. Solve All Obligations with program_simpl; prep_matrix_equality; lca. -Program Instance M_is_group : forall n m, Group (Matrix n m) := +#[global] Program Instance M_is_group : forall n m, Group (Matrix n m) := { Gopp := Mopp }. Solve All Obligations with program_simpl; prep_matrix_equality; lca. -Program Instance M_is_comm_group : forall n m, Comm_Group (Matrix n m). +#[global] Program Instance M_is_comm_group : forall n m, Comm_Group (Matrix n m). Solve All Obligations with program_simpl; prep_matrix_equality; lca. -Program Instance M_is_module_space : forall n m, Module_Space (Matrix n m) C := +#[global] Program Instance M_is_module_space : forall n m, Module_Space (Matrix n m) C := { Vscale := scale }. Solve All Obligations with program_simpl; prep_matrix_equality; lca. -Program Instance M_is_vector_space : forall n m, Vector_Space (Matrix n m) C. +#[global] Program Instance M_is_vector_space : forall n m, Vector_Space (Matrix n m) C. (** Notations *) @@ -4008,23 +4008,23 @@ Qed. (* Old: -Hint Rewrite kron_1_l kron_1_r Mmult_1_l Mmult_1_r id_kron id_adjoint_eq +#[global] Hint Rewrite kron_1_l kron_1_r Mmult_1_l Mmult_1_r id_kron id_adjoint_eq @Mmult_adjoint Mplus_adjoint @kron_adjoint @kron_mixed_product id_adjoint_eq adjoint_involutive using (auto 100 with wf_db; autorewrite with M_db; auto 100 with wf_db; lia) : M_db. *) (* eauto will cause major choking... *) -Hint Rewrite @kron_1_l @kron_1_r @Mmult_1_l @Mmult_1_r @Mscale_1_l +#[global] Hint Rewrite @kron_1_l @kron_1_r @Mmult_1_l @Mmult_1_r @Mscale_1_l @id_adjoint_eq @id_transpose_eq using (auto 100 with wf_db) : M_db_light. -Hint Rewrite @kron_0_l @kron_0_r @Mmult_0_l @Mmult_0_r @Mplus_0_l @Mplus_0_r +#[global] Hint Rewrite @kron_0_l @kron_0_r @Mmult_0_l @Mmult_0_r @Mplus_0_l @Mplus_0_r @Mscale_0_l @Mscale_0_r @zero_adjoint_eq @zero_transpose_eq using (auto 100 with wf_db) : M_db_light. (* I don't like always doing restore_dims first, but otherwise sometimes leaves unsolvable WF_Matrix goals. *) Ltac Msimpl_light := try restore_dims; autorewrite with M_db_light. -Hint Rewrite @Mmult_adjoint @Mplus_adjoint @kron_adjoint @kron_mixed_product +#[global] Hint Rewrite @Mmult_adjoint @Mplus_adjoint @kron_adjoint @kron_mixed_product @adjoint_involutive using (auto 100 with wf_db) : M_db. Ltac Msimpl := try restore_dims; autorewrite with M_db_light M_db. @@ -4347,7 +4347,7 @@ Ltac fill_differences := | 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 +4375,7 @@ Ltac gridify := 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 *) diff --git a/Polar.v b/Polar.v index 14799b0..2abe185 100644 --- a/Polar.v +++ b/Polar.v @@ -56,7 +56,7 @@ Proof. intros. assert (H0 := Rmax_Cmod (x, y)). apply (Rle_trans (Rabs (fst (x, y)))) in H0; try apply Rmax_l; simpl in *. apply (Rmult_le_compat_r (/ Cmod (x, y))) in H0. - rewrite Rinv_r, <- (Rabs_pos_eq (Cmod _)), <- Rabs_Rinv, <- Rabs_mult in H0. + rewrite Rinv_r, <- (Rabs_pos_eq (Cmod _)), <- Rabs_inv, <- Rabs_mult in H0. all : try (left; apply Rinv_0_lt_compat); try apply Cmod_ge_0; try apply Cmod_gt_0. all : try (unfold not; intros; apply H; apply Cmod_eq_0; easy). destruct H0. @@ -78,7 +78,7 @@ Proof. intros. apply (Rle_trans (Rabs (fst (x, y)))) in H0; try apply Rmax_l; simpl in *. destruct H0. - apply (Rmult_lt_compat_r (/ Cmod (x, y))) in H0. - rewrite Rinv_r, <- (Rabs_pos_eq (Cmod _)), <- Rabs_Rinv, <- Rabs_mult in H0. + rewrite Rinv_r, <- (Rabs_pos_eq (Cmod _)), <- Rabs_inv, <- Rabs_mult in H0. all : try (apply Rinv_0_lt_compat; apply Cmod_gt_0). all : try apply Cmod_ge_0. all : try (unfold not; intros; apply H'; apply Cmod_eq_0; easy). @@ -160,7 +160,7 @@ Lemma div_subtract_helper : forall (x y : R), Proof. intros. unfold Rdiv. rewrite Rsqr_mult. - rewrite Rsqr_inv. + rewrite Rsqr_inv'. rewrite <- (Rinv_r ((Cmod (x, y))²)). replace (((Cmod (x, y))² * / (Cmod (x, y))² + - (x² * / (Cmod (x, y))²))%R) with ( ((Cmod (x, y))² - x²) * / ((Cmod (x, y))²))%R by lra. @@ -173,7 +173,6 @@ Proof. intros. unfold Rsqr in H0. apply Rmult_integral in H0; apply Cmod_eq_0. destruct H0; easy. - apply Cmod_eq_0; easy. Qed. Lemma rect_to_polar_to_rect : forall (z : C), diff --git a/Polynomial.v b/Polynomial.v index ab8f08d..6111e5d 100644 --- a/Polynomial.v +++ b/Polynomial.v @@ -1705,7 +1705,7 @@ Proof. split; intros. unfold Rdiv in *. unfold pow in *. apply (Rmult_le_pos a) in H1; try lra. - rewrite Rmult_plus_distr_l, Rinv_mult_distr, Rmult_plus_distr_l in H1; try lra. + rewrite Rmult_plus_distr_l, Rinv_mult, Rmult_plus_distr_l in H1; try lra. replace (a * (b * (- b * (/ 2 * / a))))%R with (- b * b * (a * / a) * / 2)%R in H1 by lra. replace (a * (a * (- b * (/ 2 * / a) * (- b * (/ 2 * / a) * 1))))%R diff --git a/Quantum.v b/Quantum.v index 0ff4b25..661be1f 100644 --- a/Quantum.v +++ b/Quantum.v @@ -481,10 +481,10 @@ Proof. Msimpl; reflexivity. Qed. -Hint Rewrite Mmult00 Mmult01 Mmult10 Mmult11 Mmult0X MmultX0 Mmult1X MmultX1 : Q_db. -Hint Rewrite MmultXX MmultYY MmultZZ MmultHH Mplus01 Mplus10 EPRpair_creation : Q_db. -Hint Rewrite σx_on_right0 σx_on_right1 σx_on_left0 σx_on_left1 : Q_db. -Hint Rewrite cancel00 cancel01 cancel10 cancel11 using (auto with wf_db) : Q_db. +#[global] Hint Rewrite Mmult00 Mmult01 Mmult10 Mmult11 Mmult0X MmultX0 Mmult1X MmultX1 : Q_db. +#[global] Hint Rewrite MmultXX MmultYY MmultZZ MmultHH Mplus01 Mplus10 EPRpair_creation : Q_db. +#[global] Hint Rewrite σx_on_right0 σx_on_right1 σx_on_left0 σx_on_left1 : Q_db. +#[global] Hint Rewrite cancel00 cancel01 cancel10 cancel11 using (auto with wf_db) : Q_db. Lemma swap_swap : swap × swap = I (2*2). Proof. solve_matrix. Qed. @@ -499,7 +499,7 @@ Proof. reflexivity. Qed. -Hint Rewrite swap_swap swap_swap_r using (auto 100 with wf_db): Q_db. +#[global] Hint Rewrite swap_swap swap_swap_r using (auto 100 with wf_db): Q_db. (* TODO: move these swap lemmas to Permutation.v? *) @@ -1264,10 +1264,10 @@ Qed. Lemma braqubit0_sa : ∣0⟩⟨0∣† = ∣0⟩⟨0∣. Proof. lma. Qed. Lemma braqubit1_sa : ∣1⟩⟨1∣† = ∣1⟩⟨1∣. Proof. lma. Qed. -Hint Rewrite hadamard_sa σx_sa σy_sa σz_sa cnot_sa swap_sa braqubit1_sa braqubit0_sa control_adjoint phase_adjoint rotation_adjoint : Q_db. +#[global] Hint Rewrite hadamard_sa σx_sa σy_sa σz_sa cnot_sa swap_sa braqubit1_sa braqubit0_sa control_adjoint phase_adjoint rotation_adjoint : Q_db. (* Rather use control_adjoint : -Hint Rewrite control_sa using (autorewrite with M_db; reflexivity) : M_db. *) +#[global] Hint Rewrite control_sa using (autorewrite with M_db; reflexivity) : M_db. *) Lemma cnot_decomposition : ∣1⟩⟨1∣ ⊗ σx .+ ∣0⟩⟨0∣ ⊗ I 2 = cnot. Proof. solve_matrix. Qed. @@ -1345,7 +1345,7 @@ Proof. Qed. -Hint Rewrite phase_0 phase_2pi phase_pi phase_neg_pi : Q_db. +#[global] Hint Rewrite phase_0 phase_2pi phase_pi phase_neg_pi : Q_db. (* now we get some more identities: *) @@ -1365,7 +1365,7 @@ Proof. unfold Sgate, Tgate. apply f_equal; lra. Qed. -Hint Rewrite MmultSS MmultTT : Q_db. +#[global] Hint Rewrite MmultSS MmultTT : Q_db. (*****************************) @@ -1804,7 +1804,7 @@ Proof. lca. Qed. -Hint Rewrite swap_spec using (auto 100 with wf_db) : Q_db. +#[global] Hint Rewrite swap_spec using (auto 100 with wf_db) : Q_db. Example swap_to_0_test_24 : forall (q0 q1 q2 q3 : Vector 2), WF_Matrix q0 -> WF_Matrix q1 -> WF_Matrix q2 -> WF_Matrix q3 -> diff --git a/RealAux.v b/RealAux.v index 29c9ca1..817687e 100644 --- a/RealAux.v +++ b/RealAux.v @@ -24,10 +24,10 @@ Lemma Rminus_lt_0 : forall a b, a < b <-> 0 < b - a. Proof. intros. lra. Qed. Lemma Rminus_unfold : forall r1 r2, (r1 - r2 = r1 + -r2). Proof. reflexivity. Qed. Lemma Rdiv_unfold : forall r1 r2, (r1 / r2 = r1 */ r2). Proof. reflexivity. Qed. -Hint Rewrite Rminus_unfold Rdiv_unfold Ropp_0 Ropp_involutive Rplus_0_l +#[export] Hint Rewrite Rminus_unfold Rdiv_unfold Ropp_0 Ropp_involutive Rplus_0_l Rplus_0_r Rmult_0_l Rmult_0_r Rmult_1_l Rmult_1_r : R_db. -Hint Rewrite <- Ropp_mult_distr_l Ropp_mult_distr_r : R_db. -Hint Rewrite Rinv_l Rinv_r sqrt_sqrt using lra : R_db. +#[export] Hint Rewrite <- Ropp_mult_distr_l Ropp_mult_distr_r : R_db. +#[export] Hint Rewrite Rinv_l Rinv_r sqrt_sqrt using lra : R_db. Notation "√ n" := (sqrt n) (at level 20) : R_scope. @@ -38,7 +38,7 @@ Proof. intros. unfold Rdiv. rewrite Rmult_assoc. reflexivity. Qed. Lemma Rmult_div : forall r1 r2 r3 r4 : R, r2 <> 0 -> r4 <> 0 -> r1 / r2 * (r3 / r4) = r1 * r3 / (r2 * r4). -Proof. intros. unfold Rdiv. rewrite Rinv_mult_distr; trivial. lra. Qed. +Proof. intros. unfold Rdiv. rewrite Rinv_mult; trivial. lra. Qed. Lemma Rdiv_cancel : forall r r1 r2 : R, r1 = r2 -> r / r1 = r / r2. Proof. intros. rewrite H. reflexivity. Qed. @@ -562,7 +562,7 @@ Proof. apply sin_upper_bound_aux; lra. Qed. -Hint Rewrite sin_0 sin_PI4 sin_PI2 sin_PI cos_0 cos_PI4 cos_PI2 +#[export] Hint Rewrite sin_0 sin_PI4 sin_PI2 sin_PI cos_0 cos_PI4 cos_PI2 cos_PI sin_neg cos_neg : trig_db. (** * glb support *) diff --git a/Rings.v b/Rings.v index e404087..59fa4e1 100644 --- a/Rings.v +++ b/Rings.v @@ -328,7 +328,7 @@ Qed. -Hint Rewrite plus_IZR minus_IZR opp_IZR mult_IZR ZtoC_pow : ZtoR_db. +#[global] Hint Rewrite plus_IZR minus_IZR opp_IZR mult_IZR ZtoC_pow : ZtoR_db. (* NB: use plus_IZR, mult_IZR, RtoC_plus, RtoC_mult to move between types: *) (* quick helper tactic. TODO: centralize these *) @@ -719,7 +719,7 @@ Proof. intros. Qed. -Hint Rewrite DtoC_plus DtoC_opp DtoC_minus DtoC_mult DtoC_pow : DtoC_db. +#[global] Hint Rewrite DtoC_plus DtoC_opp DtoC_minus DtoC_mult DtoC_pow : DtoC_db. Ltac lDa_try1 := apply DtoC_inj; autorewrite with DtoC_db; lca. @@ -1753,7 +1753,7 @@ Proof. intros. Qed. -Hint Rewrite D8toC_plus D8toC_opp D8toC_mult : D8toC_db. +#[global] Hint Rewrite D8toC_plus D8toC_opp D8toC_mult : D8toC_db. (*TODO: show that the above proves defacto that D8 is a ring *) diff --git a/Summation.v b/Summation.v index 364048b..6159482 100644 --- a/Summation.v +++ b/Summation.v @@ -1,7 +1,5 @@ Require Import List. -Require Export Prelim. - - +Require Export Prelim. Declare Scope group_scope. Delimit Scope group_scope with G. diff --git a/VectorStates.v b/VectorStates.v index cab22ba..542cdcd 100644 --- a/VectorStates.v +++ b/VectorStates.v @@ -152,23 +152,23 @@ Proof. intros. destruct x,y; lma'. Qed. (* Automation *) (* General matrix rewrites *) -Hint Rewrite bra0_equiv bra1_equiv ket0_equiv ket1_equiv : ket_db. -Hint Rewrite bra0ket0 bra0ket1 bra1ket0 bra1ket1 : ket_db. -Hint Rewrite Mmult_plus_distr_l Mmult_plus_distr_r kron_plus_distr_l kron_plus_distr_r Mscale_plus_distr_r : ket_db. -Hint Rewrite Mscale_mult_dist_l Mscale_mult_dist_r Mscale_kron_dist_l Mscale_kron_dist_r : ket_db. -Hint Rewrite Mscale_assoc @Mmult_assoc : ket_db. -Hint Rewrite Mmult_1_l Mmult_1_r kron_1_l kron_1_r Mscale_0_l Mscale_0_r Mscale_1_l Mplus_0_l Mplus_0_r using (auto with wf_db) : ket_db. -Hint Rewrite kron_0_l kron_0_r Mmult_0_l Mmult_0_r : ket_db. -Hint Rewrite @kron_mixed_product : ket_db. +#[global] Hint Rewrite bra0_equiv bra1_equiv ket0_equiv ket1_equiv : ket_db. +#[global] Hint Rewrite bra0ket0 bra0ket1 bra1ket0 bra1ket1 : ket_db. +#[global] Hint Rewrite Mmult_plus_distr_l Mmult_plus_distr_r kron_plus_distr_l kron_plus_distr_r Mscale_plus_distr_r : ket_db. +#[global] Hint Rewrite Mscale_mult_dist_l Mscale_mult_dist_r Mscale_kron_dist_l Mscale_kron_dist_r : ket_db. +#[global] Hint Rewrite Mscale_assoc @Mmult_assoc : ket_db. +#[global] Hint Rewrite Mmult_1_l Mmult_1_r kron_1_l kron_1_r Mscale_0_l Mscale_0_r Mscale_1_l Mplus_0_l Mplus_0_r using (auto with wf_db) : ket_db. +#[global] Hint Rewrite kron_0_l kron_0_r Mmult_0_l Mmult_0_r : ket_db. +#[global] Hint Rewrite @kron_mixed_product : ket_db. (* Quantum-specific identities *) -Hint Rewrite H0_spec H1_spec Hplus_spec Hminus_spec X0_spec X1_spec Y0_spec Y1_spec +#[global] Hint Rewrite H0_spec H1_spec Hplus_spec Hminus_spec X0_spec X1_spec Y0_spec Y1_spec Z0_spec Z1_spec phase0_spec phase1_spec : ket_db. -Hint Rewrite CNOT00_spec CNOT01_spec CNOT10_spec CNOT11_spec SWAP_spec : ket_db. +#[global] Hint Rewrite CNOT00_spec CNOT01_spec CNOT10_spec CNOT11_spec SWAP_spec : ket_db. Lemma ket2bra : forall n, (ket n) † = bra n. Proof. destruct n; reflexivity. Qed. -Hint Rewrite ket2bra : ket_db. +#[global] Hint Rewrite ket2bra : ket_db. (* TODO: add transpose and adjoint lemmas to ket_db? *) Lemma ket0_transpose_bra0 : (ket 0) ⊤ = bra 0. @@ -1174,8 +1174,8 @@ Qed. Local Close Scope R_scope. -Hint Rewrite f_to_vec_cnot f_to_vec_σx f_to_vec_phase_shift using lia : f_to_vec_db. -Hint Rewrite (@update_index_eq bool) (@update_index_neq bool) (@update_twice_eq bool) (@update_same bool) using lia : f_to_vec_db. +#[global] Hint Rewrite f_to_vec_cnot f_to_vec_σx f_to_vec_phase_shift using lia : f_to_vec_db. +#[global] Hint Rewrite (@update_index_eq bool) (@update_index_neq bool) (@update_twice_eq bool) (@update_same bool) using lia : f_to_vec_db. (*******************************) From a8d111fff0c7e602f587b72894edbbded71ef6a6 Mon Sep 17 00:00:00 2001 From: Adrian Lehmann Date: Wed, 24 Jan 2024 18:33:15 -0600 Subject: [PATCH 2/7] Remove deprecation issue for 8.16+ --- .github/workflows/coq-action.yml | 6 ++--- .gitignore | 2 ++ CITATION.cff | 2 +- DiscreteProb.v | 10 ++++---- Eigenvectors.v | 10 ++++---- GenMatrix.v | 8 +++--- Matrix.v | 42 ++++++++++++++++---------------- Measurement.v | 2 +- Pad.v | 28 ++++++++++----------- Permutations.v | 6 ++--- Prelim.v | 5 +++- Quantum.v | 2 +- Rings.v | 2 +- VectorStates.v | 13 +++++----- coq-quantumlib.opam | 2 +- dune-project | 2 +- 16 files changed, 73 insertions(+), 69 deletions(-) diff --git a/.github/workflows/coq-action.yml b/.github/workflows/coq-action.yml index 7a72eee..c54534c 100644 --- a/.github/workflows/coq-action.yml +++ b/.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' diff --git a/.gitignore b/.gitignore index 6ddf536..318f794 100644 --- a/.gitignore +++ b/.gitignore @@ -49,8 +49,10 @@ time-of-build-pretty.log .CoqMakefile.d CoqMakefile* Makefile.coq* +Makefile.conf _build docs /.vscode +.DS_Store \ No newline at end of file diff --git a/CITATION.cff b/CITATION.cff index 86a29bd..8cc2aa4 100644 --- a/CITATION.cff +++ b/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" diff --git a/DiscreteProb.v b/DiscreteProb.v index 30d905d..5d20d2c 100644 --- a/DiscreteProb.v +++ b/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. diff --git a/Eigenvectors.v b/Eigenvectors.v index 33760ab..8d8e0a4 100644 --- a/Eigenvectors.v +++ b/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. diff --git a/GenMatrix.v b/GenMatrix.v index 67391e4..0b2d196 100644 --- a/GenMatrix.v +++ b/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. diff --git a/Matrix.v b/Matrix.v index f1aa2e9..7fef483 100644 --- a/Matrix.v +++ b/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) 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 - 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. diff --git a/Permutations.v b/Permutations.v index c122bfc..3257566 100644 --- a/Permutations.v +++ b/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. diff --git a/Prelim.v b/Prelim.v index 6650848..d41e395 100644 --- a/Prelim.v +++ b/Prelim.v @@ -14,7 +14,10 @@ Export ListNotations. (* a lemma that was removed from Coq in 8.16 that I found quite helpful *) Lemma le_plus_minus' : forall m n, m <= n -> n = m + (n - m). -Proof. lia. Qed. +Proof. intros. rewrite Nat.add_comm. rewrite Nat.sub_add; easy. Qed. + +Lemma le_plus_minus_r': forall n m : nat, n <= m -> n + (m - n) = m. +Proof. intros. rewrite Nat.add_comm. rewrite Nat.sub_add; easy. Qed. diff --git a/Quantum.v b/Quantum.v index 661be1f..1f4c1d0 100644 --- a/Quantum.v +++ b/Quantum.v @@ -1147,7 +1147,7 @@ Proof. distribute_adjoint. distribute_scale. rewrite UA, Cmult_comm, H. - lma'. + lma. Qed. diff --git a/Rings.v b/Rings.v index 59fa4e1..32465d6 100644 --- a/Rings.v +++ b/Rings.v @@ -1457,7 +1457,7 @@ Proof. unfold Cz8. apply injective_projections; simpl; try lra. rewrite Rmult_1_r, Rmult_0_l, Rplus_0_r. unfold Rdiv. - rewrite Rinv_mult_distr, <- Rmult_assoc, Rinv_r. lra. + rewrite Rinv_mult, <- Rmult_assoc, Rinv_r. lra. all: apply sqrt2_neq_0. Qed. diff --git a/VectorStates.v b/VectorStates.v index 542cdcd..2f9b60e 100644 --- a/VectorStates.v +++ b/VectorStates.v @@ -67,7 +67,7 @@ Proof. induction n; simpl. - Msimpl_light. reflexivity. - replace (2^n + (2^n + 0)) with (2^n * 2) by lia. - replace (1^n + 0) with (1*1) by (rewrite Nat.pow_1_l, plus_0_r; lia). + replace (1^n + 0) with (1*1) by (rewrite Nat.pow_1_l, Nat.add_0_r; lia). rewrite Nat.pow_1_l. rewrite kron_mixed_product. rewrite <- IHn. @@ -445,7 +445,7 @@ Proof. reflexivity. exists j. repeat split; trivial. - rewrite <- 2 beq_nat_refl; simpl; lca. + rewrite 2 Nat.eqb_refl; simpl; lca. intros j' Hj. bdestruct_all; auto. all : intros; simpl; try lca. @@ -646,7 +646,7 @@ Proof. repeat rewrite Nat.add_0_r. rewrite <- Nat.add_succ_l. replace (S (2 ^ n - 1)) with (1 + (2 ^ n - 1)) by easy. - rewrite <- le_plus_minus. + rewrite <- le_plus_minus'. rewrite <- Nat.add_sub_assoc. reflexivity. all: induction n; simpl; try lia. @@ -1605,7 +1605,8 @@ Qed. Lemma product_0 : forall f n, product (fun _ : nat => false) f n = false. Proof. intros f n. - induction n; simpl; auto. + induction n; simpl. + reflexivity. rewrite IHn; reflexivity. Qed. @@ -1729,8 +1730,8 @@ Proof. rewrite Mscale_vkron_distr_r. apply f_equal2. repeat rewrite <- RtoC_inv by nonzero. - rewrite RtoC_pow. - rewrite <- Rinv_pow by nonzero. + rewrite RtoC_pow. + rewrite pow_inv by nonzero. rewrite <- sqrt_pow by lra. reflexivity. apply vkron_to_vsum2. diff --git a/coq-quantumlib.opam b/coq-quantumlib.opam index ffb429b..bc8b929 100644 --- a/coq-quantumlib.opam +++ b/coq-quantumlib.opam @@ -1,6 +1,6 @@ # This file is generated by dune, edit dune-project instead opam-version: "2.0" -version: "1.2.0" +version: "1.3.0" synopsis: "Coq library for reasoning about quantum programs" description: """ inQWIRE's QuantumLib is a Coq library for reasoning diff --git a/dune-project b/dune-project index e80ee42..cecdbce 100644 --- a/dune-project +++ b/dune-project @@ -1,6 +1,6 @@ (lang dune 2.8) (name coq-quantumlib) -(version 1.2.0) +(version 1.3.0) (using coq 0.2) (generate_opam_files true) From 63736c59d23fc1378bf7273962647769fdbc2da6 Mon Sep 17 00:00:00 2001 From: Adrian Lehmann Date: Wed, 24 Jan 2024 21:45:11 -0600 Subject: [PATCH 3/7] Remove all possible 8.18 deprecation warnings while keeping 8.16 working --- Complex.v | 3 ++- FiniteGroups.v | 2 +- Polynomial.v | 10 ++++++---- Prelim.v | 8 ++++---- Quantum.v | 6 ++++-- 5 files changed, 17 insertions(+), 12 deletions(-) diff --git a/Complex.v b/Complex.v index 3b09ebc..d3546a5 100644 --- a/Complex.v +++ b/Complex.v @@ -624,6 +624,7 @@ Proof. intros. rewrite <- H' in H2. easy. Qed. + Lemma Cinv_mult_distr : forall c1 c2 : C, c1 <> 0 -> c2 <> 0 -> / (c1 * c2) = / c1 * / c2. Proof. intros. @@ -634,7 +635,7 @@ Proof. rewrite Rmult_div. rewrite Rmult_opp_opp. unfold Rminus. - rewrite <- RIneq.Ropp_div. + rewrite <- Ropp_div. rewrite <- Rdiv_plus_distr. rewrite Rmult_plus_distr_r. rewrite Rmult_plus_distr_l. diff --git a/FiniteGroups.v b/FiniteGroups.v index a07ed42..29eb619 100644 --- a/FiniteGroups.v +++ b/FiniteGroups.v @@ -16,7 +16,7 @@ Global Program Instance list_is_monoid {X} : Monoid (list X) := { Gzero := [] ; Gplus := @app X }. -Next Obligation. rewrite app_nil_end; easy. Qed. +Next Obligation. rewrite <- app_nil_r; easy. Qed. Next Obligation. rewrite app_assoc; easy. Qed. diff --git a/Polynomial.v b/Polynomial.v index 6111e5d..bfbf089 100644 --- a/Polynomial.v +++ b/Polynomial.v @@ -1031,7 +1031,7 @@ Lemma Peq_skipn_Peq_nil : forall (p1 p2 : Polynomial), skipn (length p1) p2 ≅ []. Proof. intros. apply Peq_firstn_eq in H0; auto. - rewrite (app_nil_end p1) in H. + rewrite <- (app_nil_r p1) in H. rewrite H0, <- (firstn_skipn (length p1)) in H. apply Peq_app_Peq in H. easy. @@ -1378,14 +1378,16 @@ Proof. apply ind_from_end; try easy. destruct H0 as [n [a [p' [H1 H2] ] ] ]. exists (S n), a, p'. split; auto. - rewrite H2, app_assoc_reverse. + rewrite H2, <- app_assoc. apply f_equal_gen; try easy. simpl. rewrite repeat_cons. easy. - exists 0, x, l. - split; auto. - apply app_nil_end. + split; auto. + simpl. + rewrite app_nil_r. + easy. Qed. Lemma compactify_breakdown : forall (p : Polynomial), diff --git a/Prelim.v b/Prelim.v index d41e395..e0c252a 100644 --- a/Prelim.v +++ b/Prelim.v @@ -290,13 +290,13 @@ Tactic Notation "gen" ident(X1) ident(X2) ident(X3) ident(X4) ident(X5) := Lemma double_mult : forall (n : nat), (n + n = 2 * n)%nat. Proof. intros. lia. Qed. Lemma pow_two_succ_l : forall x, (2^x * 2 = 2 ^ (x + 1))%nat. -Proof. intros. rewrite Nat.mul_comm. rewrite <- Nat.pow_succ_r'. intuition. Qed. +Proof. intros. rewrite Nat.mul_comm. rewrite <- Nat.pow_succ_r'. auto with *. Qed. Lemma pow_two_succ_r : forall x, (2 * 2^x = 2 ^ (x + 1))%nat. -Proof. intros. rewrite <- Nat.pow_succ_r'. intuition. Qed. +Proof. intros. rewrite <- Nat.pow_succ_r'. auto with *. Qed. Lemma double_pow : forall (n : nat), (2^n + 2^n = 2^(n+1))%nat. Proof. intros. rewrite double_mult. rewrite pow_two_succ_r. reflexivity. Qed. Lemma pow_components : forall (a b m n : nat), a = b -> m = n -> (a^m = b^n)%nat. -Proof. intuition. Qed. +Proof. auto with *. Qed. Lemma pow_positive : forall a b, a <> 0 -> 0 < a ^ b. Proof. intros. induction b; simpl; lia. Qed. @@ -378,7 +378,7 @@ Qed. Corollary subset_self : forall (X : Type) (l1 : list X), l1 ⊆ l1. Proof. intros X l1. assert (H: l1 ⊆ (l1 ++ [])). { apply subset_concat_l. } - rewrite <- app_nil_end in H. apply H. + rewrite app_nil_r in H. apply H. Qed. Lemma subsets_add : forall (X : Type) (l1 l2 l3 : list X), diff --git a/Quantum.v b/Quantum.v index 1f4c1d0..941dcbe 100644 --- a/Quantum.v +++ b/Quantum.v @@ -898,7 +898,8 @@ Proof. ++ apply functional_extensionality. intros x. bdestructΩ (n + x Date: Wed, 24 Jan 2024 22:28:57 -0600 Subject: [PATCH 4/7] Adapt to 8.19's removal of mult_O_le_stt --- DiscreteProb.v | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/DiscreteProb.v b/DiscreteProb.v index 5d20d2c..10e2ed3 100644 --- a/DiscreteProb.v +++ b/DiscreteProb.v @@ -1472,6 +1472,10 @@ Proof. assumption. Qed. +(* This was removed from std lib without replacement in 8.19 *) +Lemma mult_O_le_stt : forall n m : nat, (m = 0 \/ n <= m * n)%nat. +Proof. intros. induction m. auto. right. lia. Qed. + Lemma rewrite_pr_outcome_sum : forall n k (u : Square (2 ^ (n + k))) f, WF_Matrix u -> pr_outcome_sum (apply_u u) (fun x => f (fst k x)) @@ -1503,7 +1507,7 @@ Proof. rewrite <- le_plus_minus' in H0. rewrite Nat.add_comm in H0. assumption. - destruct (Arith_prebase.mult_O_le_stt (2^k) (2^n))%nat; auto. + destruct (mult_O_le_stt (2^k) (2^n))%nat; auto. assert (2 <> 0)%nat by lia. apply (pow_positive 2 n) in H2. lia. From 8081c43beb58ac1fbccca4aab1c4aa5d62396665 Mon Sep 17 00:00:00 2001 From: Adrian Lehmann Date: Wed, 24 Jan 2024 22:44:58 -0600 Subject: [PATCH 5/7] Remove 8.19 from CI for now until released on opam --- .github/workflows/coq-action.yml | 2 -- 1 file changed, 2 deletions(-) diff --git a/.github/workflows/coq-action.yml b/.github/workflows/coq-action.yml index c54534c..ffe6225 100644 --- a/.github/workflows/coq-action.yml +++ b/.github/workflows/coq-action.yml @@ -15,8 +15,6 @@ jobs: - '8.16' - '8.17' - '8.18' - - '8.19' - - 'dev' ocaml_version: - 'default' fail-fast: false # don't stop jobs if one fails From 49e462980e5cbd5846d4b666f0f38a029e93ecf8 Mon Sep 17 00:00:00 2001 From: Adrian Lehmann Date: Thu, 25 Jan 2024 11:07:03 -0600 Subject: [PATCH 6/7] Update opam depenency versions --- coq-quantumlib.opam | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/coq-quantumlib.opam b/coq-quantumlib.opam index bc8b929..139c5dc 100644 --- a/coq-quantumlib.opam +++ b/coq-quantumlib.opam @@ -14,7 +14,7 @@ doc: "https://inqwire.github.io/QuantumLib/toc.html" bug-reports: "https://github.com/inQWIRE/QuantumLib/issues" depends: [ "dune" {>= "2.8"} - "coq" {>= "8.12"} + "coq" {>= "8.16" < "8.20"} "odoc" {with-doc} ] build: [ From fe4b0d3d90ba075edf79c2acc0edf40a2119f13f Mon Sep 17 00:00:00 2001 From: Adrian Lehmann Date: Mon, 29 Jan 2024 15:36:44 -0600 Subject: [PATCH 7/7] Add 8.19 to CI --- .github/workflows/coq-action.yml | 1 + 1 file changed, 1 insertion(+) diff --git a/.github/workflows/coq-action.yml b/.github/workflows/coq-action.yml index ffe6225..6b8ec05 100644 --- a/.github/workflows/coq-action.yml +++ b/.github/workflows/coq-action.yml @@ -15,6 +15,7 @@ jobs: - '8.16' - '8.17' - '8.18' + - '8.19' ocaml_version: - 'default' fail-fast: false # don't stop jobs if one fails