removed warnings

inQWIRE · Nov 16, 2021 · 7b2769d · 7b2769d
1 parent c3260d5
commit 7b2769d
Show file tree

Hide file tree

Showing 5 changed files with 33 additions and 37 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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 ->