Update lean-toolchain for leanprover/lean4#10524

Author: leanprover-community-mathlib4-bot

Batteries/Data/Fin/Lemmas.lean

@@ -5,11 +5,26 @@ Authors: Mario Carneiro
 -/
 import Batteries.Data.Fin.Basic
 import Batteries.Util.ProofWanted
+import Batteries.Tactic.Alias
 
 namespace Fin
 
 attribute [norm_cast] val_last
 
+/-! ### foldl/foldr -/
+
+theorem foldl_assoc {op : α → α → α} [ha : Std.Associative op] {f : Fin n → α} {a₁ a₂} :
+    foldl n (fun x i => op x (f i)) (op a₁ a₂) = op a₁ (foldl n (fun x i => op x (f i)) a₂) := by
+  induction n generalizing a₂ with
+  | zero => rfl
+  | succ n ih => simp only [foldl_succ, ha.assoc, ih]
+
+theorem foldr_assoc {op : α → α → α} [ha : Std.Associative op] {f : Fin n → α} {a₁ a₂} :
+    foldr n (fun i x => op (f i) x) (op a₁ a₂) = op (foldr n (fun i x => op (f i) x) a₁) a₂ := by
+  induction n generalizing a₂ with
+  | zero => rfl
+  | succ n ih => simp only [foldr_succ, ha.assoc, ih]
+
 /-! ### clamp -/
 
 @[simp] theorem coe_clamp (n m : Nat) : (clamp n m : Nat) = min n m := rfl
@@ -21,14 +36,9 @@ attribute [norm_cast] val_last
 @[simp] theorem findSome?_one {f : Fin 1 → Option α} : findSome? f = f 0 := rfl
 
 theorem findSome?_succ {f : Fin (n+1) → Option α} :
-    findSome? f = (f 0 <|> findSome? fun i => f i.succ) := by
-  simp only [findSome?, foldl_succ]
-  cases f 0
-  · rw [Option.orElse_eq_orElse, Option.orElse_none, Option.orElse_none]
-  · simp only [Option.orElse_some, Option.orElse_eq_orElse, Option.orElse_none]
-    induction n with
-    | zero => rfl
-    | succ n ih => rw [foldl_succ, Option.orElse_some, ih (f := fun i => f i.succ)]
+    findSome? f = (f 0).or (findSome? fun i => f i.succ) := by
+  simp only [findSome?, foldl_succ, Option.orElse_eq_orElse, Option.orElse_eq_or]
+  exact Eq.trans (by cases (f 0) <;> rfl) foldl_assoc
 
 theorem findSome?_succ_of_some {f : Fin (n+1) → Option α} (h : f 0 = some x) :
     findSome? f = some x := by simp [findSome?_succ, h]
@@ -42,68 +52,67 @@ theorem findSome?_succ_of_none {f : Fin (n+1) → Option α} (h : f 0 = none) :
 theorem findSome?_succ_of_isNone {f : Fin (n+1) → Option α} (h : (f 0).isNone) :
     findSome? f = findSome? fun i => f i.succ := by simp_all [findSome?_succ_of_none]
 
-theorem exists_of_findSome?_eq_some {f : Fin n → Option α} (h : findSome? f = some x) :
-    ∃ i, f i = some x := by
+@[simp, grind =]
+theorem findSome?_eq_some_iff {f : Fin n → Option α} :
+    findSome? f = some a ↔ ∃ i, f i = some a ∧ ∀ j < i, f j = none := by
   induction n with
-  | zero => rw [findSome?_zero] at h; contradiction
+  | zero =>
+    simp only [findSome?_zero, (Option.some_ne_none _).symm, false_iff]
+    exact fun  ⟨i, _⟩ => i.elim0
   | succ n ih =>
-    rw [findSome?_succ] at h
-    match heq : f 0 with
-    | some x =>
-      rw [heq, Option.orElse_eq_orElse, Option.orElse_some] at h
-      exists 0
-      rw [heq, h]
-    | none =>
-      rw [heq, Option.orElse_eq_orElse, Option.orElse_none] at h
-      match ih h with | ⟨i, _⟩ => exists i.succ
+    simp only [findSome?_succ, Option.or_eq_some_iff, Fin.exists_fin_succ, Fin.forall_fin_succ,
+      not_lt_zero, false_implies, implies_true, and_true, succ_lt_succ_iff, succ_pos,
+      forall_const, ih, and_left_comm (b := f 0 = none), exists_and_left]
 
-theorem eq_none_of_findSome?_eq_none {f : Fin n → Option α} (h : findSome? f = none) (i) :
-    f i = none := by
+@[simp, grind =] theorem findSome?_eq_none_iff {f : Fin n → Option α} :
+    findSome? f = none ↔ ∀ i, f i = none := by
   induction n with
-  | zero => cases i; contradiction
+  | zero =>
+    simp only [findSome?_zero, true_iff]
+    exact fun i => i.elim0
   | succ n ih =>
-    rw [findSome?_succ] at h
-    match heq : f 0 with
-    | some x =>
-      rw [heq, Option.orElse_eq_orElse, Option.orElse_some] at h
-      contradiction
-    | none =>
-      rw [heq, Option.orElse_eq_orElse, Option.orElse_none] at h
-      cases i using Fin.cases with
-      | zero => exact heq
-      | succ i => exact ih h i
-
-@[simp] theorem findSome?_isSome_iff {f : Fin n → Option α} :
-    (findSome? f).isSome ↔ ∃ i, (f i).isSome := by
-  simp only [Option.isSome_iff_exists]
-  constructor
-  · intro ⟨x, hx⟩
-    match exists_of_findSome?_eq_some hx with
-    | ⟨i, hi⟩ => exists i, x
-  · intro ⟨i, x, hix⟩
-    match h : findSome? f with
-    | some x => exists x
-    | none => rw [eq_none_of_findSome?_eq_none h i] at hix; contradiction
-
-@[simp] theorem findSome?_eq_none_iff {f : Fin n → Option α} :
-    findSome? f = none ↔ ∀ i, f i = none := by
-  constructor
-  · exact eq_none_of_findSome?_eq_none
-  · intro hf
-    match h : findSome? f with
-    | none => rfl
-    | some x =>
-      match exists_of_findSome?_eq_some h with
-      | ⟨i, h⟩ => rw [hf] at h; contradiction
-
-theorem findSome?_isNone_iff {f : Fin n → Option α} :
+    simp only [findSome?_succ, Option.or_eq_none_iff, ih, forall_fin_succ]
+
+theorem isNone_findSome?_iff {f : Fin n → Option α} :
     (findSome? f).isNone ↔ ∀ i, (f i).isNone := by simp
 
+@[deprecated (since := "2025-09-28")]
+alias findSome?_isNone_iff := isNone_findSome?_iff
+
+@[simp] theorem isSome_findSome?_iff {f : Fin n → Option α} :
+    (findSome? f).isSome ↔ ∃ i, (f i).isSome := by
+  cases h : findSome? f with (simp only [findSome?_eq_none_iff, findSome?_eq_some_iff] at h; grind)
+
+@[deprecated (since := "2025-09-28")]
+alias findSome?_isSome_iff := isSome_findSome?_iff
+
+theorem exists_minimal_of_findSome?_eq_some {f : Fin n → Option α}
+    (h : findSome? f = some x) : ∃ i, f i = some x ∧ ∀ j < i, f j = none :=
+  findSome?_eq_some_iff.1 h
+
+theorem exists_eq_some_of_findSome?_eq_some {f : Fin n → Option α}
+    (h : findSome? f = some x) : ∃ i, f i = some x := by grind
+
+@[deprecated (since := "2025-09-28")]
+alias exists_of_findSome?_eq_some := exists_eq_some_of_findSome?_eq_some
+
+theorem eq_none_of_findSome?_eq_none {f : Fin n → Option α} (h : findSome? f = none) (i) :
+    f i = none := findSome?_eq_none_iff.1 h i
+
+theorem exists_isSome_of_isSome_findSome? {f : Fin n → Option α} (h : (findSome? f).isSome) :
+    ∃ i, (f i).isSome := isSome_findSome?_iff.1 h
+
+theorem isNone_of_isNone_findSome? {f : Fin n → Option α} (h : (findSome? f).isNone) :
+    (f i).isNone := isNone_findSome?_iff.1 h i
+
+theorem isSome_findSome?_of_isSome {f : Fin n → Option α} (h : (f i).isSome) :
+    (findSome? f).isSome := isSome_findSome?_iff.2 ⟨_, h⟩
+
 theorem map_findSome? (f : Fin n → Option α) (g : α → β) :
-    (findSome? f).map g = findSome? (Option.map g ∘ f) := by
+    (findSome? f).map g = findSome? (Option.map g <| f ·) := by
   induction n with
   | zero => rfl
-  | succ n ih => simp [findSome?_succ, Function.comp_def, Option.map_or, ih]
+  | succ n ih => simp [findSome?_succ, Option.map_or, ih]
 
 theorem findSome?_guard {p : Fin n → Bool} : findSome? (Option.guard p) = find? p := rfl
 
@@ -123,38 +132,62 @@ theorem findSome?_eq_findSome?_finRange (f : Fin n → Option α) :
 
 theorem find?_succ {p : Fin (n+1) → Bool} :
     find? p = if p 0 then some 0 else (find? fun i => p i.succ).map Fin.succ := by
-  simp only [find?, findSome?_succ, Option.guard]
-  split <;> simp [map_findSome?, Function.comp_def, Option.guard]
+  simp only [find?, findSome?_succ, Option.guard, fun a => apply_ite (Option.or · a),
+    Option.some_or, Option.none_or, map_findSome?, Option.map_if]
 
-theorem eq_true_of_find?_eq_some {p : Fin n → Bool} (h : find? p = some i) : p i = true := by
-  match exists_of_findSome?_eq_some h with
-  | ⟨i, hi⟩ =>
-    simp only [Option.guard] at hi
-    split at hi
-    · cases hi; assumption
-    · contradiction
+@[simp, grind =]
+theorem find?_eq_some_iff {p : Fin n → Bool} :
+    find? p = some i ↔ p i ∧ ∀ j, j < i → p j = false := by simp [find?, and_assoc]
 
-theorem eq_false_of_find?_eq_none {p : Fin n → Bool} (h : find? p = none) (i) : p i = false := by
-  have hi := eq_none_of_findSome?_eq_none h i
-  simp only [Option.guard] at hi
-  split at hi
-  · contradiction
-  · simp [*]
+theorem isSome_find?_iff {p : Fin n → Bool} :
+    (find? p).isSome ↔ ∃ i, p i := by simp [find?]
 
-theorem find?_isSome_iff {p : Fin n → Bool} : (find? p).isSome ↔ ∃ i, p i := by
-  simp [find?]
+@[deprecated (since := "2025-09-28")]
+alias find?_isSome_iff := isSome_find?_iff
 
-theorem find?_isNone_iff {p : Fin n → Bool} : (find? p).isNone ↔ ∀ i, ¬ p i := by
-  simp [find?]
+@[simp, grind =]
+theorem find?_eq_none_iff {p : Fin n → Bool} : find? p = none ↔ ∀ i, p i = false := by simp [find?]
 
-proof_wanted find?_eq_some_iff {p : Fin n → Bool} : find? p = some i ↔ p i ∧ ∀ j, j < i → ¬ p j
+theorem isNone_find?_iff {p : Fin n → Bool} : (find? p).isNone ↔ ∀ i, p i = false := by simp [find?]
 
-theorem find?_eq_none_iff {p : Fin n → Bool} : find? p = none ↔ ∀ i, ¬ p i := by
-  rw [← find?_isNone_iff, Option.isNone_iff_eq_none]
+@[deprecated (since := "2025-09-28")]
+alias find?_isNone_iff := isNone_find?_iff
 
-theorem find?_eq_find?_finRange {p : Fin n → Bool} : find? p = (List.finRange n).find? p := by
-  induction n with
-  | zero => rfl
-  | succ n ih =>
-    rw [find?_succ, List.finRange_succ, List.find?_cons]
-    split <;> simp [Function.comp_def, *]
+theorem eq_true_of_find?_eq_some {p : Fin n → Bool} (h : find? p = some i) : p i :=
+    (find?_eq_some_iff.mp h).1
+
+theorem eq_false_of_find?_eq_some_of_lt {p : Fin n → Bool} (h : find? p = some i) :
+    ∀ j < i, p j = false := (find?_eq_some_iff.mp h).2
+
+theorem eq_false_of_find?_eq_none {p : Fin n → Bool} (h : find? p = none) (i) :
+    p i = false := find?_eq_none_iff.1 h i
+
+theorem exists_eq_true_of_isSome_find? {p : Fin n → Bool} (h : (find? p).isSome) :
+    ∃ i, p i := isSome_find?_iff.1 h
+
+theorem eq_false_of_isNone_find? {p : Fin n → Bool}  (h : (find? p).isNone) : p i = false :=
+  isNone_find?_iff.1 h i
+
+theorem isSome_find?_of_eq_true {p : Fin n → Bool}  (h : p i) :
+    (find? p).isSome := isSome_find?_iff.2 ⟨_, h⟩
+
+theorem get_find?_eq_true {p : Fin n → Bool} (h : (find? p).isSome) : p ((find? p).get h) :=
+  eq_true_of_find?_eq_some (Option.some_get _).symm
+
+theorem get_find?_minimal {p : Fin n → Bool}  (h : (find? p).isSome) :
+    ∀ j, j < (find? p).get h → p j = false :=
+  eq_false_of_find?_eq_some_of_lt (Option.some_get _).symm
+
+theorem find?_eq_find?_finRange {p : Fin n → Bool} : find? p = (List.finRange n).find? p :=
+  (findSome?_eq_findSome?_finRange _).trans (List.findSome?_guard)
+
+/-! ### exists -/
+
+theorem exists_eq_true_iff_exists_minimal_eq_true (p : Fin n → Bool):
+    (∃ i, p i) ↔ ∃ i, p i ∧ ∀ j < i, p j = false := by
+  cases h : find? p <;> grind
+
+theorem exists_iff_exists_minimal (p : Fin n → Prop) [DecidablePred p] :
+    (∃ i, p i) ↔ ∃ i, p i ∧ ∀ j < i, ¬ p j := by
+  simpa only [decide_eq_true_iff, decide_eq_false_iff_not] using
+    exists_eq_true_iff_exists_minimal_eq_true (p ·)

Batteries/Data/List/Basic.lean

@@ -555,29 +555,55 @@ pwFilter (·<·) [0, 1, 5, 2, 6, 3, 4] = [0, 1, 2, 3, 4]
 def pwFilter (R : α → α → Prop) [DecidableRel R] (l : List α) : List α :=
   l.foldr (fun x IH => if ∀ y ∈ IH, R x y then x :: IH else IH) []
 
-section Chain
+/-- `IsChain R l` means that `R` holds between adjacent elements of `l`.
+```
+IsChain R [a, b, c, d] ↔ R a b ∧ R b c ∧ R c d
+``` -/
+inductive IsChain (R : α → α → Prop) : List α → Prop where
+  /-- A list of length 0 is a chain. -/
+  | nil : IsChain R []
+  /-- A list of length 1 is a chain. -/
+  | singleton (a : α) : IsChain R [a]
+  /-- If `a` relates to `b` and `b::l` is a chain, then `a :: b :: l` is also a chain. -/
+  | cons_cons (hr : R a b) (h : IsChain R (b :: l)) : IsChain R (a :: b :: l)
+
+attribute [simp, grind ←] IsChain.nil
+attribute [simp, grind ←] IsChain.singleton
+
+@[simp, grind =] theorem isChain_cons_cons : IsChain R (a :: b :: l) ↔ R a b ∧ IsChain R (b :: l) :=
+  ⟨fun | .cons_cons hr h => ⟨hr, h⟩, fun ⟨hr, h⟩ => .cons_cons hr h⟩
 
-variable (R : α → α → Prop)
+instance instDecidableIsChain {R : α → α → Prop} [h : DecidableRel R] (l : List α) :
+    Decidable (l.IsChain R) := match l with | [] => isTrue .nil | a :: l => go a l
+  where
+    go (a : α) (l : List α) : Decidable ((a :: l).IsChain R) :=
+      match l with
+      | [] => isTrue <| .singleton a
+      | b :: l => haveI := (go b l); decidable_of_iff' _ isChain_cons_cons
 
 /-- `Chain R a l` means that `R` holds between adjacent elements of `a::l`.
 ```
 Chain R a [b, c, d] ↔ R a b ∧ R b c ∧ R c d
 ``` -/
-inductive Chain : α → List α → Prop
-  /-- A chain of length 1 is trivially a chain. -/
-  | nil {a : α} : Chain a []
-  /-- If `a` relates to `b` and `b::l` is a chain, then `a :: b :: l` is also a chain. -/
-  | cons : ∀ {a b : α} {l : List α}, R a b → Chain b l → Chain a (b :: l)
+@[deprecated IsChain (since := "2025-09-19")]
+def Chain : (α → α → Prop) → α → List α → Prop := (IsChain · <| · :: ·)
+
+set_option linter.deprecated false in
+/-- A list of length 1 is a chain. -/
+@[deprecated IsChain.singleton (since := "2025-09-19")]
+theorem Chain.nil {a : α} : Chain R a [] := IsChain.singleton a
+
+set_option linter.deprecated false in
+/-- If `a` relates to `b` and `b::l` is a chain, then `a :: b :: l` is also a chain. -/
+@[deprecated IsChain.cons_cons (since := "2025-09-19")]
+theorem Chain.cons : R a b → Chain R b l → Chain R a (b :: l)  := IsChain.cons_cons
 
 /-- `Chain' R l` means that `R` holds between adjacent elements of `l`.
 ```
 Chain' R [a, b, c, d] ↔ R a b ∧ R b c ∧ R c d
 ``` -/
-def Chain' : List α → Prop
-  | [] => True
-  | a :: l => Chain R a l
-
-end Chain
+@[deprecated IsChain (since := "2025-09-19")]
+def Chain' : (α → α → Prop) → List α → Prop := (IsChain · ·)
 
 /-- `eraseDup l` removes duplicates from `l` (taking only the first occurrence).
 Defined as `pwFilter (≠)`.