chore: adaptations for nightly-2024-10-30 (#18435)

Co-authored-by: leanprover-community-mathlib4-bot <[email protected]>

Mathlib.lean

@@ -2404,7 +2404,6 @@ import Mathlib.Data.List.Enum
 import Mathlib.Data.List.FinRange
 import Mathlib.Data.List.Forall2
 import Mathlib.Data.List.GetD
-import Mathlib.Data.List.GroupBy
 import Mathlib.Data.List.Indexes
 import Mathlib.Data.List.Infix
 import Mathlib.Data.List.InsertIdx
@@ -2436,6 +2435,7 @@ import Mathlib.Data.List.Rotate
 import Mathlib.Data.List.Sections
 import Mathlib.Data.List.Sigma
 import Mathlib.Data.List.Sort
+import Mathlib.Data.List.SplitBy
 import Mathlib.Data.List.Sublists
 import Mathlib.Data.List.Sym
 import Mathlib.Data.List.TFAE

Mathlib/Data/List/SplitBy.lean

@@ -0,0 +1,151 @@
+/-
+Copyright (c) 2024 Violeta Hernández Palacios. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Violeta Hernández Palacios
+-/
+import Mathlib.Data.List.Chain
+
+/-!
+# Split a list into contiguous runs of elements which pairwise satisfy a relation.
+
+This file provides the basic API for `List.splitBy` which is defined in Core.
+The main results are the following:
+
+- `List.join_splitBy`: the lists in `List.splitBy` join to the original list.
+- `List.nil_not_mem_splitBy`: the empty list is not contained in `List.splitBy`.
+- `List.chain'_of_mem_splitBy`: any two adjacent elements in a list in `List.splitBy` are related by
+  the specified relation.
+- `List.chain'_getLast_head_splitBy`: the last element of each list in `List.splitBy` is not
+  related to the first element of the next list.
+-/
+
+namespace List
+
+variable {α : Type*} {m : List α}
+
+@[simp]
+theorem splitBy_nil (r : α → α → Bool) : splitBy r [] = [] :=
+  rfl
+
+private theorem splitByLoop_eq_append {r : α → α → Bool} {l : List α} {a : α} {g : List α}
+    (gs : List (List α)) : splitBy.loop r l a g gs = gs.reverse ++ splitBy.loop r l a g [] := by
+  induction l generalizing a g gs with
+  | nil => simp [splitBy.loop]
+  | cons b l IH =>
+    simp_rw [splitBy.loop]
+    split <;> rw [IH]
+    conv_rhs => rw [IH]
+    simp
+
+private theorem flatten_splitByLoop {r : α → α → Bool} {l : List α} {a : α} {g : List α} :
+    (splitBy.loop r l a g []).flatten = g.reverse ++ a :: l := by
+  induction l generalizing a g with
+  | nil => simp [splitBy.loop]
+  | cons b l IH =>
+    rw [splitBy.loop, splitByLoop_eq_append [_]]
+    split <;> simp [IH]
+
+@[simp]
+theorem flatten_splitBy (r : α → α → Bool) (l : List α) : (l.splitBy r).flatten = l :=
+  match l with
+  | nil => rfl
+  | cons _ _ => flatten_splitByLoop
+
+private theorem nil_not_mem_splitByLoop {r : α → α → Bool} {l : List α} {a : α} {g : List α} :
+    [] ∉ splitBy.loop r l a g [] := by
+  induction l generalizing a g with
+  | nil =>
+    simp [splitBy.loop]
+  | cons b l IH =>
+    rw [splitBy.loop]
+    split
+    · exact IH
+    · rw [splitByLoop_eq_append, mem_append]
+      simpa using IH
+
+theorem nil_not_mem_splitBy (r : α → α → Bool) (l : List α) : [] ∉ l.splitBy r :=
+  match l with
+  | nil => not_mem_nil _
+  | cons _ _ => nil_not_mem_splitByLoop
+
+theorem ne_nil_of_mem_splitBy (r : α → α → Bool) {l : List α} (h : m ∈ l.splitBy r) : m ≠ [] := by
+  rintro rfl
+  exact nil_not_mem_splitBy r l h
+
+private theorem chain'_of_mem_splitByLoop {r : α → α → Bool} {l : List α} {a : α} {g : List α}
+    (hga : ∀ b ∈ g.head?, r b a) (hg : g.Chain' fun y x ↦ r x y)
+    (h : m ∈ splitBy.loop r l a g []) : m.Chain' fun x y ↦ r x y := by
+  induction l generalizing a g with
+  | nil =>
+    rw [splitBy.loop, reverse_cons, mem_append, mem_reverse, mem_singleton] at h
+    obtain hm | rfl := h
+    · exact (not_mem_nil m hm).elim
+    · apply List.chain'_reverse.1
+      rw [reverse_reverse]
+      exact chain'_cons'.2 ⟨hga, hg⟩
+  | cons b l IH =>
+    simp [splitBy.loop] at h
+    split at h
+    · apply IH _ (chain'_cons'.2 ⟨hga, hg⟩) h
+      intro b hb
+      rw [head?_cons, Option.mem_some_iff] at hb
+      rwa [← hb]
+    · rw [splitByLoop_eq_append, mem_append, reverse_singleton, mem_singleton] at h
+      obtain rfl | hm := h
+      · apply List.chain'_reverse.1
+        rw [reverse_append, reverse_cons, reverse_nil, nil_append, reverse_reverse]
+        exact chain'_cons'.2 ⟨hga, hg⟩
+      · apply IH _ chain'_nil hm
+        rintro _ ⟨⟩
+
+theorem chain'_of_mem_splitBy {r : α → α → Bool} {l : List α} (h : m ∈ l.splitBy r) :
+    m.Chain' fun x y ↦ r x y := by
+  cases l with
+  | nil => cases h
+  | cons a l =>
+    apply chain'_of_mem_splitByLoop _ _ h
+    · rintro _ ⟨⟩
+    · exact chain'_nil
+
+private theorem chain'_getLast_head_splitByLoop {r : α → α → Bool} (l : List α) {a : α}
+    {g : List α} {gs : List (List α)} (hgs' : [] ∉ gs)
+    (hgs : gs.Chain' fun b a ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false)
+    (hga : ∀ m ∈ gs.head?, ∃ ha hb, r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false) :
+    (splitBy.loop r l a g gs).Chain' fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false := by
+  induction l generalizing a g gs with
+  | nil =>
+    rw [splitBy.loop, reverse_cons]
+    apply List.chain'_reverse.1
+    simpa using chain'_cons'.2 ⟨hga, hgs⟩
+  | cons b l IH =>
+    rw [splitBy.loop]
+    split
+    · apply IH hgs' hgs
+      intro m hm
+      obtain ⟨ha, _, H⟩ := hga m hm
+      refine ⟨ha, append_ne_nil_of_right_ne_nil _ (cons_ne_nil _ _), ?_⟩
+      rwa [reverse_cons, head_append_of_ne_nil]
+    · apply IH
+      · simpa using hgs'
+      · rw [reverse_cons]
+        apply chain'_cons'.2 ⟨hga, hgs⟩
+      · simpa
+
+theorem chain'_getLast_head_splitBy (r : α → α → Bool) (l : List α) :
+    (l.splitBy r).Chain' fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false := by
+  cases l with
+  | nil => exact chain'_nil
+  | cons _ _ =>
+    apply chain'_getLast_head_splitByLoop _ (not_mem_nil _) chain'_nil
+    rintro _ ⟨⟩
+
+@[deprecated (since := "2024-10-30")] alias groupBy_nil := splitBy_nil
+@[deprecated (since := "2024-10-30")] alias flatten_groupBy := flatten_splitBy
+@[deprecated (since := "2024-10-15")] alias join_splitBy := flatten_splitBy
+@[deprecated (since := "2024-10-30")] alias nil_not_mem_groupBy := nil_not_mem_splitBy
+@[deprecated (since := "2024-10-30")] alias ne_nil_of_mem_groupBy := ne_nil_of_mem_splitBy
+@[deprecated (since := "2024-10-30")] alias chain'_of_mem_groupBy := chain'_of_mem_splitBy
+@[deprecated (since := "2024-10-30")]
+alias chain'_getLast_head_groupBy := chain'_getLast_head_splitBy
+
+end List

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "f2e8121bb5cc803f247435da60d8c2fc896c81ae",
+   "rev": "273c83a2622af27ff146a622c6b44f75e8ab6dd8",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "nightly-testing",

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2024-10-29
+leanprover/lean4:nightly-2024-10-30

test/MkIffOfInductive.lean

@@ -9,8 +9,8 @@ example {α : Type _} (R : α → α → Prop) (a : α) (al : List α) :
 
 -- check that the statement prints nicely
 /--
-info: test.chain_iff.{u_1} {α : Type u_1} (R : α → α → Prop) :
-  ∀ (a : α) (a_1 : List α), List.Chain R a a_1 ↔ a_1 = [] ∨ ∃ b l, R a b ∧ List.Chain R b l ∧ a_1 = b :: l
+info: test.chain_iff.{u_1} {α : Type u_1} (R : α → α → Prop) (a✝ : α) (a✝¹ : List α) :
+  List.Chain R a✝ a✝¹ ↔ a✝¹ = [] ∨ ∃ b l, R a✝ b ∧ List.Chain R b l ∧ a✝¹ = b :: l
 -/
 #guard_msgs in
 #check test.chain_iff