From f8bbd041b5e825e66d30857b1bb75704517a2700 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Thu, 31 Oct 2024 20:33:02 +1100 Subject: [PATCH] chore: adaptations for nightly-2024-10-30 (#18435) Co-authored-by: leanprover-community-mathlib4-bot --- Mathlib.lean | 2 +- Mathlib/Data/List/GroupBy.lean | 144 ------------------------------- Mathlib/Data/List/SplitBy.lean | 151 +++++++++++++++++++++++++++++++++ lake-manifest.json | 2 +- lean-toolchain | 2 +- test/MkIffOfInductive.lean | 4 +- 6 files changed, 156 insertions(+), 149 deletions(-) delete mode 100644 Mathlib/Data/List/GroupBy.lean create mode 100644 Mathlib/Data/List/SplitBy.lean diff --git a/Mathlib.lean b/Mathlib.lean index 9ff29007e3369..3dedd4e30d7d1 100644 --- a/Mathlib.lean +++ b/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 diff --git a/Mathlib/Data/List/GroupBy.lean b/Mathlib/Data/List/GroupBy.lean deleted file mode 100644 index 31f7d2baa2595..0000000000000 --- a/Mathlib/Data/List/GroupBy.lean +++ /dev/null @@ -1,144 +0,0 @@ -/- -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 - -/-! -# Group consecutive elements in a list by a relation - -This file provides the basic API for `List.groupBy` which is defined in Core. -The main results are the following: - -- `List.join_groupBy`: the lists in `List.groupBy` join to the original list. -- `List.nil_not_mem_groupBy`: the empty list is not contained in `List.groupBy`. -- `List.chain'_of_mem_groupBy`: any two adjacent elements in a list in `List.groupBy` are related by - the specified relation. -- `List.chain'_getLast_head_groupBy`: the last element of each list in `List.groupBy` is not - related to the first element of the next list. --/ - -namespace List - -variable {α : Type*} {m : List α} - -@[simp] -theorem groupBy_nil (r : α → α → Bool) : groupBy r [] = [] := - rfl - -private theorem groupByLoop_eq_append {r : α → α → Bool} {l : List α} {a : α} {g : List α} - (gs : List (List α)) : groupBy.loop r l a g gs = gs.reverse ++ groupBy.loop r l a g [] := by - induction l generalizing a g gs with - | nil => simp [groupBy.loop] - | cons b l IH => - simp_rw [groupBy.loop] - split <;> rw [IH] - conv_rhs => rw [IH] - simp - -private theorem flatten_groupByLoop {r : α → α → Bool} {l : List α} {a : α} {g : List α} : - (groupBy.loop r l a g []).flatten = g.reverse ++ a :: l := by - induction l generalizing a g with - | nil => simp [groupBy.loop] - | cons b l IH => - rw [groupBy.loop, groupByLoop_eq_append [_]] - split <;> simp [IH] - -@[simp] -theorem flatten_groupBy (r : α → α → Bool) (l : List α) : (l.groupBy r).flatten = l := - match l with - | nil => rfl - | cons _ _ => flatten_groupByLoop - -@[deprecated (since := "2024-10-15")] alias join_groupBy := flatten_groupBy - -private theorem nil_not_mem_groupByLoop {r : α → α → Bool} {l : List α} {a : α} {g : List α} : - [] ∉ groupBy.loop r l a g [] := by - induction l generalizing a g with - | nil => - simp [groupBy.loop] - | cons b l IH => - rw [groupBy.loop] - split - · exact IH - · rw [groupByLoop_eq_append, mem_append] - simpa using IH - -theorem nil_not_mem_groupBy (r : α → α → Bool) (l : List α) : [] ∉ l.groupBy r := - match l with - | nil => not_mem_nil _ - | cons _ _ => nil_not_mem_groupByLoop - -theorem ne_nil_of_mem_groupBy (r : α → α → Bool) {l : List α} (h : m ∈ l.groupBy r) : m ≠ [] := by - rintro rfl - exact nil_not_mem_groupBy r l h - -private theorem chain'_of_mem_groupByLoop {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 ∈ groupBy.loop r l a g []) : m.Chain' fun x y ↦ r x y := by - induction l generalizing a g with - | nil => - rw [groupBy.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 [groupBy.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 [groupByLoop_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_groupBy {r : α → α → Bool} {l : List α} (h : m ∈ l.groupBy r) : - m.Chain' fun x y ↦ r x y := by - cases l with - | nil => cases h - | cons a l => - apply chain'_of_mem_groupByLoop _ _ h - · rintro _ ⟨⟩ - · exact chain'_nil - -private theorem chain'_getLast_head_groupByLoop {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) : - (groupBy.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 [groupBy.loop, reverse_cons] - apply List.chain'_reverse.1 - simpa using chain'_cons'.2 ⟨hga, hgs⟩ - | cons b l IH => - rw [groupBy.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_groupBy (r : α → α → Bool) (l : List α) : - (l.groupBy 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_groupByLoop _ (not_mem_nil _) chain'_nil - rintro _ ⟨⟩ - -end List diff --git a/Mathlib/Data/List/SplitBy.lean b/Mathlib/Data/List/SplitBy.lean new file mode 100644 index 0000000000000..d14a6dd648191 --- /dev/null +++ b/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 diff --git a/lake-manifest.json b/lake-manifest.json index e9e119bbed524..0a106d1d439df 100644 --- a/lake-manifest.json +++ b/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", diff --git a/lean-toolchain b/lean-toolchain index 64aa0904e3447..fcce113e9feb6 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2024-10-29 +leanprover/lean4:nightly-2024-10-30 diff --git a/test/MkIffOfInductive.lean b/test/MkIffOfInductive.lean index 340beef419ff7..9230930110ff9 100644 --- a/test/MkIffOfInductive.lean +++ b/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