From 344bd60fa5d7531f760ff537762b7d36a4409a88 Mon Sep 17 00:00:00 2001 From: Bulhwi Cha Date: Mon, 18 Mar 2024 16:27:14 +0900 Subject: [PATCH 01/20] feat: add lemmas about lists I need these lemmas to prove `String.splitOn_of_valid`. --- Batteries/Data/List/Lemmas.lean | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/Batteries/Data/List/Lemmas.lean b/Batteries/Data/List/Lemmas.lean index 6a956f9b1d..0ed5bf978d 100644 --- a/Batteries/Data/List/Lemmas.lean +++ b/Batteries/Data/List/Lemmas.lean @@ -19,6 +19,11 @@ namespace List @[deprecated (since := "2024-08-15")] alias isEmpty_iff_eq_nil := isEmpty_iff +/-! ### head and tail -/ + +theorem head_cons_tail : ∀ l h, @head α l h :: l.tail = l + | _::_, _ => rfl + /-! ### next? -/ @[simp] theorem next?_nil : @next? α [] = none := rfl @@ -482,6 +487,12 @@ theorem Sublist.erase_diff_erase_sublist {a : α} : end Diff +/-! ### prefix, suffix, infix -/ + +theorem ne_nil_of_not_prefix (h : ¬l₁ <+: l₂) : l₁ ≠ [] := by + intro heq + simp [heq, nil_prefix] at h + /-! ### drop -/ theorem disjoint_take_drop : ∀ {l : List α}, l.Nodup → m ≤ n → Disjoint (l.take m) (l.drop n) From 87f4b94ffed5d9e1b0bc90edadd0ef9105a3e5b2 Mon Sep 17 00:00:00 2001 From: Bulhwi Cha Date: Mon, 14 Oct 2024 18:09:40 +0900 Subject: [PATCH 02/20] feat: add more lemmas about lists These are 'leftover' lemmas I created while trying to prove `String.splitOn_of_valid`. See https://github.com/leanprover-community/batteries/pull/743. --- Batteries/Data/List/Lemmas.lean | 26 ++++++++++++++++++++++++++ 1 file changed, 26 insertions(+) diff --git a/Batteries/Data/List/Lemmas.lean b/Batteries/Data/List/Lemmas.lean index 0ed5bf978d..c14cbd440e 100644 --- a/Batteries/Data/List/Lemmas.lean +++ b/Batteries/Data/List/Lemmas.lean @@ -24,6 +24,10 @@ namespace List theorem head_cons_tail : ∀ l h, @head α l h :: l.tail = l | _::_, _ => rfl +theorem singleton_head_eq_self (l : List α) (hne : l ≠ []) (htl : l.tail = []) : + [l.head hne] = l := by + conv => rhs; rw [← head_cons_tail l hne, htl] + /-! ### next? -/ @[simp] theorem next?_nil : @next? α [] = none := rfl @@ -489,10 +493,32 @@ end Diff /-! ### prefix, suffix, infix -/ +theorem singleton_prefix_cons (a) : [a] <+: a :: l := + (prefix_cons_inj a).mpr nil_prefix + theorem ne_nil_of_not_prefix (h : ¬l₁ <+: l₂) : l₁ ≠ [] := by intro heq simp [heq, nil_prefix] at h +theorem not_prefix_and_not_prefix_symm_iff_exists [BEq α] [LawfulBEq α] [DecidableEq α] + {l₁ l₂ : List α} : ¬l₁ <+: l₂ ∧ ¬l₂ <+: l₁ ↔ ∃ c₁ c₂ pre suf₁ suf₂, c₁ ≠ c₂ ∧ + l₁ = pre ++ c₁ :: suf₁ ∧ l₂ = pre ++ c₂ :: suf₂ := by + constructor <;> intro h + · obtain ⟨c₁, l₁, rfl⟩ := l₁.exists_cons_of_ne_nil (ne_nil_of_not_prefix h.1) + obtain ⟨c₂, l₂, rfl⟩ := l₂.exists_cons_of_ne_nil (ne_nil_of_not_prefix h.2) + simp only [cons_prefix_cons, not_and] at h + cases Decidable.em (c₁ = c₂) + · subst c₂ + simp only [forall_const] at h + let ⟨c₁', c₂', pre, suf₁, suf₂, hc, heq₁, heq₂⟩ := + not_prefix_and_not_prefix_symm_iff_exists.mp h + exact ⟨c₁', c₂', c₁::pre, suf₁, suf₂, hc, by simp [heq₁], by simp [heq₂]⟩ + · next hc => + exact ⟨c₁, c₂, [], l₁, l₂, hc, nil_append .., nil_append ..⟩ + · let ⟨c₁, c₂, pre, suf₁, suf₂, hc, heq₁, heq₂⟩ := h + rw [heq₁, heq₂] + simp [prefix_append_right_inj, cons_prefix_cons, hc, hc.symm] + /-! ### drop -/ theorem disjoint_take_drop : ∀ {l : List α}, l.Nodup → m ≤ n → Disjoint (l.take m) (l.drop n) From 02599d99f91b8a5b246ec656df413c0f7180d812 Mon Sep 17 00:00:00 2001 From: Bulhwi Cha Date: Tue, 15 Oct 2024 02:36:25 +0000 Subject: [PATCH 03/20] style: avoid using `@` symbol MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Using the `@` symbol is a bit old-fashioned. Co-authored-by: François G. Dorais --- Batteries/Data/List/Lemmas.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Batteries/Data/List/Lemmas.lean b/Batteries/Data/List/Lemmas.lean index c14cbd440e..2cf150d3a0 100644 --- a/Batteries/Data/List/Lemmas.lean +++ b/Batteries/Data/List/Lemmas.lean @@ -21,7 +21,7 @@ namespace List /-! ### head and tail -/ -theorem head_cons_tail : ∀ l h, @head α l h :: l.tail = l +theorem head_cons_tail : ∀ (l : List α) (hne : l ≠ []), l.head hne :: l.tail = l | _::_, _ => rfl theorem singleton_head_eq_self (l : List α) (hne : l ≠ []) (htl : l.tail = []) : From f39e00ae79d3ece7fd768ff728f376b4c6238126 Mon Sep 17 00:00:00 2001 From: Bulhwi Cha Date: Wed, 16 Oct 2024 01:11:01 +0900 Subject: [PATCH 04/20] refactor: remove implicit instances of theorem --- Batteries/Data/List/Lemmas.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Batteries/Data/List/Lemmas.lean b/Batteries/Data/List/Lemmas.lean index 2cf150d3a0..1e7a3f6d7a 100644 --- a/Batteries/Data/List/Lemmas.lean +++ b/Batteries/Data/List/Lemmas.lean @@ -500,9 +500,9 @@ theorem ne_nil_of_not_prefix (h : ¬l₁ <+: l₂) : l₁ ≠ [] := by intro heq simp [heq, nil_prefix] at h -theorem not_prefix_and_not_prefix_symm_iff_exists [BEq α] [LawfulBEq α] [DecidableEq α] - {l₁ l₂ : List α} : ¬l₁ <+: l₂ ∧ ¬l₂ <+: l₁ ↔ ∃ c₁ c₂ pre suf₁ suf₂, c₁ ≠ c₂ ∧ - l₁ = pre ++ c₁ :: suf₁ ∧ l₂ = pre ++ c₂ :: suf₂ := by +theorem not_prefix_and_not_prefix_symm_iff_exists [DecidableEq α] {l₁ l₂ : List α} : + ¬l₁ <+: l₂ ∧ ¬l₂ <+: l₁ ↔ ∃ c₁ c₂ pre suf₁ suf₂, c₁ ≠ c₂ ∧ l₁ = pre ++ c₁ :: suf₁ ∧ + l₂ = pre ++ c₂ :: suf₂ := by constructor <;> intro h · obtain ⟨c₁, l₁, rfl⟩ := l₁.exists_cons_of_ne_nil (ne_nil_of_not_prefix h.1) obtain ⟨c₂, l₂, rfl⟩ := l₂.exists_cons_of_ne_nil (ne_nil_of_not_prefix h.2) From 2d30498159047c1dac25593203c32b20e42df0e3 Mon Sep 17 00:00:00 2001 From: Bulhwi Cha Date: Wed, 16 Oct 2024 01:13:05 +0900 Subject: [PATCH 05/20] refactor: put theorem in section --- Batteries/Data/List/Lemmas.lean | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/Batteries/Data/List/Lemmas.lean b/Batteries/Data/List/Lemmas.lean index 1e7a3f6d7a..4f9bc11ed5 100644 --- a/Batteries/Data/List/Lemmas.lean +++ b/Batteries/Data/List/Lemmas.lean @@ -500,7 +500,11 @@ theorem ne_nil_of_not_prefix (h : ¬l₁ <+: l₂) : l₁ ≠ [] := by intro heq simp [heq, nil_prefix] at h -theorem not_prefix_and_not_prefix_symm_iff_exists [DecidableEq α] {l₁ l₂ : List α} : +section + +variable [DecidableEq α] + +theorem not_prefix_and_not_prefix_symm_iff_exists {l₁ l₂ : List α} : ¬l₁ <+: l₂ ∧ ¬l₂ <+: l₁ ↔ ∃ c₁ c₂ pre suf₁ suf₂, c₁ ≠ c₂ ∧ l₁ = pre ++ c₁ :: suf₁ ∧ l₂ = pre ++ c₂ :: suf₂ := by constructor <;> intro h @@ -519,6 +523,8 @@ theorem not_prefix_and_not_prefix_symm_iff_exists [DecidableEq α] {l₁ l₂ : rw [heq₁, heq₂] simp [prefix_append_right_inj, cons_prefix_cons, hc, hc.symm] +end + /-! ### drop -/ theorem disjoint_take_drop : ∀ {l : List α}, l.Nodup → m ≤ n → Disjoint (l.take m) (l.drop n) From 6b39d441f8786488f68e3882c2736589f516c694 Mon Sep 17 00:00:00 2001 From: Bulhwi Cha Date: Wed, 16 Oct 2024 01:14:50 +0900 Subject: [PATCH 06/20] feat: add `List.commonPrefix` and its lemmas The function `List.commonPrefix` returns the longest common prefix of two lists. --- Batteries/Data/List/Lemmas.lean | 42 +++++++++++++++++++++++++++++++++ 1 file changed, 42 insertions(+) diff --git a/Batteries/Data/List/Lemmas.lean b/Batteries/Data/List/Lemmas.lean index 4f9bc11ed5..78ec852c92 100644 --- a/Batteries/Data/List/Lemmas.lean +++ b/Batteries/Data/List/Lemmas.lean @@ -504,6 +504,48 @@ section variable [DecidableEq α] +/-- Returns the longest common prefix of two lists. -/ +def commonPrefix : (l₁ l₂ : List α) → List α + | [], _ => [] + | _, [] => [] + | a₁::l₁, a₂::l₂ => + if a₁ = a₂ then + a₁ :: (commonPrefix l₁ l₂) + else + [] + +theorem commonPrefix_prefix_left (l₁ l₂ : List α) : commonPrefix l₁ l₂ <+: l₁ := by + match l₁, l₂ with + | [], _ => simp [commonPrefix] + | _::_, [] => simp [commonPrefix] + | a₁::l₁, a₂::l₂ => + simp only [commonPrefix] + cases Decidable.em (a₁ = a₂) + · next h => + simp only [h, ↓reduceIte, cons_prefix_cons, true_and] + apply commonPrefix_prefix_left + · next h => + simp [h] + +theorem commonPrefix_prefix_right (l₁ l₂ : List α) : commonPrefix l₁ l₂ <+: l₂ := by + match l₁, l₂ with + | [], _ => simp [commonPrefix] + | _::_, [] => simp [commonPrefix] + | a₁::l₁, a₂::l₂ => + simp only [commonPrefix] + cases Decidable.em (a₁ = a₂) + · next h => + simp only [h, ↓reduceIte, cons_prefix_cons, true_and] + apply commonPrefix_prefix_right + · next h => + simp [h] + +theorem commonPrefix_append_append (p l₁ l₂ : List α) : + commonPrefix (p ++ l₁) (p ++ l₂) = p ++ commonPrefix l₁ l₂ := by + match p with + | [] => rfl + | a::p => simpa [commonPrefix] using commonPrefix_append_append p l₁ l₂ + theorem not_prefix_and_not_prefix_symm_iff_exists {l₁ l₂ : List α} : ¬l₁ <+: l₂ ∧ ¬l₂ <+: l₁ ↔ ∃ c₁ c₂ pre suf₁ suf₂, c₁ ≠ c₂ ∧ l₁ = pre ++ c₁ :: suf₁ ∧ l₂ = pre ++ c₂ :: suf₂ := by From ce3809902f5a2487946003caac6fa7f53c4fe310 Mon Sep 17 00:00:00 2001 From: Bulhwi Cha Date: Wed, 16 Oct 2024 01:18:27 +0900 Subject: [PATCH 07/20] refactor: rename and restate theorem * Remove the "_exists" part from the theorem's name. * Remove the existential quantifiers from the theorem's statement and add new hypotheses. --- Batteries/Data/List/Lemmas.lean | 45 ++++++++++++++++++++------------- 1 file changed, 28 insertions(+), 17 deletions(-) diff --git a/Batteries/Data/List/Lemmas.lean b/Batteries/Data/List/Lemmas.lean index 78ec852c92..fc08ffdf8a 100644 --- a/Batteries/Data/List/Lemmas.lean +++ b/Batteries/Data/List/Lemmas.lean @@ -546,24 +546,35 @@ theorem commonPrefix_append_append (p l₁ l₂ : List α) : | [] => rfl | a::p => simpa [commonPrefix] using commonPrefix_append_append p l₁ l₂ -theorem not_prefix_and_not_prefix_symm_iff_exists {l₁ l₂ : List α} : - ¬l₁ <+: l₂ ∧ ¬l₂ <+: l₁ ↔ ∃ c₁ c₂ pre suf₁ suf₂, c₁ ≠ c₂ ∧ l₁ = pre ++ c₁ :: suf₁ ∧ - l₂ = pre ++ c₂ :: suf₂ := by +theorem not_prefix_and_not_prefix_symm_iff {l₁ l₂ p t₁ t₂ : List α} (hp : commonPrefix l₁ l₂ = p) + (h₁ : l₁ = p ++ t₁) (h₂ : l₂ = p ++ t₂) : ¬l₁ <+: l₂ ∧ ¬l₂ <+: l₁ ↔ t₁ ≠ [] ∧ t₂ ≠ [] ∧ + t₁.head? ≠ t₂.head? := by constructor <;> intro h - · obtain ⟨c₁, l₁, rfl⟩ := l₁.exists_cons_of_ne_nil (ne_nil_of_not_prefix h.1) - obtain ⟨c₂, l₂, rfl⟩ := l₂.exists_cons_of_ne_nil (ne_nil_of_not_prefix h.2) - simp only [cons_prefix_cons, not_and] at h - cases Decidable.em (c₁ = c₂) - · subst c₂ - simp only [forall_const] at h - let ⟨c₁', c₂', pre, suf₁, suf₂, hc, heq₁, heq₂⟩ := - not_prefix_and_not_prefix_symm_iff_exists.mp h - exact ⟨c₁', c₂', c₁::pre, suf₁, suf₂, hc, by simp [heq₁], by simp [heq₂]⟩ - · next hc => - exact ⟨c₁, c₂, [], l₁, l₂, hc, nil_append .., nil_append ..⟩ - · let ⟨c₁, c₂, pre, suf₁, suf₂, hc, heq₁, heq₂⟩ := h - rw [heq₁, heq₂] - simp [prefix_append_right_inj, cons_prefix_cons, hc, hc.symm] + · obtain ⟨a₁, l₁, rfl⟩ := l₁.exists_cons_of_ne_nil (ne_nil_of_not_prefix h.1) + obtain ⟨a₂, l₂, rfl⟩ := l₂.exists_cons_of_ne_nil (ne_nil_of_not_prefix h.2) + cases Decidable.em (a₁ = a₂) + · subst a₂ + simp only [← hp, commonPrefix, ↓reduceIte, cons_append, cons.injEq, true_and] at h₁ h₂ + simp only [cons_prefix_cons, true_and] at h + exact (not_prefix_and_not_prefix_symm_iff rfl h₁ h₂).mp h + · next hne => + simp only [← hp, commonPrefix, hne, ↓reduceIte, nil_append] at h₁ h₂ + simp [← h₁, ← h₂, hne] + · rw [h₁, h₂] + let ⟨ht₁, ht₂, hhd⟩ := h + obtain ⟨a₁, t₁, rfl⟩ := exists_cons_of_ne_nil ht₁ + obtain ⟨a₂, t₂, rfl⟩ := exists_cons_of_ne_nil ht₂ + simp only [head?_cons, ne_eq, Option.some.injEq] at hhd + rw [← ne_eq] at hhd + simp [prefix_append_right_inj, not_and_of_not_left _ hhd, not_and_of_not_left _ hhd.symm] +termination_by l₁.length +decreasing_by + rename_i _₀ _l₁ _₁ _₂ _₃ _₄ _₅ _₆ _₇ _r _₈ _₉ _₁₀ _₁₁ _₁₂ _₁₃ _₁₄ _₁₅ _₁₆ _₁₇ _₁₈ _hl₁ _₁₉ _₂₀ _₂₁ + _₂₂ _₂₃ _₂₄ _₂₅ _₂₆ _₂₇ + clear _₀ _₁ _₂ _₃ _₄ _₅ _₆ _₇ _r _₈ _₉ _₁₀ _₁₁ _₁₂ _₁₃ _₁₄ _₁₅ _₁₆ _₁₇ _₁₈ _₁₉ _₂₀ _₂₁ _₂₂ _₂₃ _₂₄ + _₂₅ _₂₆ _₂₇ + subst _l₁ + simp end From 6b7c0e47e0931f316d1b77f3c4f0351aa27d873d Mon Sep 17 00:00:00 2001 From: Bulhwi Cha Date: Wed, 16 Oct 2024 02:16:12 +0900 Subject: [PATCH 08/20] chore: move definition to another file Move `List.commonPrefix` to `Batteries.Data.List.Basic`. --- Batteries/Data/List/Basic.lean | 10 ++++++++++ Batteries/Data/List/Lemmas.lean | 10 ---------- 2 files changed, 10 insertions(+), 10 deletions(-) diff --git a/Batteries/Data/List/Basic.lean b/Batteries/Data/List/Basic.lean index 49126faee0..1f2bd11f4a 100644 --- a/Batteries/Data/List/Basic.lean +++ b/Batteries/Data/List/Basic.lean @@ -10,6 +10,16 @@ namespace List /-! ## New definitions -/ +/-- Returns the longest common prefix of two lists. -/ +def commonPrefix [DecidableEq α] : (l₁ l₂ : List α) → List α + | [], _ => [] + | _, [] => [] + | a₁::l₁, a₂::l₂ => + if a₁ = a₂ then + a₁ :: (commonPrefix l₁ l₂) + else + [] + /-- Computes the "bag intersection" of `l₁` and `l₂`, that is, the collection of elements of `l₁` which are also in `l₂`. As each element diff --git a/Batteries/Data/List/Lemmas.lean b/Batteries/Data/List/Lemmas.lean index fc08ffdf8a..f05888a5a8 100644 --- a/Batteries/Data/List/Lemmas.lean +++ b/Batteries/Data/List/Lemmas.lean @@ -504,16 +504,6 @@ section variable [DecidableEq α] -/-- Returns the longest common prefix of two lists. -/ -def commonPrefix : (l₁ l₂ : List α) → List α - | [], _ => [] - | _, [] => [] - | a₁::l₁, a₂::l₂ => - if a₁ = a₂ then - a₁ :: (commonPrefix l₁ l₂) - else - [] - theorem commonPrefix_prefix_left (l₁ l₂ : List α) : commonPrefix l₁ l₂ <+: l₁ := by match l₁, l₂ with | [], _ => simp [commonPrefix] From ab8e65ad395fa26ea83527c70c2ad858cc14e848 Mon Sep 17 00:00:00 2001 From: Bulhwi Cha Date: Wed, 16 Oct 2024 12:11:59 +0900 Subject: [PATCH 09/20] feat: add theorem `List.commonPrefix_comm` This theorem will simplify the proof of the theorem `List.commonPrefix_prefix_right`. Co-authored-by: Kyle Miller --- Batteries/Data/List/Lemmas.lean | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/Batteries/Data/List/Lemmas.lean b/Batteries/Data/List/Lemmas.lean index f05888a5a8..f4768b716d 100644 --- a/Batteries/Data/List/Lemmas.lean +++ b/Batteries/Data/List/Lemmas.lean @@ -504,6 +504,16 @@ section variable [DecidableEq α] +theorem commonPrefix_comm (l₁ l₂ : List α) : commonPrefix l₁ l₂ = commonPrefix l₂ l₁ := by + cases l₁ <;> cases l₂ <;> simp only [commonPrefix] + next a₁ l₁ a₂ l₂ => + split + · subst a₁ + simp only [↓reduceIte, cons.injEq, true_and] + apply commonPrefix_comm + · next h => + simp [Ne.symm h] + theorem commonPrefix_prefix_left (l₁ l₂ : List α) : commonPrefix l₁ l₂ <+: l₁ := by match l₁, l₂ with | [], _ => simp [commonPrefix] From 9e0d971b9fb808fc3c26cab57a141b78d1c69819 Mon Sep 17 00:00:00 2001 From: Bulhwi Cha Date: Wed, 16 Oct 2024 12:21:29 +0900 Subject: [PATCH 10/20] style: avoid using `Decidable.em` directly Co-authored-by: Kyle Miller --- Batteries/Data/List/Lemmas.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Batteries/Data/List/Lemmas.lean b/Batteries/Data/List/Lemmas.lean index f4768b716d..2931d28b0e 100644 --- a/Batteries/Data/List/Lemmas.lean +++ b/Batteries/Data/List/Lemmas.lean @@ -520,7 +520,7 @@ theorem commonPrefix_prefix_left (l₁ l₂ : List α) : commonPrefix l₁ l₂ | _::_, [] => simp [commonPrefix] | a₁::l₁, a₂::l₂ => simp only [commonPrefix] - cases Decidable.em (a₁ = a₂) + split · next h => simp only [h, ↓reduceIte, cons_prefix_cons, true_and] apply commonPrefix_prefix_left From d2571844f58882e554845706efdcea16a328c118 Mon Sep 17 00:00:00 2001 From: Bulhwi Cha Date: Wed, 16 Oct 2024 12:16:05 +0900 Subject: [PATCH 11/20] refactor: golf proofs Co-authored-by: Kyle Miller --- Batteries/Data/List/Lemmas.lean | 50 +++++++-------------------------- 1 file changed, 10 insertions(+), 40 deletions(-) diff --git a/Batteries/Data/List/Lemmas.lean b/Batteries/Data/List/Lemmas.lean index 2931d28b0e..6a0d5faff9 100644 --- a/Batteries/Data/List/Lemmas.lean +++ b/Batteries/Data/List/Lemmas.lean @@ -528,17 +528,8 @@ theorem commonPrefix_prefix_left (l₁ l₂ : List α) : commonPrefix l₁ l₂ simp [h] theorem commonPrefix_prefix_right (l₁ l₂ : List α) : commonPrefix l₁ l₂ <+: l₂ := by - match l₁, l₂ with - | [], _ => simp [commonPrefix] - | _::_, [] => simp [commonPrefix] - | a₁::l₁, a₂::l₂ => - simp only [commonPrefix] - cases Decidable.em (a₁ = a₂) - · next h => - simp only [h, ↓reduceIte, cons_prefix_cons, true_and] - apply commonPrefix_prefix_right - · next h => - simp [h] + rw [commonPrefix_comm] + apply commonPrefix_prefix_left theorem commonPrefix_append_append (p l₁ l₂ : List α) : commonPrefix (p ++ l₁) (p ++ l₂) = p ++ commonPrefix l₁ l₂ := by @@ -546,35 +537,14 @@ theorem commonPrefix_append_append (p l₁ l₂ : List α) : | [] => rfl | a::p => simpa [commonPrefix] using commonPrefix_append_append p l₁ l₂ -theorem not_prefix_and_not_prefix_symm_iff {l₁ l₂ p t₁ t₂ : List α} (hp : commonPrefix l₁ l₂ = p) - (h₁ : l₁ = p ++ t₁) (h₂ : l₂ = p ++ t₂) : ¬l₁ <+: l₂ ∧ ¬l₂ <+: l₁ ↔ t₁ ≠ [] ∧ t₂ ≠ [] ∧ - t₁.head? ≠ t₂.head? := by - constructor <;> intro h - · obtain ⟨a₁, l₁, rfl⟩ := l₁.exists_cons_of_ne_nil (ne_nil_of_not_prefix h.1) - obtain ⟨a₂, l₂, rfl⟩ := l₂.exists_cons_of_ne_nil (ne_nil_of_not_prefix h.2) - cases Decidable.em (a₁ = a₂) - · subst a₂ - simp only [← hp, commonPrefix, ↓reduceIte, cons_append, cons.injEq, true_and] at h₁ h₂ - simp only [cons_prefix_cons, true_and] at h - exact (not_prefix_and_not_prefix_symm_iff rfl h₁ h₂).mp h - · next hne => - simp only [← hp, commonPrefix, hne, ↓reduceIte, nil_append] at h₁ h₂ - simp [← h₁, ← h₂, hne] - · rw [h₁, h₂] - let ⟨ht₁, ht₂, hhd⟩ := h - obtain ⟨a₁, t₁, rfl⟩ := exists_cons_of_ne_nil ht₁ - obtain ⟨a₂, t₂, rfl⟩ := exists_cons_of_ne_nil ht₂ - simp only [head?_cons, ne_eq, Option.some.injEq] at hhd - rw [← ne_eq] at hhd - simp [prefix_append_right_inj, not_and_of_not_left _ hhd, not_and_of_not_left _ hhd.symm] -termination_by l₁.length -decreasing_by - rename_i _₀ _l₁ _₁ _₂ _₃ _₄ _₅ _₆ _₇ _r _₈ _₉ _₁₀ _₁₁ _₁₂ _₁₃ _₁₄ _₁₅ _₁₆ _₁₇ _₁₈ _hl₁ _₁₉ _₂₀ _₂₁ - _₂₂ _₂₃ _₂₄ _₂₅ _₂₆ _₂₇ - clear _₀ _₁ _₂ _₃ _₄ _₅ _₆ _₇ _r _₈ _₉ _₁₀ _₁₁ _₁₂ _₁₃ _₁₄ _₁₅ _₁₆ _₁₇ _₁₈ _₁₉ _₂₀ _₂₁ _₂₂ _₂₃ _₂₄ - _₂₅ _₂₆ _₂₇ - subst _l₁ - simp +theorem not_prefix_and_not_prefix_symm_iff {l₁ l₂ : List α} (hp : commonPrefix l₁ l₂ = []) : + ¬l₁ <+: l₂ ∧ ¬l₂ <+: l₁ ↔ l₁ ≠ [] ∧ l₂ ≠ [] ∧ l₁.head? ≠ l₂.head? := by + match l₁, l₂ with + | [], _ => simp + | _, [] => simp + | a₁::l₁, a₂::l₂ => + simp only [commonPrefix, ite_eq_right_iff, reduceCtorEq, imp_false] at hp + simp [hp, Ne.symm hp] end From fa83dc735a7d272faef5f85b76e8de94fd45cb6e Mon Sep 17 00:00:00 2001 From: Bulhwi Cha Date: Wed, 16 Oct 2024 18:54:29 +0900 Subject: [PATCH 12/20] Revert "refactor: golf proofs" This reverts commit d2571844f58882e554845706efdcea16a328c118. --- Batteries/Data/List/Lemmas.lean | 50 ++++++++++++++++++++++++++------- 1 file changed, 40 insertions(+), 10 deletions(-) diff --git a/Batteries/Data/List/Lemmas.lean b/Batteries/Data/List/Lemmas.lean index 6a0d5faff9..2931d28b0e 100644 --- a/Batteries/Data/List/Lemmas.lean +++ b/Batteries/Data/List/Lemmas.lean @@ -528,8 +528,17 @@ theorem commonPrefix_prefix_left (l₁ l₂ : List α) : commonPrefix l₁ l₂ simp [h] theorem commonPrefix_prefix_right (l₁ l₂ : List α) : commonPrefix l₁ l₂ <+: l₂ := by - rw [commonPrefix_comm] - apply commonPrefix_prefix_left + match l₁, l₂ with + | [], _ => simp [commonPrefix] + | _::_, [] => simp [commonPrefix] + | a₁::l₁, a₂::l₂ => + simp only [commonPrefix] + cases Decidable.em (a₁ = a₂) + · next h => + simp only [h, ↓reduceIte, cons_prefix_cons, true_and] + apply commonPrefix_prefix_right + · next h => + simp [h] theorem commonPrefix_append_append (p l₁ l₂ : List α) : commonPrefix (p ++ l₁) (p ++ l₂) = p ++ commonPrefix l₁ l₂ := by @@ -537,14 +546,35 @@ theorem commonPrefix_append_append (p l₁ l₂ : List α) : | [] => rfl | a::p => simpa [commonPrefix] using commonPrefix_append_append p l₁ l₂ -theorem not_prefix_and_not_prefix_symm_iff {l₁ l₂ : List α} (hp : commonPrefix l₁ l₂ = []) : - ¬l₁ <+: l₂ ∧ ¬l₂ <+: l₁ ↔ l₁ ≠ [] ∧ l₂ ≠ [] ∧ l₁.head? ≠ l₂.head? := by - match l₁, l₂ with - | [], _ => simp - | _, [] => simp - | a₁::l₁, a₂::l₂ => - simp only [commonPrefix, ite_eq_right_iff, reduceCtorEq, imp_false] at hp - simp [hp, Ne.symm hp] +theorem not_prefix_and_not_prefix_symm_iff {l₁ l₂ p t₁ t₂ : List α} (hp : commonPrefix l₁ l₂ = p) + (h₁ : l₁ = p ++ t₁) (h₂ : l₂ = p ++ t₂) : ¬l₁ <+: l₂ ∧ ¬l₂ <+: l₁ ↔ t₁ ≠ [] ∧ t₂ ≠ [] ∧ + t₁.head? ≠ t₂.head? := by + constructor <;> intro h + · obtain ⟨a₁, l₁, rfl⟩ := l₁.exists_cons_of_ne_nil (ne_nil_of_not_prefix h.1) + obtain ⟨a₂, l₂, rfl⟩ := l₂.exists_cons_of_ne_nil (ne_nil_of_not_prefix h.2) + cases Decidable.em (a₁ = a₂) + · subst a₂ + simp only [← hp, commonPrefix, ↓reduceIte, cons_append, cons.injEq, true_and] at h₁ h₂ + simp only [cons_prefix_cons, true_and] at h + exact (not_prefix_and_not_prefix_symm_iff rfl h₁ h₂).mp h + · next hne => + simp only [← hp, commonPrefix, hne, ↓reduceIte, nil_append] at h₁ h₂ + simp [← h₁, ← h₂, hne] + · rw [h₁, h₂] + let ⟨ht₁, ht₂, hhd⟩ := h + obtain ⟨a₁, t₁, rfl⟩ := exists_cons_of_ne_nil ht₁ + obtain ⟨a₂, t₂, rfl⟩ := exists_cons_of_ne_nil ht₂ + simp only [head?_cons, ne_eq, Option.some.injEq] at hhd + rw [← ne_eq] at hhd + simp [prefix_append_right_inj, not_and_of_not_left _ hhd, not_and_of_not_left _ hhd.symm] +termination_by l₁.length +decreasing_by + rename_i _₀ _l₁ _₁ _₂ _₃ _₄ _₅ _₆ _₇ _r _₈ _₉ _₁₀ _₁₁ _₁₂ _₁₃ _₁₄ _₁₅ _₁₆ _₁₇ _₁₈ _hl₁ _₁₉ _₂₀ _₂₁ + _₂₂ _₂₃ _₂₄ _₂₅ _₂₆ _₂₇ + clear _₀ _₁ _₂ _₃ _₄ _₅ _₆ _₇ _r _₈ _₉ _₁₀ _₁₁ _₁₂ _₁₃ _₁₄ _₁₅ _₁₆ _₁₇ _₁₈ _₁₉ _₂₀ _₂₁ _₂₂ _₂₃ _₂₄ + _₂₅ _₂₆ _₂₇ + subst _l₁ + simp end From ffbd01f3e5572a13c0f27f729393aabac7af043d Mon Sep 17 00:00:00 2001 From: Bulhwi Cha Date: Wed, 16 Oct 2024 18:54:33 +0900 Subject: [PATCH 13/20] Revert "style: avoid using `Decidable.em` directly" This reverts commit 9e0d971b9fb808fc3c26cab57a141b78d1c69819. --- Batteries/Data/List/Lemmas.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Batteries/Data/List/Lemmas.lean b/Batteries/Data/List/Lemmas.lean index 2931d28b0e..f4768b716d 100644 --- a/Batteries/Data/List/Lemmas.lean +++ b/Batteries/Data/List/Lemmas.lean @@ -520,7 +520,7 @@ theorem commonPrefix_prefix_left (l₁ l₂ : List α) : commonPrefix l₁ l₂ | _::_, [] => simp [commonPrefix] | a₁::l₁, a₂::l₂ => simp only [commonPrefix] - split + cases Decidable.em (a₁ = a₂) · next h => simp only [h, ↓reduceIte, cons_prefix_cons, true_and] apply commonPrefix_prefix_left From 49f306e91bac3bd4c698b18367e3be3b1fd50fde Mon Sep 17 00:00:00 2001 From: Bulhwi Cha Date: Wed, 16 Oct 2024 18:54:39 +0900 Subject: [PATCH 14/20] Revert "feat: add theorem `List.commonPrefix_comm`" This reverts commit ab8e65ad395fa26ea83527c70c2ad858cc14e848. --- Batteries/Data/List/Lemmas.lean | 10 ---------- 1 file changed, 10 deletions(-) diff --git a/Batteries/Data/List/Lemmas.lean b/Batteries/Data/List/Lemmas.lean index f4768b716d..f05888a5a8 100644 --- a/Batteries/Data/List/Lemmas.lean +++ b/Batteries/Data/List/Lemmas.lean @@ -504,16 +504,6 @@ section variable [DecidableEq α] -theorem commonPrefix_comm (l₁ l₂ : List α) : commonPrefix l₁ l₂ = commonPrefix l₂ l₁ := by - cases l₁ <;> cases l₂ <;> simp only [commonPrefix] - next a₁ l₁ a₂ l₂ => - split - · subst a₁ - simp only [↓reduceIte, cons.injEq, true_and] - apply commonPrefix_comm - · next h => - simp [Ne.symm h] - theorem commonPrefix_prefix_left (l₁ l₂ : List α) : commonPrefix l₁ l₂ <+: l₁ := by match l₁, l₂ with | [], _ => simp [commonPrefix] From 0e6bfd88e1e89eb32c690584397df60f895eb654 Mon Sep 17 00:00:00 2001 From: Bulhwi Cha Date: Wed, 16 Oct 2024 18:54:41 +0900 Subject: [PATCH 15/20] Revert "chore: move definition to another file" This reverts commit 6b7c0e47e0931f316d1b77f3c4f0351aa27d873d. --- Batteries/Data/List/Basic.lean | 10 ---------- Batteries/Data/List/Lemmas.lean | 10 ++++++++++ 2 files changed, 10 insertions(+), 10 deletions(-) diff --git a/Batteries/Data/List/Basic.lean b/Batteries/Data/List/Basic.lean index 1f2bd11f4a..49126faee0 100644 --- a/Batteries/Data/List/Basic.lean +++ b/Batteries/Data/List/Basic.lean @@ -10,16 +10,6 @@ namespace List /-! ## New definitions -/ -/-- Returns the longest common prefix of two lists. -/ -def commonPrefix [DecidableEq α] : (l₁ l₂ : List α) → List α - | [], _ => [] - | _, [] => [] - | a₁::l₁, a₂::l₂ => - if a₁ = a₂ then - a₁ :: (commonPrefix l₁ l₂) - else - [] - /-- Computes the "bag intersection" of `l₁` and `l₂`, that is, the collection of elements of `l₁` which are also in `l₂`. As each element diff --git a/Batteries/Data/List/Lemmas.lean b/Batteries/Data/List/Lemmas.lean index f05888a5a8..fc08ffdf8a 100644 --- a/Batteries/Data/List/Lemmas.lean +++ b/Batteries/Data/List/Lemmas.lean @@ -504,6 +504,16 @@ section variable [DecidableEq α] +/-- Returns the longest common prefix of two lists. -/ +def commonPrefix : (l₁ l₂ : List α) → List α + | [], _ => [] + | _, [] => [] + | a₁::l₁, a₂::l₂ => + if a₁ = a₂ then + a₁ :: (commonPrefix l₁ l₂) + else + [] + theorem commonPrefix_prefix_left (l₁ l₂ : List α) : commonPrefix l₁ l₂ <+: l₁ := by match l₁, l₂ with | [], _ => simp [commonPrefix] From 10a0c0ded7a6cf9e30e1e233a32b2aec036d9e60 Mon Sep 17 00:00:00 2001 From: Bulhwi Cha Date: Wed, 16 Oct 2024 18:54:42 +0900 Subject: [PATCH 16/20] Revert "refactor: rename and restate theorem" This reverts commit ce3809902f5a2487946003caac6fa7f53c4fe310. --- Batteries/Data/List/Lemmas.lean | 45 +++++++++++++-------------------- 1 file changed, 17 insertions(+), 28 deletions(-) diff --git a/Batteries/Data/List/Lemmas.lean b/Batteries/Data/List/Lemmas.lean index fc08ffdf8a..78ec852c92 100644 --- a/Batteries/Data/List/Lemmas.lean +++ b/Batteries/Data/List/Lemmas.lean @@ -546,35 +546,24 @@ theorem commonPrefix_append_append (p l₁ l₂ : List α) : | [] => rfl | a::p => simpa [commonPrefix] using commonPrefix_append_append p l₁ l₂ -theorem not_prefix_and_not_prefix_symm_iff {l₁ l₂ p t₁ t₂ : List α} (hp : commonPrefix l₁ l₂ = p) - (h₁ : l₁ = p ++ t₁) (h₂ : l₂ = p ++ t₂) : ¬l₁ <+: l₂ ∧ ¬l₂ <+: l₁ ↔ t₁ ≠ [] ∧ t₂ ≠ [] ∧ - t₁.head? ≠ t₂.head? := by +theorem not_prefix_and_not_prefix_symm_iff_exists {l₁ l₂ : List α} : + ¬l₁ <+: l₂ ∧ ¬l₂ <+: l₁ ↔ ∃ c₁ c₂ pre suf₁ suf₂, c₁ ≠ c₂ ∧ l₁ = pre ++ c₁ :: suf₁ ∧ + l₂ = pre ++ c₂ :: suf₂ := by constructor <;> intro h - · obtain ⟨a₁, l₁, rfl⟩ := l₁.exists_cons_of_ne_nil (ne_nil_of_not_prefix h.1) - obtain ⟨a₂, l₂, rfl⟩ := l₂.exists_cons_of_ne_nil (ne_nil_of_not_prefix h.2) - cases Decidable.em (a₁ = a₂) - · subst a₂ - simp only [← hp, commonPrefix, ↓reduceIte, cons_append, cons.injEq, true_and] at h₁ h₂ - simp only [cons_prefix_cons, true_and] at h - exact (not_prefix_and_not_prefix_symm_iff rfl h₁ h₂).mp h - · next hne => - simp only [← hp, commonPrefix, hne, ↓reduceIte, nil_append] at h₁ h₂ - simp [← h₁, ← h₂, hne] - · rw [h₁, h₂] - let ⟨ht₁, ht₂, hhd⟩ := h - obtain ⟨a₁, t₁, rfl⟩ := exists_cons_of_ne_nil ht₁ - obtain ⟨a₂, t₂, rfl⟩ := exists_cons_of_ne_nil ht₂ - simp only [head?_cons, ne_eq, Option.some.injEq] at hhd - rw [← ne_eq] at hhd - simp [prefix_append_right_inj, not_and_of_not_left _ hhd, not_and_of_not_left _ hhd.symm] -termination_by l₁.length -decreasing_by - rename_i _₀ _l₁ _₁ _₂ _₃ _₄ _₅ _₆ _₇ _r _₈ _₉ _₁₀ _₁₁ _₁₂ _₁₃ _₁₄ _₁₅ _₁₆ _₁₇ _₁₈ _hl₁ _₁₉ _₂₀ _₂₁ - _₂₂ _₂₃ _₂₄ _₂₅ _₂₆ _₂₇ - clear _₀ _₁ _₂ _₃ _₄ _₅ _₆ _₇ _r _₈ _₉ _₁₀ _₁₁ _₁₂ _₁₃ _₁₄ _₁₅ _₁₆ _₁₇ _₁₈ _₁₉ _₂₀ _₂₁ _₂₂ _₂₃ _₂₄ - _₂₅ _₂₆ _₂₇ - subst _l₁ - simp + · obtain ⟨c₁, l₁, rfl⟩ := l₁.exists_cons_of_ne_nil (ne_nil_of_not_prefix h.1) + obtain ⟨c₂, l₂, rfl⟩ := l₂.exists_cons_of_ne_nil (ne_nil_of_not_prefix h.2) + simp only [cons_prefix_cons, not_and] at h + cases Decidable.em (c₁ = c₂) + · subst c₂ + simp only [forall_const] at h + let ⟨c₁', c₂', pre, suf₁, suf₂, hc, heq₁, heq₂⟩ := + not_prefix_and_not_prefix_symm_iff_exists.mp h + exact ⟨c₁', c₂', c₁::pre, suf₁, suf₂, hc, by simp [heq₁], by simp [heq₂]⟩ + · next hc => + exact ⟨c₁, c₂, [], l₁, l₂, hc, nil_append .., nil_append ..⟩ + · let ⟨c₁, c₂, pre, suf₁, suf₂, hc, heq₁, heq₂⟩ := h + rw [heq₁, heq₂] + simp [prefix_append_right_inj, cons_prefix_cons, hc, hc.symm] end From 75ec59078264d809f7f8008db5f6960de37cc500 Mon Sep 17 00:00:00 2001 From: Bulhwi Cha Date: Wed, 16 Oct 2024 18:54:43 +0900 Subject: [PATCH 17/20] Revert "feat: add `List.commonPrefix` and its lemmas" This reverts commit 6b39d441f8786488f68e3882c2736589f516c694. --- Batteries/Data/List/Lemmas.lean | 42 --------------------------------- 1 file changed, 42 deletions(-) diff --git a/Batteries/Data/List/Lemmas.lean b/Batteries/Data/List/Lemmas.lean index 78ec852c92..4f9bc11ed5 100644 --- a/Batteries/Data/List/Lemmas.lean +++ b/Batteries/Data/List/Lemmas.lean @@ -504,48 +504,6 @@ section variable [DecidableEq α] -/-- Returns the longest common prefix of two lists. -/ -def commonPrefix : (l₁ l₂ : List α) → List α - | [], _ => [] - | _, [] => [] - | a₁::l₁, a₂::l₂ => - if a₁ = a₂ then - a₁ :: (commonPrefix l₁ l₂) - else - [] - -theorem commonPrefix_prefix_left (l₁ l₂ : List α) : commonPrefix l₁ l₂ <+: l₁ := by - match l₁, l₂ with - | [], _ => simp [commonPrefix] - | _::_, [] => simp [commonPrefix] - | a₁::l₁, a₂::l₂ => - simp only [commonPrefix] - cases Decidable.em (a₁ = a₂) - · next h => - simp only [h, ↓reduceIte, cons_prefix_cons, true_and] - apply commonPrefix_prefix_left - · next h => - simp [h] - -theorem commonPrefix_prefix_right (l₁ l₂ : List α) : commonPrefix l₁ l₂ <+: l₂ := by - match l₁, l₂ with - | [], _ => simp [commonPrefix] - | _::_, [] => simp [commonPrefix] - | a₁::l₁, a₂::l₂ => - simp only [commonPrefix] - cases Decidable.em (a₁ = a₂) - · next h => - simp only [h, ↓reduceIte, cons_prefix_cons, true_and] - apply commonPrefix_prefix_right - · next h => - simp [h] - -theorem commonPrefix_append_append (p l₁ l₂ : List α) : - commonPrefix (p ++ l₁) (p ++ l₂) = p ++ commonPrefix l₁ l₂ := by - match p with - | [] => rfl - | a::p => simpa [commonPrefix] using commonPrefix_append_append p l₁ l₂ - theorem not_prefix_and_not_prefix_symm_iff_exists {l₁ l₂ : List α} : ¬l₁ <+: l₂ ∧ ¬l₂ <+: l₁ ↔ ∃ c₁ c₂ pre suf₁ suf₂, c₁ ≠ c₂ ∧ l₁ = pre ++ c₁ :: suf₁ ∧ l₂ = pre ++ c₂ :: suf₂ := by From f3a2b954f6c2cec8d7d262837d93db1e9530d8aa Mon Sep 17 00:00:00 2001 From: Bulhwi Cha Date: Wed, 16 Oct 2024 18:54:46 +0900 Subject: [PATCH 18/20] Revert "refactor: put theorem in section" This reverts commit 2d30498159047c1dac25593203c32b20e42df0e3. --- Batteries/Data/List/Lemmas.lean | 8 +------- 1 file changed, 1 insertion(+), 7 deletions(-) diff --git a/Batteries/Data/List/Lemmas.lean b/Batteries/Data/List/Lemmas.lean index 4f9bc11ed5..1e7a3f6d7a 100644 --- a/Batteries/Data/List/Lemmas.lean +++ b/Batteries/Data/List/Lemmas.lean @@ -500,11 +500,7 @@ theorem ne_nil_of_not_prefix (h : ¬l₁ <+: l₂) : l₁ ≠ [] := by intro heq simp [heq, nil_prefix] at h -section - -variable [DecidableEq α] - -theorem not_prefix_and_not_prefix_symm_iff_exists {l₁ l₂ : List α} : +theorem not_prefix_and_not_prefix_symm_iff_exists [DecidableEq α] {l₁ l₂ : List α} : ¬l₁ <+: l₂ ∧ ¬l₂ <+: l₁ ↔ ∃ c₁ c₂ pre suf₁ suf₂, c₁ ≠ c₂ ∧ l₁ = pre ++ c₁ :: suf₁ ∧ l₂ = pre ++ c₂ :: suf₂ := by constructor <;> intro h @@ -523,8 +519,6 @@ theorem not_prefix_and_not_prefix_symm_iff_exists {l₁ l₂ : List α} : rw [heq₁, heq₂] simp [prefix_append_right_inj, cons_prefix_cons, hc, hc.symm] -end - /-! ### drop -/ theorem disjoint_take_drop : ∀ {l : List α}, l.Nodup → m ≤ n → Disjoint (l.take m) (l.drop n) From 1d57ce4978e6f3e984c23541fcffb27f795a99aa Mon Sep 17 00:00:00 2001 From: Bulhwi Cha Date: Wed, 16 Oct 2024 18:54:47 +0900 Subject: [PATCH 19/20] Revert "refactor: remove implicit instances of theorem" This reverts commit f39e00ae79d3ece7fd768ff728f376b4c6238126. --- Batteries/Data/List/Lemmas.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Batteries/Data/List/Lemmas.lean b/Batteries/Data/List/Lemmas.lean index 1e7a3f6d7a..2cf150d3a0 100644 --- a/Batteries/Data/List/Lemmas.lean +++ b/Batteries/Data/List/Lemmas.lean @@ -500,9 +500,9 @@ theorem ne_nil_of_not_prefix (h : ¬l₁ <+: l₂) : l₁ ≠ [] := by intro heq simp [heq, nil_prefix] at h -theorem not_prefix_and_not_prefix_symm_iff_exists [DecidableEq α] {l₁ l₂ : List α} : - ¬l₁ <+: l₂ ∧ ¬l₂ <+: l₁ ↔ ∃ c₁ c₂ pre suf₁ suf₂, c₁ ≠ c₂ ∧ l₁ = pre ++ c₁ :: suf₁ ∧ - l₂ = pre ++ c₂ :: suf₂ := by +theorem not_prefix_and_not_prefix_symm_iff_exists [BEq α] [LawfulBEq α] [DecidableEq α] + {l₁ l₂ : List α} : ¬l₁ <+: l₂ ∧ ¬l₂ <+: l₁ ↔ ∃ c₁ c₂ pre suf₁ suf₂, c₁ ≠ c₂ ∧ + l₁ = pre ++ c₁ :: suf₁ ∧ l₂ = pre ++ c₂ :: suf₂ := by constructor <;> intro h · obtain ⟨c₁, l₁, rfl⟩ := l₁.exists_cons_of_ne_nil (ne_nil_of_not_prefix h.1) obtain ⟨c₂, l₂, rfl⟩ := l₂.exists_cons_of_ne_nil (ne_nil_of_not_prefix h.2) From 7c5ef34b0f0474332469b7e8dd33860ff26dff77 Mon Sep 17 00:00:00 2001 From: Bulhwi Cha Date: Wed, 16 Oct 2024 18:55:37 +0900 Subject: [PATCH 20/20] chore: remove theorem I moved the theorem to another pull request: https://github.com/leanprover-community/batteries/pull/994. --- Batteries/Data/List/Lemmas.lean | 19 ------------------- 1 file changed, 19 deletions(-) diff --git a/Batteries/Data/List/Lemmas.lean b/Batteries/Data/List/Lemmas.lean index 2cf150d3a0..e2b33809d4 100644 --- a/Batteries/Data/List/Lemmas.lean +++ b/Batteries/Data/List/Lemmas.lean @@ -500,25 +500,6 @@ theorem ne_nil_of_not_prefix (h : ¬l₁ <+: l₂) : l₁ ≠ [] := by intro heq simp [heq, nil_prefix] at h -theorem not_prefix_and_not_prefix_symm_iff_exists [BEq α] [LawfulBEq α] [DecidableEq α] - {l₁ l₂ : List α} : ¬l₁ <+: l₂ ∧ ¬l₂ <+: l₁ ↔ ∃ c₁ c₂ pre suf₁ suf₂, c₁ ≠ c₂ ∧ - l₁ = pre ++ c₁ :: suf₁ ∧ l₂ = pre ++ c₂ :: suf₂ := by - constructor <;> intro h - · obtain ⟨c₁, l₁, rfl⟩ := l₁.exists_cons_of_ne_nil (ne_nil_of_not_prefix h.1) - obtain ⟨c₂, l₂, rfl⟩ := l₂.exists_cons_of_ne_nil (ne_nil_of_not_prefix h.2) - simp only [cons_prefix_cons, not_and] at h - cases Decidable.em (c₁ = c₂) - · subst c₂ - simp only [forall_const] at h - let ⟨c₁', c₂', pre, suf₁, suf₂, hc, heq₁, heq₂⟩ := - not_prefix_and_not_prefix_symm_iff_exists.mp h - exact ⟨c₁', c₂', c₁::pre, suf₁, suf₂, hc, by simp [heq₁], by simp [heq₂]⟩ - · next hc => - exact ⟨c₁, c₂, [], l₁, l₂, hc, nil_append .., nil_append ..⟩ - · let ⟨c₁, c₂, pre, suf₁, suf₂, hc, heq₁, heq₂⟩ := h - rw [heq₁, heq₂] - simp [prefix_append_right_inj, cons_prefix_cons, hc, hc.symm] - /-! ### drop -/ theorem disjoint_take_drop : ∀ {l : List α}, l.Nodup → m ≤ n → Disjoint (l.take m) (l.drop n)