From fa4a4df5934967b252bcf8270eb6dd32f0b40cdf Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Thu, 22 Aug 2024 20:23:14 +1000 Subject: [PATCH 1/2] feat: more lemmas about List.append --- src/Init/Data/List/Nat/Basic.lean | 34 ++++++++++++++++++++++ src/Init/Data/List/Nat/Sublist.lean | 45 +++++++++++++++++++++++++++++ 2 files changed, 79 insertions(+) diff --git a/src/Init/Data/List/Nat/Basic.lean b/src/Init/Data/List/Nat/Basic.lean index 849f2a8cdc1e..4d8184321b4c 100644 --- a/src/Init/Data/List/Nat/Basic.lean +++ b/src/Init/Data/List/Nat/Basic.lean @@ -25,6 +25,40 @@ theorem length_filter_lt_length_iff_exists (l) : simpa [length_eq_countP_add_countP p l, countP_eq_length_filter] using countP_pos (fun x => ¬p x) (l := l) +/-! ### append -/ + +@[simp] theorem append_left_eq_self (xs ys : List α) : xs ++ ys = ys ↔ xs = [] := by + constructor + · intro h + replace h := congrArg length h + simp_all [Nat.add_left_eq_self] + · rintro rfl + rfl + +@[simp] theorem append_right_eq_self (xs ys : List α) : xs ++ ys = xs ↔ ys = [] := by + constructor + · intro h + replace h := congrArg length h + simp_all [Nat.add_right_eq_self] + · rintro rfl + simp + +@[simp] theorem self_eq_append_right (xs ys : List α) : xs = xs ++ ys ↔ ys = [] := by + constructor + · intro h + replace h := congrArg length h + simp_all [Nat.self_eq_add_right] + · rintro rfl + simp + +@[simp] theorem self_eq_append_left (xs ys : List α) : xs = ys ++ xs ↔ ys = [] := by + constructor + · intro h + replace h := congrArg length h + simp_all [Nat.self_eq_add_left] + · rintro rfl + simp + /-! ### reverse -/ theorem getElem_eq_getElem_reverse {l : List α} {i} (h : i < l.length) : diff --git a/src/Init/Data/List/Nat/Sublist.lean b/src/Init/Data/List/Nat/Sublist.lean index a371c0584c12..5e2af608f833 100644 --- a/src/Init/Data/List/Nat/Sublist.lean +++ b/src/Init/Data/List/Nat/Sublist.lean @@ -126,4 +126,49 @@ theorem prefix_take_le_iff {L : List α} (hm : m < L.length) : simp only [length_cons, Nat.succ_eq_add_one, Nat.add_lt_add_iff_right] at hm simp [← @IH n ls hm, Nat.min_eq_left, Nat.le_of_lt hm] +@[simp] theorem append_left_sublist_self (xs ys : List α) : xs ++ ys <+ ys ↔ xs = [] := by + constructor + · intro h + replace h := h.length_le + simp only [length_append] at h + have : xs.length = 0 := by omega + simp_all + · rintro rfl + simp +@[simp] theorem append_right_sublist_self (xs ys : List α) : xs ++ ys <+ xs ↔ ys = [] := by + constructor + · intro h + replace h := h.length_le + simp only [length_append] at h + have : ys.length = 0 := by omega + simp_all + · rintro rfl + simp + +theorem append_sublist_of_sublist_left (xs ys zs : List α) (h : zs <+ xs) : + xs ++ ys <+ zs ↔ ys = [] ∧ xs = zs := by + constructor + · intro h' + have hl := h.length_le + have hl' := h'.length_le + simp only [length_append] at hl' + have : ys.length = 0 := by omega + simp_all only [Nat.add_zero, length_eq_zero, true_and, append_nil] + exact Sublist.eq_of_length_le h' hl + · rintro ⟨rfl, rfl⟩ + simp + +theorem append_sublist_of_sublist_right (xs ys zs : List α) (h : zs <+ ys) : + xs ++ ys <+ zs ↔ xs = [] ∧ ys = zs := by + constructor + · intro h' + have hl := h.length_le + have hl' := h'.length_le + simp only [length_append] at hl' + have : xs.length = 0 := by omega + simp_all only [Nat.zero_add, length_eq_zero, true_and, append_nil] + exact Sublist.eq_of_length_le h' hl + · rintro ⟨rfl, rfl⟩ + simp + end List From e65cdfb77baf0fb05b81459874913d846d0a290e Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Thu, 22 Aug 2024 21:27:19 +1000 Subject: [PATCH 2/2] better --- src/Init/Data/List/Lemmas.lean | 12 +++++++++++ src/Init/Data/List/Nat/Basic.lean | 34 ------------------------------- 2 files changed, 12 insertions(+), 34 deletions(-) diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean index 07f8530d770e..a18c8d5c2cc4 100644 --- a/src/Init/Data/List/Lemmas.lean +++ b/src/Init/Data/List/Lemmas.lean @@ -1425,6 +1425,18 @@ theorem append_right_inj {t₁ t₂ : List α} (s) : s ++ t₁ = s ++ t₂ ↔ t theorem append_left_inj {s₁ s₂ : List α} (t) : s₁ ++ t = s₂ ++ t ↔ s₁ = s₂ := ⟨fun h => append_inj_left' h rfl, congrArg (· ++ _)⟩ +@[simp] theorem append_left_eq_self {x y : List α} : x ++ y = y ↔ x = [] := by + rw [← append_left_inj (s₁ := x), nil_append] + +@[simp] theorem self_eq_append_left {x y : List α} : y = x ++ y ↔ x = [] := by + rw [eq_comm, append_left_eq_self] + +@[simp] theorem append_right_eq_self {x y : List α} : x ++ y = x ↔ y = [] := by + rw [← append_right_inj (t₁ := y), append_nil] + +@[simp] theorem self_eq_append_right {x y : List α} : x = x ++ y ↔ y = [] := by + rw [eq_comm, append_right_eq_self] + @[simp] theorem append_eq_nil : p ++ q = [] ↔ p = [] ∧ q = [] := by cases p <;> simp diff --git a/src/Init/Data/List/Nat/Basic.lean b/src/Init/Data/List/Nat/Basic.lean index 4d8184321b4c..849f2a8cdc1e 100644 --- a/src/Init/Data/List/Nat/Basic.lean +++ b/src/Init/Data/List/Nat/Basic.lean @@ -25,40 +25,6 @@ theorem length_filter_lt_length_iff_exists (l) : simpa [length_eq_countP_add_countP p l, countP_eq_length_filter] using countP_pos (fun x => ¬p x) (l := l) -/-! ### append -/ - -@[simp] theorem append_left_eq_self (xs ys : List α) : xs ++ ys = ys ↔ xs = [] := by - constructor - · intro h - replace h := congrArg length h - simp_all [Nat.add_left_eq_self] - · rintro rfl - rfl - -@[simp] theorem append_right_eq_self (xs ys : List α) : xs ++ ys = xs ↔ ys = [] := by - constructor - · intro h - replace h := congrArg length h - simp_all [Nat.add_right_eq_self] - · rintro rfl - simp - -@[simp] theorem self_eq_append_right (xs ys : List α) : xs = xs ++ ys ↔ ys = [] := by - constructor - · intro h - replace h := congrArg length h - simp_all [Nat.self_eq_add_right] - · rintro rfl - simp - -@[simp] theorem self_eq_append_left (xs ys : List α) : xs = ys ++ xs ↔ ys = [] := by - constructor - · intro h - replace h := congrArg length h - simp_all [Nat.self_eq_add_left] - · rintro rfl - simp - /-! ### reverse -/ theorem getElem_eq_getElem_reverse {l : List α} {i} (h : i < l.length) :