Update to Lean 4.7.0

No statements have changed.

Within the proofs, the main change is that `simp` no longer has `decide := true` as a default.
Some other theorems were renamed upstream.

PiperOrigin-RevId: 631717078
Change-Id: I1c59a179f69d16081eaa8dce1c90847876a58c89

Comp/Basic.lean

@@ -101,7 +101,7 @@ lemma cost_of_not_mem (f : Comp s α) (o : I → Oracle) {i : I} (is : i ∉ s)
   · simp only [cost_sample, h, exp_const]
   · simp only [cost_query', h0, h1, ite_self, exp_const, add_zero]
     by_cases ij : i = j
-    · simp only [ij] at is; simp only [js] at is
+    · simp only [ij] at is; simp (config := {decide := true}) only [js] at is
     · simp only [ij, if_false]
 
 /-- Expanding `query'.run` -/
@@ -307,7 +307,7 @@ macro "not_mem" : tactic =>
 
 /-- Show `s ⊆ t` via `simp` -/
 macro "subset" : tactic =>
-  `(tactic| simp only [Set.mem_singleton_iff, Set.singleton_subset_iff, Set.mem_insert_iff,
+  `(tactic| simp (config := {decide := true}) only [Set.mem_singleton_iff, Set.singleton_subset_iff, Set.mem_insert_iff,
     or_false])
 
 /-- Show a cost is zero via `i : I` not being in `s` -/

Debate/Cost.lean

@@ -7,9 +7,6 @@ import Debate.Protocol
 See `Correct.lean` for the summary.
 -/
 
--- Work around https://github.com/leanprover/lean4/issues/2220
-local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- See issue lean4#2220
-
 open Classical
 open Prob
 open Option (some none)
@@ -158,10 +155,10 @@ lemma post_stepsV (alice : Alice) (bob : Bob) (vera : Vera) :
         postV, bind_assoc, step]
       apply congr_arg₂ _ rfl ?_; ext p; apply congr_arg₂ _ rfl ?_; ext b
       induction b
-      · simp only [ite_false, Comp.allow_all_pure, pure_bind]
-      · simp only [ite_true]
+      · simp only [ite_false, Comp.allow_all_pure, pure_bind, postV]
+      · simp only [ite_cond_eq_true]
         rw [Comp.allow_all, Comp.allow, bind_assoc]
-        simp only [Comp.allow, pure_bind, Comp.sample'_bind]
+        simp only [Comp.allow, pure_bind, Comp.sample'_bind, postV]
 
 /-- Vera makes few queries, regardless of Alice and Bob -/
 theorem vera_debate_cost (o : Oracle) (alice : Alice) (bob : Bob) (t : ℕ):

Debate/Details.lean

@@ -56,14 +56,14 @@ lemma alice_pr_le (e0 : 0 < e) (q0 : 0 < q) (y : Vector Bool n) :
 lemma le_alice_pr (o : Oracle) (i : OracleId) (e0 : 0 < e) (q0 : 0 < q) (y : Vector Bool n) :
     1 - q ≤ ((alice' e q i _ y).prob' o).pr (λ p ↦ |p - (o _ y).prob true| ≤ e) := by
   trans ((alice' e q i _ y).prob' o).pr (λ p ↦ |p - (o _ y).prob true| < e)
-  · rw [pr_neg']; simp only [not_lt]; linarith [alice_pr_le e0 q0 y]
+  · rw [pr_neg']; simp only [not_lt]; linarith [alice_pr_le (i := i) (o := o) e0 q0 y]
   · apply pr_mono; intro _ _ h; exact le_of_lt h
 
 /-- Honest Bob usually accepts if Alice is off by ≤ c -/
 lemma bob_complete (o : Oracle) (i : OracleId) (cs : c < s) (q0 : 0 < q) {y : Vector Bool n}
     (good : |p - (o _ y).prob true| ≤ c) :
     ((bob' c s q i _ y p).prob' o).prob false ≤ q := by
-  simp only [bob', prob_bind, prob_pure, Bool.false_eq_decide_iff, not_lt, Comp.prob',
+  simp only [bob', prob_bind, prob_pure, false_eq_decide_iff, not_lt, Comp.prob',
     Comp.prob_bind, Comp.prob_pure]
   rw [←pr]
   refine' le_trans (pr_mono _) (alice_pr_le (by linarith) q0 y)
@@ -78,7 +78,7 @@ lemma bob_complete (o : Oracle) (i : OracleId) (cs : c < s) (q0 : 0 < q) {y : Ve
 lemma bob_sound (o : Oracle) (i : OracleId) (cs : c < s) (q0 : 0 < q) {y : Vector Bool n}
     (bad : |p - (o _ y).prob true| ≥ s) :
     ((bob' c s q i _ y p).prob' o).prob true ≤ q := by
-  simp only [bob', prob_bind, prob_pure, Bool.true_eq_decide_iff, not_lt, Comp.prob',
+  simp only [bob', prob_bind, prob_pure, true_eq_decide_iff, not_lt, Comp.prob',
     Comp.prob_bind, Comp.prob_pure]
   rw [←pr]
   refine' le_trans (pr_mono _) (alice_pr_le (by linarith) q0 y)
@@ -293,7 +293,7 @@ lemma alices_close (o : Oracle) (e0 : 0 < e) (q0 : 0 < q) (q1 : q ≤ 1) :
     (1 - q)^n ≤ (alices o (alice e q) n).pr (fun (p,y) ↦ close p (o.probs y) e) := by
   induction' n with n h
   · simp only [Nat.zero_eq, pow_zero, alices, close_nil, pr_pure, if_true, le_refl]
-  · simp only [pow_succ', alices, Oracle.probs, pr_bind, pr_pure, Vector.tail_cons, close_cons, ite_and_one_zero,
+  · simp only [pow_succ, alices, Oracle.probs, pr_bind, pr_pure, Vector.tail_cons, close_cons, ite_and_one_zero,
       exp_const_mul, exp_const, exp_mul_const]
     apply le_exp_of_cut (fun (p,y) ↦ close p (o.probs y) e) ((1 - q)^n) (1 - q)
     · apply h
@@ -328,34 +328,34 @@ lemma alices_success (o : Oracle) (L : o.lipschitz t k) (e0 : 0 < e) (q0 : 0 < q
           by_cases c : close p (o.probs y) e
           · simp only [c, if_true, mul_one, snaps_prob _ c]
           · simp only [c, if_false, mul_zero]
-        simp only [pr_neg, ae]; linarith [alices_close o e0 q0 q1]
+        simp only [pr_neg, ae]; linarith [alices_close (n := t + 1) o e0 q0 q1]
 
 /-- If Alice is correct and Bob rejects, the probability of false is low -/
 lemma evil_bobs_lies' (o : Oracle) (eve : Bob) (cs : c < s) (v0 : 0 < v)
     {p : Vector ℝ n} {y : Vector Bool n} (py : close p (o.probs y) c) :
     (bobs o eve (vera c s v) p y).cond (λ r ↦ r = some false) (λ r ↦ r.isSome) ≤ v := by
   have v0' := le_of_lt v0
   induction' n with n h
-  · simp only [bobs, cond_pure, if_false, v0']
+  · simp (config := {decide := true}) only [bobs, cond_pure, if_false, v0']
   · simp only [close_succ, Vector.eq_cons_iff] at py
     apply le_trans (cond_bind_le_of_cut (λ r ↦ r.isSome)); apply max_le
     · refine' le_trans (cond_bind_le_first (λ r ↦ r = some false)
         (λ r ↦ r.isSome) (λ r ↦ r = some false) (λ r ↦ r.isSome) _ _) _;
       · intro r s pr ps r0 s0 _; match r with
-        | none => simp only at r0 | some false => rfl
-        | some true => simp only [s0, prob_pure, ite_false, ne_eq, not_true] at ps
+        | none => simp (config := {decide := true}) only at r0 | some false => rfl
+        | some true => simp (config := {decide := true}) only [s0, prob_pure, ite_false, ne_eq, not_true] at ps
       · intro r s pr ps ri; match r with
-        | none => simp only at ri
+        | none => simp (config := {decide := true}) only at ri
         | some r => simp only [prob_pure, ite_one_zero_ne_zero] at ps; simp only [ps, Option.isSome]
       · exact h py.2
     · refine' cond_bind_le_second (λ r ↦ r = some false) (λ r ↦ r.isSome)
         (λ r : Option Bool ↦ ¬r.isSome) v0' _
       intro r pr ri; match r with
-      | some _ => simp only [Option.isSome] at ri
+      | some _ => simp (config := {decide := true}) only [Option.isSome] at ri
       | none =>
           simp only; apply cond_bind_le_of_forall_le v0'
           intro b _; match b with
-          | true => simp only [if_true, bind_const, cond_pure, if_false, v0']
+          | true => simp (config := {decide := true}) only [if_true, bind_const, cond_pure, if_false, v0']
           | false =>
             simp only [if_false]; rw [cond_eq_pr]
             · refine' le_trans _ (bob_complete o VeraId cs v0 py.1)
@@ -374,13 +374,13 @@ lemma evil_bobs_lies (o : Oracle) (eve : Bob) (cs : c < s) (v0 : 0 < v)
   rw [pr_eq_cond_add_cond (λ r : Option Bool ↦ r.isSome)]
   have b1 : (bobs o eve (vera c s v) p y).cond (λ r ↦ extract ((p,y),r) = false) (λ r ↦ ¬r.isSome) = 0 := by
     apply cond_eq_zero; intro r _ ri
-    simp only [Option.not_isSome_iff_eq_none] at ri; simp only [ri, extract, yt]
+    simp only [Option.not_isSome_iff_eq_none] at ri; simp (config := {decide := true}) only [ri, extract, yt]
   simp only [b1, zero_mul, add_zero]
   refine' le_trans (mul_le_of_le_one_right cond_nonneg pr_le_one) _
   refine' le_trans (le_of_eq _) (evil_bobs_lies' o eve cs v0 py)
   apply cond_congr; intro r _ ri; match r with
   | some r => simp only [extract, Option.some_inj]
-  | none => simp only at ri
+  | none => simp (config := {decide := true}) only at ri
 
 /-- Alice wins the debate with good probability -/
 theorem completeness' (o : Oracle) (L : o.lipschitz t k) (eve : Bob)
@@ -436,7 +436,7 @@ def vera_score (v : ℝ) : Option Bool → ℝ
 
 /-- Option Bool's univ-/
 lemma option_bool_univ : (Finset.univ : Finset (Option Bool)) = {some true, some false, none} := by
-  simp only
+  simp (config := {decide := true}) only
 
 /-- If Honest Bob rejects, Vera usually complains.  The error probability is higher if Bob
     does complain, though, so we use an expectation over vera_score. -/
@@ -446,15 +446,15 @@ lemma bobs_safe (o : Oracle) (cs : c < s) (sb : s < b) (q0 : 0 < q) (v0 : 0 < v)
   induction' n with n h
   · simp only [Nat.zero_eq, pow_zero, mul_one, bobs, vera_score, exp_pure, le_refl]
   · simp only [bobs, exp_bind]; specialize h p.tail y.tail
-    simp only [Nat.succ_sub_one, vera_score, @exp_fintype (Option Bool), option_bool_univ, Finset.mem_singleton,
+    simp (config := {decide := true}) only [Nat.succ_sub_one, vera_score, @exp_fintype (Option Bool), option_bool_univ, Finset.mem_singleton,
       Finset.mem_insert, not_false_eq_true, Finset.sum_insert, mul_zero, Finset.sum_singleton, mul_one, zero_add,
       prob_pure, ite_false, zero_mul, add_zero, ite_true, one_mul, prob_bind, ←exp_add] at h ⊢
     generalize hbs : bobs o (bob s b q) (vera c s v) p.tail y.tail = bs
     simp only [hbs] at h
     generalize hbn : (bob s b q n y.tail p.head).prob' o = bn
     trans (bs.prob (some false) + bs.prob none * (1 - v)) * (1 - q)
     · refine le_trans ?_ (mul_le_mul_of_nonneg_right h (by linarith))
-      rw [mul_assoc, ←pow_succ']
+      rw [mul_assoc, ←pow_succ]
     · simp only [add_mul]; apply add_le_add
       · exact mul_le_of_le_one_right (prob_nonneg _) (by linarith)
       · rw [mul_assoc]; refine mul_le_mul_of_nonneg_left ?_ (prob_nonneg _)
@@ -485,20 +485,20 @@ lemma bobs_catches (o : Oracle) (cs : c < s) (sb : s < b) (q0 : 0 < q) (v0 : 0 <
     {p : Vector ℝ n} {y : Vector Bool n} (pb : ¬close p (o.probs y) b) :
     (1 - v) * (1 - q) ^ n ≤ (bobs o (bob s b q) (vera c s v) p y).pr (λ r ↦ r = some false) := by
   induction' n with n h
-  · simp only [Vector.eq_nil, close_nil] at pb
+  · simp (config := {decide := true}) only [Vector.eq_nil, close_nil] at pb
   · by_cases pbn : close p.tail (o.probs y.tail) b
     · have safe := bobs_safe o cs sb q0 v0 v1 qv p.tail y.tail
-      simp only [bobs, Nat.succ_sub_one, pr_bind, @exp_fintype (Option Bool), option_bool_univ,
+      simp (config := {decide := true}) only [bobs, Nat.succ_sub_one, pr_bind, @exp_fintype (Option Bool), option_bool_univ,
         Finset.mem_singleton, Finset.mem_insert, not_false_eq_true, Finset.sum_insert, pr_pure, ite_false,
         mul_zero, ite_true, mul_one, Finset.sum_singleton, zero_add, ge_iff_le, vera_score] at safe ⊢
       generalize hbs : bobs o (bob s b q) (vera c s v) p.tail y.tail = bs; simp only [hbs] at safe
       trans (bs.prob (some false) + bs.prob none * (1 - v)) * (1 - q)
       · refine le_trans ?_ (mul_le_mul_of_nonneg_right safe (by linarith))
-        rw [mul_assoc, ←pow_succ']
+        rw [mul_assoc, ←pow_succ]
       · simp only [add_mul]; apply add_le_add
         · exact mul_le_of_le_one_right (prob_nonneg _) (by linarith)
         · rw [mul_assoc]; refine mul_le_mul_of_nonneg_left ?_ (prob_nonneg _)
-          simp only [close_succ, not_and_or, pbn, Oracle.probs, Vector.tail_cons, Vector.head_cons,
+          simp (config := {decide := true}) only [close_succ, not_and_or, pbn, Oracle.probs, Vector.tail_cons, Vector.head_cons,
             or_false, Nat.succ_sub_one, not_le] at pb
           rw [mul_comm]; refine le_exp_of_cut (fun x ↦ x = false) (1-q) (1-v) ?_ ?_ ?_ (by linarith)
           · have bs := bob_sound o BobId sb q0 (le_of_lt pb)
@@ -512,7 +512,7 @@ lemma bobs_catches (o : Oracle) (cs : c < s) (sb : s < b) (q0 : 0 < q) (v0 : 0 <
           · intro _ _ t; simp only [Bool.not_eq_false] at t; simp only [t, if_true, if_false, exp_const, le_refl]
     · specialize h pbn
       refine le_trans ?_ (le_pr_bind_of_cut _ (1-q) h ?_ (by linarith))
-      · rw [mul_assoc, pow_succ']
+      · rw [mul_assoc, pow_succ]
       · intro _ _ f; simp only [f, pr_pure, if_true]; linarith
 
 /-- Bob wins the debate with probability ≥ 8/15 -/
@@ -531,7 +531,7 @@ theorem soundness' (o : Oracle) (L : o.lipschitz t k) (eve : Alice)
     · simp only at h; simp only [pr]
       have safe := bobs_safe o cs sb q0 v0 v1 qv p y
       generalize hbs : bobs o (bob s b q) (vera c s v) p y = bs; simp only [hbs] at safe
-      simp only [extract, h, @exp_fintype (Option Bool), option_bool_univ, Finset.mem_singleton,
+      simp (config := {decide := true}) only [extract, h, @exp_fintype (Option Bool), option_bool_univ, Finset.mem_singleton,
         Finset.mem_insert, mul_ite, mul_one, mul_zero, not_false_eq_true, Finset.sum_insert, ite_false,
         ite_true, Finset.sum_singleton, zero_add, ge_iff_le, vera_score] at safe ⊢
       exact le_trans safe (add_le_add_left (mul_le_of_le_one_right (prob_nonneg _) (by linarith)) _)

Misc/Finset.lean

@@ -1,7 +1,7 @@
 import Mathlib.Algebra.BigOperators.Order
 import Mathlib.Algebra.BigOperators.Ring
 import Mathlib.Data.Real.Basic
-import Mathlib.Data.Real.ENNReal
+import Mathlib.Data.ENNReal.Basic
 import Mathlib.Topology.Algebra.InfiniteSum.Basic
 import Mathlib.Topology.Instances.ENNReal
 
@@ -47,8 +47,8 @@ lemma Finset.sum_le_sum_of_map {s : Finset α} {t : Finset β} {u : α → ℝ}
   rw [e]; clear e
   refine' le_trans _ (le_add_of_nonneg_right _)
   · rw [Finset.sum_image]
-    · apply Finset.sum_le_sum; intro x m; simp only [mem_filter] at m; exact le _ m.2
-    · intro x m y n; simp only [mem_filter] at m n; apply inj _ _ m.2 n.2
+    · apply Finset.sum_le_sum; intro x m; simp only [mem_filter, s'] at m; exact le _ m.2
+    · intro x m y n; simp only [mem_filter, s'] at m n; apply inj _ _ m.2 n.2
   · apply Finset.sum_nonneg; intro y m; simp only [mem_sdiff, not_exists, not_and] at m; exact v0 _ m.1
 
 /-- `ENNReal.ofReal` commutes with `Finset.sum` for nonnegative maps -/

Misc/If.lean

@@ -13,16 +13,16 @@ lemma ite_le_ite_iff (x y : Prop) {dx : Decidable x} {dy : Decidable y} :
 lemma ite_one_zero_congr (x y : Prop) {dx : Decidable x} {dy : Decidable y} :
     @ite _ x dx (1:ℝ) 0 = @ite _ y dy (1:ℝ) 0 ↔ (x ↔ y) := by
   by_cases h : x
-  repeat { by_cases l : y; repeat simp only [h, l, if_true, if_false, one_ne_zero, zero_ne_one] }
+  repeat { by_cases l : y; repeat simp [h, l] }
 
 lemma ite_one_zero_ne_zero (x : Prop) {dx : Decidable x} : @ite _ x dx (1:ℝ) 0 ≠ 0 ↔ x := by
   by_cases h : x; repeat { simp only [h, if_true, if_false]; norm_num }
 
 lemma ite_and_one_zero (x y : Prop) {d : Decidable (x ∧ y)} :
     @ite _ (x ∧ y) d (1:ℝ) 0 =
       (@ite _ x (Classical.dec _) (1:ℝ) 0) * (@ite _ y (Classical.dec _) 1 0) := by
-  by_cases h : x
-  repeat { by_cases l : y; repeat simp only [h, l, if_true, if_false, one_mul, zero_mul] }
+  rw [ite_zero_mul_ite_zero, one_mul]
+  congr
 
 lemma ite_one_zero_nonneg {x : Prop} {d : Decidable x} : 0 ≤ @ite _ x d (1:ℝ) 0 := by
   split_ifs; repeat norm_num

Prob/Arith.lean

@@ -37,6 +37,7 @@ instance : AddCommMonoid (Prob ℝ) where
   zero_add x := by simp only [add_eq, zero_eq, pure_bind, zero_add, bind_pure]
   add_zero x := by simp only [add_eq, zero_eq, pure_bind, add_zero, bind_pure]
   add_comm x y := by simp only [add_eq]; rw [bind_comm_of_eq]; ext x y; rw [add_comm]
+  nsmul := nsmulRec
 
 /-- • distributes over + -/
 instance : DistribMulAction ℝ (Prob ℝ) where
@@ -96,12 +97,14 @@ lemma le_exp_of_forall_le {f : Prob α} {u : α → ℝ} {b : ℝ} (h : ∀ x, f
 -- Mean is linear
 lemma mean_smul (s : ℝ) (f : Prob ℝ) : (s • f).mean = s * f.mean := by
   simp only [mean, smul_eq, exp_bind, exp_pure, id, exp_const_mul s f (λ x ↦ x)]
+  rfl
 lemma mean_add (f g : Prob ℝ) : (f + g).mean = f.mean + g.mean := by
   simp only [mean, add_eq, exp_bind, exp_pure, id, λ x ↦ exp_add g (λ _ ↦ x) (λ y ↦ y), exp_const, exp_add]
+  rfl
 
 /-- Mean is multiplicative -/
 lemma mean_mul (f g : Prob ℝ) : (f * g).mean = f.mean * g.mean := by
-  simp only [mean, mul_eq, exp_bind, exp_pure, id, ←exp_mul_const]; simp only [←exp_const_mul]
+  simp only [mean, mul_eq, exp_bind, exp_pure, id, ←exp_mul_const]; simp only [←exp_const_mul]; rfl
 
 -- f.pr is between 0 and 1
 lemma pr_nonneg {f : Prob α} {p : α → Prop} : 0 ≤ f.pr p := by
@@ -166,7 +169,7 @@ lemma pr_eq_zero {f : Prob α} {p : α → Prop} : f.pr p = 0 ↔ ∀ x, f.prob
   · intro h; contrapose h; simp only [not_forall] at h ⊢; apply ne_of_gt
     rcases h with ⟨x,px,h⟩; rw [not_not] at h; rw [←pr_false]; apply pr_lt_pr
     · simp only [ne_eq, IsEmpty.forall_iff, implies_true]
-    · simp only [true_and]; use x, px, h
+    · simp only [not_false_iff, true_and]; use x, px, h
   · intro h; rw [←pr_false]; apply pr_congr; simp only [iff_false]; exact h
 
 /-- `pr ≠ 0` if there is some nonzero prob -/
@@ -186,7 +189,7 @@ lemma pr_eq_one {f : Prob α} {p : α → Prop} : f.pr p = 1 ↔ ∀ x, f.prob x
 lemma pr_neg {f : Prob α} {p : α → Prop} : f.pr (λ x ↦ ¬p x) = 1 - f.pr p := by
   rw [eq_sub_iff_add_eq, ←pr_true]; simp only [pr, ←exp_add]; apply exp_congr;
   intro x _; simp only [if_true]; by_cases h : p x
-  repeat simp only [h, if_false, if_true, zero_add, add_zero]
+  repeat simp (config := {decide := true}) only [h, if_false, if_true, zero_add, add_zero]
 lemma pr_neg' {f : Prob α} {p : α → Prop} : f.pr p = 1 - f.pr (λ x ↦ ¬p x) := by
   simp only [pr_neg, sub_sub_cancel]
 
@@ -205,7 +208,7 @@ lemma pr_or_le {f : Prob α} (p q : α → Prop) : f.pr (λ x ↦ p x ∨ q x) 
 lemma pr_eq_add_of_cut {f : Prob α} {p : α → Prop} (q : α → Prop) :
     f.pr p = f.pr (fun x ↦ p x ∧ q x) + f.pr (fun x ↦ p x ∧ ¬q x) := by
   simp only [pr, ←exp_add]; apply exp_congr; intro x _; by_cases px : p x;
-  repeat { by_cases qx : q x; repeat simp only [px, qx, if_true, if_false, add_zero, zero_add] }
+  repeat { by_cases qx : q x; repeat simp (config := {decide := true}) only [px, qx, if_true, if_false, add_zero, zero_add] }
 
 /-- Markov's inequality -/
 lemma markov' (f : Prob α) (g : α → ℝ) (f0 : ∀ x, f.prob x ≠ 0 → 0 ≤ g x) {a : ℝ} (a0 : 0 < a) :

Prob/Basics.lean

@@ -154,7 +154,7 @@ lemma bool_prob_false_of_true {f : Prob Bool} : f.prob false = 1 - f.prob true :
   apply eq_sub_of_add_eq; rw [add_comm]; exact f.bool_total
 lemma bool_prob_true_of_false {f : Prob Bool} : f.prob true = 1 - f.prob false := eq_sub_of_add_eq f.bool_total
 lemma not_bool_prob {f : Prob Bool} {x : Bool} : (not <$> f).prob x = f.prob (not x) := by
-  rw [←Bool.not_not x, map_prob_of_inj, Bool.not_not]; rw [Bool.injective_iff]; simp only
+  rw [←Bool.not_not x, map_prob_of_inj, Bool.not_not]; rw [Bool.injective_iff]; decide
 
 /-- Bound a prob bind in terms of an intermediate event -/
 lemma le_prob_bind_of_cut {f : Prob α} {g : α → Prob β} (x : α) {y : β} :