From 5d6bf75795c7efa1e6346b77e1762d1f9d0adc63 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 15 Jan 2025 12:16:19 +1100 Subject: [PATCH] feat: align `List/Array/Vector` `flatten` lemmas (#6640) This PR completes aligning `List`/`Array`/`Vector` lemmas about `flatten`. `Vector.flatten` was previously missing, and has been added (for rectangular sizes only). A small number of missing `Option` lemmas were also need to get the proofs to go through. --- src/Init/Data/Array/Basic.lean | 6 + src/Init/Data/Array/Bootstrap.lean | 10 +- src/Init/Data/Array/Find.lean | 10 +- src/Init/Data/Array/Lemmas.lean | 318 ++++++++++++++++--- src/Init/Data/List/Lemmas.lean | 70 +++- src/Init/Data/List/ToArray.lean | 23 ++ src/Init/Data/Option/Lemmas.lean | 18 ++ src/Init/Data/Vector/Basic.lean | 4 + src/Init/Data/Vector/Lemmas.lean | 121 ++++++- src/Lean/Meta/Tactic/Grind/Arith/Offset.lean | 2 - tests/lean/guessLexFailures.lean | 14 +- 11 files changed, 524 insertions(+), 72 deletions(-) diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean index 275bbffe8dfe..69d50d1a9b86 100644 --- a/src/Init/Data/Array/Basic.lean +++ b/src/Init/Data/Array/Basic.lean @@ -576,6 +576,12 @@ def foldl {α : Type u} {β : Type v} (f : β → α → β) (init : β) (as : A def foldr {α : Type u} {β : Type v} (f : α → β → β) (init : β) (as : Array α) (start := as.size) (stop := 0) : β := Id.run <| as.foldrM f init start stop +/-- Sum of an array. + +`Array.sum #[a, b, c] = a + (b + (c + 0))` -/ +def sum {α} [Add α] [Zero α] : Array α → α := + foldr (· + ·) 0 + @[inline] def map {α : Type u} {β : Type v} (f : α → β) (as : Array α) : Array β := Id.run <| as.mapM f diff --git a/src/Init/Data/Array/Bootstrap.lean b/src/Init/Data/Array/Bootstrap.lean index e039b4512961..52ab9fb1ff45 100644 --- a/src/Init/Data/Array/Bootstrap.lean +++ b/src/Init/Data/Array/Bootstrap.lean @@ -81,12 +81,18 @@ theorem foldrM_eq_reverse_foldlM_toList [Monad m] (f : α → β → m β) (init @[simp] theorem toList_empty : (#[] : Array α).toList = [] := rfl -@[simp] theorem append_nil (as : Array α) : as ++ #[] = as := by +@[simp] theorem append_empty (as : Array α) : as ++ #[] = as := by apply ext'; simp only [toList_append, toList_empty, List.append_nil] -@[simp] theorem nil_append (as : Array α) : #[] ++ as = as := by +@[deprecated append_empty (since := "2025-01-13")] +abbrev append_nil := @append_empty + +@[simp] theorem empty_append (as : Array α) : #[] ++ as = as := by apply ext'; simp only [toList_append, toList_empty, List.nil_append] +@[deprecated empty_append (since := "2025-01-13")] +abbrev nil_append := @empty_append + @[simp] theorem append_assoc (as bs cs : Array α) : as ++ bs ++ cs = as ++ (bs ++ cs) := by apply ext'; simp only [toList_append, List.append_assoc] diff --git a/src/Init/Data/Array/Find.lean b/src/Init/Data/Array/Find.lean index 38efb9e5e82f..4838ad6408a4 100644 --- a/src/Init/Data/Array/Find.lean +++ b/src/Init/Data/Array/Find.lean @@ -74,12 +74,12 @@ theorem findSome?_append {l₁ l₂ : Array α} : (l₁ ++ l₂).findSome? f = ( theorem getElem?_zero_flatten (L : Array (Array α)) : (flatten L)[0]? = L.findSome? fun l => l[0]? := by - cases L using array_array_induction + cases L using array₂_induction simp [← List.head?_eq_getElem?, List.head?_flatten, List.findSome?_map, Function.comp_def] theorem getElem_zero_flatten.proof {L : Array (Array α)} (h : 0 < L.flatten.size) : (L.findSome? fun l => l[0]?).isSome := by - cases L using array_array_induction + cases L using array₂_induction simp only [List.findSome?_toArray, List.findSome?_map, Function.comp_def, List.getElem?_toArray, List.findSome?_isSome_iff, isSome_getElem?] simp only [flatten_toArray_map_toArray, size_toArray, List.length_flatten, @@ -95,7 +95,7 @@ theorem getElem_zero_flatten {L : Array (Array α)} (h) : theorem back?_flatten {L : Array (Array α)} : (flatten L).back? = (L.findSomeRev? fun l => l.back?) := by - cases L using array_array_induction + cases L using array₂_induction simp [List.getLast?_flatten, ← List.map_reverse, List.findSome?_map, Function.comp_def] theorem findSome?_mkArray : findSome? f (mkArray n a) = if n = 0 then none else f a := by @@ -203,7 +203,7 @@ theorem get_find?_mem {xs : Array α} (h) : (xs.find? p).get h ∈ xs := by @[simp] theorem find?_flatten (xs : Array (Array α)) (p : α → Bool) : xs.flatten.find? p = xs.findSome? (·.find? p) := by - cases xs using array_array_induction + cases xs using array₂_induction simp [List.findSome?_map, Function.comp_def] theorem find?_flatten_eq_none {xs : Array (Array α)} {p : α → Bool} : @@ -220,7 +220,7 @@ theorem find?_flatten_eq_some {xs : Array (Array α)} {p : α → Bool} {a : α} p a ∧ ∃ (as : Array (Array α)) (ys zs : Array α) (bs : Array (Array α)), xs = as.push (ys.push a ++ zs) ++ bs ∧ (∀ a ∈ as, ∀ x ∈ a, !p x) ∧ (∀ x ∈ ys, !p x) := by - cases xs using array_array_induction + cases xs using array₂_induction simp only [flatten_toArray_map_toArray, List.find?_toArray, List.find?_flatten_eq_some] simp only [Bool.not_eq_eq_eq_not, Bool.not_true, exists_and_right, and_congr_right_iff] intro w diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean index 7e0549addb62..1acf464ca378 100644 --- a/src/Init/Data/Array/Lemmas.lean +++ b/src/Init/Data/Array/Lemmas.lean @@ -38,6 +38,14 @@ namespace Array @[simp] theorem length_toList {l : Array α} : l.toList.length = l.size := rfl +theorem eq_toArray : v = List.toArray a ↔ v.toList = a := by + cases v + simp + +theorem toArray_eq : List.toArray a = v ↔ a = v.toList := by + cases v + simp + /-! ### empty -/ @[simp] theorem empty_eq {xs : Array α} : #[] = xs ↔ xs = #[] := by @@ -256,6 +264,11 @@ theorem getElem?_push {a : Array α} {x} : (a.push x)[i]? = if i = a.size then s theorem getElem?_singleton (a : α) (i : Nat) : #[a][i]? = if i = 0 then some a else none := by simp [List.getElem?_singleton] +theorem ext_getElem? {l₁ l₂ : Array α} (h : ∀ i : Nat, l₁[i]? = l₂[i]?) : l₁ = l₂ := by + rcases l₁ with ⟨l₁⟩ + rcases l₂ with ⟨l₂⟩ + simpa using List.ext_getElem? (by simpa using h) + /-! ### mem -/ theorem not_mem_empty (a : α) : ¬ a ∈ #[] := by simp @@ -1089,9 +1102,21 @@ theorem forall_mem_map {f : α → β} {l : Array α} {P : β → Prop} : (∀ (i) (_ : i ∈ l.map f), P i) ↔ ∀ (j) (_ : j ∈ l), P (f j) := by simp +@[simp] theorem map_eq_empty_iff {f : α → β} {l : Array α} : map f l = #[] ↔ l = #[] := by + cases l + simp + +theorem eq_empty_of_map_eq_empty {f : α → β} {l : Array α} (h : map f l = #[]) : l = #[] := + map_eq_empty_iff.mp h + @[simp] theorem map_inj_left {f g : α → β} : map f l = map g l ↔ ∀ a ∈ l, f a = g a := by cases l <;> simp_all +theorem map_inj_right {f : α → β} (w : ∀ x y, f x = f y → x = y) : map f l = map f l' ↔ l = l' := by + cases l + cases l' + simp [List.map_inj_right w] + theorem map_congr_left (h : ∀ a ∈ l, f a = g a) : map f l = map g l := map_inj_left.2 h @@ -1100,13 +1125,6 @@ theorem map_inj : map f = map g ↔ f = g := by · intro h; ext a; replace h := congrFun h #[a]; simpa using h · intro h; subst h; rfl -@[simp] theorem map_eq_empty_iff {f : α → β} {l : Array α} : map f l = #[] ↔ l = #[] := by - cases l - simp - -theorem eq_empty_of_map_eq_empty {f : α → β} {l : Array α} (h : map f l = #[]) : l = #[] := - map_eq_empty_iff.mp h - theorem map_eq_push_iff {f : α → β} {l : Array α} {l₂ : Array β} {b : β} : map f l = l₂.push b ↔ ∃ l₁ a, l = l₁.push a ∧ map f l₁ = l₂ ∧ f a = b := by rcases l with ⟨l⟩ @@ -1189,6 +1207,30 @@ theorem mapM_map_eq_foldl (as : Array α) (f : α → β) (i) : rfl termination_by as.size - i +/-- +Use this as `induction ass using array₂_induction` on a hypothesis of the form `ass : Array (Array α)`. +The hypothesis `ass` will be replaced with a hypothesis `ass : List (List α)`, +and former appearances of `ass` in the goal will be replaced with `(ass.map List.toArray).toArray`. +-/ +-- We can't use `@[cases_eliminator]` here as +-- `Lean.Meta.getCustomEliminator?` only looks at the top-level constant. +theorem array₂_induction (P : Array (Array α) → Prop) (of : ∀ (xss : List (List α)), P (xss.map List.toArray).toArray) + (ass : Array (Array α)) : P ass := by + specialize of (ass.toList.map toList) + simpa [← toList_map, Function.comp_def, map_id] using of + +/-- +Use this as `induction ass using array₃_induction` on a hypothesis of the form `ass : Array (Array (Array α))`. +The hypothesis `ass` will be replaced with a hypothesis `ass : List (List (List α))`, +and former appearances of `ass` in the goal will be replaced with +`((ass.map (fun xs => xs.map List.toArray)).map List.toArray).toArray`. +-/ +theorem array₃_induction (P : Array (Array (Array α)) → Prop) + (of : ∀ (xss : List (List (List α))), P ((xss.map (fun xs => xs.map List.toArray)).map List.toArray).toArray) + (ass : Array (Array (Array α))) : P ass := by + specialize of ((ass.toList.map toList).map (fun as => as.map toList)) + simpa [← toList_map, Function.comp_def, map_id] using of + /-! ### filter -/ @[congr] @@ -1564,10 +1606,6 @@ 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 - -theorem append_empty (as : Array α) : as ++ #[] = as := by simp - theorem getElem_append {as bs : Array α} (h : i < (as ++ bs).size) : (as ++ bs)[i] = if h' : i < as.size then as[i] else bs[i - as.size]'(by simp at h; omega) := by cases as; cases bs @@ -1664,13 +1702,13 @@ theorem append_left_inj {s₁ s₂ : Array α} (t) : s₁ ++ t = s₂ ++ t ↔ 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] + rw [← append_left_inj (s₁ := x), empty_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] + rw [← append_right_inj (t₁ := y), append_empty] @[simp] theorem self_eq_append_right {x y : Array α} : x = x ++ y ↔ y = #[] := by rw [eq_comm, append_right_eq_self] @@ -1808,6 +1846,189 @@ 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] +/-! ### flatten -/ + +@[simp] theorem flatten_empty : (#[] : Array (Array α)).flatten = #[] := by simp [flatten]; rfl + +@[simp] theorem toList_flatten {l : Array (Array α)} : + l.flatten.toList = (l.toList.map toList).flatten := by + dsimp [flatten] + simp only [← foldl_toList] + generalize l.toList = l + have : ∀ a : Array α, (List.foldl ?_ a l).toList = a.toList ++ ?_ := ?_ + exact this #[] + induction l with + | nil => simp + | cons h => induction h.toList <;> simp [*] + +@[simp] theorem flatten_map_toArray (l : List (List α)) : + (l.toArray.map List.toArray).flatten = l.flatten.toArray := by + apply ext' + simp [Function.comp_def] + +@[simp] theorem flatten_toArray_map (l : List (List α)) : + (l.map List.toArray).toArray.flatten = l.flatten.toArray := by + rw [← flatten_map_toArray] + simp + +@[simp] theorem size_flatten (L : Array (Array α)) : L.flatten.size = (L.map size).sum := by + cases L using array₂_induction + simp [Function.comp_def] + +@[simp] theorem flatten_singleton (l : Array α) : #[l].flatten = l := by simp [flatten]; rfl + +theorem mem_flatten : ∀ {L : Array (Array α)}, a ∈ L.flatten ↔ ∃ l, l ∈ L ∧ a ∈ l := by + simp only [mem_def, toList_flatten, List.mem_flatten, List.mem_map] + intro l + constructor + · rintro ⟨_, ⟨s, m, rfl⟩, h⟩ + exact ⟨s, m, h⟩ + · rintro ⟨s, h₁, h₂⟩ + refine ⟨s.toList, ⟨⟨s, h₁, rfl⟩, h₂⟩⟩ + +@[simp] theorem flatten_eq_nil_iff {L : Array (Array α)} : L.flatten = #[] ↔ ∀ l ∈ L, l = #[] := by + induction L using array₂_induction + simp + +@[simp] theorem nil_eq_flatten_iff {L : Array (Array α)} : #[] = L.flatten ↔ ∀ l ∈ L, l = #[] := by + rw [eq_comm, flatten_eq_nil_iff] + +theorem flatten_ne_nil_iff {xs : Array (Array α)} : xs.flatten ≠ #[] ↔ ∃ x, x ∈ xs ∧ x ≠ #[] := by + simp + +theorem exists_of_mem_flatten : a ∈ flatten L → ∃ l, l ∈ L ∧ a ∈ l := mem_flatten.1 + +theorem mem_flatten_of_mem (lL : l ∈ L) (al : a ∈ l) : a ∈ flatten L := mem_flatten.2 ⟨l, lL, al⟩ + +theorem forall_mem_flatten {p : α → Prop} {L : Array (Array α)} : + (∀ (x) (_ : x ∈ flatten L), p x) ↔ ∀ (l) (_ : l ∈ L) (x) (_ : x ∈ l), p x := by + simp only [mem_flatten, forall_exists_index, and_imp] + constructor <;> (intros; solve_by_elim) + +theorem flatten_eq_flatMap {L : Array (Array α)} : flatten L = L.flatMap id := by + induction L using array₂_induction + rw [flatten_toArray_map, List.flatten_eq_flatMap] + simp [List.flatMap_map] + +@[simp] theorem map_flatten (f : α → β) (L : Array (Array α)) : + (flatten L).map f = (map (map f) L).flatten := by + induction L using array₂_induction with + | of xss => + simp only [flatten_toArray_map, List.map_toArray, List.map_flatten, List.map_map, + Function.comp_def] + rw [← Function.comp_def, ← List.map_map, flatten_toArray_map] + +@[simp] theorem filterMap_flatten (f : α → Option β) (L : Array (Array α)) : + filterMap f (flatten L) = flatten (map (filterMap f) L) := by + induction L using array₂_induction + simp only [flatten_toArray_map, size_toArray, List.length_flatten, List.filterMap_toArray', + List.filterMap_flatten, List.map_toArray, List.map_map, Function.comp_def] + rw [← Function.comp_def, ← List.map_map, flatten_toArray_map] + +@[simp] theorem filter_flatten (p : α → Bool) (L : Array (Array α)) : + filter p (flatten L) = flatten (map (filter p) L) := by + induction L using array₂_induction + simp only [flatten_toArray_map, size_toArray, List.length_flatten, List.filter_toArray', + List.filter_flatten, List.map_toArray, List.map_map, Function.comp_def] + rw [← Function.comp_def, ← List.map_map, flatten_toArray_map] + +theorem flatten_filter_not_isEmpty {L : Array (Array α)} : + flatten (L.filter fun l => !l.isEmpty) = L.flatten := by + induction L using array₂_induction + simp [List.filter_map, Function.comp_def, List.flatten_filter_not_isEmpty] + +theorem flatten_filter_ne_empty [DecidablePred fun l : Array α => l ≠ #[]] {L : Array (Array α)} : + flatten (L.filter fun l => l ≠ #[]) = L.flatten := by + simp only [ne_eq, ← isEmpty_iff, Bool.not_eq_true, Bool.decide_eq_false, + flatten_filter_not_isEmpty] + +@[simp] theorem flatten_append (L₁ L₂ : Array (Array α)) : + flatten (L₁ ++ L₂) = flatten L₁ ++ flatten L₂ := by + induction L₁ using array₂_induction + induction L₂ using array₂_induction + simp [← List.map_append] + +theorem flatten_push (L : Array (Array α)) (l : Array α) : + flatten (L.push l) = flatten L ++ l := by + induction L using array₂_induction + rcases l with ⟨l⟩ + have this : [l.toArray] = [l].map List.toArray := by simp + simp only [List.push_toArray, flatten_toArray_map, List.append_toArray] + rw [this, ← List.map_append, flatten_toArray_map] + simp + +theorem flatten_flatten {L : Array (Array (Array α))} : flatten (flatten L) = flatten (map flatten L) := by + induction L using array₃_induction with + | of xss => + rw [flatten_toArray_map] + have : (xss.map (fun xs => xs.map List.toArray)).flatten = xss.flatten.map List.toArray := by + induction xss with + | nil => simp + | cons xs xss ih => + simp only [List.map_cons, List.flatten_cons, ih, List.map_append] + rw [this, flatten_toArray_map, List.flatten_flatten, ← List.map_toArray, Array.map_map, + ← List.map_toArray, map_map, Function.comp_def] + simp only [Function.comp_apply, flatten_toArray_map] + rw [List.map_toArray, ← Function.comp_def, ← List.map_map, flatten_toArray_map] + +theorem flatten_eq_push_iff {xs : Array (Array α)} {ys : Array α} {y : α} : + xs.flatten = ys.push y ↔ + ∃ (as : Array (Array α)) (bs : Array α) (cs : Array (Array α)), + xs = as.push (bs.push y) ++ cs ∧ (∀ l, l ∈ cs → l = #[]) ∧ ys = as.flatten ++ bs := by + induction xs using array₂_induction with + | of xs => + rcases ys with ⟨ys⟩ + rw [flatten_toArray_map, List.push_toArray, mk.injEq, List.flatten_eq_append_iff] + constructor + · rintro (⟨as, bs, rfl, rfl, h⟩ | ⟨as, bs, c, cs, ds, rfl, rfl, h⟩) + · rw [List.singleton_eq_flatten_iff] at h + obtain ⟨xs, ys, rfl, h₁, h₂⟩ := h + exact ⟨((as ++ xs).map List.toArray).toArray, #[], (ys.map List.toArray).toArray, by simp, + by simpa using h₂, by rw [flatten_toArray_map]; simpa⟩ + · rw [List.singleton_eq_append_iff] at h + obtain (⟨h₁, h₂⟩ | ⟨h₁, h₂⟩) := h + · simp at h₁ + · simp at h₁ h₂ + obtain ⟨rfl, rfl⟩ := h₁ + exact ⟨(as.map List.toArray).toArray, bs.toArray, (ds.map List.toArray).toArray, by simpa⟩ + · rintro ⟨as, bs, cs, h₁, h₂, h₃⟩ + replace h₁ := congrArg (List.map Array.toList) (congrArg Array.toList h₁) + simp [Function.comp_def] at h₁ + subst h₁ + replace h₃ := congrArg Array.toList h₃ + simp at h₃ + subst h₃ + right + exact ⟨(as.map Array.toList).toList, bs.toList, y, [], (cs.map Array.toList).toList, by simpa⟩ + +theorem push_eq_flatten_iff {xs : Array (Array α)} {ys : Array α} {y : α} : + ys.push y = xs.flatten ↔ + ∃ (as : Array (Array α)) (bs : Array α) (cs : Array (Array α)), + xs = as.push (bs.push y) ++ cs ∧ (∀ l, l ∈ cs → l = #[]) ∧ ys = as.flatten ++ bs := by + rw [eq_comm, flatten_eq_push_iff] + +-- For now we omit `flatten_eq_append_iff`, +-- because it is not easily obtainable from `List.flatten_eq_append_iff`. +-- theorem flatten_eq_append_iff {xs : Array (Array α)} {ys zs : Array α} : +-- xs.flatten = ys ++ zs ↔ +-- (∃ as bs, xs = as ++ bs ∧ ys = as.flatten ∧ zs = bs.flatten) ∨ +-- ∃ (as : Array (Array α)) (bs : Array α) (c : α) (cs : Array α) (ds : Array (Array α)), +-- xs = as.push ((bs.push c ++ cs)) ++ ds ∧ ys = as.flatten ++ bs.push c ∧ +-- zs = cs ++ ds.flatten := by sorry + + +/-- Two arrays of subarrays are equal iff their flattens coincide, as well as the sizes of the +subarrays. -/ +theorem eq_iff_flatten_eq {L L' : Array (Array α)} : + L = L' ↔ L.flatten = L'.flatten ∧ map size L = map size L' := by + cases L using array₂_induction with + | of L => + cases L' using array₂_induction with + | of L' => + simp [Function.comp_def, ← List.eq_iff_flatten_eq] + rw [List.map_inj_right] + simp +contextual + /-! Content below this point has not yet been aligned with `List`. -/ -- This is a duplicate of `List.toArray_toList`. @@ -2422,28 +2643,6 @@ theorem getElem?_modify {as : Array α} {i : Nat} {f : α → α} {j : Nat} : theorem size_empty : (#[] : Array α).size = 0 := rfl -/-! ### flatten -/ - -@[simp] theorem toList_flatten {l : Array (Array α)} : - l.flatten.toList = (l.toList.map toList).flatten := by - dsimp [flatten] - simp only [← foldl_toList] - generalize l.toList = l - have : ∀ a : Array α, (List.foldl ?_ a l).toList = a.toList ++ ?_ := ?_ - exact this #[] - induction l with - | nil => simp - | cons h => induction h.toList <;> simp [*] - -theorem mem_flatten : ∀ {L : Array (Array α)}, a ∈ L.flatten ↔ ∃ l, l ∈ L ∧ a ∈ l := by - simp only [mem_def, toList_flatten, List.mem_flatten, List.mem_map] - intro l - constructor - · rintro ⟨_, ⟨s, m, rfl⟩, h⟩ - exact ⟨s, m, h⟩ - · rintro ⟨s, h₁, h₂⟩ - refine ⟨s.toList, ⟨⟨s, h₁, rfl⟩, h₂⟩⟩ - /-! ### extract -/ theorem extract_loop_zero (as bs : Array α) (start : Nat) : extract.loop as 0 start bs = bs := by @@ -2460,16 +2659,16 @@ theorem extract_loop_of_ge (as bs : Array α) (size start : Nat) (h : start ≥ theorem extract_loop_eq_aux (as bs : Array α) (size start : Nat) : extract.loop as size start bs = bs ++ extract.loop as size start #[] := by induction size using Nat.recAux generalizing start bs with - | zero => rw [extract_loop_zero, extract_loop_zero, append_nil] + | zero => rw [extract_loop_zero, extract_loop_zero, append_empty] | succ size ih => if h : start < as.size then rw [extract_loop_succ (h:=h), ih (bs.push _), push_eq_append_singleton] - rw [extract_loop_succ (h:=h), ih (#[].push _), push_eq_append_singleton, nil_append] + rw [extract_loop_succ (h:=h), ih (#[].push _), push_eq_append_singleton, empty_append] rw [append_assoc] else rw [extract_loop_of_ge (h:=Nat.le_of_not_lt h)] rw [extract_loop_of_ge (h:=Nat.le_of_not_lt h)] - rw [append_nil] + rw [append_empty] theorem extract_loop_eq (as bs : Array α) (size start : Nat) (h : start + size ≤ as.size) : extract.loop as size start bs = bs ++ as.extract start (start + size) := by @@ -2825,11 +3024,6 @@ namespace Array /-! ### map -/ -theorem array_array_induction (P : Array (Array α) → Prop) (h : ∀ (xss : List (List α)), P (xss.map List.toArray).toArray) - (ass : Array (Array α)) : P ass := by - specialize h (ass.toList.map toList) - simpa [← toList_map, Function.comp_def, map_id] using h - theorem foldl_map (f : β₁ → β₂) (g : α → β₂ → α) (l : Array β₁) (init : α) : (l.map f).foldl g init = l.foldl (fun x y => g x (f y)) init := by cases l; simp [List.foldl_map] @@ -2866,8 +3060,6 @@ theorem foldr_map' (g : α → β) (f : α → α → α) (f' : β → β → β /-! ### flatten -/ -@[simp] theorem flatten_empty : flatten (#[] : Array (Array α)) = #[] := rfl - @[simp] theorem flatten_toArray_map_toArray (xss : List (List α)) : (xss.map List.toArray).toArray.flatten = xss.flatten.toArray := by simp [flatten] @@ -2878,12 +3070,48 @@ theorem foldr_map' (g : α → β) (f : α → α → α) (f' : β → β → β | nil => simp | cons xs xss ih => simp [ih] +/-! ### sum -/ + +theorem sum_eq_sum_toList [Add α] [Zero α] (as : Array α) : as.sum = as.toList.sum := by + cases as + simp [Array.sum, List.sum] + /-! ### mkArray -/ +theorem eq_mkArray_of_mem {a : α} {l : Array α} (h : ∀ (b) (_ : b ∈ l), b = a) : l = mkArray l.size a := by + rcases l with ⟨l⟩ + have := List.eq_replicate_of_mem (by simpa using h) + rw [this] + simp + +theorem eq_mkArray_iff {a : α} {n} {l : Array α} : + l = mkArray n a ↔ l.size = n ∧ ∀ (b) (_ : b ∈ l), b = a := by + rcases l with ⟨l⟩ + simp [← List.eq_replicate_iff, toArray_eq] + +theorem map_eq_mkArray_iff {l : Array α} {f : α → β} {b : β} : + l.map f = mkArray l.size b ↔ ∀ x ∈ l, f x = b := by + simp [eq_mkArray_iff] + @[simp] theorem mem_mkArray (a : α) (n : Nat) : b ∈ mkArray n a ↔ n ≠ 0 ∧ b = a := by rw [mkArray, mem_toArray] simp +@[simp] theorem map_const (l : Array α) (b : β) : map (Function.const α b) l = mkArray l.size b := + map_eq_mkArray_iff.mpr fun _ _ => rfl + +@[simp] theorem map_const_fun (x : β) : map (Function.const α x) = (mkArray ·.size x) := by + funext l + simp + +/-- Variant of `map_const` using a lambda rather than `Function.const`. -/ +-- This can not be a `@[simp]` lemma because it would fire on every `Array.map`. +theorem map_const' (l : Array α) (b : β) : map (fun _ => b) l = mkArray l.size b := + map_const l b + +@[simp] theorem sum_mkArray_nat (n : Nat) (a : Nat) : (mkArray n a).sum = n * a := by + simp [sum_eq_sum_toList, List.sum_replicate_nat] + /-! ### reverse -/ @[simp] theorem mem_reverse {x : α} {as : Array α} : x ∈ as.reverse ↔ x ∈ as := by diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean index 095917d5bc9f..f6f11494a15d 100644 --- a/src/Init/Data/List/Lemmas.lean +++ b/src/Init/Data/List/Lemmas.lean @@ -1076,9 +1076,31 @@ theorem forall_mem_map {f : α → β} {l : List α} {P : β → Prop} : @[deprecated forall_mem_map (since := "2024-07-25")] abbrev forall_mem_map_iff := @forall_mem_map +@[simp] theorem map_eq_nil_iff {f : α → β} {l : List α} : map f l = [] ↔ l = [] := by + constructor <;> exact fun _ => match l with | [] => rfl + +@[deprecated map_eq_nil_iff (since := "2024-09-05")] abbrev map_eq_nil := @map_eq_nil_iff + +theorem eq_nil_of_map_eq_nil {f : α → β} {l : List α} (h : map f l = []) : l = [] := + map_eq_nil_iff.mp h + @[simp] theorem map_inj_left {f g : α → β} : map f l = map g l ↔ ∀ a ∈ l, f a = g a := by induction l <;> simp_all +theorem map_inj_right {f : α → β} (w : ∀ x y, f x = f y → x = y) : map f l = map f l' ↔ l = l' := by + induction l generalizing l' with + | nil => simp + | cons a l ih => + simp only [map_cons] + cases l' with + | nil => simp + | cons a' l' => + simp only [map_cons, cons.injEq, ih, and_congr_left_iff] + intro h + constructor + · apply w + · simp +contextual + theorem map_congr_left (h : ∀ a ∈ l, f a = g a) : map f l = map g l := map_inj_left.2 h @@ -1087,14 +1109,6 @@ theorem map_inj : map f = map g ↔ f = g := by · intro h; ext a; replace h := congrFun h [a]; simpa using h · intro h; subst h; rfl -@[simp] theorem map_eq_nil_iff {f : α → β} {l : List α} : map f l = [] ↔ l = [] := by - constructor <;> exact fun _ => match l with | [] => rfl - -@[deprecated map_eq_nil_iff (since := "2024-09-05")] abbrev map_eq_nil := @map_eq_nil_iff - -theorem eq_nil_of_map_eq_nil {f : α → β} {l : List α} (h : map f l = []) : l = [] := - map_eq_nil_iff.mp h - theorem map_eq_cons_iff {f : α → β} {l : List α} : map f l = b :: l₂ ↔ ∃ a l₁, l = a :: l₁ ∧ f a = b ∧ map f l₁ = l₂ := by cases l @@ -1884,7 +1898,7 @@ theorem eq_nil_or_concat : ∀ l : List α, l = [] ∨ ∃ L b, l = concat L b /-! ### flatten -/ -@[simp] theorem length_flatten (L : List (List α)) : (flatten L).length = (L.map length).sum := by +@[simp] theorem length_flatten (L : List (List α)) : L.flatten.length = (L.map length).sum := by induction L with | nil => rfl | cons => @@ -1899,6 +1913,9 @@ theorem flatten_singleton (l : List α) : [l].flatten = l := by simp @[simp] theorem flatten_eq_nil_iff {L : List (List α)} : L.flatten = [] ↔ ∀ l ∈ L, l = [] := by induction L <;> simp_all +@[simp] theorem nil_eq_flatten_iff {L : List (List α)} : [] = L.flatten ↔ ∀ l ∈ L, l = [] := by + rw [eq_comm, flatten_eq_nil_iff] + theorem flatten_ne_nil_iff {xs : List (List α)} : xs.flatten ≠ [] ↔ ∃ x, x ∈ xs ∧ x ≠ [] := by simp @@ -1924,7 +1941,8 @@ theorem head?_flatten {L : List (List α)} : (flatten L).head? = L.findSome? fun -- `getLast?_flatten` is proved later, after the `reverse` section. -- `head_flatten` and `getLast_flatten` are proved in `Init.Data.List.Find`. -@[simp] theorem map_flatten (f : α → β) (L : List (List α)) : map f (flatten L) = flatten (map (map f) L) := by +@[simp] theorem map_flatten (f : α → β) (L : List (List α)) : + (flatten L).map f = (map (map f) L).flatten := by induction L <;> simp_all @[simp] theorem filterMap_flatten (f : α → Option β) (L : List (List α)) : @@ -1977,6 +1995,26 @@ theorem flatten_eq_cons_iff {xs : List (List α)} {y : α} {ys : List α} : · rintro ⟨as, bs, cs, rfl, h₁, rfl⟩ simp [flatten_eq_nil_iff.mpr h₁] +theorem cons_eq_flatten_iff {xs : List (List α)} {y : α} {ys : List α} : + y :: ys = xs.flatten ↔ + ∃ as bs cs, xs = as ++ (y :: bs) :: cs ∧ (∀ l, l ∈ as → l = []) ∧ ys = bs ++ cs.flatten := by + rw [eq_comm, flatten_eq_cons_iff] + +theorem flatten_eq_singleton_iff {xs : List (List α)} {y : α} : + xs.flatten = [y] ↔ ∃ as bs, xs = as ++ [y] :: bs ∧ (∀ l, l ∈ as → l = []) ∧ (∀ l, l ∈ bs → l = []) := by + rw [flatten_eq_cons_iff] + constructor + · rintro ⟨as, bs, cs, rfl, h₁, h₂⟩ + simp at h₂ + obtain ⟨rfl, h₂⟩ := h₂ + exact ⟨as, cs, by simp, h₁, h₂⟩ + · rintro ⟨as, bs, rfl, h₁, h₂⟩ + exact ⟨as, [], bs, rfl, h₁, by simpa⟩ + +theorem singleton_eq_flatten_iff {xs : List (List α)} {y : α} : + [y] = xs.flatten ↔ ∃ as bs, xs = as ++ [y] :: bs ∧ (∀ l, l ∈ as → l = []) ∧ (∀ l, l ∈ bs → l = []) := by + rw [eq_comm, flatten_eq_singleton_iff] + theorem flatten_eq_append_iff {xs : List (List α)} {ys zs : List α} : xs.flatten = ys ++ zs ↔ (∃ as bs, xs = as ++ bs ∧ ys = as.flatten ∧ zs = bs.flatten) ∨ @@ -2005,6 +2043,13 @@ theorem flatten_eq_append_iff {xs : List (List α)} {ys zs : List α} : · simp · simp +theorem append_eq_flatten_iff {xs : List (List α)} {ys zs : List α} : + ys ++ zs = xs.flatten ↔ + (∃ as bs, xs = as ++ bs ∧ ys = as.flatten ∧ zs = bs.flatten) ∨ + ∃ as bs c cs ds, xs = as ++ (bs ++ c :: cs) :: ds ∧ ys = as.flatten ++ bs ∧ + zs = c :: cs ++ ds.flatten := by + rw [eq_comm, flatten_eq_append_iff] + /-- Two lists of sublists are equal iff their flattens coincide, as well as the lengths of the sublists. -/ theorem eq_iff_flatten_eq : ∀ {L L' : List (List α)}, @@ -2027,6 +2072,8 @@ theorem flatMap_def (l : List α) (f : α → List β) : l.flatMap f = flatten ( @[simp] theorem flatMap_id (l : List (List α)) : List.flatMap l id = l.flatten := by simp [flatMap_def] +@[simp] theorem flatMap_id' (l : List (List α)) : List.flatMap l (fun a => a) = l.flatten := by simp [flatMap_def] + @[simp] theorem length_flatMap (l : List α) (f : α → List β) : length (l.flatMap f) = sum (map (length ∘ f) l) := by @@ -2348,6 +2395,9 @@ theorem replicateRecOn {α : Type _} {p : List α → Prop} (m : List α) exact hi _ _ _ _ h hn (replicateRecOn (b :: l') h0 hr hi) termination_by m.length +@[simp] theorem sum_replicate_nat (n : Nat) (a : Nat) : (replicate n a).sum = n * a := by + induction n <;> simp_all [replicate_succ, Nat.add_mul, Nat.add_comm] + /-! ### reverse -/ @[simp] theorem length_reverse (as : List α) : (as.reverse).length = as.length := by diff --git a/src/Init/Data/List/ToArray.lean b/src/Init/Data/List/ToArray.lean index 6b07544c0604..d76cc01c885f 100644 --- a/src/Init/Data/List/ToArray.lean +++ b/src/Init/Data/List/ToArray.lean @@ -143,6 +143,9 @@ theorem forM_toArray [Monad m] (l : List α) (f : α → m PUnit) : subst h rw [foldl_toList] +@[simp] theorem sum_toArray [Add α] [Zero α] (l : List α) : l.toArray.sum = l.sum := by + simp [Array.sum, List.sum] + @[simp] theorem append_toArray (l₁ l₂ : List α) : l₁.toArray ++ l₂.toArray = (l₁ ++ l₂).toArray := by apply ext' @@ -394,4 +397,24 @@ theorem takeWhile_go_toArray (p : α → Bool) (l : List α) (i : Nat) : @[deprecated toArray_replicate (since := "2024-12-13")] abbrev _root_.Array.mkArray_eq_toArray_replicate := @toArray_replicate +@[simp] theorem flatMap_empty {β} (f : α → Array β) : (#[] : Array α).flatMap f = #[] := rfl + +theorem flatMap_toArray_cons {β} (f : α → Array β) (a : α) (as : List α) : + (a :: as).toArray.flatMap f = f a ++ as.toArray.flatMap f := by + simp [Array.flatMap] + suffices ∀ cs, List.foldl (fun bs a => bs ++ f a) (f a ++ cs) as = + f a ++ List.foldl (fun bs a => bs ++ f a) cs as by + erw [empty_append] -- Why doesn't this work via `simp`? + simpa using this #[] + intro cs + induction as generalizing cs <;> simp_all + +@[simp] theorem flatMap_toArray {β} (f : α → Array β) (as : List α) : + as.toArray.flatMap f = (as.flatMap (fun a => (f a).toList)).toArray := by + induction as with + | nil => simp + | cons a as ih => + apply ext' + simp [ih, flatMap_toArray_cons] + end List diff --git a/src/Init/Data/Option/Lemmas.lean b/src/Init/Data/Option/Lemmas.lean index d1712a9533a3..0b684d289458 100644 --- a/src/Init/Data/Option/Lemmas.lean +++ b/src/Init/Data/Option/Lemmas.lean @@ -208,6 +208,15 @@ theorem comp_map (h : β → γ) (g : α → β) (x : Option α) : x.map (h ∘ theorem mem_map_of_mem (g : α → β) (h : a ∈ x) : g a ∈ Option.map g x := h.symm ▸ map_some' .. +theorem map_inj_right {f : α → β} {o o' : Option α} (w : ∀ x y, f x = f y → x = y) : + o.map f = o'.map f ↔ o = o' := by + cases o with + | none => cases o' <;> simp + | some a => + cases o' with + | none => simp + | some a' => simpa using ⟨fun h => w _ _ h, fun h => congrArg f h⟩ + @[simp] theorem map_if {f : α → β} [Decidable c] : (if c then some a else none).map f = if c then some (f a) else none := by split <;> rfl @@ -629,6 +638,15 @@ theorem pbind_eq_some_iff {o : Option α} {f : (a : α) → a ∈ o → Option · rintro ⟨h, rfl⟩ rfl +@[simp] +theorem pmap_eq_map (p : α → Prop) (f : α → β) (o : Option α) (H) : + @pmap _ _ p (fun a _ => f a) o H = Option.map f o := by + cases o <;> simp + +theorem map_pmap {p : α → Prop} (g : β → γ) (f : ∀ a, p a → β) (o H) : + Option.map g (pmap f o H) = pmap (fun a h => g (f a h)) o H := by + cases o <;> simp + /-! ### pelim -/ @[simp] theorem pelim_none : pelim none b f = b := rfl diff --git a/src/Init/Data/Vector/Basic.lean b/src/Init/Data/Vector/Basic.lean index 53b9327d212a..269a6577e3d4 100644 --- a/src/Init/Data/Vector/Basic.lean +++ b/src/Init/Data/Vector/Basic.lean @@ -170,6 +170,10 @@ result is empty. If `stop` is greater than the size of the vector, the size is u @[inline] def map (f : α → β) (v : Vector α n) : Vector β n := ⟨v.toArray.map f, by simp⟩ +@[inline] def flatten (v : Vector (Vector α n) m) : Vector α (m * n) := + ⟨(v.toArray.map Vector.toArray).flatten, + by rcases v; simp_all [Function.comp_def, Array.map_const']⟩ + /-- Maps corresponding elements of two vectors of equal size using the function `f`. -/ @[inline] def zipWith (a : Vector α n) (b : Vector β n) (f : α → β → φ) : Vector φ n := ⟨Array.zipWith a.toArray b.toArray f, by simp⟩ diff --git a/src/Init/Data/Vector/Lemmas.lean b/src/Init/Data/Vector/Lemmas.lean index bce753edba49..00ea12d7cee3 100644 --- a/src/Init/Data/Vector/Lemmas.lean +++ b/src/Init/Data/Vector/Lemmas.lean @@ -5,6 +5,7 @@ Authors: Shreyas Srinivas, Francois Dorais, Kim Morrison -/ prelude import Init.Data.Vector.Basic +import Init.Data.Array.Attach /-! ## Vectors @@ -27,6 +28,9 @@ namespace Vector theorem toArray_mk (a : Array α) (h : a.size = n) : (Vector.mk a h).toArray = a := rfl +@[simp] theorem mk_toArray (v : Vector α n) : mk v.toArray v.2 = v := by + rfl + @[simp] theorem getElem_mk {data : Array α} {size : data.size = n} {i : Nat} (h : i < n) : (Vector.mk data size)[i] = data[i] := rfl @@ -1115,6 +1119,11 @@ theorem forall_mem_map {f : α → β} {l : Vector α n} {P : β → Prop} : @[simp] theorem map_inj_left {f g : α → β} : map f l = map g l ↔ ∀ a ∈ l, f a = g a := by cases l <;> simp_all +theorem map_inj_right {f : α → β} (w : ∀ x y, f x = f y → x = y) : map f l = map f l' ↔ l = l' := by + cases l + cases l' + simp [Array.map_inj_right w] + theorem map_congr_left (h : ∀ a ∈ l, f a = g a) : map f l = map g l := map_inj_left.2 h @@ -1185,6 +1194,40 @@ theorem map_eq_iff {f : α → β} {l : Vector α n} {l' : Vector β n} : cases as simp +/-- +Use this as `induction ass using vector₂_induction` on a hypothesis of the form `ass : Vector (Vector α n) m`. +The hypothesis `ass` will be replaced with a hypothesis `ass : Array (Array α)` +along with additional hypotheses `h₁ : ass.size = m` and `h₂ : ∀ xs ∈ ass, xs.size = n`. +Appearances of the original `ass` in the goal will be replaced with +`Vector.mk (xss.attach.map (fun ⟨xs, m⟩ => Vector.mk xs ⋯)) ⋯`. +-/ +-- We can't use `@[cases_eliminator]` here as +-- `Lean.Meta.getCustomEliminator?` only looks at the top-level constant. +theorem vector₂_induction (P : Vector (Vector α n) m → Prop) + (of : ∀ (xss : Array (Array α)) (h₁ : xss.size = m) (h₂ : ∀ xs ∈ xss, xs.size = n), + P (mk (xss.attach.map (fun ⟨xs, m⟩ => mk xs (h₂ xs m))) (by simpa using h₁))) + (ass : Vector (Vector α n) m) : P ass := by + specialize of (ass.map toArray).toArray (by simp) (by simp) + simpa [Array.map_attach, Array.pmap_map] using of + +/-- +Use this as `induction ass using vector₃_induction` on a hypothesis of the form `ass : Vector (Vector (Vector α n) m) k`. +The hypothesis `ass` will be replaced with a hypothesis `ass : Array (Array (Array α))` +along with additional hypotheses `h₁ : ass.size = k`, `h₂ : ∀ xs ∈ ass, xs.size = m`, +and `h₃ : ∀ xs ∈ ass, ∀ x ∈ xs, x.size = n`. +Appearances of the original `ass` in the goal will be replaced with +`Vector.mk (xss.attach.map (fun ⟨xs, m⟩ => Vector.mk (xs.attach.map (fun ⟨x, m'⟩ => Vector.mk x ⋯)) ⋯)) ⋯`. +-/ +theorem vector₃_induction (P : Vector (Vector (Vector α n) m) k → Prop) + (of : ∀ (xss : Array (Array (Array α))) (h₁ : xss.size = k) (h₂ : ∀ xs ∈ xss, xs.size = m) + (h₃ : ∀ xs ∈ xss, ∀ x ∈ xs, x.size = n), + P (mk (xss.attach.map (fun ⟨xs, m⟩ => + mk (xs.attach.map (fun ⟨x, m'⟩ => + mk x (h₃ xs m x m'))) (by simpa using h₂ xs m))) (by simpa using h₁))) + (ass : Vector (Vector (Vector α n) m) k) : P ass := by + specialize of (ass.map (fun as => (as.map toArray).toArray)).toArray (by simp) (by simp) (by simp) + simpa [Array.map_attach, Array.pmap_map] using of + /-! ### singleton -/ @[simp] theorem singleton_def (v : α) : Vector.singleton v = #v[v] := rfl @@ -1240,7 +1283,7 @@ theorem empty_append (as : Vector α n) : (#v[] : Vector α 0) ++ as = as.cast ( simp theorem append_empty (as : Vector α n) : as ++ (#v[] : Vector α 0) = as := by - rw [← toArray_inj, toArray_append, Array.append_nil] + rw [← toArray_inj, toArray_append, Array.append_empty] 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 @@ -1406,6 +1449,82 @@ 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] +/-! ### flatten -/ + +@[simp] theorem flatten_mk (L : Array (Vector α n)) (h : L.size = m) : + (mk L h).flatten = + mk (L.map toArray).flatten (by simp [Function.comp_def, Array.map_const', h]) := by + simp [flatten] + +@[simp] theorem flatten_singleton (l : Vector α n) : #v[l].flatten = l.cast (by simp) := by + simp [flatten] + +theorem mem_flatten {L : Vector (Vector α n) m} : a ∈ L.flatten ↔ ∃ l, l ∈ L ∧ a ∈ l := by + rcases L with ⟨L, rfl⟩ + simp [Array.mem_flatten] + constructor + · rintro ⟨_, ⟨l, h₁, rfl⟩, h₂⟩ + exact ⟨l, h₁, by simpa using h₂⟩ + · rintro ⟨l, h₁, h₂⟩ + exact ⟨l.toArray, ⟨l, h₁, rfl⟩, by simpa using h₂⟩ + +theorem exists_of_mem_flatten : a ∈ flatten L → ∃ l, l ∈ L ∧ a ∈ l := mem_flatten.1 + +theorem mem_flatten_of_mem (lL : l ∈ L) (al : a ∈ l) : a ∈ flatten L := mem_flatten.2 ⟨l, lL, al⟩ + +theorem forall_mem_flatten {p : α → Prop} {L : Vector (Vector α n) m} : + (∀ (x) (_ : x ∈ flatten L), p x) ↔ ∀ (l) (_ : l ∈ L) (x) (_ : x ∈ l), p x := by + simp only [mem_flatten, forall_exists_index, and_imp] + constructor <;> (intros; solve_by_elim) + +@[simp] theorem map_flatten (f : α → β) (L : Vector (Vector α n) m) : + (flatten L).map f = (map (map f) L).flatten := by + induction L using vector₂_induction with + | of xss h₁ h₂ => simp + +@[simp] theorem flatten_append (L₁ : Vector (Vector α n) m₁) (L₂ : Vector (Vector α n) m₂) : + flatten (L₁ ++ L₂) = (flatten L₁ ++ flatten L₂).cast (by simp [Nat.add_mul]) := by + induction L₁ using vector₂_induction + induction L₂ using vector₂_induction + simp + +theorem flatten_push (L : Vector (Vector α n) m) (l : Vector α n) : + flatten (L.push l) = (flatten L ++ l).cast (by simp [Nat.add_mul]) := by + induction L using vector₂_induction + rcases l with ⟨l⟩ + simp [Array.flatten_push] + +theorem flatten_flatten {L : Vector (Vector (Vector α n) m) k} : + flatten (flatten L) = (flatten (map flatten L)).cast (by simp [Nat.mul_assoc]) := by + induction L using vector₃_induction with + | of xss h₁ h₂ h₃ => + -- simp [Array.flatten_flatten] -- FIXME: `simp` produces a bad proof here! + simp [Array.map_attach, Array.flatten_flatten, Array.map_pmap] + +/-- Two vectors of constant length vectors are equal iff their flattens coincide. -/ +theorem eq_iff_flatten_eq {L L' : Vector (Vector α n) m} : + L = L' ↔ L.flatten = L'.flatten := by + induction L using vector₂_induction with | of L h₁ h₂ => + induction L' using vector₂_induction with | of L' h₁' h₂' => + simp only [eq_mk, flatten_mk, Array.map_map, Function.comp_apply, Array.map_subtype, + Array.unattach_attach, Array.map_id_fun', id_eq] + constructor + · intro h + suffices L = L' by simp_all + apply Array.ext_getElem? + intro i + replace h := congrArg (fun x => x[i]?.map (fun x => x.toArray)) h + simpa [Option.map_pmap] using h + · intro h + have w : L.map Array.size = L'.map Array.size := by + ext i h h' + · simp_all + · simp only [Array.getElem_map] + rw [h₂ _ (by simp), h₂' _ (by simp)] + have := Array.eq_iff_flatten_eq.mpr ⟨h, w⟩ + subst this + rfl + /-! 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) : diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Offset.lean b/src/Lean/Meta/Tactic/Grind/Arith/Offset.lean index cfac5021c179..c6d9921015e1 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Offset.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Offset.lean @@ -133,8 +133,6 @@ private def propagateTrue (u v : NodeId) (k : Int) (c : Cnstr NodeId) (e : Expr) return true return false -example (x y : Nat) : x + 2 ≤ y → ¬ (y ≤ x + 1) := by omega - /-- Tries to assign `e` to `False`, which is represented by constraint `c` (from `v` to `u`), using the path `u --(k)--> v`. diff --git a/tests/lean/guessLexFailures.lean b/tests/lean/guessLexFailures.lean index 667244671b93..477c7da73ebb 100644 --- a/tests/lean/guessLexFailures.lean +++ b/tests/lean/guessLexFailures.lean @@ -21,14 +21,14 @@ def noArguments : Nat := noArguments def noNonFixedArguments (n : Nat) : Nat := noNonFixedArguments n -def Array.sum (xs : Array Nat) : Nat := xs.foldl (init := 0) Nat.add +def Array.sum' (xs : Array Nat) : Nat := xs.foldl (init := 0) Nat.add namespace InterestingMatrix def f : (n m l : Nat) → Nat | n+1, m+1, l+1 => #[ f (n+1) (m+1) (l+1), f (n+1) (m-1) (l), - f (n) (m+1) (l) ].sum + f (n) (m+1) (l) ].sum' | _, _, _ => 0 decreasing_by decreasing_tactic end InterestingMatrix @@ -38,7 +38,7 @@ def f : (n m : Nat) → (h : True) → Nat → Nat | n+1, m+1, h, l+1 => #[ f (n+1) (m+1) h (l+1), f (n+1) (m-1) h (l), - f (n) (m+1) h (l) ].sum + f (n) (m+1) h (l) ].sum' | _, _, _, _ => 0 decreasing_by decreasing_tactic end InterestingMatrixWithForbiddenArguments @@ -49,7 +49,7 @@ def f (n m l : Nat) : Nat := match n, m, l with | n+1, m+1, l+1 => #[ f (n+1) (m+1) (l+1), f (n+1) (m-1) (l), - f (n) (m+1) (l) ].sum + f (n) (m+1) (l) ].sum' | _, _, _ => 0 decreasing_by decreasing_tactic end InterestingMatrixWithNames @@ -60,21 +60,21 @@ mutual | n+1, m+1, l+1 => #[ f fixed (n+1) (m+1) (l+1), f fixed (n+1) (m-1) (l), - g fixed (n) (m+1) trivial (l)].sum + g fixed (n) (m+1) trivial (l)].sum' | _, _, _ => 0 def g (fixed n m : Nat) (H : True) (l : Nat) : Nat := match n, m, l with | n+1, m+1, l+1 => #[ g fixed (m+1) (n+1) H (l+1), g fixed (m+1) (n-1) H (l), - h fixed (m) (n+1) ].sum + h fixed (m) (n+1) ].sum' | _, _, _ => 0 def h (fixed : Nat) : (n m : Nat) -> Nat | n+1, m+1 => #[ f fixed (n+1) (m+1) (n+1), h fixed (n+1) (m-1), - h fixed (n) (m+1) ].sum + h fixed (n) (m+1) ].sum' | _, _ => 0 end end Mutual