From a4240294757960441c5dbad03e4718456cfbe967 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 7 Jan 2025 09:20:09 +1100 Subject: [PATCH] feat: Array lemma alignment; fold and map (#6546) This PR continues aligning `Array` and `Vector` lemmas with `List`, working on `fold` and `map` operations. --- src/Init/Data/Array/Lemmas.lean | 385 ++++++++++++++---------- src/Init/Data/List/Lemmas.lean | 490 ++++++++++++++++--------------- src/Init/Data/Vector/Basic.lean | 12 + src/Init/Data/Vector/Lemmas.lean | 57 +++- 4 files changed, 532 insertions(+), 412 deletions(-) diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean index 2e6db2b2aa..8bb29aae6f 100644 --- a/src/Init/Data/Array/Lemmas.lean +++ b/src/Init/Data/Array/Lemmas.lean @@ -36,6 +36,8 @@ namespace Array @[simp] theorem mem_toList_iff (a : α) (l : Array α) : a ∈ l.toList ↔ a ∈ l := by cases l <;> simp +@[simp] theorem length_toList {l : Array α} : l.toList.length = l.size := rfl + /-! ### empty -/ @[simp] theorem empty_eq {xs : Array α} : #[] = xs ↔ xs = #[] := by @@ -1001,52 +1003,7 @@ private theorem beq_of_beq_singleton [BEq α] {a b : α} : #[a] == #[b] → a == /-! Content below this point has not yet been aligned with `List`. -/ -theorem singleton_eq_toArray_singleton (a : α) : #[a] = [a].toArray := rfl - -@[simp] theorem singleton_def (v : α) : singleton v = #[v] := rfl - --- This is a duplicate of `List.toArray_toList`. --- It's confusing to guess which namespace this theorem should live in, --- so we provide both. -@[simp] theorem toArray_toList (a : Array α) : a.toList.toArray = a := rfl - -@[simp] theorem length_toList {l : Array α} : l.toList.length = l.size := rfl - -@[simp] theorem mkEmpty_eq (α n) : @mkEmpty α n = #[] := rfl - -@[deprecated size_toArray (since := "2024-12-11")] -theorem size_mk (as : List α) : (Array.mk as).size = as.length := by simp [size] - -theorem foldrM_push [Monad m] (f : α → β → m β) (init : β) (arr : Array α) (a : α) : - (arr.push a).foldrM f init = f a init >>= arr.foldrM f := by - simp only [foldrM_eq_reverse_foldlM_toList, push_toList, List.reverse_append, List.reverse_cons, - List.reverse_nil, List.nil_append, List.singleton_append, List.foldlM_cons, List.foldlM_reverse] - -/-- -Variant of `foldrM_push` with `h : start = arr.size + 1` -rather than `(arr.push a).size` as the argument. --/ -@[simp] theorem foldrM_push' [Monad m] (f : α → β → m β) (init : β) (arr : Array α) (a : α) - {start} (h : start = arr.size + 1) : - (arr.push a).foldrM f init start = f a init >>= arr.foldrM f := by - simp [← foldrM_push, h] - -theorem foldr_push (f : α → β → β) (init : β) (arr : Array α) (a : α) : - (arr.push a).foldr f init = arr.foldr f (f a init) := foldrM_push .. - -/-- -Variant of `foldr_push` with the `h : start = arr.size + 1` -rather than `(arr.push a).size` as the argument. --/ -@[simp] theorem foldr_push' (f : α → β → β) (init : β) (arr : Array α) (a : α) {start} - (h : start = arr.size + 1) : (arr.push a).foldr f init start = arr.foldr f (f a init) := - foldrM_push' _ _ _ _ h - -/-- A more efficient version of `arr.toList.reverse`. -/ -@[inline] def toListRev (arr : Array α) : List α := arr.foldl (fun l t => t :: l) [] - -@[simp] theorem toListRev_eq (arr : Array α) : arr.toListRev = arr.toList.reverse := by - rw [toListRev, ← foldl_toList, ← List.foldr_reverse, List.foldr_cons_nil] +/-! ### map -/ theorem mapM_eq_foldlM [Monad m] [LawfulMonad m] (f : α → m β) (arr : Array α) : arr.mapM f = arr.foldlM (fun bs a => bs.push <$> f a) #[] := by @@ -1070,6 +1027,11 @@ where induction l generalizing arr <;> simp [*] simp [H] +@[simp] theorem _root_.List.map_toArray (f : α → β) (l : List α) : + l.toArray.map f = (l.map f).toArray := by + apply ext' + simp + @[simp] theorem size_map (f : α → β) (arr : Array α) : (arr.map f).size = arr.size := by simp only [← length_toList] simp @@ -1079,6 +1041,128 @@ where @[simp] theorem map_empty (f : α → β) : map f #[] = #[] := mapM_empty f +@[simp] theorem getElem_map (f : α → β) (a : Array α) (i : Nat) (hi : i < (a.map f).size) : + (a.map f)[i] = f (a[i]'(by simpa using hi)) := by + cases a + simp + +@[simp] theorem getElem?_map (f : α → β) (as : Array α) (i : Nat) : + (as.map f)[i]? = as[i]?.map f := by + simp [getElem?_def] + +@[simp] theorem map_id_fun : map (id : α → α) = id := by + funext l + induction l <;> simp_all + +/-- `map_id_fun'` differs from `map_id_fun` by representing the identity function as a lambda, rather than `id`. -/ +@[simp] theorem map_id_fun' : map (fun (a : α) => a) = id := map_id_fun + +-- This is not a `@[simp]` lemma because `map_id_fun` will apply. +theorem map_id (l : Array α) : map (id : α → α) l = l := by + cases l <;> simp_all + +/-- `map_id'` differs from `map_id` by representing the identity function as a lambda, rather than `id`. -/ +-- This is not a `@[simp]` lemma because `map_id_fun'` will apply. +theorem map_id' (l : Array α) : map (fun (a : α) => a) l = l := map_id l + +/-- Variant of `map_id`, with a side condition that the function is pointwise the identity. -/ +theorem map_id'' {f : α → α} (h : ∀ x, f x = x) (l : Array α) : map f l = l := by + simp [show f = id from funext h] + +theorem map_singleton (f : α → β) (a : α) : map f #[a] = #[f a] := rfl + +@[simp] theorem mem_map {f : α → β} {l : Array α} : b ∈ l.map f ↔ ∃ a, a ∈ l ∧ f a = b := by + simp only [mem_def, toList_map, List.mem_map] + +theorem exists_of_mem_map (h : b ∈ map f l) : ∃ a, a ∈ l ∧ f a = b := mem_map.1 h + +theorem mem_map_of_mem (f : α → β) (h : a ∈ l) : f a ∈ map f l := mem_map.2 ⟨_, h, rfl⟩ + +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_inj_left {f g : α → β} : map f l = map g l ↔ ∀ a ∈ l, f a = g a := by + cases l <;> simp_all + +theorem map_congr_left (h : ∀ a ∈ l, f a = g a) : map f l = map g l := + map_inj_left.2 h + +theorem map_inj : map f = map g ↔ f = g := by + constructor + · 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 + +@[simp] theorem map_map {f : α → β} {g : β → γ} {as : Array α} : + (as.map f).map g = as.map (g ∘ f) := by + cases as; simp + +@[simp] theorem map_push {f : α → β} {as : Array α} {x : α} : + (as.push x).map f = (as.map f).push (f x) := by + ext + · simp + · simp only [getElem_map, getElem_push, size_map] + split <;> rfl + +theorem mapM_eq_mapM_toList [Monad m] [LawfulMonad m] (f : α → m β) (arr : Array α) : + arr.mapM f = List.toArray <$> (arr.toList.mapM f) := by + rw [mapM_eq_foldlM, ← foldlM_toList, ← List.foldrM_reverse] + conv => rhs; rw [← List.reverse_reverse arr.toList] + induction arr.toList.reverse with + | nil => simp + | cons a l ih => simp [ih] + +@[simp] theorem toList_mapM [Monad m] [LawfulMonad m] (f : α → m β) (arr : Array α) : + toList <$> arr.mapM f = arr.toList.mapM f := by + simp [mapM_eq_mapM_toList] + +theorem mapM_map_eq_foldl (as : Array α) (f : α → β) (i) : + mapM.map (m := Id) f as i b = as.foldl (start := i) (fun r a => r.push (f a)) b := by + unfold mapM.map + split <;> rename_i h + · simp only [Id.bind_eq] + dsimp [foldl, Id.run, foldlM] + rw [mapM_map_eq_foldl, dif_pos (by omega), foldlM.loop, dif_pos h] + -- Calling `split` here gives a bad goal. + have : size as - i = Nat.succ (size as - i - 1) := by omega + rw [this] + simp [foldl, foldlM, Id.run, Nat.sub_add_eq] + · dsimp [foldl, Id.run, foldlM] + rw [dif_pos (by omega), foldlM.loop, dif_neg h] + rfl +termination_by as.size - i + +theorem map_eq_foldl (as : Array α) (f : α → β) : + as.map f = as.foldl (fun r a => r.push (f a)) #[] := + mapM_map_eq_foldl _ _ _ + +theorem singleton_eq_toArray_singleton (a : α) : #[a] = [a].toArray := rfl + +@[simp] theorem singleton_def (v : α) : singleton v = #[v] := rfl + +-- This is a duplicate of `List.toArray_toList`. +-- It's confusing to guess which namespace this theorem should live in, +-- so we provide both. +@[simp] theorem toArray_toList (a : Array α) : a.toList.toArray = a := rfl + +@[simp] theorem mkEmpty_eq (α n) : @mkEmpty α n = #[] := rfl + +@[deprecated size_toArray (since := "2024-12-11")] +theorem size_mk (as : List α) : (Array.mk as).size = as.length := by simp [size] + +/-- A more efficient version of `arr.toList.reverse`. -/ +@[inline] def toListRev (arr : Array α) : List α := arr.foldl (fun l t => t :: l) [] + +@[simp] theorem toListRev_eq (arr : Array α) : arr.toListRev = arr.toList.reverse := by + rw [toListRev, ← foldl_toList, ← List.foldr_reverse, List.foldr_cons_nil] + @[simp] theorem appendList_nil (arr : Array α) : arr ++ ([] : List α) = arr := Array.ext' (by simp) @[simp] theorem appendList_cons (arr : Array α) (a : α) (l : List α) : @@ -1094,7 +1178,6 @@ theorem foldl_toList_eq_map (l : List α) (acc : Array β) (G : α → β) : (l.foldl (fun acc a => acc.push (G a)) acc).toList = acc.toList ++ l.map G := by induction l generalizing acc <;> simp [*] - /-! # uset -/ attribute [simp] uset @@ -1270,18 +1353,16 @@ theorem get_set (a : Array α) (i : Nat) (hi : i < a.size) (j : Nat) (hj : j < a (h : i ≠ j) : (a.set i v)[j]'(by simp [*]) = a[j] := by simp only [set, ← getElem_toList, List.getElem_set_ne h] -private theorem fin_cast_val (e : n = n') (i : Fin n) : e ▸ i = ⟨i.1, e ▸ i.2⟩ := by cases e; rfl - theorem swap_def (a : Array α) (i j : Nat) (hi hj) : a.swap i j hi hj = (a.set i a[j]).set j a[i] (by simpa using hj) := by - simp [swap, fin_cast_val] + simp [swap] @[simp] theorem toList_swap (a : Array α) (i j : Nat) (hi hj) : (a.swap i j hi hj).toList = (a.toList.set i a[j]).set j a[i] := by simp [swap_def] theorem getElem?_swap (a : Array α) (i j : Nat) (hi hj) (k : Nat) : (a.swap i j hi hj)[k]? = if j = k then some a[i] else if i = k then some a[j] else a[k]? := by - simp [swap_def, get?_set, ← getElem_fin_eq_getElem_toList] + simp [swap_def, get?_set] @[simp] theorem swapAt_def (a : Array α) (i : Nat) (v : α) (hi) : a.swapAt i v hi = (a[i], a.set i v) := rfl @@ -1396,6 +1477,90 @@ theorem getElem_range {n : Nat} {x : Nat} (h : x < (Array.range n).size) : (Arra true_and, Nat.not_lt] at h rw [List.getElem?_eq_none_iff.2 ‹_›, List.getElem?_eq_none_iff.2 (a.toList.length_reverse ▸ ‹_›)] +end Array + +open Array + +namespace List + +@[simp] theorem reverse_toArray (l : List α) : l.toArray.reverse = l.reverse.toArray := by + apply ext' + simp only [toList_reverse] + +end List + +namespace Array + +/-! ### foldlM and foldrM -/ + +theorem foldlM_append [Monad m] [LawfulMonad m] (f : β → α → m β) (b) (l l' : Array α) : + (l ++ l').foldlM f b = l.foldlM f b >>= l'.foldlM f := by + cases l + cases l' + rw [List.append_toArray] + simp + +/-- Variant of `foldM_append` with `h : stop = (l ++ l').size`. -/ +@[simp] theorem foldlM_append' [Monad m] [LawfulMonad m] (f : β → α → m β) (b) (l l' : Array α) + (h : stop = (l ++ l').size) : + (l ++ l').foldlM f b 0 stop = l.foldlM f b >>= l'.foldlM f := by + subst h + rw [foldlM_append] + +theorem foldrM_push [Monad m] (f : α → β → m β) (init : β) (arr : Array α) (a : α) : + (arr.push a).foldrM f init = f a init >>= arr.foldrM f := by + simp only [foldrM_eq_reverse_foldlM_toList, push_toList, List.reverse_append, List.reverse_cons, + List.reverse_nil, List.nil_append, List.singleton_append, List.foldlM_cons, List.foldlM_reverse] + +/-- +Variant of `foldrM_push` with `h : start = arr.size + 1` +rather than `(arr.push a).size` as the argument. +-/ +@[simp] theorem foldrM_push' [Monad m] (f : α → β → m β) (init : β) (arr : Array α) (a : α) + {start} (h : start = arr.size + 1) : + (arr.push a).foldrM f init start = f a init >>= arr.foldrM f := by + simp [← foldrM_push, h] + +theorem foldl_eq_foldlM (f : β → α → β) (b) (l : Array α) : + l.foldl f b = l.foldlM (m := Id) f b := by + cases l + simp [List.foldl_eq_foldlM] + +theorem foldr_eq_foldrM (f : α → β → β) (b) (l : Array α) : + l.foldr f b = l.foldrM (m := Id) f b := by + cases l + simp [List.foldr_eq_foldrM] + +@[simp] theorem id_run_foldlM (f : β → α → Id β) (b) (l : Array α) : + Id.run (l.foldlM f b) = l.foldl f b := (foldl_eq_foldlM f b l).symm + +@[simp] theorem id_run_foldrM (f : α → β → Id β) (b) (l : Array α) : + Id.run (l.foldrM f b) = l.foldr f b := (foldr_eq_foldrM f b l).symm + +/-! ### foldl and foldr -/ + +theorem foldr_push (f : α → β → β) (init : β) (arr : Array α) (a : α) : + (arr.push a).foldr f init = arr.foldr f (f a init) := foldrM_push .. + +/-- +Variant of `foldr_push` with the `h : start = arr.size + 1` +rather than `(arr.push a).size` as the argument. +-/ +@[simp] theorem foldr_push' (f : α → β → β) (init : β) (arr : Array α) (a : α) {start} + (h : start = arr.size + 1) : (arr.push a).foldr f init start = arr.foldr f (f a init) := + foldrM_push' _ _ _ _ h + +@[simp] theorem foldl_push_eq_append (l l' : Array α) : l.foldl push l' = l' ++ l := by + cases l + cases l' + simp + +@[simp] theorem foldr_flip_push_eq_append (l l' : Array α) : + l.foldr (fun x y => push y x) l' = l' ++ l.reverse := by + cases l + cases l' + simp + /-! ### take -/ @[simp] theorem size_take_loop (a : Array α) (n : Nat) : (take.loop n a).size = a.size - n := by @@ -1508,22 +1673,6 @@ theorem foldr_congr {as bs : Array α} (h₀ : as = bs) {f g : α → β → β} as.foldr f a start stop = bs.foldr g b start' stop' := by congr -theorem foldl_eq_foldlM (f : β → α → β) (b) (l : Array α) : - l.foldl f b = l.foldlM (m := Id) f b := by - cases l - simp [List.foldl_eq_foldlM] - -theorem foldr_eq_foldrM (f : α → β → β) (b) (l : Array α) : - l.foldr f b = l.foldrM (m := Id) f b := by - cases l - simp [List.foldr_eq_foldrM] - -@[simp] theorem id_run_foldlM (f : β → α → Id β) (b) (l : Array α) : - Id.run (l.foldlM f b) = l.foldl f b := (foldl_eq_foldlM f b l).symm - -@[simp] theorem id_run_foldrM (f : α → β → Id β) (b) (l : Array α) : - Id.run (l.foldrM f b) = l.foldr f b := (foldr_eq_foldrM f b l).symm - theorem foldl_hom (f : α₁ → α₂) (g₁ : α₁ → β → α₁) (g₂ : α₂ → β → α₂) (l : Array β) (init : α₁) (H : ∀ x y, g₂ (f x) y = f (g₁ x y)) : l.foldl g₂ (f init) = f (l.foldl g₁ init) := by cases l @@ -1538,45 +1687,13 @@ theorem foldr_hom (f : β₁ → β₂) (g₁ : α → β₁ → β₁) (g₂ : /-! ### map -/ -@[simp] theorem mem_map {f : α → β} {l : Array α} : b ∈ l.map f ↔ ∃ a, a ∈ l ∧ f a = b := by - simp only [mem_def, toList_map, List.mem_map] - -theorem exists_of_mem_map (h : b ∈ map f l) : ∃ a, a ∈ l ∧ f a = b := mem_map.1 h - -theorem mem_map_of_mem (f : α → β) (h : a ∈ l) : f a ∈ map f l := mem_map.2 ⟨_, h, rfl⟩ - -theorem mapM_eq_mapM_toList [Monad m] [LawfulMonad m] (f : α → m β) (arr : Array α) : - arr.mapM f = List.toArray <$> (arr.toList.mapM f) := by - rw [mapM_eq_foldlM, ← foldlM_toList, ← List.foldrM_reverse] - conv => rhs; rw [← List.reverse_reverse arr.toList] - induction arr.toList.reverse with - | nil => simp - | cons a l ih => simp [ih] - -@[simp] theorem toList_mapM [Monad m] [LawfulMonad m] (f : α → m β) (arr : Array α) : - toList <$> arr.mapM f = arr.toList.mapM f := by - simp [mapM_eq_mapM_toList] - -theorem mapM_map_eq_foldl (as : Array α) (f : α → β) (i) : - mapM.map (m := Id) f as i b = as.foldl (start := i) (fun r a => r.push (f a)) b := by - unfold mapM.map - split <;> rename_i h - · simp only [Id.bind_eq] - dsimp [foldl, Id.run, foldlM] - rw [mapM_map_eq_foldl, dif_pos (by omega), foldlM.loop, dif_pos h] - -- Calling `split` here gives a bad goal. - have : size as - i = Nat.succ (size as - i - 1) := by omega - rw [this] - simp [foldl, foldlM, Id.run, Nat.sub_add_eq] - · dsimp [foldl, Id.run, foldlM] - rw [dif_pos (by omega), foldlM.loop, dif_neg h] - rfl -termination_by as.size - i - -theorem map_eq_foldl (as : Array α) (f : α → β) : - as.map f = as.foldl (fun r a => r.push (f a)) #[] := - mapM_map_eq_foldl _ _ _ +@[simp] theorem map_pop {f : α → β} {as : Array α} : + as.pop.map f = (as.map f).pop := by + ext + · simp + · simp only [getElem_map, getElem_pop, size_map] +@[deprecated "Use `toList_map` or `List.map_toArray` to characterize `Array.map`." (since := "2025-01-06")] theorem map_induction (as : Array α) (f : α → β) (motive : Nat → Prop) (h0 : motive 0) (p : Fin as.size → β → Prop) (hs : ∀ i, motive i.1 → p i (f as[i]) ∧ motive (i+1)) : motive as.size ∧ @@ -1604,36 +1721,13 @@ theorem map_induction (as : Array α) (f : α → β) (motive : Nat → Prop) (h simp only [show j = i by omega] exact (hs _ m).1 +set_option linter.deprecated false in +@[deprecated "Use `toList_map` or `List.map_toArray` to characterize `Array.map`." (since := "2025-01-06")] theorem map_spec (as : Array α) (f : α → β) (p : Fin as.size → β → Prop) (hs : ∀ i, p i (f as[i])) : ∃ eq : (as.map f).size = as.size, ∀ i h, p ⟨i, h⟩ ((as.map f)[i]) := by simpa using map_induction as f (fun _ => True) trivial p (by simp_all) -@[simp] theorem getElem_map (f : α → β) (as : Array α) (i : Nat) (h) : - (as.map f)[i] = f (as[i]'(size_map .. ▸ h)) := by - have := map_spec as f (fun i b => b = f (as[i])) - simp only [implies_true, true_implies] at this - obtain ⟨eq, w⟩ := this - apply w - simp_all - -@[simp] theorem getElem?_map (f : α → β) (as : Array α) (i : Nat) : - (as.map f)[i]? = as[i]?.map f := by - simp [getElem?_def] - -@[simp] theorem map_push {f : α → β} {as : Array α} {x : α} : - (as.push x).map f = (as.map f).push (f x) := by - ext - · simp - · simp only [getElem_map, getElem_push, size_map] - split <;> rfl - -@[simp] theorem map_pop {f : α → β} {as : Array α} : - as.pop.map f = (as.map f).pop := by - ext - · simp - · simp only [getElem_map, getElem_pop, size_map] - /-! ### modify -/ @[simp] theorem size_modify (a : Array α) (i : Nat) (f : α → α) : (a.modify i f).size = a.size := by @@ -2120,10 +2214,6 @@ theorem toListRev_toArray (l : List α) : l.toArray.toListRev = l.reverse := by rw [size_toArray, mapM'_cons, foldlM_toArray] simp [ih] -@[simp] theorem map_toArray (f : α → β) (l : List α) : l.toArray.map f = (l.map f).toArray := by - apply ext' - simp - theorem uset_toArray (l : List α) (i : USize) (a : α) (h : i.toNat < l.toArray.size) : l.toArray.uset i a h = (l.set i.toNat a).toArray := by simp @@ -2132,10 +2222,6 @@ theorem uset_toArray (l : List α) (i : USize) (a : α) (h : i.toNat < l.toArray apply ext' simp -@[simp] theorem reverse_toArray (l : List α) : l.toArray.reverse = l.reverse.toArray := by - apply ext' - simp - @[simp] theorem modify_toArray (f : α → α) (l : List α) : l.toArray.modify i f = (l.modify f i).toArray := by apply ext' @@ -2229,29 +2315,6 @@ namespace Array /-! ### map -/ -@[simp] theorem map_map {f : α → β} {g : β → γ} {as : Array α} : - (as.map f).map g = as.map (g ∘ f) := by - cases as; simp - -@[simp] theorem map_id_fun : map (id : α → α) = id := by - funext l - induction l <;> simp_all - -/-- `map_id_fun'` differs from `map_id_fun` by representing the identity function as a lambda, rather than `id`. -/ -@[simp] theorem map_id_fun' : map (fun (a : α) => a) = id := map_id_fun - --- This is not a `@[simp]` lemma because `map_id_fun` will apply. -theorem map_id (as : Array α) : map (id : α → α) as = as := by - cases as <;> simp_all - -/-- `map_id'` differs from `map_id` by representing the identity function as a lambda, rather than `id`. -/ --- This is not a `@[simp]` lemma because `map_id_fun'` will apply. -theorem map_id' (as : Array α) : map (fun (a : α) => a) as = as := map_id as - -/-- Variant of `map_id`, with a side condition that the function is pointwise the identity. -/ -theorem map_id'' {f : α → α} (h : ∀ x, f x = x) (as : Array α) : map f as = as := by - simp [show f = id from funext h] - 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) diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean index a06c12d4d9..e29c161a31 100644 --- a/src/Init/Data/List/Lemmas.lean +++ b/src/Init/Data/List/Lemmas.lean @@ -757,207 +757,6 @@ theorem length_eq_of_beq [BEq α] {l₁ l₂ : List α} (h : l₁ == l₂) : l | nil => simp | cons b l₂ => simp [isEqv, ih] -/-! ### foldlM and foldrM -/ - -@[simp] theorem foldlM_reverse [Monad m] (l : List α) (f : β → α → m β) (b) : - l.reverse.foldlM f b = l.foldrM (fun x y => f y x) b := rfl - -@[simp] theorem foldlM_append [Monad m] [LawfulMonad m] (f : β → α → m β) (b) (l l' : List α) : - (l ++ l').foldlM f b = l.foldlM f b >>= l'.foldlM f := by - induction l generalizing b <;> simp [*] - -@[simp] theorem foldrM_cons [Monad m] [LawfulMonad m] (a : α) (l) (f : α → β → m β) (b) : - (a :: l).foldrM f b = l.foldrM f b >>= f a := by - simp only [foldrM] - induction l <;> simp_all - -theorem foldl_eq_foldlM (f : β → α → β) (b) (l : List α) : - l.foldl f b = l.foldlM (m := Id) f b := by - induction l generalizing b <;> simp [*, foldl] - -theorem foldr_eq_foldrM (f : α → β → β) (b) (l : List α) : - l.foldr f b = l.foldrM (m := Id) f b := by - induction l <;> simp [*, foldr] - -@[simp] theorem id_run_foldlM (f : β → α → Id β) (b) (l : List α) : - Id.run (l.foldlM f b) = l.foldl f b := (foldl_eq_foldlM f b l).symm - -@[simp] theorem id_run_foldrM (f : α → β → Id β) (b) (l : List α) : - Id.run (l.foldrM f b) = l.foldr f b := (foldr_eq_foldrM f b l).symm - -/-! ### foldl and foldr -/ - -@[simp] theorem foldr_cons_eq_append (l : List α) : l.foldr cons l' = l ++ l' := by - induction l <;> simp [*] - -@[deprecated foldr_cons_eq_append (since := "2024-08-22")] abbrev foldr_self_append := @foldr_cons_eq_append - -@[simp] theorem foldl_flip_cons_eq_append (l : List α) : l.foldl (fun x y => y :: x) l' = l.reverse ++ l' := by - induction l generalizing l' <;> simp [*] - -theorem foldr_cons_nil (l : List α) : l.foldr cons [] = l := by simp - -@[deprecated foldr_cons_nil (since := "2024-09-04")] abbrev foldr_self := @foldr_cons_nil - -theorem foldl_map (f : β₁ → β₂) (g : α → β₂ → α) (l : List β₁) (init : α) : - (l.map f).foldl g init = l.foldl (fun x y => g x (f y)) init := by - induction l generalizing init <;> simp [*] - -theorem foldr_map (f : α₁ → α₂) (g : α₂ → β → β) (l : List α₁) (init : β) : - (l.map f).foldr g init = l.foldr (fun x y => g (f x) y) init := by - induction l generalizing init <;> simp [*] - -theorem foldl_filterMap (f : α → Option β) (g : γ → β → γ) (l : List α) (init : γ) : - (l.filterMap f).foldl g init = l.foldl (fun x y => match f y with | some b => g x b | none => x) init := by - induction l generalizing init with - | nil => rfl - | cons a l ih => - simp only [filterMap_cons, foldl_cons] - cases f a <;> simp [ih] - -theorem foldr_filterMap (f : α → Option β) (g : β → γ → γ) (l : List α) (init : γ) : - (l.filterMap f).foldr g init = l.foldr (fun x y => match f x with | some b => g b y | none => y) init := by - induction l generalizing init with - | nil => rfl - | cons a l ih => - simp only [filterMap_cons, foldr_cons] - cases f a <;> simp [ih] - -theorem foldl_map' (g : α → β) (f : α → α → α) (f' : β → β → β) (a : α) (l : List α) - (h : ∀ x y, f' (g x) (g y) = g (f x y)) : - (l.map g).foldl f' (g a) = g (l.foldl f a) := by - induction l generalizing a - · simp - · simp [*, h] - -theorem foldr_map' (g : α → β) (f : α → α → α) (f' : β → β → β) (a : α) (l : List α) - (h : ∀ x y, f' (g x) (g y) = g (f x y)) : - (l.map g).foldr f' (g a) = g (l.foldr f a) := by - induction l generalizing a - · simp - · simp [*, h] - -theorem foldl_assoc {op : α → α → α} [ha : Std.Associative op] : - ∀ {l : List α} {a₁ a₂}, l.foldl op (op a₁ a₂) = op a₁ (l.foldl op a₂) - | [], a₁, a₂ => rfl - | a :: l, a₁, a₂ => by - simp only [foldl_cons, ha.assoc] - rw [foldl_assoc] - -theorem foldr_assoc {op : α → α → α} [ha : Std.Associative op] : - ∀ {l : List α} {a₁ a₂}, l.foldr op (op a₁ a₂) = op (l.foldr op a₁) a₂ - | [], a₁, a₂ => rfl - | a :: l, a₁, a₂ => by - simp only [foldr_cons, ha.assoc] - rw [foldr_assoc] - -theorem foldl_hom (f : α₁ → α₂) (g₁ : α₁ → β → α₁) (g₂ : α₂ → β → α₂) (l : List β) (init : α₁) - (H : ∀ x y, g₂ (f x) y = f (g₁ x y)) : l.foldl g₂ (f init) = f (l.foldl g₁ init) := by - induction l generalizing init <;> simp [*, H] - -theorem foldr_hom (f : β₁ → β₂) (g₁ : α → β₁ → β₁) (g₂ : α → β₂ → β₂) (l : List α) (init : β₁) - (H : ∀ x y, g₂ x (f y) = f (g₁ x y)) : l.foldr g₂ (f init) = f (l.foldr g₁ init) := by - induction l <;> simp [*, H] - -/-- -Prove a proposition about the result of `List.foldl`, -by proving it for the initial data, -and the implication that the operation applied to any element of the list preserves the property. - -The motive can take values in `Sort _`, so this may be used to construct data, -as well as to prove propositions. --/ -def foldlRecOn {motive : β → Sort _} : ∀ (l : List α) (op : β → α → β) (b : β) (_ : motive b) - (_ : ∀ (b : β) (_ : motive b) (a : α) (_ : a ∈ l), motive (op b a)), motive (List.foldl op b l) - | [], _, _, hb, _ => hb - | hd :: tl, op, b, hb, hl => - foldlRecOn tl op (op b hd) (hl b hb hd (mem_cons_self hd tl)) - fun y hy x hx => hl y hy x (mem_cons_of_mem hd hx) - -@[simp] theorem foldlRecOn_nil {motive : β → Sort _} (hb : motive b) - (hl : ∀ (b : β) (_ : motive b) (a : α) (_ : a ∈ []), motive (op b a)) : - foldlRecOn [] op b hb hl = hb := rfl - -@[simp] theorem foldlRecOn_cons {motive : β → Sort _} (hb : motive b) - (hl : ∀ (b : β) (_ : motive b) (a : α) (_ : a ∈ x :: l), motive (op b a)) : - foldlRecOn (x :: l) op b hb hl = - foldlRecOn l op (op b x) (hl b hb x (mem_cons_self x l)) - (fun b c a m => hl b c a (mem_cons_of_mem x m)) := - rfl - -/-- -Prove a proposition about the result of `List.foldr`, -by proving it for the initial data, -and the implication that the operation applied to any element of the list preserves the property. - -The motive can take values in `Sort _`, so this may be used to construct data, -as well as to prove propositions. --/ -def foldrRecOn {motive : β → Sort _} : ∀ (l : List α) (op : α → β → β) (b : β) (_ : motive b) - (_ : ∀ (b : β) (_ : motive b) (a : α) (_ : a ∈ l), motive (op a b)), motive (List.foldr op b l) - | nil, _, _, hb, _ => hb - | x :: l, op, b, hb, hl => - hl (foldr op b l) - (foldrRecOn l op b hb fun b c a m => hl b c a (mem_cons_of_mem x m)) x (mem_cons_self x l) - -@[simp] theorem foldrRecOn_nil {motive : β → Sort _} (hb : motive b) - (hl : ∀ (b : β) (_ : motive b) (a : α) (_ : a ∈ []), motive (op a b)) : - foldrRecOn [] op b hb hl = hb := rfl - -@[simp] theorem foldrRecOn_cons {motive : β → Sort _} (hb : motive b) - (hl : ∀ (b : β) (_ : motive b) (a : α) (_ : a ∈ x :: l), motive (op a b)) : - foldrRecOn (x :: l) op b hb hl = - hl _ (foldrRecOn l op b hb fun b c a m => hl b c a (mem_cons_of_mem x m)) - x (mem_cons_self x l) := - rfl - -/-- -We can prove that two folds over the same list are related (by some arbitrary relation) -if we know that the initial elements are related and the folding function, for each element of the list, -preserves the relation. --/ -theorem foldl_rel {l : List α} {f g : β → α → β} {a b : β} (r : β → β → Prop) - (h : r a b) (h' : ∀ (a : α), a ∈ l → ∀ (c c' : β), r c c' → r (f c a) (g c' a)) : - r (l.foldl (fun acc a => f acc a) a) (l.foldl (fun acc a => g acc a) b) := by - induction l generalizing a b with - | nil => simp_all - | cons a l ih => - simp only [foldl_cons] - apply ih - · simp_all - · exact fun a m c c' h => h' _ (by simp_all) _ _ h - -/-- -We can prove that two folds over the same list are related (by some arbitrary relation) -if we know that the initial elements are related and the folding function, for each element of the list, -preserves the relation. --/ -theorem foldr_rel {l : List α} {f g : α → β → β} {a b : β} (r : β → β → Prop) - (h : r a b) (h' : ∀ (a : α), a ∈ l → ∀ (c c' : β), r c c' → r (f a c) (g a c')) : - r (l.foldr (fun a acc => f a acc) a) (l.foldr (fun a acc => g a acc) b) := by - induction l generalizing a b with - | nil => simp_all - | cons a l ih => - simp only [foldr_cons] - apply h' - · simp - · exact ih h fun a m c c' h => h' _ (by simp_all) _ _ h - -@[simp] theorem foldl_add_const (l : List α) (a b : Nat) : - l.foldl (fun x _ => x + a) b = b + a * l.length := by - induction l generalizing b with - | nil => simp - | cons y l ih => - simp only [foldl_cons, ih, length_cons, Nat.mul_add, Nat.mul_one, Nat.add_assoc, - Nat.add_comm a] - -@[simp] theorem foldr_add_const (l : List α) (a b : Nat) : - l.foldr (fun _ x => x + a) b = b + a * l.length := by - induction l generalizing b with - | nil => simp - | cons y l ih => - simp only [foldr_cons, ih, length_cons, Nat.mul_add, Nat.mul_one, Nat.add_assoc] - /-! ### getLast -/ theorem getLast_eq_getElem : ∀ (l : List α) (h : l ≠ []), @@ -1216,27 +1015,6 @@ theorem getLast?_tail (l : List α) : (tail l).getLast? = if l.length = 1 then n /-! ### map -/ -@[simp] theorem map_id_fun : map (id : α → α) = id := by - funext l - induction l <;> simp_all - -/-- `map_id_fun'` differs from `map_id_fun` by representing the identity function as a lambda, rather than `id`. -/ -@[simp] theorem map_id_fun' : map (fun (a : α) => a) = id := map_id_fun - --- This is not a `@[simp]` lemma because `map_id_fun` will apply. -theorem map_id (l : List α) : map (id : α → α) l = l := by - induction l <;> simp_all - -/-- `map_id'` differs from `map_id` by representing the identity function as a lambda, rather than `id`. -/ --- This is not a `@[simp]` lemma because `map_id_fun'` will apply. -theorem map_id' (l : List α) : map (fun (a : α) => a) l = l := map_id l - -/-- Variant of `map_id`, with a side condition that the function is pointwise the identity. -/ -theorem map_id'' {f : α → α} (h : ∀ x, f x = x) (l : List α) : map f l = l := by - simp [show f = id from funext h] - -theorem map_singleton (f : α → β) (a : α) : map f [a] = [f a] := rfl - @[simp] theorem length_map (as : List α) (f : α → β) : (as.map f).length = as.length := by induction as with | nil => simp [List.map] @@ -1262,6 +1040,27 @@ theorem get_map (f : α → β) {l i} : get (map f l) i = f (get l ⟨i, length_map l f ▸ i.2⟩) := by simp +@[simp] theorem map_id_fun : map (id : α → α) = id := by + funext l + induction l <;> simp_all + +/-- `map_id_fun'` differs from `map_id_fun` by representing the identity function as a lambda, rather than `id`. -/ +@[simp] theorem map_id_fun' : map (fun (a : α) => a) = id := map_id_fun + +-- This is not a `@[simp]` lemma because `map_id_fun` will apply. +theorem map_id (l : List α) : map (id : α → α) l = l := by + induction l <;> simp_all + +/-- `map_id'` differs from `map_id` by representing the identity function as a lambda, rather than `id`. -/ +-- This is not a `@[simp]` lemma because `map_id_fun'` will apply. +theorem map_id' (l : List α) : map (fun (a : α) => a) l = l := map_id l + +/-- Variant of `map_id`, with a side condition that the function is pointwise the identity. -/ +theorem map_id'' {f : α → α} (h : ∀ x, f x = x) (l : List α) : map f l = l := by + simp [show f = id from funext h] + +theorem map_singleton (f : α → β) (a : α) : map f [a] = [f a] := rfl + @[simp] theorem mem_map {f : α → β} : ∀ {l : List α}, b ∈ l.map f ↔ ∃ a, a ∈ l ∧ f a = b | [] => by simp | _ :: l => by simp [mem_map (l := l), eq_comm (a := b)] @@ -1961,16 +1760,6 @@ theorem set_append {s t : List α} : (s ++ t).set i x = s ++ t.set (i - s.length) x := by rw [set_append, if_neg (by simp_all)] -@[simp] theorem foldrM_append [Monad m] [LawfulMonad m] (f : α → β → m β) (b) (l l' : List α) : - (l ++ l').foldrM f b = l'.foldrM f b >>= l.foldrM f := by - induction l <;> simp [*] - -@[simp] theorem foldl_append {β : Type _} (f : β → α → β) (b) (l l' : List α) : - (l ++ l').foldl f b = l'.foldl f (l.foldl f b) := by simp [foldl_eq_foldlM] - -@[simp] theorem foldr_append (f : α → β → β) (b) (l l' : List α) : - (l ++ l').foldr f b = l.foldr f (l'.foldr f b) := by simp [foldr_eq_foldrM] - 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 constructor @@ -2119,14 +1908,6 @@ 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`. -theorem foldl_flatten (f : β → α → β) (b : β) (L : List (List α)) : - (flatten L).foldl f b = L.foldl (fun b l => l.foldl f b) b := by - induction L generalizing b <;> simp_all - -theorem foldr_flatten (f : α → β → β) (b : β) (L : List (List α)) : - (flatten L).foldr f b = L.foldr (fun l b => l.foldr f b) b := by - induction L <;> simp_all - @[simp] theorem map_flatten (f : α → β) (L : List (List α)) : map f (flatten L) = flatten (map (map f) L) := by induction L <;> simp_all @@ -2699,10 +2480,114 @@ theorem flatMap_reverse {β} (l : List α) (f : α → List β) : (l.reverse.fla @[simp] theorem reverseAux_eq (as bs : List α) : reverseAux as bs = reverse as ++ bs := reverseAux_eq_append .. +@[simp] theorem reverse_replicate (n) (a : α) : reverse (replicate n a) = replicate n a := + eq_replicate_iff.2 + ⟨by rw [length_reverse, length_replicate], + fun _ h => eq_of_mem_replicate (mem_reverse.1 h)⟩ + + +/-! ### foldlM and foldrM -/ + +@[simp] theorem foldlM_append [Monad m] [LawfulMonad m] (f : β → α → m β) (b) (l l' : List α) : + (l ++ l').foldlM f b = l.foldlM f b >>= l'.foldlM f := by + induction l generalizing b <;> simp [*] + +@[simp] theorem foldrM_cons [Monad m] [LawfulMonad m] (a : α) (l) (f : α → β → m β) (b) : + (a :: l).foldrM f b = l.foldrM f b >>= f a := by + simp only [foldrM] + induction l <;> simp_all + +theorem foldl_eq_foldlM (f : β → α → β) (b) (l : List α) : + l.foldl f b = l.foldlM (m := Id) f b := by + induction l generalizing b <;> simp [*, foldl] + +theorem foldr_eq_foldrM (f : α → β → β) (b) (l : List α) : + l.foldr f b = l.foldrM (m := Id) f b := by + induction l <;> simp [*, foldr] + +@[simp] theorem id_run_foldlM (f : β → α → Id β) (b) (l : List α) : + Id.run (l.foldlM f b) = l.foldl f b := (foldl_eq_foldlM f b l).symm + +@[simp] theorem id_run_foldrM (f : α → β → Id β) (b) (l : List α) : + Id.run (l.foldrM f b) = l.foldr f b := (foldr_eq_foldrM f b l).symm + +@[simp] theorem foldlM_reverse [Monad m] (l : List α) (f : β → α → m β) (b) : + l.reverse.foldlM f b = l.foldrM (fun x y => f y x) b := rfl + @[simp] theorem foldrM_reverse [Monad m] (l : List α) (f : α → β → m β) (b) : l.reverse.foldrM f b = l.foldlM (fun x y => f y x) b := (foldlM_reverse ..).symm.trans <| by simp +/-! ### foldl and foldr -/ + +@[simp] theorem foldr_cons_eq_append (l : List α) : l.foldr cons l' = l ++ l' := by + induction l <;> simp [*] + +@[deprecated foldr_cons_eq_append (since := "2024-08-22")] abbrev foldr_self_append := @foldr_cons_eq_append + +@[simp] theorem foldl_flip_cons_eq_append (l : List α) : l.foldl (fun x y => y :: x) l' = l.reverse ++ l' := by + induction l generalizing l' <;> simp [*] + +theorem foldr_cons_nil (l : List α) : l.foldr cons [] = l := by simp + +@[deprecated foldr_cons_nil (since := "2024-09-04")] abbrev foldr_self := @foldr_cons_nil + +theorem foldl_map (f : β₁ → β₂) (g : α → β₂ → α) (l : List β₁) (init : α) : + (l.map f).foldl g init = l.foldl (fun x y => g x (f y)) init := by + induction l generalizing init <;> simp [*] + +theorem foldr_map (f : α₁ → α₂) (g : α₂ → β → β) (l : List α₁) (init : β) : + (l.map f).foldr g init = l.foldr (fun x y => g (f x) y) init := by + induction l generalizing init <;> simp [*] + +theorem foldl_filterMap (f : α → Option β) (g : γ → β → γ) (l : List α) (init : γ) : + (l.filterMap f).foldl g init = l.foldl (fun x y => match f y with | some b => g x b | none => x) init := by + induction l generalizing init with + | nil => rfl + | cons a l ih => + simp only [filterMap_cons, foldl_cons] + cases f a <;> simp [ih] + +theorem foldr_filterMap (f : α → Option β) (g : β → γ → γ) (l : List α) (init : γ) : + (l.filterMap f).foldr g init = l.foldr (fun x y => match f x with | some b => g b y | none => y) init := by + induction l generalizing init with + | nil => rfl + | cons a l ih => + simp only [filterMap_cons, foldr_cons] + cases f a <;> simp [ih] + +theorem foldl_map' (g : α → β) (f : α → α → α) (f' : β → β → β) (a : α) (l : List α) + (h : ∀ x y, f' (g x) (g y) = g (f x y)) : + (l.map g).foldl f' (g a) = g (l.foldl f a) := by + induction l generalizing a + · simp + · simp [*, h] + +theorem foldr_map' (g : α → β) (f : α → α → α) (f' : β → β → β) (a : α) (l : List α) + (h : ∀ x y, f' (g x) (g y) = g (f x y)) : + (l.map g).foldr f' (g a) = g (l.foldr f a) := by + induction l generalizing a + · simp + · simp [*, h] + +@[simp] theorem foldrM_append [Monad m] [LawfulMonad m] (f : α → β → m β) (b) (l l' : List α) : + (l ++ l').foldrM f b = l'.foldrM f b >>= l.foldrM f := by + induction l <;> simp [*] + +@[simp] theorem foldl_append {β : Type _} (f : β → α → β) (b) (l l' : List α) : + (l ++ l').foldl f b = l'.foldl f (l.foldl f b) := by simp [foldl_eq_foldlM] + +@[simp] theorem foldr_append (f : α → β → β) (b) (l l' : List α) : + (l ++ l').foldr f b = l.foldr f (l'.foldr f b) := by simp [foldr_eq_foldrM] + +theorem foldl_flatten (f : β → α → β) (b : β) (L : List (List α)) : + (flatten L).foldl f b = L.foldl (fun b l => l.foldl f b) b := by + induction L generalizing b <;> simp_all + +theorem foldr_flatten (f : α → β → β) (b : β) (L : List (List α)) : + (flatten L).foldr f b = L.foldr (fun l b => l.foldr f b) b := by + induction L <;> simp_all + @[simp] theorem foldl_reverse (l : List α) (f : β → α → β) (b) : l.reverse.foldl f b = l.foldr (fun x y => f y x) b := by simp [foldl_eq_foldlM, foldr_eq_foldrM] @@ -2716,10 +2601,127 @@ theorem foldl_eq_foldr_reverse (l : List α) (f : β → α → β) (b) : theorem foldr_eq_foldl_reverse (l : List α) (f : α → β → β) (b) : l.foldr f b = l.reverse.foldl (fun x y => f y x) b := by simp -@[simp] theorem reverse_replicate (n) (a : α) : reverse (replicate n a) = replicate n a := - eq_replicate_iff.2 - ⟨by rw [length_reverse, length_replicate], - fun _ h => eq_of_mem_replicate (mem_reverse.1 h)⟩ +theorem foldl_assoc {op : α → α → α} [ha : Std.Associative op] : + ∀ {l : List α} {a₁ a₂}, l.foldl op (op a₁ a₂) = op a₁ (l.foldl op a₂) + | [], a₁, a₂ => rfl + | a :: l, a₁, a₂ => by + simp only [foldl_cons, ha.assoc] + rw [foldl_assoc] + +theorem foldr_assoc {op : α → α → α} [ha : Std.Associative op] : + ∀ {l : List α} {a₁ a₂}, l.foldr op (op a₁ a₂) = op (l.foldr op a₁) a₂ + | [], a₁, a₂ => rfl + | a :: l, a₁, a₂ => by + simp only [foldr_cons, ha.assoc] + rw [foldr_assoc] + +theorem foldl_hom (f : α₁ → α₂) (g₁ : α₁ → β → α₁) (g₂ : α₂ → β → α₂) (l : List β) (init : α₁) + (H : ∀ x y, g₂ (f x) y = f (g₁ x y)) : l.foldl g₂ (f init) = f (l.foldl g₁ init) := by + induction l generalizing init <;> simp [*, H] + +theorem foldr_hom (f : β₁ → β₂) (g₁ : α → β₁ → β₁) (g₂ : α → β₂ → β₂) (l : List α) (init : β₁) + (H : ∀ x y, g₂ x (f y) = f (g₁ x y)) : l.foldr g₂ (f init) = f (l.foldr g₁ init) := by + induction l <;> simp [*, H] + +/-- +Prove a proposition about the result of `List.foldl`, +by proving it for the initial data, +and the implication that the operation applied to any element of the list preserves the property. + +The motive can take values in `Sort _`, so this may be used to construct data, +as well as to prove propositions. +-/ +def foldlRecOn {motive : β → Sort _} : ∀ (l : List α) (op : β → α → β) (b : β) (_ : motive b) + (_ : ∀ (b : β) (_ : motive b) (a : α) (_ : a ∈ l), motive (op b a)), motive (List.foldl op b l) + | [], _, _, hb, _ => hb + | hd :: tl, op, b, hb, hl => + foldlRecOn tl op (op b hd) (hl b hb hd (mem_cons_self hd tl)) + fun y hy x hx => hl y hy x (mem_cons_of_mem hd hx) + +@[simp] theorem foldlRecOn_nil {motive : β → Sort _} (hb : motive b) + (hl : ∀ (b : β) (_ : motive b) (a : α) (_ : a ∈ []), motive (op b a)) : + foldlRecOn [] op b hb hl = hb := rfl + +@[simp] theorem foldlRecOn_cons {motive : β → Sort _} (hb : motive b) + (hl : ∀ (b : β) (_ : motive b) (a : α) (_ : a ∈ x :: l), motive (op b a)) : + foldlRecOn (x :: l) op b hb hl = + foldlRecOn l op (op b x) (hl b hb x (mem_cons_self x l)) + (fun b c a m => hl b c a (mem_cons_of_mem x m)) := + rfl + +/-- +Prove a proposition about the result of `List.foldr`, +by proving it for the initial data, +and the implication that the operation applied to any element of the list preserves the property. + +The motive can take values in `Sort _`, so this may be used to construct data, +as well as to prove propositions. +-/ +def foldrRecOn {motive : β → Sort _} : ∀ (l : List α) (op : α → β → β) (b : β) (_ : motive b) + (_ : ∀ (b : β) (_ : motive b) (a : α) (_ : a ∈ l), motive (op a b)), motive (List.foldr op b l) + | nil, _, _, hb, _ => hb + | x :: l, op, b, hb, hl => + hl (foldr op b l) + (foldrRecOn l op b hb fun b c a m => hl b c a (mem_cons_of_mem x m)) x (mem_cons_self x l) + +@[simp] theorem foldrRecOn_nil {motive : β → Sort _} (hb : motive b) + (hl : ∀ (b : β) (_ : motive b) (a : α) (_ : a ∈ []), motive (op a b)) : + foldrRecOn [] op b hb hl = hb := rfl + +@[simp] theorem foldrRecOn_cons {motive : β → Sort _} (hb : motive b) + (hl : ∀ (b : β) (_ : motive b) (a : α) (_ : a ∈ x :: l), motive (op a b)) : + foldrRecOn (x :: l) op b hb hl = + hl _ (foldrRecOn l op b hb fun b c a m => hl b c a (mem_cons_of_mem x m)) + x (mem_cons_self x l) := + rfl + +/-- +We can prove that two folds over the same list are related (by some arbitrary relation) +if we know that the initial elements are related and the folding function, for each element of the list, +preserves the relation. +-/ +theorem foldl_rel {l : List α} {f g : β → α → β} {a b : β} (r : β → β → Prop) + (h : r a b) (h' : ∀ (a : α), a ∈ l → ∀ (c c' : β), r c c' → r (f c a) (g c' a)) : + r (l.foldl (fun acc a => f acc a) a) (l.foldl (fun acc a => g acc a) b) := by + induction l generalizing a b with + | nil => simp_all + | cons a l ih => + simp only [foldl_cons] + apply ih + · simp_all + · exact fun a m c c' h => h' _ (by simp_all) _ _ h + +/-- +We can prove that two folds over the same list are related (by some arbitrary relation) +if we know that the initial elements are related and the folding function, for each element of the list, +preserves the relation. +-/ +theorem foldr_rel {l : List α} {f g : α → β → β} {a b : β} (r : β → β → Prop) + (h : r a b) (h' : ∀ (a : α), a ∈ l → ∀ (c c' : β), r c c' → r (f a c) (g a c')) : + r (l.foldr (fun a acc => f a acc) a) (l.foldr (fun a acc => g a acc) b) := by + induction l generalizing a b with + | nil => simp_all + | cons a l ih => + simp only [foldr_cons] + apply h' + · simp + · exact ih h fun a m c c' h => h' _ (by simp_all) _ _ h + +@[simp] theorem foldl_add_const (l : List α) (a b : Nat) : + l.foldl (fun x _ => x + a) b = b + a * l.length := by + induction l generalizing b with + | nil => simp + | cons y l ih => + simp only [foldl_cons, ih, length_cons, Nat.mul_add, Nat.mul_one, Nat.add_assoc, + Nat.add_comm a] + +@[simp] theorem foldr_add_const (l : List α) (a b : Nat) : + l.foldr (fun _ x => x + a) b = b + a * l.length := by + induction l generalizing b with + | nil => simp + | cons y l ih => + simp only [foldr_cons, ih, length_cons, Nat.mul_add, Nat.mul_one, Nat.add_assoc] + /-! #### Further results about `getLast` and `getLast?` -/ diff --git a/src/Init/Data/Vector/Basic.lean b/src/Init/Data/Vector/Basic.lean index 44553e7634..31e3e430bc 100644 --- a/src/Init/Data/Vector/Basic.lean +++ b/src/Init/Data/Vector/Basic.lean @@ -136,6 +136,18 @@ This will perform the update destructively provided that the vector has a refere @[inline] def set! (v : Vector α n) (i : Nat) (x : α) : Vector α n := ⟨v.toArray.set! i x, by simp⟩ +@[inline] def foldlM [Monad m] (f : β → α → m β) (b : β) (v : Vector α n) : m β := + v.toArray.foldlM f b + +@[inline] def foldrM [Monad m] (f : α → β → m β) (b : β) (v : Vector α n) : m β := + v.toArray.foldrM f b + +@[inline] def foldl (f : β → α → β) (b : β) (v : Vector α n) : β := + v.toArray.foldl f b + +@[inline] def foldr (f : α → β → β) (b : β) (v : Vector α n) : β := + v.toArray.foldr f b + /-- Append two vectors. -/ @[inline] def append (v : Vector α n) (w : Vector α m) : Vector α (n + m) := ⟨v.toArray ++ w.toArray, by simp⟩ diff --git a/src/Init/Data/Vector/Lemmas.lean b/src/Init/Data/Vector/Lemmas.lean index 0f91c8ba9d..88ccbc6dcb 100644 --- a/src/Init/Data/Vector/Lemmas.lean +++ b/src/Init/Data/Vector/Lemmas.lean @@ -66,6 +66,18 @@ theorem toArray_mk (a : Array α) (h : a.size = n) : (Vector.mk a h).toArray = a @[simp] theorem back?_mk (a : Array α) (h : a.size = n) : (Vector.mk a h).back? = a.back? := rfl +@[simp] theorem foldlM_mk [Monad m] (f : β → α → m β) (b : β) (a : Array α) (h : a.size = n) : + (Vector.mk a h).foldlM f b = a.foldlM f b := rfl + +@[simp] theorem foldrM_mk [Monad m] (f : α → β → m β) (b : β) (a : Array α) (h : a.size = n) : + (Vector.mk a h).foldrM f b = a.foldrM f b := rfl + +@[simp] theorem foldl_mk (f : β → α → β) (b : β) (a : Array α) (h : a.size = n) : + (Vector.mk a h).foldl f b = a.foldl f b := rfl + +@[simp] theorem foldr_mk (f : α → β → β) (b : β) (a : Array α) (h : a.size = n) : + (Vector.mk a h).foldr f b = a.foldr f b := rfl + @[simp] theorem drop_mk (a : Array α) (h : a.size = n) (m) : (Vector.mk a h).drop m = Vector.mk (a.extract m a.size) (by simp [h]) := rfl @@ -1025,6 +1037,13 @@ theorem mem_setIfInBounds (v : Vector α n) (i : Nat) (hi : i < n) (a : α) : /-! Content below this point has not yet been aligned with `List` and `Array`. -/ +/-! ### map -/ + +@[simp] theorem getElem_map (f : α → β) (a : Vector α n) (i : Nat) (hi : i < n) : + (a.map f)[i] = f a[i] := by + cases a + simp + @[simp] theorem getElem_ofFn {α n} (f : Fin n → α) (i : Nat) (h : i < n) : (Vector.ofFn f)[i] = f ⟨i, by simpa using h⟩ := by simp [ofFn] @@ -1088,13 +1107,6 @@ theorem getElem_append_right {a : Vector α n} {b : Vector α m} {i : Nat} (h : cases a simp -/-! ### map -/ - -@[simp] theorem getElem_map (f : α → β) (a : Vector α n) (i : Nat) (hi : i < n) : - (a.map f)[i] = f a[i] := by - cases a - simp - /-! ### zipWith -/ @[simp] theorem getElem_zipWith (f : α → β → γ) (a : Vector α n) (b : Vector β n) (i : Nat) @@ -1103,6 +1115,37 @@ theorem getElem_append_right {a : Vector α n} {b : Vector α m} {i : Nat} (h : cases b simp +/-! ### foldlM and foldrM -/ + +@[simp] theorem foldlM_append [Monad m] [LawfulMonad m] (f : β → α → m β) (b) (l : Vector α n) (l' : Vector α n') : + (l ++ l').foldlM f b = l.foldlM f b >>= l'.foldlM f := by + cases l + cases l' + simp + +@[simp] theorem foldrM_push [Monad m] (f : α → β → m β) (init : β) (l : Vector α n) (a : α) : + (l.push a).foldrM f init = f a init >>= l.foldrM f := by + cases l + simp + +theorem foldl_eq_foldlM (f : β → α → β) (b) (l : Vector α n) : + l.foldl f b = l.foldlM (m := Id) f b := by + cases l + simp [Array.foldl_eq_foldlM] + +theorem foldr_eq_foldrM (f : α → β → β) (b) (l : Vector α n) : + l.foldr f b = l.foldrM (m := Id) f b := by + cases l + simp [Array.foldr_eq_foldrM] + +@[simp] theorem id_run_foldlM (f : β → α → Id β) (b) (l : Vector α n) : + Id.run (l.foldlM f b) = l.foldl f b := (foldl_eq_foldlM f b l).symm + +@[simp] theorem id_run_foldrM (f : α → β → Id β) (b) (l : Vector α n) : + Id.run (l.foldrM f b) = l.foldr f b := (foldr_eq_foldrM f b l).symm + +/-! ### foldl and foldr -/ + /-! ### take -/ @[simp] theorem take_size (a : Vector α n) : a.take n = a.cast (by simp) := by