From fce82eba400ea282ebc8d29bc9ba55727647c9a6 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Thu, 11 Jul 2024 08:19:12 +1000 Subject: [PATCH] feat: further theorems for List.erase (#4723) --- src/Init/Data/List/Lemmas.lean | 274 +++++++++++++++++++++++++++++---- src/Init/Data/Nat/Basic.lean | 7 + src/Init/PropLemmas.lean | 2 + 3 files changed, 253 insertions(+), 30 deletions(-) diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean index ef36ef7d22..61e75805c4 100644 --- a/src/Init/Data/List/Lemmas.lean +++ b/src/Init/Data/List/Lemmas.lean @@ -350,6 +350,26 @@ theorem forall_mem_cons {p : α → Prop} {a : α} {l : List α} : theorem forall_mem_ne {a : α} {l : List α} : (∀ a' : α, a' ∈ l → ¬a = a') ↔ a ∉ l := ⟨fun h m => h _ m rfl, fun h _ m e => h (e.symm ▸ m)⟩ +@[simp] +theorem forall_mem_ne' {a : α} {l : List α} : (∀ a' : α, a' ∈ l → ¬a' = a) ↔ a ∉ l := + ⟨fun h m => h _ m rfl, fun h _ m e => h (e.symm ▸ m)⟩ + +@[simp] +theorem any_beq [BEq α] [LawfulBEq α] {l : List α} : (l.any fun x => a == x) ↔ a ∈ l := by + induction l <;> simp_all + +@[simp] +theorem any_beq' [BEq α] [LawfulBEq α] {l : List α} : (l.any fun x => x == a) ↔ a ∈ l := by + induction l <;> simp_all [eq_comm (a := a)] + +@[simp] +theorem all_bne [BEq α] [LawfulBEq α] {l : List α} : (l.all fun x => a != x) ↔ a ∉ l := by + induction l <;> simp_all + +@[simp] +theorem all_bne' [BEq α] [LawfulBEq α] {l : List α} : (l.all fun x => x != a) ↔ a ∉ l := by + induction l <;> simp_all [eq_comm (a := a)] + theorem exists_mem_nil (p : α → Prop) : ¬ (∃ x, ∃ _ : x ∈ @nil α, p x) := nofun theorem forall_mem_nil (p : α → Prop) : ∀ (x) (_ : x ∈ @nil α), p x := nofun @@ -932,10 +952,10 @@ theorem forall_mem_map_iff {f : α → β} {l : List α} {P : β → Prop} : /-! ### filter -/ -@[simp] theorem filter_cons_of_pos {p : α → Bool} {a : α} (l) (pa : p a) : +@[simp] theorem filter_cons_of_pos {p : α → Bool} {a : α} {l} (pa : p a) : filter p (a :: l) = a :: filter p l := by rw [filter, pa] -@[simp] theorem filter_cons_of_neg {p : α → Bool} {a : α} (l) (pa : ¬ p a) : +@[simp] theorem filter_cons_of_neg {p : α → Bool} {a : α} {l} (pa : ¬ p a) : filter p (a :: l) = filter p l := by rw [filter, eq_false_of_ne_true pa] theorem filter_cons : @@ -1030,10 +1050,10 @@ theorem head_filter_of_pos {p : α → Bool} {l : List α} (w : l ≠ []) (h : p /-! ### filterMap -/ -@[simp] theorem filterMap_cons_none {f : α → Option β} (a : α) (l : List α) (h : f a = none) : +@[simp] theorem filterMap_cons_none {f : α → Option β} {a : α} {l : List α} (h : f a = none) : filterMap f (a :: l) = filterMap f l := by simp only [filterMap, h] -@[simp] theorem filterMap_cons_some (f : α → Option β) (a : α) (l : List α) {b : β} (h : f a = some b) : +@[simp] theorem filterMap_cons_some {f : α → Option β} {a : α} {l : List α} {b : β} (h : f a = some b) : filterMap f (a :: l) = b :: filterMap f l := by simp only [filterMap, h] @[simp] @@ -2005,10 +2025,26 @@ theorem takeWhile_cons (p : α → Bool) (a : α) (l : List α) : simp only [takeWhile] by_cases h: p a <;> simp [h] +@[simp] theorem takeWhile_cons_of_pos {p : α → Bool} {a : α} {l : List α} (h : p a) : + (a :: l).takeWhile p = a :: l.takeWhile p := by + simp [takeWhile_cons, h] + +@[simp] theorem takeWhile_cons_of_neg {p : α → Bool} {a : α} {l : List α} (h : ¬ p a) : + (a :: l).takeWhile p = [] := by + simp [takeWhile_cons, h] + theorem dropWhile_cons : (x :: xs : List α).dropWhile p = if p x then xs.dropWhile p else x :: xs := by split <;> simp_all [dropWhile] +@[simp] theorem dropWhile_cons_of_pos {a : α} {l : List α} (h : p a) : + (a :: l).dropWhile p = l.dropWhile p := by + simp [dropWhile_cons, h] + +@[simp] theorem dropWhile_cons_of_neg {a : α} {l : List α} (h : ¬ p a) : + (a :: l).dropWhile p = a :: l := by + simp [dropWhile_cons, h] + theorem head?_takeWhile (p : α → Bool) (l : List α) : (l.takeWhile p).head? = l.head?.filter p := by cases l with | nil => rfl @@ -2058,6 +2094,24 @@ theorem dropWhile_map (f : α → β) (p : β → Bool) (l : List α) : | [] => rfl | x :: xs => by simp [takeWhile, dropWhile]; cases p x <;> simp [takeWhile_append_dropWhile p xs] +theorem takeWhile_append {xs ys : List α} : + (xs ++ ys).takeWhile p = + if (xs.takeWhile p).length = xs.length then xs ++ ys.takeWhile p else xs.takeWhile p := by + induction xs with + | nil => simp + | cons x xs ih => + simp only [cons_append, takeWhile_cons] + split + · simp_all only [length_cons, add_one_inj] + split <;> rfl + · simp_all + +@[simp] theorem takeWhile_append_of_pos {p : α → Bool} {l₁ l₂ : List α} (h : ∀ a ∈ l₁, p a) : + (l₁ ++ l₂).takeWhile p = l₁ ++ l₂.takeWhile p := by + induction l₁ with + | nil => simp + | cons x xs ih => simp_all [takeWhile_cons] + theorem dropWhile_append {xs ys : List α} : (xs ++ ys).dropWhile p = if (xs.dropWhile p).isEmpty then ys.dropWhile p else xs.dropWhile p ++ ys := by @@ -2067,6 +2121,12 @@ theorem dropWhile_append {xs ys : List α} : simp only [cons_append, dropWhile_cons] split <;> simp_all +@[simp] theorem dropWhile_append_of_pos {p : α → Bool} {l₁ l₂ : List α} (h : ∀ a ∈ l₁, p a) : + (l₁ ++ l₂).dropWhile p = l₂.dropWhile p := by + induction l₁ with + | nil => simp + | cons x xs ih => simp_all [dropWhile_cons] + @[simp] theorem takeWhile_replicate_eq_filter (p : α → Bool) : (replicate n a).takeWhile p = (replicate n a).filter p := by induction n with @@ -2317,6 +2377,9 @@ theorem Sublist.eq_of_length : l₁ <+ l₂ → length l₁ = length l₂ → l theorem Sublist.eq_of_length_le (s : l₁ <+ l₂) (h : length l₂ ≤ length l₁) : l₁ = l₂ := s.eq_of_length <| Nat.le_antisymm s.length_le h +theorem Sublist.length_eq (s : l₁ <+ l₂) : length l₁ = length l₂ ↔ l₁ = l₂ := + ⟨s.eq_of_length, congrArg _⟩ + protected theorem Sublist.map (f : α → β) {l₁ l₂} (s : l₁ <+ l₂) : map f l₁ <+ map f l₂ := by induction s with | slnil => simp @@ -2824,10 +2887,10 @@ end insert theorem eraseP_cons (a : α) (l : List α) : (a :: l).eraseP p = bif p a then l else a :: l.eraseP p := rfl -@[simp] theorem eraseP_cons_of_pos {l : List α} (p) (h : p a) : (a :: l).eraseP p = l := by +@[simp] theorem eraseP_cons_of_pos {l : List α} {p} (h : p a) : (a :: l).eraseP p = l := by simp [eraseP_cons, h] -@[simp] theorem eraseP_cons_of_neg {l : List α} (p) (h : ¬p a) : +@[simp] theorem eraseP_cons_of_neg {l : List α} {p} (h : ¬p a) : (a :: l).eraseP p = a :: l.eraseP p := by simp [eraseP_cons, h] theorem eraseP_of_forall_not {l : List α} (h : ∀ a, a ∈ l → ¬p a) : l.eraseP p = l := by @@ -2858,22 +2921,18 @@ theorem exists_or_eq_self_of_eraseP (p) (l : List α) : .inl (eraseP_of_forall_not (h ⟨·, ·, ·⟩)) @[simp] theorem length_eraseP_of_mem (al : a ∈ l) (pa : p a) : - length (l.eraseP p) = Nat.pred (length l) := by + length (l.eraseP p) = length l - 1 := by let ⟨_, l₁, l₂, _, _, e₁, e₂⟩ := exists_of_eraseP al pa rw [e₂]; simp [length_append, e₁]; rfl -theorem eraseP_append_left {a : α} (pa : p a) : - ∀ {l₁ : List α} l₂, a ∈ l₁ → (l₁++l₂).eraseP p = l₁.eraseP p ++ l₂ - | x :: xs, l₂, h => by - by_cases h' : p x <;> simp [h'] - rw [eraseP_append_left pa l₂ ((mem_cons.1 h).resolve_left (mt _ h'))] - intro | rfl => exact pa - -theorem eraseP_append_right : - ∀ {l₁ : List α} l₂, (∀ b ∈ l₁, ¬p b) → eraseP p (l₁++l₂) = l₁ ++ l₂.eraseP p - | [], l₂, _ => rfl - | x :: xs, l₂, h => by - simp [(forall_mem_cons.1 h).1, eraseP_append_right _ (forall_mem_cons.1 h).2] +theorem length_eraseP {l : List α} : (l.eraseP p).length = if l.any p then l.length - 1 else l.length := by + split <;> rename_i h + · simp only [any_eq_true] at h + obtain ⟨x, m, h⟩ := h + simp [length_eraseP_of_mem m h] + · simp only [any_eq_true] at h + rw [eraseP_of_forall_not] + simp_all theorem eraseP_sublist (l : List α) : l.eraseP p <+ l := by match exists_or_eq_self_of_eraseP p l with @@ -2904,10 +2963,126 @@ theorem mem_of_mem_eraseP {l : List α} : a ∈ l.eraseP p → a ∈ l := (erase have : a ≠ c := fun h => (h ▸ pa).elim h₂ simp [this] at al; simp [al] +@[simp] theorem eraseP_eq_self_iff {p} {l : List α} : l.eraseP p = l ↔ ∀ a ∈ l, ¬ p a := by + rw [← Sublist.length_eq (eraseP_sublist l), length_eraseP] + split <;> rename_i h + · simp only [any_eq_true, length_eq_zero] at h + constructor + · intro; simp_all [Nat.sub_one_eq_self] + · intro; obtain ⟨x, m, h⟩ := h; simp_all + · simp_all + theorem eraseP_map (f : β → α) : ∀ (l : List β), (map f l).eraseP p = map f (l.eraseP (p ∘ f)) | [] => rfl | b::l => by by_cases h : p (f b) <;> simp [h, eraseP_map f l, eraseP_cons_of_pos] +theorem eraseP_filterMap (f : α → Option β) : ∀ (l : List α), + (filterMap f l).eraseP p = filterMap f (l.eraseP (fun x => match f x with | some y => p y | none => false)) + | [] => rfl + | a::l => by + rw [filterMap_cons, eraseP_cons] + split <;> rename_i h + · simp [h, eraseP_filterMap] + · rename_i b + rw [h, eraseP_cons] + by_cases w : p b + · simp [w] + · simp only [w, cond_false] + rw [filterMap_cons_some h, eraseP_filterMap] + +theorem eraseP_filter (f : α → Bool) (l : List α) : + (filter f l).eraseP p = filter f (l.eraseP (fun x => p x && f x)) := by + rw [← filterMap_eq_filter, eraseP_filterMap] + congr + ext x + simp only [Option.guard] + split <;> split at * <;> simp_all + +theorem eraseP_append_left {a : α} (pa : p a) : + ∀ {l₁ : List α} l₂, a ∈ l₁ → (l₁++l₂).eraseP p = l₁.eraseP p ++ l₂ + | x :: xs, l₂, h => by + by_cases h' : p x <;> simp [h'] + rw [eraseP_append_left pa l₂ ((mem_cons.1 h).resolve_left (mt _ h'))] + intro | rfl => exact pa + +theorem eraseP_append_right : + ∀ {l₁ : List α} l₂, (∀ b ∈ l₁, ¬p b) → eraseP p (l₁++l₂) = l₁ ++ l₂.eraseP p + | [], l₂, _ => rfl + | x :: xs, l₂, h => by + simp [(forall_mem_cons.1 h).1, eraseP_append_right _ (forall_mem_cons.1 h).2] + +theorem eraseP_append (l₁ l₂ : List α) : + (l₁ ++ l₂).eraseP p = if l₁.any p then l₁.eraseP p ++ l₂ else l₁ ++ l₂.eraseP p := by + split <;> rename_i h + · simp only [any_eq_true] at h + obtain ⟨x, m, h⟩ := h + rw [eraseP_append_left h _ m] + · simp only [any_eq_true] at h + rw [eraseP_append_right _] + simp_all + +theorem eraseP_eq_iff {p} {l : List α} : + l.eraseP p = l' ↔ + ((∀ a ∈ l, ¬ p a) ∧ l = l') ∨ + ∃ a l₁ l₂, (∀ b ∈ l₁, ¬ p b) ∧ p a ∧ l = l₁ ++ a :: l₂ ∧ l' = l₁ ++ l₂ := by + cases exists_or_eq_self_of_eraseP p l with + | inl h => + constructor + · intro h' + left + exact ⟨eraseP_eq_self_iff.1 h, by simp_all⟩ + · rintro (⟨-, rfl⟩ | ⟨a, l₁, l₂, h₁, h₂, rfl, rfl⟩) + · assumption + · rw [eraseP_append_right _ h₁, eraseP_cons_of_pos h₂] + | inr h => + obtain ⟨a, l₁, l₂, h₁, h₂, w₁, w₂⟩ := h + rw [w₂] + subst w₁ + constructor + · rintro rfl + right + refine ⟨a, l₁, l₂, ?_⟩ + simp_all + · rintro (h | h) + · simp_all + · obtain ⟨a', l₁', l₂', h₁', h₂', h, rfl⟩ := h + have p : l₁ = l₁' := by + have q : l₁ = takeWhile (fun x => !p x) (l₁ ++ a :: l₂) := by + rw [takeWhile_append_of_pos (by simp_all), + takeWhile_cons_of_neg (by simp [h₂]), append_nil] + have q' : l₁' = takeWhile (fun x => !p x) (l₁' ++ a' :: l₂') := by + rw [takeWhile_append_of_pos (by simpa using h₁'), + takeWhile_cons_of_neg (by simp [h₂']), append_nil] + simp [h] at q + rw [q', q] + subst p + simp_all + +@[simp] theorem eraseP_replicate_of_pos {n : Nat} {a : α} (h : p a) : + (replicate n a).eraseP p = replicate (n - 1) a := by + cases n <;> simp [replicate_succ, h] + +@[simp] theorem eraseP_replicate_of_neg {n : Nat} {a : α} (h : ¬p a) : + (replicate n a).eraseP p = replicate n a := by + rw [eraseP_of_forall_not (by simp_all)] + +theorem Nodup.eraseP [BEq α] [LawfulBEq α] (p) : Nodup l → Nodup (l.eraseP p) := + Nodup.sublist <| eraseP_sublist _ + +theorem eraseP_comm {l : List α} (h : ∀ a ∈ l, ¬ p a ∨ ¬ q a) : + (l.eraseP p).eraseP q = (l.eraseP q).eraseP p := by + induction l with + | nil => rfl + | cons a l ih => + simp only [eraseP_cons] + by_cases h₁ : p a + · by_cases h₂ : q a + · simp_all + · simp [h₁, h₂, ih (fun b m => h b (mem_cons_of_mem _ m))] + · by_cases h₂ : q a + · simp [h₁, h₂, ih (fun b m => h b (mem_cons_of_mem _ m))] + · simp [h₁, h₂, ih (fun b m => h b (mem_cons_of_mem _ m))] + /-! ### erase -/ section erase variable [BEq α] @@ -2915,7 +3090,7 @@ variable [BEq α] @[simp] theorem erase_cons_head [LawfulBEq α] (a : α) (l : List α) : (a :: l).erase a = l := by simp [erase_cons] -@[simp] theorem erase_cons_tail {a b : α} (l : List α) (h : ¬(b == a)) : +@[simp] theorem erase_cons_tail {a b : α} {l : List α} (h : ¬(b == a)) : (b :: l).erase a = b :: l.erase a := by simp only [erase_cons, if_neg h] theorem erase_of_not_mem [LawfulBEq α] {a : α} : ∀ {l : List α}, a ∉ l → l.erase a = l @@ -2945,14 +3120,13 @@ theorem exists_erase_eq [LawfulBEq α] {a : α} {l : List α} (h : a ∈ l) : length (l.erase a) = length l - 1 := by rw [erase_eq_eraseP]; exact length_eraseP_of_mem h (beq_self_eq_true a) -theorem erase_sublist (a : α) (l : List α) : l.erase a <+ l := by - induction l with - | nil => simp - | cons b l ih => - simp only [erase_cons] - split - · exact sublist_cons b l - · exact cons_sublist_cons.mpr ih +theorem length_erase [LawfulBEq α] (a : α) (l : List α) : + length (l.erase a) = if a ∈ l then length l - 1 else length l := by + rw [erase_eq_eraseP, length_eraseP] + split <;> split <;> simp_all + +theorem erase_sublist (a : α) (l : List α) : l.erase a <+ l := + erase_eq_eraseP' a l ▸ eraseP_sublist .. theorem erase_subset (a : α) (l : List α) : l.erase a ⊆ l := (erase_sublist a l).subset @@ -2965,6 +3139,28 @@ theorem mem_of_mem_erase {a b : α} {l : List α} (h : a ∈ l.erase b) : a ∈ a ∈ l.erase b ↔ a ∈ l := erase_eq_eraseP b l ▸ mem_eraseP_of_neg (mt eq_of_beq ab.symm) +@[simp] theorem erase_eq_self_iff [LawfulBEq α] {l : List α} : l.erase a = l ↔ a ∉ l := by + rw [erase_eq_eraseP', eraseP_eq_self_iff] + simp + +theorem erase_filter [LawfulBEq α] (f : α → Bool) (l : List α) : + (filter f l).erase a = filter f (l.erase a) := by + induction l with + | nil => rfl + | cons x xs ih => + by_cases h : a = x + · rw [erase_cons] + simp only [h, beq_self_eq_true, ↓reduceIte] + rw [filter_cons] + split + · rw [erase_cons_head] + · rw [erase_of_not_mem] + simp_all [mem_filter] + · rw [erase_cons_tail (by simpa using Ne.symm h), filter_cons, filter_cons] + split + · rw [erase_cons_tail (by simpa using Ne.symm h), ih] + · rw [ih] + theorem erase_append_left [LawfulBEq α] {l₁ : List α} (l₂) (h : a ∈ l₁) : (l₁ ++ l₂).erase a = l₁.erase a ++ l₂ := by simp [erase_eq_eraseP]; exact eraseP_append_left (beq_self_eq_true a) l₂ h @@ -2974,6 +3170,10 @@ theorem erase_append_right [LawfulBEq α] {a : α} {l₁ : List α} (l₂ : List rw [erase_eq_eraseP, erase_eq_eraseP, eraseP_append_right] intros b h' h''; rw [eq_of_beq h''] at h; exact h h' +theorem erase_append [LawfulBEq α] {a : α} {l₁ l₂ : List α} : + (l₁ ++ l₂).erase a = if a ∈ l₁ then l₁.erase a ++ l₂ else l₁ ++ l₂.erase a := by + simp [erase_eq_eraseP, eraseP_append] + theorem erase_comm [LawfulBEq α] (a b : α) (l : List α) : (l.erase a).erase b = (l.erase b).erase a := by if ab : a == b then rw [eq_of_beq ab] else ?_ @@ -2988,7 +3188,21 @@ theorem erase_comm [LawfulBEq α] (a b : α) (l : List α) : erase_append_right _ (mt mem_of_mem_erase ha'), erase_cons_head] else rw [erase_append_right _ h₁, erase_append_right _ h₁, erase_append_right _ ha', - erase_cons_tail _ ab, erase_cons_head] + erase_cons_tail ab, erase_cons_head] + +theorem erase_eq_iff [LawfulBEq α] {a : α} {l : List α} : + l.erase a = l' ↔ + (a ∉ l ∧ l = l') ∨ + ∃ l₁ l₂, a ∉ l₁ ∧ l = l₁ ++ a :: l₂ ∧ l' = l₁ ++ l₂ := by + rw [erase_eq_eraseP', eraseP_eq_iff] + simp only [beq_iff_eq, forall_mem_ne', exists_and_left] + constructor + · rintro (⟨h, rfl⟩ | ⟨a', l', h, rfl, x, rfl, rfl⟩) + · left; simp_all + · right; refine ⟨l', h, x, by simp⟩ + · rintro (⟨h, rfl⟩ | ⟨l₁, h, x, rfl, rfl⟩) + · left; simp_all + · right; refine ⟨a, l₁, h, by simp⟩ @[simp] theorem erase_replicate_self [LawfulBEq α] {a : α} : (replicate n a).erase a = replicate (n - 1) a := by @@ -3006,7 +3220,7 @@ theorem Nodup.erase_eq_filter [BEq α] [LawfulBEq α] {l} (d : Nodup l) (a : α) rename_i b l by_cases h : b = a · subst h - rw [erase_cons_head, filter_cons_of_neg _ (by simp)] + rw [erase_cons_head, filter_cons_of_neg (by simp)] apply Eq.symm rw [filter_eq_self] simpa [@eq_comm α] using m diff --git a/src/Init/Data/Nat/Basic.lean b/src/Init/Data/Nat/Basic.lean index eacd583453..967a7cd24d 100644 --- a/src/Init/Data/Nat/Basic.lean +++ b/src/Init/Data/Nat/Basic.lean @@ -634,6 +634,10 @@ theorem succ_lt_succ_iff : succ a < succ b ↔ a < b := ⟨lt_of_succ_lt_succ, s theorem add_one_inj : a + 1 = b + 1 ↔ a = b := succ_inj' +theorem ne_add_one (n : Nat) : n ≠ n + 1 := fun h => by cases h + +theorem add_one_ne (n : Nat) : n + 1 ≠ n := fun h => by cases h + theorem add_one_le_add_one_iff : a + 1 ≤ b + 1 ↔ a ≤ b := succ_le_succ_iff theorem add_one_lt_add_one_iff : a + 1 < b + 1 ↔ a < b := succ_lt_succ_iff @@ -815,6 +819,9 @@ protected theorem pred_succ (n : Nat) : pred n.succ = n := rfl @[simp] protected theorem zero_sub_one : 0 - 1 = 0 := rfl @[simp] protected theorem add_one_sub_one (n : Nat) : n + 1 - 1 = n := rfl +theorem sub_one_eq_self (n : Nat) : n - 1 = n ↔ n = 0 := by cases n <;> simp [ne_add_one] +theorem eq_self_sub_one (n : Nat) : n = n - 1 ↔ n = 0 := by cases n <;> simp [add_one_ne] + theorem succ_pred {a : Nat} (h : a ≠ 0) : a.pred.succ = a := by induction a with | zero => contradiction diff --git a/src/Init/PropLemmas.lean b/src/Init/PropLemmas.lean index 726654ce72..ef47f75ce4 100644 --- a/src/Init/PropLemmas.lean +++ b/src/Init/PropLemmas.lean @@ -295,6 +295,8 @@ theorem not_forall_of_exists_not {p : α → Prop} : (∃ x, ¬p x) → ¬∀ x, @[simp] theorem exists_eq_left' : (∃ a, a' = a ∧ p a) ↔ p a' := by simp [@eq_comm _ a'] +@[simp] theorem exists_eq_right' : (∃ a, p a ∧ a' = a) ↔ p a' := by simp [@eq_comm _ a'] + @[simp] theorem forall_eq_or_imp : (∀ a, a = a' ∨ q a → p a) ↔ p a' ∧ ∀ a, q a → p a := by simp only [or_imp, forall_and, forall_eq]