From 623dec1047d855a1c0659d0c44c016aeb823ab7d Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Thu, 9 Jan 2025 13:27:20 +1100 Subject: [PATCH] feat: aligning `List/Array/Vector` lemmas for `map` (#6586) This PR continues aligning `List/Array/Vector` lemmas, finishing up lemmas about `map`. --- src/Init/Data/Array/Lemmas.lean | 94 ++++++++++++++++------ src/Init/Data/List/Lemmas.lean | 7 +- src/Init/Data/Vector/Basic.lean | 2 +- src/Init/Data/Vector/Lemmas.lean | 133 +++++++++++++++++++++++++++++-- 4 files changed, 203 insertions(+), 33 deletions(-) diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean index 8bb29aae6fae..a93201ab419b 100644 --- a/src/Init/Data/Array/Lemmas.lean +++ b/src/Init/Data/Array/Lemmas.lean @@ -1,7 +1,7 @@ /- Copyright (c) 2022 Mario Carneiro. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Mario Carneiro +Authors: Mario Carneiro, Kim Morrison -/ prelude import Init.Data.Nat.Lemmas @@ -1001,8 +1001,6 @@ private theorem beq_of_beq_singleton [BEq α] {a b : α} : #[a] == #[b] → a == cases l₂ simp -/-! Content below this point has not yet been aligned with `List`. -/ - /-! ### map -/ theorem mapM_eq_foldlM [Monad m] [LawfulMonad m] (f : α → m β) (arr : Array α) : @@ -1036,11 +1034,6 @@ where simp only [← length_toList] simp -@[simp] theorem mapM_empty [Monad m] (f : α → m β) : mapM f #[] = pure #[] := by - rw [mapM, mapM.map]; rfl - -@[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 @@ -1050,6 +1043,18 @@ where (as.map f)[i]? = as[i]?.map f := by simp [getElem?_def] +@[simp] theorem mapM_empty [Monad m] (f : α → m β) : mapM f #[] = pure #[] := by + rw [mapM, mapM.map]; rfl + +@[simp] theorem map_empty (f : α → β) : map f #[] = #[] := mapM_empty f + +@[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_id_fun : map (id : α → α) = id := by funext l induction l <;> simp_all @@ -1100,17 +1105,59 @@ theorem map_inj : map f = map g ↔ f = g := by 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⟩ + rcases l₂ with ⟨l₂⟩ + simp only [List.map_toArray, List.push_toArray, mk.injEq, List.map_eq_append_iff] + constructor + · rintro ⟨l₁, l₂, rfl, rfl, h⟩ + simp only [List.map_eq_singleton_iff] at h + obtain ⟨a, rfl, rfl⟩ := h + refine ⟨l₁.toArray, a, by simp⟩ + · rintro ⟨⟨l₁⟩, a, h₁, h₂, rfl⟩ + refine ⟨l₁, [a], by simp_all⟩ + +@[simp] theorem map_eq_singleton_iff {f : α → β} {l : Array α} {b : β} : + map f l = #[b] ↔ ∃ a, l = #[a] ∧ f a = b := by + cases l + simp + +theorem map_eq_map_iff {f g : α → β} {l : Array α} : + map f l = map g l ↔ ∀ a ∈ l, f a = g a := by + cases l <;> simp_all + +theorem map_eq_iff : map f l = l' ↔ ∀ i : Nat, l'[i]? = l[i]?.map f := by + cases l + cases l' + simp [List.map_eq_iff] + +theorem map_eq_foldl (f : α → β) (l : Array α) : + map f l = foldl (fun bs a => bs.push (f a)) #[] l := by + simpa using mapM_eq_foldlM (m := Id) f l + +@[simp] theorem map_set {f : α → β} {l : Array α} {i : Nat} {h : i < l.size} {a : α} : + (l.set i a).map f = (l.map f).set i (f a) (by simpa using h) := by + cases l + simp + +@[simp] theorem map_setIfInBounds {f : α → β} {l : Array α} {i : Nat} {a : α} : + (l.setIfInBounds i a).map f = (l.map f).setIfInBounds i (f a) := by + cases l + simp + +@[simp] theorem map_pop {f : α → β} {l : Array α} : l.pop.map f = (l.map f).pop := by + cases l + simp + +@[simp] theorem back?_map {f : α → β} {l : Array α} : (l.map f).back? = l.back?.map f := by + cases l + simp + @[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] @@ -1123,6 +1170,7 @@ theorem mapM_eq_mapM_toList [Monad m] [LawfulMonad m] (f : α → m β) (arr : A toList <$> arr.mapM f = arr.toList.mapM f := by simp [mapM_eq_mapM_toList] +@[deprecated "Use `mapM_eq_foldlM` instead" (since := "2025-01-08")] 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 @@ -1139,9 +1187,7 @@ theorem mapM_map_eq_foldl (as : Array α) (f : α → β) (i) : 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 _ _ _ +/-! Content below this point has not yet been aligned with `List`. -/ theorem singleton_eq_toArray_singleton (a : α) : #[a] = [a].toArray := rfl @@ -1687,12 +1733,6 @@ theorem foldr_hom (f : β₁ → β₂) (g₁ : α → β₁ → β₁) (g₂ : /-! ### map -/ -@[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)) : @@ -2368,6 +2408,12 @@ theorem foldr_map' (g : α → β) (f : α → α → α) (f' : β → β → β | nil => simp | cons xs xss ih => simp [ih] +/-! ### mkArray -/ + +@[simp] theorem mem_mkArray (a : α) (n : Nat) : b ∈ mkArray n a ↔ n ≠ 0 ∧ b = a := by + rw [mkArray, mem_toArray] + simp + /-! ### 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 e29c161a31f0..49333f6b8b90 100644 --- a/src/Init/Data/List/Lemmas.lean +++ b/src/Init/Data/List/Lemmas.lean @@ -1,7 +1,8 @@ /- Copyright (c) 2014 Parikshit Khanna. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Mario Carneiro +Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Mario Carneiro, + Kim Morrison -/ prelude import Init.Data.Bool @@ -1114,6 +1115,10 @@ theorem map_eq_cons_iff' {f : α → β} {l : List α} : @[deprecated map_eq_cons' (since := "2024-09-05")] abbrev map_eq_cons' := @map_eq_cons_iff' +@[simp] theorem map_eq_singleton_iff {f : α → β} {l : List α} {b : β} : + map f l = [b] ↔ ∃ a, l = [a] ∧ f a = b := by + simp [map_eq_cons_iff] + theorem map_eq_map_iff : map f l = map g l ↔ ∀ a ∈ l, f a = g a := by induction l <;> simp diff --git a/src/Init/Data/Vector/Basic.lean b/src/Init/Data/Vector/Basic.lean index 31e3e430bc69..53b9327d212a 100644 --- a/src/Init/Data/Vector/Basic.lean +++ b/src/Init/Data/Vector/Basic.lean @@ -103,7 +103,7 @@ of bounds. @[inline] def head [NeZero n] (v : Vector α n) := v[0]'(Nat.pos_of_neZero n) /-- Push an element `x` to the end of a vector. -/ -@[inline] def push (x : α) (v : Vector α n) : Vector α (n + 1) := +@[inline] def push (v : Vector α n) (x : α) : Vector α (n + 1) := ⟨v.toArray.push x, by simp⟩ /-- Remove the last element of a vector. -/ diff --git a/src/Init/Data/Vector/Lemmas.lean b/src/Init/Data/Vector/Lemmas.lean index 88ccbc6dcb63..f8fb2eaf2e0c 100644 --- a/src/Init/Data/Vector/Lemmas.lean +++ b/src/Init/Data/Vector/Lemmas.lean @@ -1,7 +1,7 @@ /- Copyright (c) 2024 Shreyas Srinivas. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Shreyas Srinivas, Francois Dorais +Authors: Shreyas Srinivas, Francois Dorais, Kim Morrison -/ prelude import Init.Data.Vector.Basic @@ -153,6 +153,14 @@ theorem toArray_mk (a : Array α) (h : a.size = n) : (Vector.mk a h).toArray = a @[simp] theorem all_mk (p : α → Bool) (a : Array α) (h : a.size = n) : (Vector.mk a h).all p = a.all p := rfl +@[simp] theorem eq_mk : v = Vector.mk a h ↔ v.toArray = a := by + cases v + simp + +@[simp] theorem mk_eq : Vector.mk a h = v ↔ a = v.toArray := by + cases v + simp + /-! ### toArray lemmas -/ @[simp] theorem getElem_toArray {α n} (xs : Vector α n) (i : Nat) (h : i < xs.toArray.size) : @@ -1035,8 +1043,6 @@ theorem mem_setIfInBounds (v : Vector α n) (i : Nat) (hi : i < n) (a : α) : cases l₂ simp -/-! 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) : @@ -1044,16 +1050,129 @@ theorem mem_setIfInBounds (v : Vector α n) (i : Nat) (hi : i < n) (a : α) : 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] - /-- The empty vector maps to the empty vector. -/ @[simp] theorem map_empty (f : α → β) : map f #v[] = #v[] := by rw [map, mk.injEq] exact Array.map_empty f +@[simp] theorem map_push {f : α → β} {as : Vector α n} {x : α} : + (as.push x).map f = (as.map f).push (f x) := by + cases as + simp + +@[simp] theorem map_id_fun : map (n := n) (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 (n := n) (fun (a : α) => a) = id := map_id_fun + +-- This is not a `@[simp]` lemma because `map_id_fun` will apply. +theorem map_id (l : Vector α n) : 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 : Vector α n) : 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 : Vector α n) : map f l = l := by + simp [show f = id from funext h] + +theorem map_singleton (f : α → β) (a : α) : map f #v[a] = #v[f a] := rfl + +@[simp] theorem mem_map {f : α → β} {l : Vector α n} : b ∈ l.map f ↔ ∃ a, a ∈ l ∧ f a = b := by + cases l + simp + +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 : Vector α n} {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 [NeZero n] : map (n := n) f = map g ↔ f = g := by + constructor + · intro h + ext a + replace h := congrFun h (mkVector n a) + simp only [mkVector, map_mk, mk.injEq, Array.map_inj_left, Array.mem_mkArray, and_imp, + forall_eq_apply_imp_iff] at h + exact h (NeZero.ne n) + · intro h; subst h; rfl + +theorem map_eq_push_iff {f : α → β} {l : Vector α (n + 1)} {l₂ : Vector β n} {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, h⟩ + rcases l₂ with ⟨l₂, rfl⟩ + simp only [map_mk, push_mk, mk.injEq, Array.map_eq_push_iff] + constructor + · rintro ⟨l₁, a, rfl, rfl, rfl⟩ + refine ⟨⟨l₁, by simp⟩, a, by simp⟩ + · rintro ⟨l₁, a, h₁, h₂, rfl⟩ + refine ⟨l₁.toArray, a, by simp_all⟩ + +@[simp] theorem map_eq_singleton_iff {f : α → β} {l : Vector α 1} {b : β} : + map f l = #v[b] ↔ ∃ a, l = #v[a] ∧ f a = b := by + cases l + simp + +theorem map_eq_map_iff {f g : α → β} {l : Vector α n} : + map f l = map g l ↔ ∀ a ∈ l, f a = g a := by + cases l <;> simp_all + +theorem map_eq_iff {f : α → β} {l : Vector α n} {l' : Vector β n} : + map f l = l' ↔ ∀ i (h : i < n), l'[i] = f l[i] := by + rcases l with ⟨l, rfl⟩ + rcases l' with ⟨l', h'⟩ + simp only [map_mk, eq_mk, Array.map_eq_iff, getElem_mk] + constructor + · intro w i h + simpa [h, h'] using w i + · intro w i + if h : i < l.size then + simpa [h, h'] using w i h + else + rw [getElem?_neg, getElem?_neg, Option.map_none'] <;> omega + +@[simp] theorem map_set {f : α → β} {l : Vector α n} {i : Nat} {h : i < n} {a : α} : + (l.set i a).map f = (l.map f).set i (f a) (by simpa using h) := by + cases l + simp + +@[simp] theorem map_setIfInBounds {f : α → β} {l : Vector α n} {i : Nat} {a : α} : + (l.setIfInBounds i a).map f = (l.map f).setIfInBounds i (f a) := by + cases l + simp + +@[simp] theorem map_pop {f : α → β} {l : Vector α n} : l.pop.map f = (l.map f).pop := by + cases l + simp + +@[simp] theorem back?_map {f : α → β} {l : Vector α n} : (l.map f).back? = l.back?.map f := by + cases l + simp + +@[simp] theorem map_map {f : α → β} {g : β → γ} {as : Vector α n} : + (as.map f).map g = as.map (g ∘ f) := by + cases as + simp + +/-! 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) : + (Vector.ofFn f)[i] = f ⟨i, by simpa using h⟩ := by + simp [ofFn] + @[simp] theorem getElem_push_last {v : Vector α n} {x : α} : (v.push x)[n] = x := by rcases v with ⟨data, rfl⟩ simp