From 603108e34c457a8644aade2da418b1d9213ed441 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 13 Jan 2025 13:00:49 +1100 Subject: [PATCH] feat: finish alignment of `List/Array/Vector.append` lemmas (#6617) This PR completes alignment of `List`/`Array`/`Vector` `append` lemmas. --- src/Init/Data/Array/Lemmas.lean | 218 +++++++++++++++++++++++++- src/Init/Data/List/Lemmas.lean | 149 ++++++++++-------- src/Init/Data/List/Zip.lean | 4 +- src/Init/Data/Vector/Lemmas.lean | 261 ++++++++++++++++++++++++++++--- 4 files changed, 535 insertions(+), 97 deletions(-) diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean index 3eee4ef437..7e0549addb 100644 --- a/src/Init/Data/Array/Lemmas.lean +++ b/src/Init/Data/Array/Lemmas.lean @@ -1504,14 +1504,20 @@ theorem filterMap_eq_push_iff {f : α → Option β} {l : Array α} {l' : Array · rintro ⟨⟨l₁⟩, a, ⟨l₂⟩, h₁, h₂, h₃, h₄⟩ refine ⟨l₂.reverse, a, l₁.reverse, by simp_all⟩ -/-! Content below this point has not yet been aligned with `List`. -/ - /-! ### singleton -/ @[simp] theorem singleton_def (v : α) : Array.singleton v = #[v] := rfl /-! ### append -/ +@[simp] theorem size_append (as bs : Array α) : (as ++ bs).size = as.size + bs.size := by + simp only [size, toList_append, List.length_append] + +@[simp] theorem append_push {as bs : Array α} {a : α} : as ++ bs.push a = (as ++ bs).push a := by + cases as + cases bs + simp + @[simp] theorem toArray_eq_append_iff {xs : List α} {as bs : Array α} : xs.toArray = as ++ bs ↔ xs = as.toList ++ bs.toList := by cases as @@ -1539,8 +1545,24 @@ theorem mem_append_left {a : α} {l₁ : Array α} (l₂ : Array α) (h : a ∈ theorem mem_append_right {a : α} (l₁ : Array α) {l₂ : Array α} (h : a ∈ l₂) : a ∈ l₁ ++ l₂ := mem_append.2 (Or.inr h) -@[simp] theorem size_append (as bs : Array α) : (as ++ bs).size = as.size + bs.size := by - simp only [size, toList_append, List.length_append] +theorem not_mem_append {a : α} {s t : Array α} (h₁ : a ∉ s) (h₂ : a ∉ t) : a ∉ s ++ t := + mt mem_append.1 $ not_or.mpr ⟨h₁, h₂⟩ + +/-- +See also `eq_push_append_of_mem`, which proves a stronger version +in which the initial array must not contain the element. +-/ +theorem append_of_mem {a : α} {l : Array α} (h : a ∈ l) : ∃ s t : Array α, l = s.push a ++ t := by + obtain ⟨s, t, w⟩ := List.append_of_mem (l := l.toList) (by simpa using h) + replace w := congrArg List.toArray w + refine ⟨s.toArray, t.toArray, by simp_all⟩ + +theorem mem_iff_append {a : α} {l : Array α} : a ∈ l ↔ ∃ s t : Array α, l = s.push a ++ t := + ⟨append_of_mem, fun ⟨s, t, e⟩ => e ▸ by simp⟩ + +theorem forall_mem_append {p : α → Prop} {l₁ l₂ : Array α} : + (∀ (x) (_ : x ∈ l₁ ++ l₂), p x) ↔ (∀ (x) (_ : x ∈ l₁), p x) ∧ (∀ (x) (_ : x ∈ l₂), p x) := by + simp only [mem_append, or_imp, forall_and] theorem empty_append (as : Array α) : #[] ++ as = as := by simp @@ -1599,6 +1621,194 @@ theorem getElem_of_append {l l₁ l₂ : Array α} (eq : l = l₁.push a ++ l₂ rw [← getElem?_eq_getElem, eq, getElem?_append_left (by simp; omega), ← h] simp +@[simp 1100] theorem append_singleton {a : α} {as : Array α} : as ++ #[a] = as.push a := by + cases as + simp + +theorem append_inj {s₁ s₂ t₁ t₂ : Array α} (h : s₁ ++ t₁ = s₂ ++ t₂) (hl : s₁.size = s₂.size) : + s₁ = s₂ ∧ t₁ = t₂ := by + rcases s₁ with ⟨s₁⟩ + rcases s₂ with ⟨s₂⟩ + rcases t₁ with ⟨t₁⟩ + rcases t₂ with ⟨t₂⟩ + simpa using List.append_inj (by simpa using h) (by simpa using hl) + +theorem append_inj_right {s₁ s₂ t₁ t₂ : Array α} + (h : s₁ ++ t₁ = s₂ ++ t₂) (hl : s₁.size = s₂.size) : t₁ = t₂ := + (append_inj h hl).right + +theorem append_inj_left {s₁ s₂ t₁ t₂ : Array α} + (h : s₁ ++ t₁ = s₂ ++ t₂) (hl : s₁.size = s₂.size) : s₁ = s₂ := + (append_inj h hl).left + +/-- Variant of `append_inj` instead requiring equality of the sizes of the second arrays. -/ +theorem append_inj' {s₁ s₂ t₁ t₂ : Array α} (h : s₁ ++ t₁ = s₂ ++ t₂) (hl : t₁.size = t₂.size) : + s₁ = s₂ ∧ t₁ = t₂ := + append_inj h <| @Nat.add_right_cancel _ t₁.size _ <| by + let hap := congrArg size h; simp only [size_append, ← hl] at hap; exact hap + +/-- Variant of `append_inj_right` instead requiring equality of the sizes of the second arrays. -/ +theorem append_inj_right' {s₁ s₂ t₁ t₂ : Array α} + (h : s₁ ++ t₁ = s₂ ++ t₂) (hl : t₁.size = t₂.size) : t₁ = t₂ := + (append_inj' h hl).right + +/-- Variant of `append_inj_left` instead requiring equality of the sizes of the second arrays. -/ +theorem append_inj_left' {s₁ s₂ t₁ t₂ : Array α} + (h : s₁ ++ t₁ = s₂ ++ t₂) (hl : t₁.size = t₂.size) : s₁ = s₂ := + (append_inj' h hl).left + +theorem append_right_inj {t₁ t₂ : Array α} (s) : s ++ t₁ = s ++ t₂ ↔ t₁ = t₂ := + ⟨fun h => append_inj_right h rfl, congrArg _⟩ + +theorem append_left_inj {s₁ s₂ : Array α} (t) : s₁ ++ t = s₂ ++ t ↔ s₁ = s₂ := + ⟨fun h => append_inj_left' h rfl, congrArg (· ++ _)⟩ + +@[simp] theorem append_left_eq_self {x y : Array α} : x ++ y = y ↔ x = #[] := by + rw [← append_left_inj (s₁ := x), nil_append] + +@[simp] theorem self_eq_append_left {x y : Array α} : y = x ++ y ↔ x = #[] := by + rw [eq_comm, append_left_eq_self] + +@[simp] theorem append_right_eq_self {x y : Array α} : x ++ y = x ↔ y = #[] := by + rw [← append_right_inj (t₁ := y), append_nil] + +@[simp] theorem self_eq_append_right {x y : Array α} : x = x ++ y ↔ y = #[] := by + rw [eq_comm, append_right_eq_self] + +@[simp] theorem append_eq_empty_iff : p ++ q = #[] ↔ p = #[] ∧ q = #[] := by + cases p <;> simp + +@[simp] theorem empty_eq_append_iff : #[] = a ++ b ↔ a = #[] ∧ b = #[] := by + rw [eq_comm, append_eq_empty_iff] + +theorem append_ne_empty_of_left_ne_empty {s : Array α} (h : s ≠ #[]) (t : Array α) : + s ++ t ≠ #[] := by + simp_all + +theorem append_ne_empty_of_right_ne_empty (s : Array α) : t ≠ #[] → s ++ t ≠ #[] := by + simp_all + +theorem append_eq_push_iff {a b c : Array α} {x : α} : + a ++ b = c.push x ↔ (b = #[] ∧ a = c.push x) ∨ (∃ b', b = b'.push x ∧ c = a ++ b') := by + rcases a with ⟨a⟩ + rcases b with ⟨b⟩ + rcases c with ⟨c⟩ + simp only [List.append_toArray, List.push_toArray, mk.injEq, List.append_eq_append_iff, + toArray_eq_append_iff] + constructor + · rintro (⟨a', rfl, rfl⟩ | ⟨b', rfl, h⟩) + · right; exact ⟨⟨a'⟩, by simp⟩ + · rw [List.singleton_eq_append_iff] at h + obtain (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩) := h + · right; exact ⟨#[], by simp⟩ + · left; simp + · rintro (⟨rfl, rfl⟩ | ⟨b', h, rfl⟩) + · right; exact ⟨[x], by simp⟩ + · left; refine ⟨b'.toList, ?_⟩ + replace h := congrArg Array.toList h + simp_all + +theorem push_eq_append_iff {a b c : Array α} {x : α} : + c.push x = a ++ b ↔ (b = #[] ∧ a = c.push x) ∨ (∃ b', b = b'.push x ∧ c = a ++ b') := by + rw [eq_comm, append_eq_push_iff] + +theorem append_eq_singleton_iff {a b : Array α} {x : α} : + a ++ b = #[x] ↔ (a = #[] ∧ b = #[x]) ∨ (a = #[x] ∧ b = #[]) := by + rcases a with ⟨a⟩ + rcases b with ⟨b⟩ + simp only [List.append_toArray, mk.injEq, List.append_eq_singleton_iff, toArray_eq_append_iff] + +theorem singleton_eq_append_iff {a b : Array α} {x : α} : + #[x] = a ++ b ↔ (a = #[] ∧ b = #[x]) ∨ (a = #[x] ∧ b = #[]) := by + rw [eq_comm, append_eq_singleton_iff] + +theorem append_eq_append_iff {a b c d : Array α} : + a ++ b = c ++ d ↔ (∃ a', c = a ++ a' ∧ b = a' ++ d) ∨ ∃ c', a = c ++ c' ∧ d = c' ++ b := by + rcases a with ⟨a⟩ + rcases b with ⟨b⟩ + rcases c with ⟨c⟩ + rcases d with ⟨d⟩ + simp only [List.append_toArray, mk.injEq, List.append_eq_append_iff, toArray_eq_append_iff] + constructor + · rintro (⟨a', rfl, rfl⟩ | ⟨c', rfl, rfl⟩) + · left; exact ⟨⟨a'⟩, by simp⟩ + · right; exact ⟨⟨c'⟩, by simp⟩ + · rintro (⟨a', rfl, rfl⟩ | ⟨c', rfl, rfl⟩) + · left; exact ⟨a'.toList, by simp⟩ + · right; exact ⟨c'.toList, by simp⟩ + +theorem set_append {s t : Array α} {i : Nat} {x : α} (h : i < (s ++ t).size) : + (s ++ t).set i x = + if h' : i < s.size then + s.set i x ++ t + else + s ++ t.set (i - s.size) x (by simp at h; omega) := by + rcases s with ⟨s⟩ + rcases t with ⟨t⟩ + simp only [List.append_toArray, List.set_toArray, List.set_append] + split <;> simp + +@[simp] theorem set_append_left {s t : Array α} {i : Nat} {x : α} (h : i < s.size) : + (s ++ t).set i x (by simp; omega) = s.set i x ++ t := by + simp [set_append, h] + +@[simp] theorem set_append_right {s t : Array α} {i : Nat} {x : α} + (h' : i < (s ++ t).size) (h : s.size ≤ i) : + (s ++ t).set i x = s ++ t.set (i - s.size) x (by simp at h'; omega) := by + rw [set_append, dif_neg (by omega)] + +theorem setIfInBounds_append {s t : Array α} {i : Nat} {x : α} : + (s ++ t).setIfInBounds i x = + if i < s.size then + s.setIfInBounds i x ++ t + else + s ++ t.setIfInBounds (i - s.size) x := by + rcases s with ⟨s⟩ + rcases t with ⟨t⟩ + simp only [List.append_toArray, List.setIfInBounds_toArray, List.set_append] + split <;> simp + +@[simp] theorem setIfInBounds_append_left {s t : Array α} {i : Nat} {x : α} (h : i < s.size) : + (s ++ t).setIfInBounds i x = s.setIfInBounds i x ++ t := by + simp [setIfInBounds_append, h] + +@[simp] theorem setIfInBounds_append_right {s t : Array α} {i : Nat} {x : α} (h : s.size ≤ i) : + (s ++ t).setIfInBounds i x = s ++ t.setIfInBounds (i - s.size) x := by + rw [setIfInBounds_append, if_neg (by omega)] + +theorem filterMap_eq_append_iff {f : α → Option β} : + filterMap f l = L₁ ++ L₂ ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ filterMap f l₁ = L₁ ∧ filterMap f l₂ = L₂ := by + rcases l with ⟨l⟩ + rcases L₁ with ⟨L₁⟩ + rcases L₂ with ⟨L₂⟩ + simp only [size_toArray, List.filterMap_toArray', List.append_toArray, mk.injEq, + List.filterMap_eq_append_iff, toArray_eq_append_iff] + constructor + · rintro ⟨l₁, l₂, rfl, rfl, rfl⟩ + exact ⟨⟨l₁⟩, ⟨l₂⟩, by simp⟩ + · rintro ⟨⟨l₁⟩, ⟨l₂⟩, rfl, h₁, h₂⟩ + exact ⟨l₁, l₂, by simp_all⟩ + +theorem append_eq_filterMap_iff {f : α → Option β} : + L₁ ++ L₂ = filterMap f l ↔ + ∃ l₁ l₂, l = l₁ ++ l₂ ∧ filterMap f l₁ = L₁ ∧ filterMap f l₂ = L₂ := by + rw [eq_comm, filterMap_eq_append_iff] + +@[simp] theorem map_append (f : α → β) (l₁ l₂ : Array α) : + map f (l₁ ++ l₂) = map f l₁ ++ map f l₂ := by + cases l₁ + cases l₂ + simp + +theorem map_eq_append_iff {f : α → β} : + map f l = L₁ ++ L₂ ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ map f l₁ = L₁ ∧ map f l₂ = L₂ := by + rw [← filterMap_eq_map, filterMap_eq_append_iff] + +theorem append_eq_map_iff {f : α → β} : + L₁ ++ L₂ = map f l ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ map f l₁ = L₁ ∧ map f l₂ = L₂ := by + rw [eq_comm, map_eq_append_iff] + +/-! Content below this point has not yet been aligned with `List`. -/ -- This is a duplicate of `List.toArray_toList`. -- It's confusing to guess which namespace this theorem should live in, diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean index 934456403a..095917d5bc 100644 --- a/src/Init/Data/List/Lemmas.lean +++ b/src/Init/Data/List/Lemmas.lean @@ -1494,6 +1494,34 @@ theorem filterMap_eq_cons_iff {l} {b} {bs} : @[simp] theorem cons_append_fun (a : α) (as : List α) : (fun bs => ((a :: as) ++ bs)) = fun bs => a :: (as ++ bs) := rfl +@[simp] theorem mem_append {a : α} {s t : List α} : a ∈ s ++ t ↔ a ∈ s ∨ a ∈ t := by + induction s <;> simp_all [or_assoc] + +theorem not_mem_append {a : α} {s t : List α} (h₁ : a ∉ s) (h₂ : a ∉ t) : a ∉ s ++ t := + mt mem_append.1 $ not_or.mpr ⟨h₁, h₂⟩ + +@[deprecated mem_append (since := "2025-01-13")] +theorem mem_append_eq (a : α) (s t : List α) : (a ∈ s ++ t) = (a ∈ s ∨ a ∈ t) := + propext mem_append + +@[deprecated mem_append_left (since := "2024-11-20")] abbrev mem_append_of_mem_left := @mem_append_left +@[deprecated mem_append_right (since := "2024-11-20")] abbrev mem_append_of_mem_right := @mem_append_right + +/-- +See also `eq_append_cons_of_mem`, which proves a stronger version +in which the initial list must not contain the element. +-/ +theorem append_of_mem {a : α} {l : List α} : a ∈ l → ∃ s t : List α, l = s ++ a :: t + | .head l => ⟨[], l, rfl⟩ + | .tail b h => let ⟨s, t, h'⟩ := append_of_mem h; ⟨b::s, t, by rw [h', cons_append]⟩ + +theorem mem_iff_append {a : α} {l : List α} : a ∈ l ↔ ∃ s t : List α, l = s ++ a :: t := + ⟨append_of_mem, fun ⟨s, t, e⟩ => e ▸ by simp⟩ + +theorem forall_mem_append {p : α → Prop} {l₁ l₂ : List α} : + (∀ (x) (_ : x ∈ l₁ ++ l₂), p x) ↔ (∀ (x) (_ : x ∈ l₁), p x) ∧ (∀ (x) (_ : x ∈ l₂), p x) := by + simp only [mem_append, or_imp, forall_and] + theorem getElem_append {l₁ l₂ : List α} (i : Nat) (h : i < (l₁ ++ l₂).length) : (l₁ ++ l₂)[i] = if h' : i < l₁.length then l₁[i] else l₂[i - l₁.length]'(by simp at h h'; exact Nat.sub_lt_left_of_lt_add h' h) := by split <;> rename_i h' @@ -1561,14 +1589,6 @@ theorem get_of_append {l : List α} (eq : l = l₁ ++ a :: l₂) (h : l₁.lengt l.get ⟨i, get_of_append_proof eq h⟩ = a := Option.some.inj <| by rw [← get?_eq_get, eq, get?_append_right (h ▸ Nat.le_refl _), h, Nat.sub_self]; rfl -/-- -See also `eq_append_cons_of_mem`, which proves a stronger version -in which the initial list must not contain the element. --/ -theorem append_of_mem {a : α} {l : List α} : a ∈ l → ∃ s t : List α, l = s ++ a :: t - | .head l => ⟨[], l, rfl⟩ - | .tail b h => let ⟨s, t, h'⟩ := append_of_mem h; ⟨b::s, t, by rw [h', cons_append]⟩ - @[simp 1100] theorem singleton_append : [x] ++ l = x :: l := rfl theorem append_inj : @@ -1585,8 +1605,8 @@ theorem append_inj_left (h : s₁ ++ t₁ = s₂ ++ t₂) (hl : length s₁ = le /-- Variant of `append_inj` instead requiring equality of the lengths of the second lists. -/ theorem append_inj' (h : s₁ ++ t₁ = s₂ ++ t₂) (hl : length t₁ = length t₂) : s₁ = s₂ ∧ t₁ = t₂ := - append_inj h <| @Nat.add_right_cancel _ (length t₁) _ <| by - let hap := congrArg length h; simp only [length_append, ← hl] at hap; exact hap + append_inj h <| @Nat.add_right_cancel _ t₁.length _ <| by + let hap := congrArg length h; simp only [length_append, ← hl] at hap; exact hap /-- Variant of `append_inj_right` instead requiring equality of the lengths of the second lists. -/ theorem append_inj_right' (h : s₁ ++ t₁ = s₂ ++ t₂) (hl : length t₁ = length t₂) : t₁ = t₂ := @@ -1614,9 +1634,6 @@ theorem append_left_inj {s₁ s₂ : List α} (t) : s₁ ++ t = s₂ ++ t ↔ s @[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 - theorem getLast_concat {a : α} : ∀ (l : List α), getLast (l ++ [a]) (by simp) = a | [] => rfl | a::t => by @@ -1642,6 +1659,54 @@ theorem get?_append {l₁ l₂ : List α} {n : Nat} (hn : n < l₁.length) : (l₁ ++ l₂).get? n = l₁.get? n := by simp [getElem?_append_left hn] +@[simp] theorem append_eq_nil_iff : p ++ q = [] ↔ p = [] ∧ q = [] := by + cases p <;> simp + +@[deprecated append_eq_nil_iff (since := "2025-01-13")] abbrev append_eq_nil := @append_eq_nil_iff + +@[simp] theorem nil_eq_append_iff : [] = a ++ b ↔ a = [] ∧ b = [] := by + rw [eq_comm, append_eq_nil_iff] + +@[deprecated nil_eq_append_iff (since := "2024-07-24")] abbrev nil_eq_append := @nil_eq_append_iff + +theorem append_ne_nil_of_left_ne_nil {s : List α} (h : s ≠ []) (t : List α) : s ++ t ≠ [] := by simp_all +theorem append_ne_nil_of_right_ne_nil (s : List α) : t ≠ [] → s ++ t ≠ [] := by simp_all + +@[deprecated append_ne_nil_of_left_ne_nil (since := "2024-07-24")] +theorem append_ne_nil_of_ne_nil_left {s : List α} (h : s ≠ []) (t : List α) : s ++ t ≠ [] := by simp_all +@[deprecated append_ne_nil_of_right_ne_nil (since := "2024-07-24")] +theorem append_ne_nil_of_ne_nil_right (s : List α) : t ≠ [] → s ++ t ≠ [] := by simp_all + +theorem append_eq_cons_iff : + a ++ b = x :: c ↔ (a = [] ∧ b = x :: c) ∨ (∃ a', a = x :: a' ∧ c = a' ++ b) := by + cases a with simp | cons a as => ?_ + exact ⟨fun h => ⟨as, by simp [h]⟩, fun ⟨a', ⟨aeq, aseq⟩, h⟩ => ⟨aeq, by rw [aseq, h]⟩⟩ + +@[deprecated append_eq_cons_iff (since := "2024-07-24")] abbrev append_eq_cons := @append_eq_cons_iff + +theorem cons_eq_append_iff : + x :: c = a ++ b ↔ (a = [] ∧ b = x :: c) ∨ (∃ a', a = x :: a' ∧ c = a' ++ b) := by + rw [eq_comm, append_eq_cons_iff] + +@[deprecated cons_eq_append_iff (since := "2024-07-24")] abbrev cons_eq_append := @cons_eq_append_iff + +theorem append_eq_singleton_iff : + a ++ b = [x] ↔ (a = [] ∧ b = [x]) ∨ (a = [x] ∧ b = []) := by + cases a <;> cases b <;> simp + +theorem singleton_eq_append_iff : + [x] = a ++ b ↔ (a = [] ∧ b = [x]) ∨ (a = [x] ∧ b = []) := by + cases a <;> cases b <;> simp [eq_comm] + +theorem append_eq_append_iff {a b c d : List α} : + a ++ b = c ++ d ↔ (∃ a', c = a ++ a' ∧ b = a' ++ d) ∨ ∃ c', a = c ++ c' ∧ d = c' ++ b := by + induction a generalizing c with + | nil => simp_all + | cons a as ih => cases c <;> simp [eq_comm, and_assoc, ih, and_or_left] + +@[deprecated append_inj (since := "2024-07-24")] abbrev append_inj_of_length_left := @append_inj +@[deprecated append_inj' (since := "2024-07-24")] abbrev append_inj_of_length_right := @append_inj' + @[simp] theorem head_append_of_ne_nil {l : List α} {w₁} (w₂) : head (l ++ l') w₁ = head l w₂ := by match l, w₂ with @@ -1691,60 +1756,6 @@ theorem tail_append {l l' : List α} : (l ++ l').tail = if l.isEmpty then l'.tai @[deprecated tail_append_of_ne_nil (since := "2024-07-24")] abbrev tail_append_left := @tail_append_of_ne_nil -theorem nil_eq_append_iff : [] = a ++ b ↔ a = [] ∧ b = [] := by - rw [eq_comm, append_eq_nil] - -@[deprecated nil_eq_append_iff (since := "2024-07-24")] abbrev nil_eq_append := @nil_eq_append_iff - -theorem append_ne_nil_of_left_ne_nil {s : List α} (h : s ≠ []) (t : List α) : s ++ t ≠ [] := by simp_all -theorem append_ne_nil_of_right_ne_nil (s : List α) : t ≠ [] → s ++ t ≠ [] := by simp_all - -@[deprecated append_ne_nil_of_left_ne_nil (since := "2024-07-24")] -theorem append_ne_nil_of_ne_nil_left {s : List α} (h : s ≠ []) (t : List α) : s ++ t ≠ [] := by simp_all -@[deprecated append_ne_nil_of_right_ne_nil (since := "2024-07-24")] -theorem append_ne_nil_of_ne_nil_right (s : List α) : t ≠ [] → s ++ t ≠ [] := by simp_all - -theorem append_eq_cons_iff : - a ++ b = x :: c ↔ (a = [] ∧ b = x :: c) ∨ (∃ a', a = x :: a' ∧ c = a' ++ b) := by - cases a with simp | cons a as => ?_ - exact ⟨fun h => ⟨as, by simp [h]⟩, fun ⟨a', ⟨aeq, aseq⟩, h⟩ => ⟨aeq, by rw [aseq, h]⟩⟩ - -@[deprecated append_eq_cons_iff (since := "2024-07-24")] abbrev append_eq_cons := @append_eq_cons_iff - -theorem cons_eq_append_iff : - x :: c = a ++ b ↔ (a = [] ∧ b = x :: c) ∨ (∃ a', a = x :: a' ∧ c = a' ++ b) := by - rw [eq_comm, append_eq_cons_iff] - -@[deprecated cons_eq_append_iff (since := "2024-07-24")] abbrev cons_eq_append := @cons_eq_append_iff - -theorem append_eq_append_iff {a b c d : List α} : - a ++ b = c ++ d ↔ (∃ a', c = a ++ a' ∧ b = a' ++ d) ∨ ∃ c', a = c ++ c' ∧ d = c' ++ b := by - induction a generalizing c with - | nil => simp_all - | cons a as ih => cases c <;> simp [eq_comm, and_assoc, ih, and_or_left] - -@[deprecated append_inj (since := "2024-07-24")] abbrev append_inj_of_length_left := @append_inj -@[deprecated append_inj' (since := "2024-07-24")] abbrev append_inj_of_length_right := @append_inj' - -@[simp] theorem mem_append {a : α} {s t : List α} : a ∈ s ++ t ↔ a ∈ s ∨ a ∈ t := by - induction s <;> simp_all [or_assoc] - -theorem not_mem_append {a : α} {s t : List α} (h₁ : a ∉ s) (h₂ : a ∉ t) : a ∉ s ++ t := - mt mem_append.1 $ not_or.mpr ⟨h₁, h₂⟩ - -theorem mem_append_eq (a : α) (s t : List α) : (a ∈ s ++ t) = (a ∈ s ∨ a ∈ t) := - propext mem_append - -@[deprecated mem_append_left (since := "2024-11-20")] abbrev mem_append_of_mem_left := @mem_append_left -@[deprecated mem_append_right (since := "2024-11-20")] abbrev mem_append_of_mem_right := @mem_append_right - -theorem mem_iff_append {a : α} {l : List α} : a ∈ l ↔ ∃ s t : List α, l = s ++ a :: t := - ⟨append_of_mem, fun ⟨s, t, e⟩ => e ▸ by simp⟩ - -theorem forall_mem_append {p : α → Prop} {l₁ l₂ : List α} : - (∀ (x) (_ : x ∈ l₁ ++ l₂), p x) ↔ (∀ (x) (_ : x ∈ l₁), p x) ∧ (∀ (x) (_ : x ∈ l₂), p x) := by - simp only [mem_append, or_imp, forall_and] - theorem set_append {s t : List α} : (s ++ t).set i x = if i < s.length then s.set i x ++ t else s ++ t.set (i - s.length) x := by induction s generalizing i with @@ -1974,8 +1985,8 @@ theorem flatten_eq_append_iff {xs : List (List α)} {ys zs : List α} : constructor · induction xs generalizing ys with | nil => - simp only [flatten_nil, nil_eq, append_eq_nil, and_false, cons_append, false_and, exists_const, - exists_false, or_false, and_imp, List.cons_ne_nil] + simp only [flatten_nil, nil_eq, append_eq_nil_iff, and_false, cons_append, false_and, + exists_const, exists_false, or_false, and_imp, List.cons_ne_nil] rintro rfl rfl exact ⟨[], [], by simp⟩ | cons x xs ih => diff --git a/src/Init/Data/List/Zip.lean b/src/Init/Data/List/Zip.lean index 8b0b80808b..4ffb4b08d3 100644 --- a/src/Init/Data/List/Zip.lean +++ b/src/Init/Data/List/Zip.lean @@ -203,11 +203,11 @@ theorem zipWith_eq_append_iff {f : α → β → γ} {l₁ : List α} {l₂ : Li cases l₂ with | nil => constructor - · simp only [zipWith_nil_right, nil_eq, append_eq_nil, exists_and_left, and_imp] + · simp only [zipWith_nil_right, nil_eq, append_eq_nil_iff, exists_and_left, and_imp] rintro rfl rfl exact ⟨[], x₁ :: l₁, [], by simp⟩ · rintro ⟨w, x, y, z, h₁, _, h₃, rfl, rfl⟩ - simp only [nil_eq, append_eq_nil] at h₃ + simp only [nil_eq, append_eq_nil_iff] at h₃ obtain ⟨rfl, rfl⟩ := h₃ simp | cons x₂ l₂ => diff --git a/src/Init/Data/Vector/Lemmas.lean b/src/Init/Data/Vector/Lemmas.lean index f8fb2eaf2e..bce753edba 100644 --- a/src/Init/Data/Vector/Lemmas.lean +++ b/src/Init/Data/Vector/Lemmas.lean @@ -693,6 +693,24 @@ theorem forall_getElem {l : Vector α n} {p : α → Prop} : rcases l with ⟨l, rfl⟩ simp [Array.forall_getElem] + +/-! ### cast -/ + +@[simp] theorem getElem_cast (a : Vector α n) (h : n = m) (i : Nat) (hi : i < m) : + (a.cast h)[i] = a[i] := by + cases a + simp + +@[simp] theorem getElem?_cast {l : Vector α n} {m : Nat} {w : n = m} {i : Nat} : + (l.cast w)[i]? = l[i]? := by + rcases l with ⟨l, rfl⟩ + simp + +@[simp] theorem mem_cast {a : α} {l : Vector α n} {m : Nat} {w : n = m} : + a ∈ l.cast w ↔ a ∈ l := by + rcases l with ⟨l, rfl⟩ + simp + /-! ### Decidability of bounded quantifiers -/ instance {xs : Vector α n} {p : α → Prop} [DecidablePred p] : @@ -1167,6 +1185,227 @@ theorem map_eq_iff {f : α → β} {l : Vector α n} {l' : Vector β n} : cases as simp +/-! ### singleton -/ + +@[simp] theorem singleton_def (v : α) : Vector.singleton v = #v[v] := rfl + +/-! ### append -/ + +@[simp] theorem append_push {as : Vector α n} {bs : Vector α m} {a : α} : + as ++ bs.push a = (as ++ bs).push a := by + cases as + cases bs + simp + +theorem singleton_eq_toVector_singleton (a : α) : #v[a] = #[a].toVector := rfl + +@[simp] theorem mem_append {a : α} {s : Vector α n} {t : Vector α m} : + a ∈ s ++ t ↔ a ∈ s ∨ a ∈ t := by + cases s + cases t + simp + +theorem mem_append_left {a : α} {s : Vector α n} {t : Vector α m} (h : a ∈ s) : a ∈ s ++ t := + mem_append.2 (Or.inl h) + +theorem mem_append_right {a : α} {s : Vector α n} {t : Vector α m} (h : a ∈ t) : a ∈ s ++ t := + mem_append.2 (Or.inr h) + +theorem not_mem_append {a : α} {s : Vector α n} {t : Vector α m} (h₁ : a ∉ s) (h₂ : a ∉ t) : + a ∉ s ++ t := + mt mem_append.1 $ not_or.mpr ⟨h₁, h₂⟩ + +/-- +See also `eq_push_append_of_mem`, which proves a stronger version +in which the initial array must not contain the element. +-/ +theorem append_of_mem {a : α} {l : Vector α n} (h : a ∈ l) : + ∃ (m k : Nat) (w : m + 1 + k = n) (s : Vector α m) (t : Vector α k), + l = (s.push a ++ t).cast w := by + rcases l with ⟨l, rfl⟩ + obtain ⟨s, t, rfl⟩ := Array.append_of_mem (by simpa using h) + refine ⟨_, _, by simp, s.toVector, t.toVector, by simp_all⟩ + +theorem mem_iff_append {a : α} {l : Vector α n} : + a ∈ l ↔ ∃ (m k : Nat) (w : m + 1 + k = n) (s : Vector α m) (t : Vector α k), + l = (s.push a ++ t).cast w := + ⟨append_of_mem, by rintro ⟨m, k, rfl, s, t, rfl⟩; simp⟩ + +theorem forall_mem_append {p : α → Prop} {l₁ : Vector α n} {l₂ : Vector α m} : + (∀ (x) (_ : x ∈ l₁ ++ l₂), p x) ↔ (∀ (x) (_ : x ∈ l₁), p x) ∧ (∀ (x) (_ : x ∈ l₂), p x) := by + simp only [mem_append, or_imp, forall_and] + +theorem empty_append (as : Vector α n) : (#v[] : Vector α 0) ++ as = as.cast (by omega) := by + rcases as with ⟨as, rfl⟩ + simp + +theorem append_empty (as : Vector α n) : as ++ (#v[] : Vector α 0) = as := by + rw [← toArray_inj, toArray_append, Array.append_nil] + +theorem getElem_append (a : Vector α n) (b : Vector α m) (i : Nat) (hi : i < n + m) : + (a ++ b)[i] = if h : i < n then a[i] else b[i - n] := by + rcases a with ⟨a, rfl⟩ + rcases b with ⟨b, rfl⟩ + simp [Array.getElem_append, hi] + +theorem getElem_append_left {a : Vector α n} {b : Vector α m} {i : Nat} (hi : i < n) : + (a ++ b)[i] = a[i] := by simp [getElem_append, hi] + +theorem getElem_append_right {a : Vector α n} {b : Vector α m} {i : Nat} (h : i < n + m) (hi : n ≤ i) : + (a ++ b)[i] = b[i - n] := by + rw [getElem_append, dif_neg (by omega)] + +theorem getElem?_append_left {as : Vector α n} {bs : Vector α m} {i : Nat} (hn : i < n) : + (as ++ bs)[i]? = as[i]? := by + have hn' : i < n + m := by omega + simp_all [getElem?_eq_getElem, getElem_append] + +theorem getElem?_append_right {as : Vector α n} {bs : Vector α m} {i : Nat} (h : n ≤ i) : + (as ++ bs)[i]? = bs[i - n]? := by + rcases as with ⟨as, rfl⟩ + rcases bs with ⟨bs, rfl⟩ + simp [Array.getElem?_append_right, h] + +theorem getElem?_append {as : Vector α n} {bs : Vector α m} {i : Nat} : + (as ++ bs)[i]? = if i < n then as[i]? else bs[i - n]? := by + split <;> rename_i h + · exact getElem?_append_left h + · exact getElem?_append_right (by simpa using h) + +/-- Variant of `getElem_append_left` useful for rewriting from the small array to the big array. -/ +theorem getElem_append_left' (l₁ : Vector α m) {l₂ : Vector α n} {i : Nat} (hi : i < m) : + l₁[i] = (l₁ ++ l₂)[i] := by + rw [getElem_append_left] <;> simp + +/-- Variant of `getElem_append_right` useful for rewriting from the small array to the big array. -/ +theorem getElem_append_right' (l₁ : Vector α m) {l₂ : Vector α n} {i : Nat} (hi : i < n) : + l₂[i] = (l₁ ++ l₂)[i + m] := by + rw [getElem_append_right] <;> simp [*, Nat.le_add_left] + +theorem getElem_of_append {l : Vector α n} {l₁ : Vector α m} {l₂ : Vector α k} + (w : m + 1 + k = n) (eq : l = (l₁.push a ++ l₂).cast w) : + l[m] = a := Option.some.inj <| by + rw [← getElem?_eq_getElem, eq, getElem?_cast, getElem?_append_left (by simp)] + simp + +@[simp 1100] theorem append_singleton {a : α} {as : Vector α n} : as ++ #v[a] = as.push a := by + cases as + simp + +theorem append_inj {s₁ s₂ : Vector α n} {t₁ t₂ : Vector α m} (h : s₁ ++ t₁ = s₂ ++ t₂) : + s₁ = s₂ ∧ t₁ = t₂ := by + rcases s₁ with ⟨s₁, rfl⟩ + rcases s₂ with ⟨s₂, hs⟩ + rcases t₁ with ⟨t₁, rfl⟩ + rcases t₂ with ⟨t₂, ht⟩ + simpa using Array.append_inj (by simpa using h) (by omega) + +theorem append_inj_right {s₁ s₂ : Vector α n} {t₁ t₂ : Vector α m} + (h : s₁ ++ t₁ = s₂ ++ t₂) : t₁ = t₂ := + (append_inj h).right + +theorem append_inj_left {s₁ s₂ : Vector α n} {t₁ t₂ : Vector α m} + (h : s₁ ++ t₁ = s₂ ++ t₂) : s₁ = s₂ := + (append_inj h).left + +theorem append_right_inj {t₁ t₂ : Vector α m} (s : Vector α n) : s ++ t₁ = s ++ t₂ ↔ t₁ = t₂ := + ⟨fun h => append_inj_right h, congrArg _⟩ + +theorem append_left_inj {s₁ s₂ : Vector α n} (t : Vector α m) : s₁ ++ t = s₂ ++ t ↔ s₁ = s₂ := + ⟨fun h => append_inj_left h, congrArg (· ++ _)⟩ + +theorem append_eq_append_iff {a : Vector α n} {b : Vector α m} {c : Vector α k} {d : Vector α l} + (w : k + l = n + m) : + a ++ b = (c ++ d).cast w ↔ + if h : n ≤ k then + ∃ a' : Vector α (k - n), c = (a ++ a').cast (by omega) ∧ b = (a' ++ d).cast (by omega) + else + ∃ c' : Vector α (n - k), a = (c ++ c').cast (by omega) ∧ d = (c' ++ b).cast (by omega) := by + rcases a with ⟨a, rfl⟩ + rcases b with ⟨b, rfl⟩ + rcases c with ⟨c, rfl⟩ + rcases d with ⟨d, rfl⟩ + simp only [mk_append_mk, Array.append_eq_append_iff, mk_eq, toArray_cast] + constructor + · rintro (⟨a', rfl, rfl⟩ | ⟨c', rfl, rfl⟩) + · rw [dif_pos (by simp)] + exact ⟨a'.toVector.cast (by simp; omega), by simp⟩ + · split <;> rename_i h + · have hc : c'.size = 0 := by simp at h; omega + simp at hc + exact ⟨#v[].cast (by simp; omega), by simp_all⟩ + · exact ⟨c'.toVector.cast (by simp; omega), by simp⟩ + · split <;> rename_i h + · rintro ⟨a', hc, rfl⟩ + left + refine ⟨a'.toArray, hc, rfl⟩ + · rintro ⟨c', ha, rfl⟩ + right + refine ⟨c'.toArray, ha, rfl⟩ + +theorem set_append {s : Vector α n} {t : Vector α m} {i : Nat} {x : α} (h : i < n + m) : + (s ++ t).set i x = + if h' : i < n then + s.set i x ++ t + else + s ++ t.set (i - n) x := by + rcases s with ⟨s, rfl⟩ + rcases t with ⟨t, rfl⟩ + simp only [mk_append_mk, set_mk, Array.set_append] + split <;> simp + +@[simp] theorem set_append_left {s : Vector α n} {t : Vector α m} {i : Nat} {x : α} (h : i < n) : + (s ++ t).set i x = s.set i x ++ t := by + simp [set_append, h] + +@[simp] theorem set_append_right {s : Vector α n} {t : Vector α m} {i : Nat} {x : α} + (h' : i < n + m) (h : n ≤ i) : + (s ++ t).set i x = s ++ t.set (i - n) x := by + rw [set_append, dif_neg (by omega)] + +theorem setIfInBounds_append {s : Vector α n} {t : Vector α m} {i : Nat} {x : α} : + (s ++ t).setIfInBounds i x = + if i < n then + s.setIfInBounds i x ++ t + else + s ++ t.setIfInBounds (i - n) x := by + rcases s with ⟨s, rfl⟩ + rcases t with ⟨t, rfl⟩ + simp only [mk_append_mk, setIfInBounds_mk, Array.setIfInBounds_append] + split <;> simp + +@[simp] theorem setIfInBounds_append_left {s : Vector α n} {t : Vector α m} {i : Nat} {x : α} (h : i < n) : + (s ++ t).setIfInBounds i x = s.setIfInBounds i x ++ t := by + simp [setIfInBounds_append, h] + +@[simp] theorem setIfInBounds_append_right {s : Vector α n} {t : Vector α m} {i : Nat} {x : α} + (h : n ≤ i) : + (s ++ t).setIfInBounds i x = s ++ t.setIfInBounds (i - n) x := by + rw [setIfInBounds_append, if_neg (by omega)] + +@[simp] theorem map_append (f : α → β) (l₁ : Vector α n) (l₂ : Vector α m) : + map f (l₁ ++ l₂) = map f l₁ ++ map f l₂ := by + rcases l₁ with ⟨l₁, rfl⟩ + rcases l₂ with ⟨l₂, rfl⟩ + simp + +theorem map_eq_append_iff {f : α → β} : + map f l = L₁ ++ L₂ ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ map f l₁ = L₁ ∧ map f l₂ = L₂ := by + rcases l with ⟨l, h⟩ + rcases L₁ with ⟨L₁, rfl⟩ + rcases L₂ with ⟨L₂, rfl⟩ + simp only [map_mk, mk_append_mk, eq_mk, Array.map_eq_append_iff, mk_eq, toArray_append, + toArray_map] + constructor + · rintro ⟨l₁, l₂, rfl, rfl, rfl⟩ + exact ⟨l₁.toVector.cast (by simp), l₂.toVector.cast (by simp), by simp⟩ + · rintro ⟨⟨l₁⟩, ⟨l₂⟩, rfl, h₁, h₂⟩ + exact ⟨l₁, l₂, by simp_all⟩ + +theorem append_eq_map_iff {f : α → β} : + L₁ ++ L₂ = map f l ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ map f l₁ = L₁ ∧ map f l₂ = L₂ := by + rw [eq_comm, map_eq_append_iff] + /-! Content below this point has not yet been aligned with `List` and `Array`. -/ @[simp] theorem getElem_ofFn {α n} (f : Fin n → α) (i : Nat) (h : i < n) : @@ -1197,28 +1436,6 @@ defeq issues in the implicit size argument. subst h simp [pop, back, back!, ← Array.eq_push_pop_back!_of_size_ne_zero] -/-! ### append -/ - -theorem getElem_append (a : Vector α n) (b : Vector α m) (i : Nat) (hi : i < n + m) : - (a ++ b)[i] = if h : i < n then a[i] else b[i - n] := by - rcases a with ⟨a, rfl⟩ - rcases b with ⟨b, rfl⟩ - simp [Array.getElem_append, hi] - -theorem getElem_append_left {a : Vector α n} {b : Vector α m} {i : Nat} (hi : i < n) : - (a ++ b)[i] = a[i] := by simp [getElem_append, hi] - -theorem getElem_append_right {a : Vector α n} {b : Vector α m} {i : Nat} (h : i < n + m) (hi : n ≤ i) : - (a ++ b)[i] = b[i - n] := by - rw [getElem_append, dif_neg (by omega)] - -/-! ### cast -/ - -@[simp] theorem getElem_cast (a : Vector α n) (h : n = m) (i : Nat) (hi : i < m) : - (a.cast h)[i] = a[i] := by - cases a - simp - /-! ### extract -/ @[simp] theorem getElem_extract (a : Vector α n) (start stop) (i : Nat) (hi : i < min stop n - start) :