Reduce QuantumQuery proof elaboration cost

LeanPool/QuantumQuery/Adversary.lean

@@ -297,7 +297,7 @@ lemma abs_apply_le_sqrt_dotProduct_self (x : n → ℝ) (i : n) :
 
 lemma dotProduct_mulVec_eq_sum (A : Matrix n n ℝ) (u w : n → ℝ) :
     u ⬝ᵥ A *ᵥ w = ∑ x, ∑ y, u x * A x y * w y := by
-  simp [dotProduct, Matrix.mulVec, Finset.mul_sum, mul_assoc]
+  simp only [dotProduct, Matrix.mulVec, Finset.mul_sum, mul_assoc]
 
 variable [DecidableEq n]
 
@@ -345,7 +345,8 @@ theorem l2_opNorm_le_of_forall_dotProduct (A : Matrix n n ℝ) {c : ℝ}
   · rw [← h0]
     positivity
   · rw [habs, hww] at key
-    nlinarith [key, h0, Real.sqrt_nonneg (y ⬝ᵥ y)]
+    rw [mul_right_comm c s] at key
+    exact (mul_le_mul_iff_left₀ h0).mp key
 
 /-- Every entry is bounded by the L2 operator norm. -/
 theorem abs_entry_le_l2_opNorm (A : Matrix n n ℝ) (x y : n) : |A x y| ≤ ‖A‖ := by
@@ -595,7 +596,7 @@ lemma norm_le_of_feasible (h1 : IsAdvMatrix f Γ)
       Finset.sum_le_sum fun x _ => Finset.sum_le_sum fun y _ =>
         abs_apply_le_one_of_feasible h1 h2 x y
     _ = (Fintype.card (ι → σ) : ℝ) ^ 2 := by
-      simp [Finset.sum_const, Finset.card_univ, pow_two]
+      simp only [Finset.sum_const, Finset.card_univ, nsmul_eq_mul, mul_one, pow_two]
 
 lemma bddAbove_advPM_set (f : (ι → σ) → O) :
     BddAbove {r : ℝ | ∃ Γ, IsAdvMatrix f Γ ∧ (∀ i, ‖Γ ⊙ advD i‖ ≤ 1) ∧
@@ -681,9 +682,7 @@ lemma pairMatrix_isHermitian (x y : ι → σ) :
 lemma single_one_mulVec (a b : ι → σ) (u : (ι → σ) → ℝ) :
     Matrix.single a b (1 : ℝ) *ᵥ u = fun w => if a = w then u b else 0 := by
   funext w
-  by_cases haw : a = w
-  · simp [Matrix.mulVec, dotProduct, Matrix.single_apply, haw]
-  · simp [Matrix.mulVec, dotProduct, haw]
+  simp only [Matrix.single_mulVec, one_mul, Function.update_apply, Pi.zero_apply, eq_comm]
 
 lemma pairMatrix_mulVec (x y : ι → σ) (u : (ι → σ) → ℝ) :
     pairMatrix x y *ᵥ u
@@ -919,13 +918,12 @@ lemma mulVec_brestrict {M : Matrix U U ℝ} {χ : U → Bool}
     by_cases hv : χ v = b
     · rw [ite_eq_left hv, hM u v (hu.trans hv.symm), zero_mul]
     · rw [ite_eq_right hv]
-  · have hu' : χ u = !b := by cases hcu : χ u <;> cases b <;> simp_all
+  · have hu' : χ u = !b := Bool.eq_not_of_ne hu
     rw [ite_eq_left hu']
     refine Finset.sum_congr rfl fun v _ => ?_
     by_cases hv : χ v = b
     · rw [ite_eq_left hv]
-    · have hv' : χ v = χ u := by
-        cases hcv : χ v <;> cases hcu : χ u <;> cases b <;> simp_all
+    · have hv' : χ v = χ u := (Bool.eq_not_of_ne hv).trans hu'.symm
       rw [ite_eq_right hv, hM u v hv'.symm, zero_mul]
 
 lemma mulVec_brestrict_eigen {M : Matrix U U ℝ} {χ : U → Bool}
@@ -3064,8 +3062,8 @@ lemma hat_guarded_row_sumGen {g : (Y) → Bool}
         by_cases h : g u = b
         · rw [ite_eq_left h]
         · rw [ite_eq_right h]
-          have hgg : g u = g u₀ := by
-            cases hgu : g u <;> cases hgu0 : g u₀ <;> cases b <;> simp_all
+          have hgg : g u = g u₀ :=
+            (Bool.eq_not_of_ne h).trans (Bool.eq_not_of_ne h0).symm
           rw [hN.apply_eq_zero hgg.symm, zero_mul]
       rw [Finset.sum_congr rfl fun u _ => hall u]
       have hcf := congrFun hv u₀
@@ -3901,7 +3899,7 @@ lemma norm_le_of_feasibleOn (hdet : ∀ x y, read x = read y → f x = f y)
       Finset.sum_le_sum fun x _ => Finset.sum_le_sum fun y _ =>
         abs_apply_le_one_of_feasibleOn hdet h1 h2 x y
     _ = (Fintype.card X : ℝ) ^ 2 := by
-      simp [Finset.sum_const, Finset.card_univ, pow_two]
+      simp only [Finset.sum_const, Finset.card_univ, nsmul_eq_mul, mul_one, pow_two]
 
 omit [DecidableEq ι] [Fintype ι] in
 lemma bddAbove_advPMOn_set (hdet : ∀ x y, read x = read y → f x = f y) :
@@ -4684,7 +4682,7 @@ theorem lt_advPMOn_of_certificate {read : X → ι → σ} {f : X → Bool}
       l2_opNorm_hadamard_dualTargetOn_le f _
     have h2 : ‖(2 : ℝ)⁻¹‖ = (2 : ℝ)⁻¹ := by norm_num
     rw [h2]
-    nlinarith [hnorm i, norm_nonneg ((Γ' ⊙ advDOn read i) ⊙ dualTargetOn f)]
+    linarith only [h1, hnorm i]
   set R := Real.sqrt (∑ x, p x) with hR
   have hR0 : 0 < R := Real.sqrt_pos.mpr hsum
   have hRR : R * R = ∑ x, p x := Real.mul_self_sqrt hsum.le
@@ -4713,7 +4711,7 @@ theorem lt_advPMOn_of_certificate {read : X → ι → σ} {f : X → Bool}
     field_simp
   have hlt : c < a ⬝ᵥ Γ'' *ᵥ a := by
     rw [hval, lt_div_iff₀ (by positivity)]
-    linarith [hobj]
+    linarith only [hobj]
   have hbound : a ⬝ᵥ Γ'' *ᵥ a ≤ ‖Γ''‖ := by
     have := abs_dotProduct_mulVec_le Γ'' a a
     rw [haa, Real.sqrt_one] at this
@@ -5245,7 +5243,7 @@ theorem exists_dualPairOn_of_advPMOn_lt {read : X → ι → σ} {f : X → Bool
     have hexp : κ * ((∑ x, s x * s x) + ∑ x, t x * t x)
         = κ * (∑ x, s x * s x) + κ * (∑ x, t x * t x) := by ring
     rw [hexp] at h
-    linarith
+    linarith only [h]
   have hquadabs : ∀ (i : ι) (s t : X → ℝ),
       |s ⬝ᵥ (Ξ ⊙ advDOn read i) *ᵥ t|
         ≤ (∑ x, P false x * (s x * s x)) + ∑ x, P true x * (t x * t x) := by
@@ -5261,7 +5259,7 @@ theorem exists_dualPairOn_of_advPMOn_lt {read : X → ι → σ} {f : X → Bool
         = ∑ x, P false x * (s x * s x) :=
       Finset.sum_congr rfl fun x _ => by ring
     rw [hneg, hsq] at h2
-    exact abs_le.mpr ⟨by linarith, by linarith⟩
+    exact abs_le.mpr ⟨by linarith only [h2], h1⟩
   -- the weights are strictly positive
   have hsingle_ne : ∀ x : X, (Pi.single x (1 : ℝ) : X → ℝ) ≠ 0 := by
     intro x h
@@ -5279,7 +5277,7 @@ theorem exists_dualPairOn_of_advPMOn_lt {read : X → ι → σ} {f : X → Bool
         simp only [Pi.zero_apply, mul_zero, Finset.sum_const_zero, add_zero,
           hz, zero_add] at h
         rw [hP]
-        linarith
+        linarith only [h]
     | true =>
         have h := hQbound (concVecOn i₀ 0 (Pi.single x 1))
           (concVecOn_ne_zero_right (hsingle_ne x))
@@ -5289,7 +5287,7 @@ theorem exists_dualPairOn_of_advPMOn_lt {read : X → ι → σ} {f : X → Bool
         simp only [Pi.zero_apply, mul_zero, Finset.sum_const_zero, zero_add,
           hz] at h
         rw [hP]
-        linarith
+        linarith only [h]
   -- the objective hypothesis of the certificate
   have hcorner := hbox _ (dualCornerOn_mem (f := f) hc0.le)
   have hcornerval : φ (dualCornerOn f c)
@@ -5322,7 +5320,7 @@ theorem exists_dualPairOn_of_advPMOn_lt {read : X → ι → σ} {f : X → Bool
       rw [← hkappa, hTdef]
       ring
     rw [hLHS]
-    linarith
+    linarith only [hcorner, huv]
   exact absurd
     (lt_advPMOn_of_certificate_two hdet (hPpos false) (hPpos true) hquadabs hobj)
     (not_lt.mpr hc.le)
@@ -6810,8 +6808,9 @@ lemma sqrt_card_le_norm_starMatrix {S : Finset (ι → σ)} {c : ι → σ}
     ring
   have h2k : Real.sqrt (2 * k) * Real.sqrt (2 * k) = 2 * k :=
     Real.mul_self_sqrt (by positivity)
-  rw [habs] at h
-  nlinarith [h, h2k, hkpos, Real.sqrt_nonneg k]
+  rw [habs, mul_assoc ‖starMatrix S c‖, h2k,
+    mul_comm ‖starMatrix S c‖ (2 * k)] at h
+  exact le_of_mul_le_mul_left h (mul_pos (by norm_num) hkpos)
 
 theorem norm_starMatrix {S : Finset (ι → σ)} {c : ι → σ} (hc : c ∉ S)
     (hS : S.Nonempty) : ‖starMatrix S c‖ = Real.sqrt (S.card : ℝ) :=
@@ -6994,8 +6993,9 @@ lemma sqrt_starWeight_le_norm_wStarMatrix {S : Finset (ι → σ)}
     ring
   have h2W : Real.sqrt (2 * W) * Real.sqrt (2 * W) = 2 * W :=
     Real.mul_self_sqrt (by positivity)
-  rw [habs] at h
-  nlinarith [h, h2W, hW, Real.sqrt_nonneg W]
+  rw [habs, mul_assoc ‖wStarMatrix S c w‖, h2W,
+    mul_comm ‖wStarMatrix S c w‖ (2 * W)] at h
+  exact le_of_mul_le_mul_left h (mul_pos (by norm_num) hW)
 
 theorem norm_wStarMatrix {S : Finset (ι → σ)} {c : ι → σ} (hc : c ∉ S)
     {w : (ι → σ) → ℝ} (hW : 0 < starWeight S w) :
@@ -7308,10 +7308,7 @@ noncomputable def orNDual [Nonempty ι] : DualPair Unit (orN : (ι → Bool) →
 omit [DecidableEq ι] in
 lemma orNDual_isCostLe [Nonempty ι] :
     (orNDual (ι := ι)).IsCostLe (Real.sqrt (Fintype.card ι : ℝ)) := by
-  have hδ : orNDelta ι ≠ 0 := orNDelta_ne_zero
   have hn : (0:ℝ) < (Fintype.card ι : ℝ) := by exact_mod_cast Fintype.card_pos
-  have hs : Real.sqrt (Fintype.card ι : ℝ) * Real.sqrt (Fintype.card ι : ℝ)
-      = (Fintype.card ι : ℝ) := Real.mul_self_sqrt hn.le
   have key : ∀ x : ι → Bool,
       (∑ i : ι, ∑ _k : Unit, orNDualVec x i * orNDualVec x i)
         ≤ Real.sqrt (Fintype.card ι : ℝ) := by
@@ -7347,16 +7344,13 @@ lemma orNDual_isCostLe [Nonempty ι] :
           ((1 / ((supportCard x : ℝ) * orNDelta ι)) *
             (1 / ((supportCard x : ℝ) * orNDelta ι)))
           = Real.sqrt (Fintype.card ι : ℝ) / (supportCard x : ℝ) := by
-        rw [orNDelta] at *
+        rw [div_mul_div_comm, one_mul, mul_mul_mul_comm, orNDelta_sq]
         field_simp
-        nlinarith [hs, Real.sq_sqrt (Real.sqrt_nonneg (Fintype.card ι : ℝ)),
-          Real.sqrt_nonneg (Fintype.card ι : ℝ),
-          Real.mul_self_sqrt (Real.sqrt_nonneg (Fintype.card ι : ℝ))]
       rw [hval]
       have hone : (1:ℝ) ≤ (supportCard x : ℝ) := by
         exact_mod_cast supportCard_pos hx
       rw [div_le_iff₀ hpos]
-      nlinarith [Real.sqrt_nonneg (Fintype.card ι : ℝ), hone]
+      exact le_mul_of_one_le_right (Real.sqrt_nonneg _) hone
   exact ⟨key, key⟩
 
 omit [DecidableEq ι] in

LeanPool/QuantumQuery/Algorithms.lean

@@ -504,7 +504,7 @@ lemma sum_prod_majority_le {k t : ℕ} {ε : ℝ} (hε0 : 0 ≤ ε) (hε1 : ε 
       have hne : y j ≠ b j := by
         simpa [hS] using (Finset.mem_filter.mp hj).2
       have hval : y j = !(b j) := by
-        cases hb : b j <;> cases hyj : y j <;> simp_all
+        exact Bool.eq_not_of_ne hne
       rw [hval]
       exact hpe j
     have h2 : (∏ j ∈ Sᶜ, p j (y j)) ≤ 1 :=
@@ -1509,19 +1509,19 @@ private lemma blockDiagonal_mulVec_embed
     rw [Matrix.blockDiagonal_apply]
     by_cases h : u' = u
     · subst h
-      by_cases h2 : u' = v <;> simp [h2]
-    · simp [h, Ne.symm h]
+      by_cases h2 : u' = v <;> simp only [h2, ↓reduceIte, mul_zero]
+    · simp only [ite_eq_right h, ite_eq_right (Ne.symm h), zero_mul]
   simp only [hterm]
   rw [show (∑ s : QBasis ι σ W, ∑ u : V,
       (if u = u' then (if u' = v then fam u' s' s * ψ s else 0) else 0))
       = ∑ s : QBasis ι σ W, (if u' = v then fam u' s' s * ψ s else 0) from
     Finset.sum_congr rfl fun s _ => by
       rw [Finset.sum_ite_eq' Finset.univ u' (fun _ => (if u' = v then fam u' s' s * ψ s else 0))]
-      simp]
+      simp only [Finset.mem_univ, ↓reduceIte]]
   by_cases h : u' = v
   · subst h
-    simp [Matrix.mulVec, dotProduct]
-  · simp [h]
+    simp only [Matrix.mulVec, dotProduct, ↓reduceIte]
+  · simp only [ite_eq_right h, Finset.sum_const_zero]
 
 omit [DecidableEq W] [DecidableEq ι] [DecidableEq σ] in
 /-- **The action on the encoded subspace.** -/
@@ -4101,7 +4101,7 @@ theorem pairRoutine_run_prodState (R₁ : QRoutine ι σ W₁)
     rw [pairRoutine, QRoutine.comp_run, QRoutine.comp_run, QRoutine.comp_run,
       QRoutine.comp_run, QRoutine.comp_run, QRoutine.ofUnitary_run,
       QRoutine.ofUnitary_run]
-    noncomm_ring
+    simp only [Matrix.mul_assoc]
   rw [hrun, ← Matrix.mulVec_mulVec, ← Matrix.mulVec_mulVec,
     ← Matrix.mulVec_mulVec, ← Matrix.mulVec_mulVec, ← Matrix.mulVec_mulVec,
     pairSwap₁_mulVec_prodState]

LeanPool/QuantumQuery/QueryBounds.lean

@@ -1161,8 +1161,8 @@ private lemma sqrt_cross_sum_le {β β' ε : ℝ} (hβ0 : 0 ≤ β) (hβ'0 : 0 
     Real.sqrt (1 - β) * Real.sqrt β' + Real.sqrt β * Real.sqrt (1 - β')
       ≤ 2 * Real.sqrt (ε * (1 - ε)) := by
   have hε0 : 0 ≤ ε := le_trans hβ0 hβε
-  have hβ1 : β ≤ 1 := by linarith
-  have hβ'1 : β' ≤ 1 := by linarith
+  have hβ1 : β ≤ 1 := hβε.trans (hε2.trans (by norm_num))
+  have hβ'1 : β' ≤ 1 := hβ'ε.trans (hε2.trans (by norm_num))
   set s := Real.sqrt β with hs
   set s' := Real.sqrt β' with hs'
   set c := Real.sqrt (1 - β) with hc
@@ -1174,8 +1174,8 @@ private lemma sqrt_cross_sum_le {β β' ε : ℝ} (hβ0 : 0 ≤ β) (hβ'0 : 0 
   have hc'0 : 0 ≤ c' := Real.sqrt_nonneg _
   have hs2 : s ^ 2 = β := Real.sq_sqrt hβ0
   have hs'2 : s' ^ 2 = β' := Real.sq_sqrt hβ'0
-  have hc2 : c ^ 2 = 1 - β := Real.sq_sqrt (by linarith)
-  have hc'2 : c' ^ 2 = 1 - β' := Real.sq_sqrt (by linarith)
+  have hc2 : c ^ 2 = 1 - β := Real.sq_sqrt (sub_nonneg.mpr hβ1)
+  have hc'2 : c' ^ 2 = 1 - β' := Real.sq_sqrt (sub_nonneg.mpr hβ'1)
   have he2 : e ^ 2 = ε := Real.sq_sqrt hε0
   have hse : s ≤ e := by rw [hs, he]; exact Real.sqrt_le_sqrt hβε
   have hs'e : s' ≤ e := by rw [hs', he]; exact Real.sqrt_le_sqrt hβ'ε
@@ -1186,7 +1186,7 @@ private lemma sqrt_cross_sum_le {β β' ε : ℝ} (hβ0 : 0 ≤ β) (hβ'0 : 0 
     rw [show (c - c') ^ 2 = c ^ 2 - 2 * (c * c') + c' ^ 2 from by ring,
       hc2, hc'2] at hsq
     rw [hs2, hs'2]
-    linarith
+    linarith only [hsq]
   -- the squared left side, against the polynomial
   have hLsq : (c * s' + s * c') ^ 2 ≤ (s + s') ^ 2 * (1 - s * s') := by
     have h1 : (c * s' + s * c') ^ 2
@@ -1201,14 +1201,16 @@ private lemma sqrt_cross_sum_le {β β' ε : ℝ} (hβ0 : 0 ≤ β) (hβ'0 : 0 
           + 2 * (s * s') * (1 - (s ^ 2 + s' ^ 2) / 2)
         = (s + s') ^ 2 * (1 - s * s') := by
       rw [← hs2, ← hs'2]; ring
-    linarith [h1, h2, h3]
+    rw [h1, ← h3]
+    exact add_le_add_right h2 _
   have hpoly := poly_bound hs0 hs'0 hse hs'e heh
   -- conclude by monotone square root
   have hL0 : 0 ≤ c * s' + s * c' :=
     add_nonneg (mul_nonneg hc0 hs'0) (mul_nonneg hs0 hc'0)
   have hchain : (c * s' + s * c') ^ 2 ≤ (2 * Real.sqrt (ε * (1 - ε))) ^ 2 := by
     have hRsq : (2 * Real.sqrt (ε * (1 - ε))) ^ 2 = 4 * (ε * (1 - ε)) := by
-      rw [mul_pow, Real.sq_sqrt (by nlinarith : (0 : ℝ) ≤ ε * (1 - ε))]
+      rw [mul_pow, Real.sq_sqrt
+        (mul_nonneg hε0 (sub_nonneg.mpr (hε2.trans (by norm_num))))]
       norm_num
     rw [hRsq]
     calc (c * s' + s * c') ^ 2 ≤ (s + s') ^ 2 * (1 - s * s') := hLsq