From 7b2769d9604b8e145f25ee2c9af395cf173f56be Mon Sep 17 00:00:00 2001 From: Jake Zweifler Date: Tue, 16 Nov 2021 15:59:15 -0600 Subject: [PATCH] removed warnings --- Complex.v | 16 ++++++++-------- Dirac.v | 22 +++++++++++----------- Matrix.v | 8 ++++---- Pad.v | 6 +----- Quantum.v | 18 +++++++++--------- 5 files changed, 33 insertions(+), 37 deletions(-) diff --git a/Complex.v b/Complex.v index d8fea2b..47d48f8 100644 --- a/Complex.v +++ b/Complex.v @@ -1024,7 +1024,7 @@ Proof. Qed. -#[global] Hint Rewrite Cexp_0 Cexp_PI Cexp_PI2 Cexp_2PI Cexp_3PI2 Cexp_PI4 Cexp_PIm4 +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_db. @@ -1065,23 +1065,23 @@ Ltac nonzero := | |- Rle _ _ => lra end. -#[global] Hint Rewrite Cminus_unfold Cdiv_unfold Ci2 Cconj_R Cconj_opp Cconj_rad2 +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. -#[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. +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. (* Previously in the other direction *) -#[global] Hint Rewrite Cinv_mult_distr using nonzero : C_db. +Hint Rewrite Cinv_mult_distr using nonzero : C_db. (* Light rewriting db *) -#[global] Hint Rewrite Cplus_0_l Cplus_0_r Cmult_0_l Cmult_0_r Copp_0 +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 *) -#[global] Hint Rewrite Cmult_plus_distr_l Cmult_plus_distr_r Copp_plus_distr Copp_mult_distr_l +Hint Rewrite Cmult_plus_distr_l Cmult_plus_distr_r Copp_plus_distr Copp_mult_distr_l Copp_involutive : Cdist_db. diff --git a/Dirac.v b/Dirac.v index 4b2542c..034dec4 100644 --- a/Dirac.v +++ b/Dirac.v @@ -124,23 +124,23 @@ Proof. intros. destruct x,y; lma'. Qed. (* Automation *) (* General matrix rewrites *) -#[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. +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. (* Quantum-specific identities *) -#[global] Hint Rewrite H0_spec H1_spec Hplus_spec Hminus_spec X0_spec X1_spec Y0_spec Y1_spec +Hint Rewrite H0_spec H1_spec Hplus_spec Hminus_spec X0_spec X1_spec Y0_spec Y1_spec Z0_spec Z1_spec : ket_db. -#[global] Hint Rewrite CNOT00_spec CNOT01_spec CNOT10_spec CNOT11_spec SWAP_spec : ket_db. +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. -#[global] Hint Rewrite ket2bra : ket_db. +Hint Rewrite ket2bra : ket_db. (* Examples using ket_db *) Lemma XYZ0 : -Ci .* σx × σy × σz × ∣ 0 ⟩ = ∣ 0 ⟩. diff --git a/Matrix.v b/Matrix.v index 5f308b3..94f430c 100644 --- a/Matrix.v +++ b/Matrix.v @@ -1545,7 +1545,7 @@ Proof. intros. bdestruct (y =? 0). subst. simpl. bdestruct (z =? 0). subst. easy. apply Nat.mod_0_l. easy. - bdestruct (z =? 0). subst. rewrite Nat.mul_0_r. simpl; easy. + bdestruct (z =? 0). subst. rewrite Nat.mul_0_r. simpl. rewrite Nat.div_0_l; easy. pattern x at 1. rewrite (Nat.div_mod x (y * z)) by nia. replace (y * z * (x / (y * z))) with ((z * (x / (y * z))) * y) by lia. rewrite Nat.div_add_l with (b := y) by easy. @@ -3973,16 +3973,16 @@ Tactic Notation "restore_dims" := restore_dims (repeat rewrite Nat.pow_1_l; try *) (* eauto will cause major choking... *) -#[global] Hint Rewrite @kron_1_l @kron_1_r @Mmult_1_l @Mmult_1_r @Mscale_1_l +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. -#[global] Hint Rewrite @kron_0_l @kron_0_r @Mmult_0_l @Mmult_0_r @Mplus_0_l @Mplus_0_r +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. -#[global] Hint Rewrite @Mmult_adjoint @Mplus_adjoint @kron_adjoint @kron_mixed_product +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. diff --git a/Pad.v b/Pad.v index a1da7c8..5c8b2f2 100644 --- a/Pad.v +++ b/Pad.v @@ -45,10 +45,6 @@ Definition ctrl_U (dim m n: nat) (U: Square 2) := (** some helper lemmas *) -Lemma smpl_U_extend_miss : forall - - - (** Well-formedness **) @@ -69,4 +65,4 @@ Lemma WF_ctrl_U : forall dim m n U, WF_Matrix U -> WF_Matrix (ctrl_U dim m n U). all : apply WF_pad; rewrite H'; apply WF_plus; auto with wf_db. Qed. -Hint Resolve WF_pad WF_smpl_U WF_ctrl_U : wf_db. +#[global] Hint Resolve WF_pad WF_smpl_U WF_ctrl_U : wf_db. diff --git a/Quantum.v b/Quantum.v index 13a0c11..14c1361 100644 --- a/Quantum.v +++ b/Quantum.v @@ -447,10 +447,10 @@ Proof. Msimpl; reflexivity. Qed. -#[global] Hint Rewrite Mmult00 Mmult01 Mmult10 Mmult11 Mmult0X MmultX0 Mmult1X MmultX1 : Q_db. -#[global] Hint Rewrite MmultXX MmultYY MmultZZ MmultHH Mplus01 Mplus10 : 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. +Hint Rewrite Mmult00 Mmult01 Mmult10 Mmult11 Mmult0X MmultX0 Mmult1X MmultX1 : Q_db. +Hint Rewrite MmultXX MmultYY MmultZZ MmultHH Mplus01 Mplus10 : 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. Lemma swap_swap : swap × swap = I (2*2). Proof. solve_matrix. Qed. @@ -465,7 +465,7 @@ Proof. reflexivity. Qed. -#[global] Hint Rewrite swap_swap swap_swap_r using (auto 100 with wf_db): Q_db. +Hint Rewrite swap_swap swap_swap_r using (auto 100 with wf_db): Q_db. @@ -1078,10 +1078,10 @@ Qed. Lemma braqubit0_sa : ∣0⟩⟨0∣† = ∣0⟩⟨0∣. Proof. lma. Qed. Lemma braqubit1_sa : ∣1⟩⟨1∣† = ∣1⟩⟨1∣. Proof. lma. Qed. -#[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. +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 : -#[global] Hint Rewrite control_sa using (autorewrite with M_db; reflexivity) : M_db. *) +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. @@ -1148,7 +1148,7 @@ Proof. Qed. -#[global] Hint Rewrite phase_0 phase_2pi phase_pi phase_neg_pi : Q_db. +Hint Rewrite phase_0 phase_2pi phase_pi phase_neg_pi : Q_db. (*****************************) @@ -1696,7 +1696,7 @@ Proof. lca. Qed. -#[global] Hint Rewrite swap_spec using (auto 100 with wf_db) : Q_db. +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 ->