Update lean-toolchain for leanprover/lean4#11416

Author: leanprover-community-mathlib4-bot

Batteries/Data/Char/Basic.lean

@@ -6,6 +6,7 @@ Authors: Jannis Limperg, François G. Dorais
 module
 
 public import Batteries.Classes.Order
+public import Batteries.Data.List.Lemmas
 
 @[expose] public section
 

Batteries/Data/Fin/Basic.lean

@@ -88,6 +88,18 @@ This is the dependent version of `Fin.foldl`. -/
     (f : ∀ (i : Fin n), α i.castSucc → α i.succ) (init : α 0) : α (last n) :=
   dfoldlM (m := Id) n α f init
 
+/-- Sum of a tuple indexed by `Fin n`. -/
+@[inline] protected def sum [Zero α] [Add α] (x : Fin n → α) : α :=
+  foldr n (x · + ·) 0
+
+/-- Product of a tuple indexed by `Fin n`. -/
+@[inline] protected def prod [One α] [Mul α] (x : Fin n → α) : α :=
+  foldr n (x · * ·) 1
+
+/-- Count the number of true values of a decidable predicate on `Fin n`. -/
+@[inline] protected def countP (p : Fin n → Bool) : Nat :=
+  Fin.sum (p · |>.toNat)
+
 /--
 `findSome? f` returns `f i` for the first `i` for which `f i` is `some _`, or `none` if no such
 element is found. The function `f` is not evaluated on further inputs after the first `i` is found.

Batteries/Data/Fin/Lemmas.lean

@@ -7,6 +7,7 @@ module
 
 public import Batteries.Data.Fin.Basic
 public import Batteries.Data.Nat.Lemmas
+public import Batteries.Data.List.Basic
 public import Batteries.Util.ProofWanted
 public import Batteries.Tactic.Alias
 
@@ -39,6 +40,67 @@ theorem foldr_assoc {op : α → α → α} [ha : Std.Associative op] {f : Fin n
 
 @[simp] theorem coe_clamp (n m : Nat) : (clamp n m : Nat) = min n m := rfl
 
+/-! ### sum -/
+
+@[simp, grind =]
+theorem sum_zero [Zero α] [Add α] (x : Fin 0 → α) :
+    Fin.sum x = 0 := by
+  simp [Fin.sum]
+
+theorem sum_succ [Zero α] [Add α] (x : Fin (n + 1) → α) :
+    Fin.sum x = x 0 + Fin.sum (x ·.succ) := by
+  simp [Fin.sum, foldr_succ]
+
+@[simp, grind =]
+theorem sum_eq_sum_map_finRange [Zero α] [Add α] (x : Fin n → α) :
+    Fin.sum x = (List.finRange n |>.map x).sum := by
+  simp only [Fin.sum, foldr_eq_finRange_foldr, List.sum, List.foldr_map]
+
+/-! ### prod -/
+
+@[simp, grind =]
+theorem prod_zero [One α] [Mul α] (x : Fin 0 → α) :
+    Fin.prod x = 1 := by
+  simp [Fin.prod]
+
+theorem prod_succ [One α] [Mul α] (x : Fin (n + 1) → α) :
+    Fin.prod x = x 0 * Fin.prod (x ·.succ) := by
+  simp [Fin.prod, foldr_succ]
+
+@[simp, grind =]
+theorem prod_eq_prod_map_finRange [One α] [Mul α] (x : Fin n → α) :
+    Fin.prod x = (List.finRange n |>.map x).prod := by
+  simp only [Fin.prod, foldr_eq_finRange_foldr, List.prod, List.foldr_map]
+
+/-! ### countP -/
+
+@[simp, grind =] theorem countP_zero (p : Fin 0 → Bool) : Fin.countP p = 0 := by
+  simp [Fin.countP]
+
+@[simp, grind =] theorem countP_one (p : Fin 1 → Bool) : Fin.countP p = (p 0).toNat := by
+  simp [Fin.countP, List.finRange_succ]
+
+theorem countP_succ (p : Fin (n + 1) → Bool) :
+    Fin.countP p = (p 0).toNat + Fin.countP (p ·.succ) := by
+  simp [Fin.countP, List.finRange_succ]; rfl
+
+@[simp, grind =]
+theorem countP_eq_countP_map_finRange (x : Fin n → Bool) :
+    Fin.countP x = (List.finRange n).countP x := by
+  induction n with
+  | zero => rfl
+  | succ n ih => simp +arith [countP_succ, List.finRange_succ, List.countP_cons, List.countP_map,
+      Bool.cond_eq_ite, Bool.toNat, ih]; rfl
+
+@[grind .]
+theorem countP_le (p : Fin n → Bool) : Fin.countP p ≤ n := by
+  induction n with simp only [countP_zero, countP_succ, Nat.le_refl]
+  | succ _ ih =>
+    rw [Nat.add_comm]
+    apply Nat.add_le_add
+    · exact ih ..
+    · exact Bool.toNat_le ..
+
 /-! ### findSome? -/
 
 @[simp] theorem findSome?_zero {f : Fin 0 → Option α} : findSome? f = none := by simp [findSome?]

Batteries/Data/List/Lemmas.lean

@@ -926,6 +926,41 @@ theorem append_eq_of_isPrefixOf?_eq_some [BEq α] [LawfulBEq α] {xs ys zs : Lis
 theorem append_eq_of_isSuffixOf?_eq_some [BEq α] [LawfulBEq α] {xs ys zs : List α}
     (h : xs.isSuffixOf? ys = some zs) : zs ++ xs = ys := by simp_all
 
+/-! ### finRange -/
+
+theorem get_finRange (i : Fin (finRange n).length) :
+    (finRange n).get i = Fin.cast length_finRange i := by simp
+
+@[simp, grind =]
+theorem finRange_eq_nil_iff : finRange n = [] ↔ n = 0 := by
+  simp [eq_nil_iff_length_eq_zero]
+
+theorem finRange_eq_pmap_range : finRange n = (range n).pmap Fin.mk (by simp) := by
+  apply List.ext_getElem <;> simp [finRange]
+
+theorem nodup_finRange (n) : (finRange n).Nodup := by
+  rw [finRange_eq_pmap_range]
+  exact (Pairwise.pmap nodup_range _) fun _ _ _ _ => @Fin.ne_of_val_ne _ ⟨_, _⟩ ⟨_, _⟩
+
+theorem pairwise_lt_finRange (n) : Pairwise (· < ·) (finRange n) := by
+  rw [finRange_eq_pmap_range]
+  exact List.pairwise_lt_range.pmap (by simp) (by simp)
+
+theorem pairwise_le_finRange (n) : Pairwise (· ≤ ·) (finRange n) := by
+  rw [finRange_eq_pmap_range]
+  exact List.pairwise_le_range.pmap (by simp) (by simp)
+
+@[simp]
+theorem map_get_finRange (l : List α) : (finRange l.length).map l.get = l := by
+  apply ext_getElem <;> simp
+
+@[simp]
+theorem map_getElem_finRange (l : List α) : (finRange l.length).map (l[·.1]) = l := by
+  apply ext_getElem <;> simp
+
+@[simp]
+theorem map_coe_finRange_eq_range : (finRange n).map (↑·) = List.range n := by
+  apply List.ext_getElem <;> simp
 /-! ### sum/prod -/
 
 private theorem foldr_eq_foldl_aux (f : α → α → α) (init : α) [Std.Associative f]

Batteries/Tactic/Init.lean

@@ -31,23 +31,31 @@ elab (name := exacts) "exacts " "[" hs:term,* "]" : tactic => do
     evalTactic (← `(tactic| exact $stx))
   evalTactic (← `(tactic| done))
 
+/--
+`by_contra_core` is the component of `by_contra` that turns the goal into the form `p → False`.
+`by_contra h` is defined as `by_contra_core` followed by `rintro h`.
+* If the goal is a negation `¬q`, the goal becomes `q → False`.
+* If the goal has a `Decidable` instance, it uses `Decidable.byContradiction` instead of
+  `Classical.byContradiction`.
+-/
+scoped macro "by_contra_core" : tactic => `(tactic| first
+  | guard_target = Not _; change _ → False
+  | refine @Decidable.byContradiction _ _ ?_
+  | refine @Classical.byContradiction _ ?_)
+
 /--
 `by_contra h` proves `⊢ p` by contradiction,
 introducing a hypothesis `h : ¬p` and proving `False`.
 * If `p` is a negation `¬q`, `h : q` will be introduced instead of `¬¬q`.
 * If `p` is decidable, it uses `Decidable.byContradiction` instead of `Classical.byContradiction`.
-* If `h` is omitted, the introduced variable `_: ¬p` will be anonymous.
+* If `h` is omitted, the introduced variable will be called `this`.
 -/
-macro (name := byContra) tk:"by_contra" e?:(ppSpace colGt binderIdent)? : tactic => do
-  let e := match e? with
-    | some e => match e with
-      | `(binderIdent| $e:ident) => e
-      | e => Unhygienic.run `(_%$e) -- HACK: hover fails without Unhygienic here
-    | none => Unhygienic.run `(_%$tk)
-  `(tactic| first
-    | guard_target = Not _; intro $e:term
-    | refine @Decidable.byContradiction _ _ fun $e => ?_
-    | refine @Classical.byContradiction _ fun $e => ?_)
+syntax (name := byContra) "by_contra" (ppSpace colGt rcasesPatMed)? (" : " term)? : tactic
+
+macro_rules
+| `(tactic| by_contra $[$pat?]? $[: $ty?]?) => do
+  let pat ← pat?.getDM `(rcasesPatMed| $(mkIdent `this):ident)
+  `(tactic| (by_contra_core; rintro ($pat:rcasesPatMed) $[: $ty?]?))
 
 /--
 Given a proof `h` of `p`, `absurd h` changes the goal to `⊢ ¬ p`.

Batteries/Tactic/Lint/Simp.lean

@@ -102,8 +102,10 @@ def formatLemmas (usedSimps : Simp.UsedSimps) (simpName : String) (higherOrder :
 @[env_linter] def simpNF : Linter where
   noErrorsFound := "All left-hand sides of simp lemmas are in simp-normal form."
   errorsFound := "SOME SIMP LEMMAS ARE NOT IN SIMP-NORMAL FORM.
-see note [simp-normal form] for tips how to debug this.
-https://leanprover-community.github.io/mathlib_docs/notes.html#simp-normal%20form"
+Please change the lemma to make sure their left-hand sides are in simp normal form.
+To learn about simp normal forms, see
+https://leanprover-community.github.io/extras/simp.html#simp-normal-form
+and https://lean-lang.org/doc/reference/latest/The-Simplifier/Simp-Normal-Forms/."
   test := fun declName => do
     unless ← isSimpTheorem declName do return none
     withConfig Elab.Term.setElabConfig do

BatteriesTest/by_contra.lean

@@ -21,12 +21,12 @@ example (P : Prop) [Decidable P] : nonDecid P = decid P := by
 
 example (P : Prop) : P → P := by
   by_contra
-  guard_hyp ‹_› : ¬(P → P)
+  guard_hyp this : ¬(P → P)
   exact ‹¬(P → P)› id
 
 example (P : Prop) : {_ : P} → P := by
   by_contra
-  guard_hyp ‹_› : ¬(P → P)
+  guard_hyp this : ¬(P → P)
   exact ‹¬(P → P)› id
 
 /-!
@@ -42,11 +42,44 @@ case left
 ---
 error: unsolved goals
 case right
-x✝ : ¬True
+this : ¬True
 ⊢ False
 -/
 #guard_msgs in
 example : True ∧ True := by
   constructor
   · skip
   · by_contra
+
+example (n : Nat) (h : n ≠ 0) : n ≠ 0 := by
+  by_contra rfl
+  simp only [Ne, not_true_eq_false] at h
+
+example (p q : Prop) (hnp : ¬ p) : ¬ (p ∧ q) := by
+  by_contra ⟨hp, _⟩
+  exact hnp hp
+
+example (p q : Prop) (hnp : ¬ p) (hnq : ¬ q) : ¬ (p ∨ q) := by
+  by_contra hp | hq
+  · exact hnp hp
+  · exact hnq hq
+
+/--
+error: unsolved goals
+n : Nat
+this : n ≠ 0
+⊢ False
+-/
+#guard_msgs in
+example (n : Nat) : n = 0 := by
+  by_contra : n ≠ 0
+
+/--
+error: unsolved goals
+n : Nat
+h_ne : n ≠ 0
+⊢ False
+-/
+#guard_msgs in
+example (n : Nat) : n = 0 := by
+  by_contra h_ne : n ≠ 0

BatteriesTest/print_prefix.lean

@@ -5,8 +5,8 @@ inductive TEmpty : Type
 info: TEmpty : Type
 TEmpty.casesOn.{u} (motive : TEmpty → Sort u) (t : TEmpty) : motive t
 TEmpty.ctorIdx : TEmpty → Nat
-TEmpty.noConfusion.{u} {P : Sort u} {x1 x2 : TEmpty} (h12 : x1 = x2) : TEmpty.noConfusionType P x1 x2
-TEmpty.noConfusionType.{u} (P : Sort u) (x1 x2 : TEmpty) : Sort u
+TEmpty.noConfusion.{u} {P : Sort u} {t t' : TEmpty} (eq : t = t') : TEmpty.noConfusionType P t t'
+TEmpty.noConfusionType.{u} (P : Sort u) (t t' : TEmpty) : Sort u
 TEmpty.rec.{u} (motive : TEmpty → Sort u) (t : TEmpty) : motive t
 TEmpty.recOn.{u} (motive : TEmpty → Sort u) (t : TEmpty) : motive t
 -/
@@ -58,11 +58,11 @@ TestStruct.mk.inj {foo bar foo✝ bar✝ : Int} :
   { foo := foo, bar := bar } = { foo := foo✝, bar := bar✝ } → foo = foo✝ ∧ bar = bar✝
 TestStruct.mk.injEq (foo bar foo✝ bar✝ : Int) :
   ({ foo := foo, bar := bar } = { foo := foo✝, bar := bar✝ }) = (foo = foo✝ ∧ bar = bar✝)
-TestStruct.mk.noConfusion.{u} (P : Sort u) (foo bar foo' bar' : Int)
-  (h : { foo := foo, bar := bar } = { foo := foo', bar := bar' }) (k : foo = foo' → bar = bar' → P) : P
+TestStruct.mk.noConfusion.{u} {P : Sort u} {foo bar foo' bar' : Int}
+  (eq : { foo := foo, bar := bar } = { foo := foo', bar := bar' }) (k : foo = foo' → bar = bar' → P) : P
 TestStruct.mk.sizeOf_spec (foo bar : Int) : sizeOf { foo := foo, bar := bar } = 1 + sizeOf foo + sizeOf bar
-TestStruct.noConfusion.{u} {P : Sort u} {x1 x2 : TestStruct} (h12 : x1 = x2) : TestStruct.noConfusionType P x1 x2
-TestStruct.noConfusionType.{u} (P : Sort u) (x1 x2 : TestStruct) : Sort u
+TestStruct.noConfusion.{u} {P : Sort u} {t t' : TestStruct} (eq : t = t') : TestStruct.noConfusionType P t t'
+TestStruct.noConfusionType.{u} (P : Sort u) (t t' : TestStruct) : Sort u
 TestStruct.rec.{u} {motive : TestStruct → Sort u} (mk : (foo bar : Int) → motive { foo := foo, bar := bar })
   (t : TestStruct) : motive t
 TestStruct.recOn.{u} {motive : TestStruct → Sort u} (t : TestStruct)
@@ -79,10 +79,10 @@ TestStruct.casesOn.{u} {motive : TestStruct → Sort u} (t : TestStruct)
 TestStruct.ctorIdx : TestStruct → Nat
 TestStruct.foo (self : TestStruct) : Int
 TestStruct.mk (foo bar : Int) : TestStruct
-TestStruct.mk.noConfusion.{u} (P : Sort u) (foo bar foo' bar' : Int)
-  (h : { foo := foo, bar := bar } = { foo := foo', bar := bar' }) (k : foo = foo' → bar = bar' → P) : P
-TestStruct.noConfusion.{u} {P : Sort u} {x1 x2 : TestStruct} (h12 : x1 = x2) : TestStruct.noConfusionType P x1 x2
-TestStruct.noConfusionType.{u} (P : Sort u) (x1 x2 : TestStruct) : Sort u
+TestStruct.mk.noConfusion.{u} {P : Sort u} {foo bar foo' bar' : Int}
+  (eq : { foo := foo, bar := bar } = { foo := foo', bar := bar' }) (k : foo = foo' → bar = bar' → P) : P
+TestStruct.noConfusion.{u} {P : Sort u} {t t' : TestStruct} (eq : t = t') : TestStruct.noConfusionType P t t'
+TestStruct.noConfusionType.{u} (P : Sort u) (t t' : TestStruct) : Sort u
 TestStruct.rec.{u} {motive : TestStruct → Sort u} (mk : (foo bar : Int) → motive { foo := foo, bar := bar })
   (t : TestStruct) : motive t
 TestStruct.recOn.{u} {motive : TestStruct → Sort u} (t : TestStruct)

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4-pr-releases:pr-release-11416-8580d0e
+leanprover/lean4-pr-releases:pr-release-11416-22e91fa