chore: alignment of Array and List lemmas
diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean index 8e2a62e..b04bb16 100644 --- a/src/Init/Data/Array/Basic.lean +++ b/src/Init/Data/Array/Basic.lean
@@ -11,7 +11,7 @@ import Init.Data.Repr import Init.Data.ToString.Basic import Init.GetElem -import Init.Data.List.ToArray +import Init.Data.List.ToArrayImpl import Init.Data.Array.Set universe u v w @@ -99,6 +99,9 @@ theorem mem_def {a : α} {as : Array α} : a ∈ as ↔ a ∈ as.toList := ⟨fun | .mk h => h, Array.Mem.mk⟩ +@[simp] theorem mem_toArray {a : α} {l : List α} : a ∈ l.toArray ↔ a ∈ l := by + simp [mem_def] + @[simp] theorem getElem_mem {l : Array α} {i : Nat} (h : i < l.size) : l[i] ∈ l := by rw [Array.mem_def, ← getElem_toList] apply List.getElem_mem @@ -244,7 +247,7 @@ mkArray 1 v def back! [Inhabited α] (a : Array α) : α := - a.get! (a.size - 1) + a[a.size - 1]! @[deprecated back! (since := "2024-10-31")] abbrev back := @back!
diff --git a/src/Init/Data/Array/Find.lean b/src/Init/Data/Array/Find.lean index 48c02b9..cf522fa 100644 --- a/src/Init/Data/Array/Find.lean +++ b/src/Init/Data/Array/Find.lean
@@ -81,7 +81,7 @@ (L.findSome? fun l => l[0]?).isSome := by cases L using array_array_induction simp only [List.findSome?_toArray, List.findSome?_map, Function.comp_def, List.getElem?_toArray, - List.findSome?_isSome_iff, List.isSome_getElem?] + List.findSome?_isSome_iff, isSome_getElem?] simp only [flatten_toArray_map_toArray, size_toArray, List.length_flatten, Nat.sum_pos_iff_exists_pos, List.mem_map] at h obtain ⟨_, ⟨xs, m, rfl⟩, h⟩ := h
diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean index 75a760a..afeeaf5 100644 --- a/src/Init/Data/Array/Lemmas.lean +++ b/src/Init/Data/Array/Lemmas.lean
@@ -5,409 +5,21 @@ -/ prelude import Init.Data.Nat.Lemmas -import Init.Data.List.Impl -import Init.Data.List.Monadic import Init.Data.List.Range import Init.Data.List.Nat.TakeDrop import Init.Data.List.Nat.Modify -import Init.Data.List.Nat.Erase import Init.Data.List.Monadic import Init.Data.List.OfFn import Init.Data.Array.Mem import Init.Data.Array.DecidableEq import Init.TacticsExtra +import Init.Data.List.ToArray /-! ## Theorems about `Array`. -/ -/-! ### Preliminaries about `Array` needed for `List.toArray` lemmas. - -This section contains only the bare minimum lemmas about `Array` -that we need to write lemmas about `List.toArray`. --/ -namespace Array - -@[simp] theorem getElem?_eq_getElem {a : Array α} {i : Nat} (h : i < a.size) : a[i]? = some a[i] := - getElem?_pos .. - -@[simp] theorem getElem?_eq_none_iff {a : Array α} : a[i]? = none ↔ a.size ≤ i := by - by_cases h : i < a.size - · simp [getElem?_eq_getElem, h] - · rw [getElem?_neg a i h] - simp_all - -@[simp] theorem get_eq_getElem (a : Array α) (i : Nat) (h) : a.get i h = a[i] := rfl - -@[simp] theorem get!_eq_getElem! [Inhabited α] (a : Array α) (i : Nat) : a.get! i = a[i]! := by - simp [getElem!_def, get!, getD] - split <;> rename_i h - · simp [getElem?_eq_getElem h] - · simp [getElem?_eq_none_iff.2 (by simpa using h)] - -@[simp] theorem mem_toArray {a : α} {l : List α} : a ∈ l.toArray ↔ a ∈ l := by - simp [mem_def] - -end Array - -/-! ### Lemmas about `List.toArray`. - -We prefer to pull `List.toArray` outwards. --/ -namespace List - -open Array - -theorem toArray_inj {a b : List α} (h : a.toArray = b.toArray) : a = b := by - cases a with - | nil => simpa using h - | cons a as => - cases b with - | nil => simp at h - | cons b bs => simpa using h - -@[simp] theorem size_toArrayAux {a : List α} {b : Array α} : - (a.toArrayAux b).size = b.size + a.length := by - simp [size] - -@[simp] theorem push_toArray (l : List α) (a : α) : l.toArray.push a = (l ++ [a]).toArray := by - apply ext' - simp - -/-- Unapplied variant of `push_toArray`, useful for monadic reasoning. -/ -@[simp] theorem push_toArray_fun (l : List α) : l.toArray.push = fun a => (l ++ [a]).toArray := by - funext a - simp - -@[simp] theorem isEmpty_toArray (l : List α) : l.toArray.isEmpty = l.isEmpty := by - cases l <;> simp - -@[simp] theorem toArray_singleton (a : α) : (List.singleton a).toArray = singleton a := rfl - -@[simp] theorem back!_toArray [Inhabited α] (l : List α) : l.toArray.back! = l.getLast! := by - simp only [back!, size_toArray, Array.get!_eq_getElem!, getElem!_toArray, getLast!_eq_getElem!] - -@[simp] theorem back?_toArray (l : List α) : l.toArray.back? = l.getLast? := by - simp [back?, List.getLast?_eq_getElem?] - -@[simp] theorem set_toArray (l : List α) (i : Nat) (a : α) (h : i < l.length) : - (l.toArray.set i a) = (l.set i a).toArray := rfl - -@[simp] theorem forIn'_loop_toArray [Monad m] (l : List α) (f : (a : α) → a ∈ l.toArray → β → m (ForInStep β)) (i : Nat) - (h : i ≤ l.length) (b : β) : - Array.forIn'.loop l.toArray f i h b = - forIn' (l.drop (l.length - i)) b (fun a m b => f a (by simpa using mem_of_mem_drop m) b) := by - induction i generalizing l b with - | zero => - simp [Array.forIn'.loop] - | succ i ih => - simp only [Array.forIn'.loop, size_toArray, getElem_toArray, ih] - have t : drop (l.length - (i + 1)) l = l[l.length - i - 1] :: drop (l.length - i) l := by - simp only [Nat.sub_add_eq] - rw [List.drop_sub_one (by omega), List.getElem?_eq_getElem (by omega)] - simp only [Option.toList_some, singleton_append] - simp [t] - have t : l.length - 1 - i = l.length - i - 1 := by omega - simp only [t] - congr - -@[simp] theorem forIn'_toArray [Monad m] (l : List α) (b : β) (f : (a : α) → a ∈ l.toArray → β → m (ForInStep β)) : - forIn' l.toArray b f = forIn' l b (fun a m b => f a (mem_toArray.mpr m) b) := by - change Array.forIn' _ _ _ = List.forIn' _ _ _ - rw [Array.forIn', forIn'_loop_toArray] - simp - -@[simp] theorem forIn_toArray [Monad m] (l : List α) (b : β) (f : α → β → m (ForInStep β)) : - forIn l.toArray b f = forIn l b f := by - simpa using forIn'_toArray l b fun a m b => f a b - -theorem foldrM_toArray [Monad m] (f : α → β → m β) (init : β) (l : List α) : - l.toArray.foldrM f init = l.foldrM f init := by - rw [foldrM_eq_reverse_foldlM_toList] - simp - -theorem foldlM_toArray [Monad m] (f : β → α → m β) (init : β) (l : List α) : - l.toArray.foldlM f init = l.foldlM f init := by - rw [foldlM_toList] - -theorem foldr_toArray (f : α → β → β) (init : β) (l : List α) : - l.toArray.foldr f init = l.foldr f init := by - rw [foldr_toList] - -theorem foldl_toArray (f : β → α → β) (init : β) (l : List α) : - l.toArray.foldl f init = l.foldl f init := by - rw [foldl_toList] - -/-- Variant of `foldrM_toArray` with a side condition for the `start` argument. -/ -@[simp] theorem foldrM_toArray' [Monad m] (f : α → β → m β) (init : β) (l : List α) - (h : start = l.toArray.size) : - l.toArray.foldrM f init start 0 = l.foldrM f init := by - subst h - rw [foldrM_eq_reverse_foldlM_toList] - simp - -/-- Variant of `foldlM_toArray` with a side condition for the `stop` argument. -/ -@[simp] theorem foldlM_toArray' [Monad m] (f : β → α → m β) (init : β) (l : List α) - (h : stop = l.toArray.size) : - l.toArray.foldlM f init 0 stop = l.foldlM f init := by - subst h - rw [foldlM_toList] - -/-- Variant of `foldr_toArray` with a side condition for the `start` argument. -/ -@[simp] theorem foldr_toArray' (f : α → β → β) (init : β) (l : List α) - (h : start = l.toArray.size) : - l.toArray.foldr f init start 0 = l.foldr f init := by - subst h - rw [foldr_toList] - -/-- Variant of `foldl_toArray` with a side condition for the `stop` argument. -/ -@[simp] theorem foldl_toArray' (f : β → α → β) (init : β) (l : List α) - (h : stop = l.toArray.size) : - l.toArray.foldl f init 0 stop = l.foldl f init := by - subst h - rw [foldl_toList] - -@[simp] theorem append_toArray (l₁ l₂ : List α) : - l₁.toArray ++ l₂.toArray = (l₁ ++ l₂).toArray := by - apply ext' - simp - -@[simp] theorem push_append_toArray {as : Array α} {a : α} {bs : List α} : as.push a ++ bs.toArray = as ++ (a ::bs).toArray := by - cases as - simp - -@[simp] theorem foldl_push {l : List α} {as : Array α} : l.foldl Array.push as = as ++ l.toArray := by - induction l generalizing as <;> simp [*] - -@[simp] theorem foldr_push {l : List α} {as : Array α} : l.foldr (fun a b => push b a) as = as ++ l.reverse.toArray := by - rw [foldr_eq_foldl_reverse, foldl_push] - -@[simp] theorem findSomeM?_toArray [Monad m] [LawfulMonad m] (f : α → m (Option β)) (l : List α) : - l.toArray.findSomeM? f = l.findSomeM? f := by - rw [Array.findSomeM?] - simp only [bind_pure_comp, map_pure, forIn_toArray] - induction l with - | nil => simp - | cons a l ih => - simp only [forIn_cons, LawfulMonad.bind_assoc, findSomeM?] - congr - ext1 (_|_) <;> simp [ih] - -theorem findSomeRevM?_find_toArray [Monad m] [LawfulMonad m] (f : α → m (Option β)) (l : List α) - (i : Nat) (h) : - findSomeRevM?.find f l.toArray i h = (l.take i).reverse.findSomeM? f := by - induction i generalizing l with - | zero => simp [Array.findSomeRevM?.find.eq_def] - | succ i ih => - rw [size_toArray] at h - rw [Array.findSomeRevM?.find, take_succ, getElem?_eq_getElem (by omega)] - simp only [ih, reverse_append] - congr - ext1 (_|_) <;> simp - --- This is not marked as `@[simp]` as later we simplify all occurrences of `findSomeRevM?`. -theorem findSomeRevM?_toArray [Monad m] [LawfulMonad m] (f : α → m (Option β)) (l : List α) : - l.toArray.findSomeRevM? f = l.reverse.findSomeM? f := by - simp [Array.findSomeRevM?, findSomeRevM?_find_toArray] - --- This is not marked as `@[simp]` as later we simplify all occurrences of `findRevM?`. -theorem findRevM?_toArray [Monad m] [LawfulMonad m] (f : α → m Bool) (l : List α) : - l.toArray.findRevM? f = l.reverse.findM? f := by - rw [Array.findRevM?, findSomeRevM?_toArray, findM?_eq_findSomeM?] - -@[simp] theorem findM?_toArray [Monad m] [LawfulMonad m] (f : α → m Bool) (l : List α) : - l.toArray.findM? f = l.findM? f := by - rw [Array.findM?] - simp only [bind_pure_comp, map_pure, forIn_toArray] - induction l with - | nil => simp - | cons a l ih => - simp only [forIn_cons, LawfulMonad.bind_assoc, findM?] - congr - ext1 (_|_) <;> simp [ih] - -@[simp] theorem findSome?_toArray (f : α → Option β) (l : List α) : - l.toArray.findSome? f = l.findSome? f := by - rw [Array.findSome?, ← findSomeM?_id, findSomeM?_toArray, Id.run] - -@[simp] theorem find?_toArray (f : α → Bool) (l : List α) : - l.toArray.find? f = l.find? f := by - rw [Array.find?] - simp only [Id.run, Id, Id.pure_eq, Id.bind_eq, forIn_toArray] - induction l with - | nil => simp - | cons a l ih => - simp only [forIn_cons, Id.pure_eq, Id.bind_eq, find?] - by_cases f a <;> simp_all - -theorem isPrefixOfAux_toArray_succ [BEq α] (l₁ l₂ : List α) (hle : l₁.length ≤ l₂.length) (i : Nat) : - Array.isPrefixOfAux l₁.toArray l₂.toArray hle (i + 1) = - Array.isPrefixOfAux l₁.tail.toArray l₂.tail.toArray (by simp; omega) i := by - rw [Array.isPrefixOfAux] - conv => rhs; rw [Array.isPrefixOfAux] - simp only [size_toArray, getElem_toArray, Bool.if_false_right, length_tail, getElem_tail] - split <;> rename_i h₁ <;> split <;> rename_i h₂ - · rw [isPrefixOfAux_toArray_succ] - · omega - · omega - · rfl - -theorem isPrefixOfAux_toArray_succ' [BEq α] (l₁ l₂ : List α) (hle : l₁.length ≤ l₂.length) (i : Nat) : - Array.isPrefixOfAux l₁.toArray l₂.toArray hle (i + 1) = - Array.isPrefixOfAux (l₁.drop (i+1)).toArray (l₂.drop (i+1)).toArray (by simp; omega) 0 := by - induction i generalizing l₁ l₂ with - | zero => simp [isPrefixOfAux_toArray_succ] - | succ i ih => - rw [isPrefixOfAux_toArray_succ, ih] - simp - -theorem isPrefixOfAux_toArray_zero [BEq α] (l₁ l₂ : List α) (hle : l₁.length ≤ l₂.length) : - Array.isPrefixOfAux l₁.toArray l₂.toArray hle 0 = - l₁.isPrefixOf l₂ := by - rw [Array.isPrefixOfAux] - match l₁, l₂ with - | [], _ => rw [dif_neg] <;> simp - | _::_, [] => simp at hle - | a::l₁, b::l₂ => - simp [isPrefixOf_cons₂, isPrefixOfAux_toArray_succ', isPrefixOfAux_toArray_zero] - -@[simp] theorem isPrefixOf_toArray [BEq α] (l₁ l₂ : List α) : - l₁.toArray.isPrefixOf l₂.toArray = l₁.isPrefixOf l₂ := by - rw [Array.isPrefixOf] - split <;> rename_i h - · simp [isPrefixOfAux_toArray_zero] - · simp only [Bool.false_eq] - induction l₁ generalizing l₂ with - | nil => simp at h - | cons a l₁ ih => - cases l₂ with - | nil => simp - | cons b l₂ => - simp only [isPrefixOf_cons₂, Bool.and_eq_false_imp] - intro w - rw [ih] - simp_all - -theorem zipWithAux_toArray_succ (as : List α) (bs : List β) (f : α → β → γ) (i : Nat) (cs : Array γ) : - zipWithAux as.toArray bs.toArray f (i + 1) cs = zipWithAux as.tail.toArray bs.tail.toArray f i cs := by - rw [zipWithAux] - conv => rhs; rw [zipWithAux] - simp only [size_toArray, getElem_toArray, length_tail, getElem_tail] - split <;> rename_i h₁ - · split <;> rename_i h₂ - · rw [dif_pos (by omega), dif_pos (by omega), zipWithAux_toArray_succ] - · rw [dif_pos (by omega)] - rw [dif_neg (by omega)] - · rw [dif_neg (by omega)] - -theorem zipWithAux_toArray_succ' (as : List α) (bs : List β) (f : α → β → γ) (i : Nat) (cs : Array γ) : - zipWithAux as.toArray bs.toArray f (i + 1) cs = zipWithAux (as.drop (i+1)).toArray (bs.drop (i+1)).toArray f 0 cs := by - induction i generalizing as bs cs with - | zero => simp [zipWithAux_toArray_succ] - | succ i ih => - rw [zipWithAux_toArray_succ, ih] - simp - -theorem zipWithAux_toArray_zero (f : α → β → γ) (as : List α) (bs : List β) (cs : Array γ) : - zipWithAux as.toArray bs.toArray f 0 cs = cs ++ (List.zipWith f as bs).toArray := by - rw [Array.zipWithAux] - match as, bs with - | [], _ => simp - | _, [] => simp - | a :: as, b :: bs => - simp [zipWith_cons_cons, zipWithAux_toArray_succ', zipWithAux_toArray_zero, push_append_toArray] - -@[simp] theorem zipWith_toArray (as : List α) (bs : List β) (f : α → β → γ) : - Array.zipWith as.toArray bs.toArray f = (List.zipWith f as bs).toArray := by - rw [Array.zipWith] - simp [zipWithAux_toArray_zero] - -@[simp] theorem zip_toArray (as : List α) (bs : List β) : - Array.zip as.toArray bs.toArray = (List.zip as bs).toArray := by - simp [Array.zip, zipWith_toArray, zip] - -theorem zipWithAll_go_toArray (as : List α) (bs : List β) (f : Option α → Option β → γ) (i : Nat) (cs : Array γ) : - zipWithAll.go f as.toArray bs.toArray i cs = cs ++ (List.zipWithAll f (as.drop i) (bs.drop i)).toArray := by - unfold zipWithAll.go - split <;> rename_i h - · rw [zipWithAll_go_toArray] - simp at h - simp only [getElem?_toArray, push_append_toArray] - if ha : i < as.length then - if hb : i < bs.length then - rw [List.drop_eq_getElem_cons ha, List.drop_eq_getElem_cons hb] - simp only [ha, hb, getElem?_eq_getElem, zipWithAll_cons_cons] - else - simp only [Nat.not_lt] at hb - rw [List.drop_eq_getElem_cons ha] - rw [(drop_eq_nil_iff (l := bs)).mpr (by omega), (drop_eq_nil_iff (l := bs)).mpr (by omega)] - simp only [zipWithAll_nil, map_drop, map_cons] - rw [getElem?_eq_getElem ha] - rw [getElem?_eq_none hb] - else - if hb : i < bs.length then - simp only [Nat.not_lt] at ha - rw [List.drop_eq_getElem_cons hb] - rw [(drop_eq_nil_iff (l := as)).mpr (by omega), (drop_eq_nil_iff (l := as)).mpr (by omega)] - simp only [nil_zipWithAll, map_drop, map_cons] - rw [getElem?_eq_getElem hb] - rw [getElem?_eq_none ha] - else - omega - · simp only [size_toArray, Nat.not_lt] at h - rw [drop_eq_nil_of_le (by omega), drop_eq_nil_of_le (by omega)] - simp - termination_by max as.length bs.length - i - decreasing_by simp_wf; decreasing_trivial_pre_omega - -@[simp] theorem zipWithAll_toArray (f : Option α → Option β → γ) (as : List α) (bs : List β) : - Array.zipWithAll as.toArray bs.toArray f = (List.zipWithAll f as bs).toArray := by - simp [Array.zipWithAll, zipWithAll_go_toArray] - -@[simp] theorem toArray_appendList (l₁ l₂ : List α) : - l₁.toArray ++ l₂ = (l₁ ++ l₂).toArray := by - apply ext' - simp - -@[simp] theorem pop_toArray (l : List α) : l.toArray.pop = l.dropLast.toArray := by - apply ext' - simp - -theorem takeWhile_go_succ (p : α → Bool) (a : α) (l : List α) (i : Nat) : - takeWhile.go p (a :: l).toArray (i+1) r = takeWhile.go p l.toArray i r := by - rw [takeWhile.go, takeWhile.go] - simp only [size_toArray, length_cons, Nat.add_lt_add_iff_right, Array.get_eq_getElem, - getElem_toArray, getElem_cons_succ] - split - rw [takeWhile_go_succ] - rfl - -theorem takeWhile_go_toArray (p : α → Bool) (l : List α) (i : Nat) : - Array.takeWhile.go p l.toArray i r = r ++ (takeWhile p (l.drop i)).toArray := by - induction l generalizing i r with - | nil => simp [takeWhile.go] - | cons a l ih => - rw [takeWhile.go] - cases i with - | zero => - simp [takeWhile_go_succ, ih, takeWhile_cons] - split <;> simp - | succ i => - simp only [size_toArray, length_cons, Nat.add_lt_add_iff_right, Array.get_eq_getElem, - getElem_toArray, getElem_cons_succ, drop_succ_cons] - split <;> rename_i h₁ - · rw [takeWhile_go_succ, ih] - rw [← getElem_cons_drop_succ_eq_drop h₁, takeWhile_cons] - split <;> simp_all - · simp_all [drop_eq_nil_of_le] - -@[simp] theorem takeWhile_toArray (p : α → Bool) (l : List α) : - l.toArray.takeWhile p = (l.takeWhile p).toArray := by - simp [Array.takeWhile, takeWhile_go_toArray] - -end List - namespace Array @@ -418,6 +30,12 @@ theorem toList_inj {a b : Array α} (h : a.toList = b.toList) : a = b := by cases a; cases b; simpa using h +@[simp] theorem toList_eq_nil_iff (l : Array α) : l.toList = [] ↔ l = #[] := by + cases l <;> simp + +@[simp] theorem mem_toList_iff (a : α) (l : Array α) : a ∈ l.toList ↔ a ∈ l := by + cases l <;> simp + /-! ### empty -/ @[simp] theorem empty_eq {xs : Array α} : #[] = xs ↔ xs = #[] := by @@ -529,24 +147,27 @@ /-! ## L[i] and L[i]? -/ --- getElem?_eq_none_iff is above. +@[simp] theorem getElem?_eq_none_iff {a : Array α} : a[i]? = none ↔ a.size ≤ i := by + by_cases h : i < a.size + · simp [getElem?_pos, h] + · rw [getElem?_neg a i h] + simp_all @[simp] theorem none_eq_getElem?_iff {a : Array α} {i : Nat} : none = a[i]? ↔ a.size ≤ i := by simp [eq_comm (a := none)] -theorem getElem?_eq_some_iff {a : Array α} : a[i]? = some b ↔ ∃ h : i < a.size, a[i] = b := by - simp [getElem?_def] - theorem getElem?_eq_none {a : Array α} (h : a.size ≤ i) : a[i]? = none := by simp [getElem?_eq_none_iff, h] --- getElem?_eq_getElem is above. +@[simp] theorem getElem?_eq_getElem {a : Array α} {i : Nat} (h : i < a.size) : a[i]? = some a[i] := + getElem?_pos .. + +theorem getElem?_eq_some_iff {a : Array α} : a[i]? = some b ↔ ∃ h : i < a.size, a[i] = b := by + simp [getElem?_def] theorem some_eq_getElem?_iff {a : Array α} : some b = a[i]? ↔ ∃ h : i < a.size, a[i] = b := by rw [eq_comm, getElem?_eq_some_iff] --- getElem?_eq_some_iff is above. - @[simp] theorem some_getElem_eq_getElem?_iff (a : Array α) (i : Nat) (h : i < a.size) : (some a[i] = a[i]?) ↔ True := by simp [h] @@ -588,15 +209,134 @@ @[simp] theorem getElem?_push_size {a : Array α} {x} : (a.push x)[a.size]? = some x := by simp [getElem?_push] +@[simp] theorem getElem_singleton (a : α) (h : i < 1) : #[a][i] = a := + match i, h with + | 0, _ => rfl + +theorem getElem?_singleton (a : α) (i : Nat) : #[a][i]? = if i = 0 then some a else none := by + simp [List.getElem?_singleton] + +/-! ### mem -/ + +@[simp] theorem not_mem_empty (a : α) : ¬ a ∈ #[] := nofun + @[simp] theorem mem_push {a : Array α} {x y : α} : x ∈ a.push y ↔ x ∈ a ∨ x = y := by - simp [mem_def] + simp only [mem_def] + simp theorem mem_push_self {a : Array α} {x : α} : x ∈ a.push x := mem_push.2 (Or.inr rfl) +theorem eq_push_append_of_mem {xs : Array α} {x : α} (h : x ∈ xs) : + ∃ (as bs : Array α), xs = as.push x ++ bs ∧ x ∉ as:= by + rcases xs with ⟨xs⟩ + obtain ⟨as, bs, h, w⟩ := List.eq_append_cons_of_mem (mem_def.1 h) + simp only at h + obtain rfl := h + exact ⟨as.toArray, bs.toArray, by simp, by simpa using w⟩ + theorem mem_push_of_mem {a : Array α} {x : α} (y : α) (h : x ∈ a) : x ∈ a.push y := mem_push.2 (Or.inl h) +theorem exists_mem_of_ne_empty (l : Array α) (h : l ≠ #[]) : ∃ x, x ∈ l := by + simpa using List.exists_mem_of_ne_nil l.toList (by simpa using h) + +theorem eq_empty_iff_forall_not_mem {l : Array α} : l = #[] ↔ ∀ a, a ∉ l := by + cases l + simp [List.eq_nil_iff_forall_not_mem] + +@[simp] theorem mem_dite_nil_left {x : α} [Decidable p] {l : ¬ p → Array α} : + (x ∈ if h : p then #[] else l h) ↔ ∃ h : ¬ p, x ∈ l h := by + split <;> simp_all + +@[simp] theorem mem_dite_nil_right {x : α} [Decidable p] {l : p → Array α} : + (x ∈ if h : p then l h else #[]) ↔ ∃ h : p, x ∈ l h := by + split <;> simp_all + +@[simp] theorem mem_ite_nil_left {x : α} [Decidable p] {l : Array α} : + (x ∈ if p then #[] else l) ↔ ¬ p ∧ x ∈ l := by + split <;> simp_all + +@[simp] theorem mem_ite_nil_right {x : α} [Decidable p] {l : Array α} : + (x ∈ if p then l else #[]) ↔ p ∧ x ∈ l := by + split <;> simp_all + +theorem eq_of_mem_singleton (h : a ∈ #[b]) : a = b := by + simpa using h + +@[simp] theorem mem_singleton {a b : α} : a ∈ #[b] ↔ a = b := + ⟨eq_of_mem_singleton, (by simp [·])⟩ + +theorem forall_mem_push {p : α → Prop} {xs : Array α} {a : α} : + (∀ x, x ∈ xs.push a → p x) ↔ p a ∧ ∀ x, x ∈ xs → p x := by + cases xs + simp [or_comm, forall_eq_or_imp] + +theorem forall_mem_ne {a : α} {l : Array α} : (∀ a' : α, a' ∈ l → ¬a = a') ↔ a ∉ l := + ⟨fun h m => h _ m rfl, fun h _ m e => h (e.symm ▸ m)⟩ + +theorem forall_mem_ne' {a : α} {l : Array α} : (∀ a' : α, a' ∈ l → ¬a' = a) ↔ a ∉ l := + ⟨fun h m => h _ m rfl, fun h _ m e => h (e.symm ▸ m)⟩ + +theorem exists_mem_empty (p : α → Prop) : ¬ (∃ x, ∃ _ : x ∈ #[], p x) := nofun + +theorem forall_mem_empty (p : α → Prop) : ∀ (x) (_ : x ∈ #[]), p x := nofun + +theorem exists_mem_push {p : α → Prop} {a : α} {xs : Array α} : + (∃ x, ∃ _ : x ∈ xs.push a, p x) ↔ p a ∨ ∃ x, ∃ _ : x ∈ xs, p x := by + simp + constructor + · rintro ⟨x, (h | rfl), h'⟩ + · exact .inr ⟨x, h, h'⟩ + · exact .inl h' + · rintro (h | ⟨x, h, h'⟩) + · exact ⟨a, by simp, h⟩ + · exact ⟨x, .inl h, h'⟩ + +theorem forall_mem_singleton {p : α → Prop} {a : α} : (∀ (x) (_ : x ∈ #[a]), p x) ↔ p a := by + simp only [mem_singleton, forall_eq] + +theorem mem_empty_iff (a : α) : a ∈ (#[] : Array α) ↔ False := by simp + +theorem mem_singleton_self (a : α) : a ∈ #[a] := by simp + +theorem mem_of_mem_push_of_mem {a b : α} {l : Array α} : a ∈ l.push b → b ∈ l → a ∈ l := by + cases l + simp only [List.push_toArray, mem_toArray, List.mem_append, List.mem_singleton] + rintro (h | rfl) + · intro _ + exact h + · exact id + +theorem eq_or_ne_mem_of_mem {a b : α} {l : Array α} (h' : a ∈ l.push b) : + a = b ∨ (a ≠ b ∧ a ∈ l) := by + if h : a = b then + exact .inl h + else + simp [h] at h' + exact .inr ⟨h, h'⟩ + +theorem ne_empty_of_mem {a : α} {l : Array α} (h : a ∈ l) : l ≠ #[] := by + cases l + simp [List.ne_nil_of_mem (by simpa using h)] + +theorem mem_of_ne_of_mem {a y : α} {l : Array α} (h₁ : a ≠ y) (h₂ : a ∈ l.push y) : a ∈ l := by + simpa [h₁] using h₂ + +theorem ne_of_not_mem_push {a b : α} {l : Array α} (h : a ∉ l.push b) : a ≠ b := by + simp only [mem_push, not_or] at h + exact h.2 + +theorem not_mem_of_not_mem_push {a b : α} {l : Array α} (h : a ∉ l.push b) : a ∉ l := by + simp only [mem_push, not_or] at h + exact h.1 + +theorem not_mem_push_of_ne_of_not_mem {a y : α} {l : Array α} : a ≠ y → a ∉ l → a ∉ l.push y := + mt ∘ mem_of_ne_of_mem + +theorem ne_and_not_mem_of_not_mem_push {a y : α} {l : Array α} : a ∉ l.push y → a ≠ y ∧ a ∉ l := by + simp +contextual + theorem getElem_of_mem {a} {l : Array α} (h : a ∈ l) : ∃ (n : Nat) (h : n < l.size), l[n]'h = a := by cases l simp [List.getElem_of_mem (by simpa using h)] @@ -728,9 +468,6 @@ (h : min stop as.size ≤ start) : anyM p as start stop = pure false := by rw [anyM_eq_anyM_loop, anyM.loop, dif_neg (Nat.not_lt.2 h)] -@[simp] theorem not_mem_empty (a : α) : ¬(a ∈ #[]) := by - simp [mem_def] - /-! # uset -/ attribute [simp] uset @@ -956,7 +693,7 @@ simp only [get!_eq_getElem?, get?_eq_getElem?] theorem back!_eq_back? [Inhabited α] (a : Array α) : a.back! = a.back?.getD default := by - simp only [back!, get!_eq_getElem?, get?_eq_getElem?, back?] + simp [back!, back?, getElem!_def, Option.getD]; rfl @[simp] theorem back?_push (a : Array α) : (a.push x).back? = some x := by simp [back?, ← getElem?_toList] @@ -1064,7 +801,9 @@ else have heq : i = as.pop.size := Nat.le_antisymm (size_pop .. ▸ Nat.le_pred_of_lt h) (Nat.le_of_not_gt hlt) - cases heq; rw [getElem_push_eq, back!, ←size_pop, get!_eq_getD, getD, dif_pos h]; rfl + cases heq + rw [getElem_push_eq, back!] + simp [← getElem!_pos] theorem eq_push_of_size_ne_zero {as : Array α} (h : as.size ≠ 0) : ∃ (bs : Array α) (c : α), as = bs.push c :=
diff --git a/src/Init/Data/List.lean b/src/Init/Data/List.lean index 7c321db..2ed68e0 100644 --- a/src/Init/Data/List.lean +++ b/src/Init/Data/List.lean
@@ -24,6 +24,7 @@ import Init.Data.List.Perm import Init.Data.List.Sort import Init.Data.List.ToArray +import Init.Data.List.ToArrayImpl import Init.Data.List.MapIdx import Init.Data.List.OfFn import Init.Data.List.FinRange
diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean index e48820b..6e17e22 100644 --- a/src/Init/Data/List/Lemmas.lean +++ b/src/Init/Data/List/Lemmas.lean
@@ -253,12 +253,6 @@ l[i] = l[i]?.get (by simp [getElem?_eq_getElem, h]) := by simp [getElem_eq_iff] -theorem isSome_getElem? {l : List α} {n : Nat} : l[n]?.isSome ↔ n < l.length := by - simp - -theorem isNone_getElem? {l : List α} {n : Nat} : l[n]?.isNone ↔ l.length ≤ n := by - simp - @[simp] theorem getElem?_nil {n : Nat} : ([] : List α)[n]? = none := rfl theorem getElem?_cons_zero {l : List α} : (a::l)[0]? = some a := by simp @@ -270,6 +264,11 @@ theorem getElem?_cons : (a :: l)[i]? = if i = 0 then some a else l[i-1]? := by cases i <;> simp +theorem getElem_cons {l : List α} (w : i < (a :: l).length) : + (a :: l)[i] = + if h : i = 0 then a else l[i-1]'(match i, h with | i+1, _ => succ_lt_succ_iff.mp w) := by + cases i <;> simp + @[simp] theorem getElem_singleton (a : α) (h : i < 1) : [a][i] = a := match i, h with | 0, _ => rfl @@ -3532,7 +3531,12 @@ getElem?_def _ _ @[deprecated getElem?_eq_none (since := "2024-11-29")] abbrev getElem?_len_le := @getElem?_eq_none +@[deprecated _root_.isSome_getElem? (since := "2024-12-09")] +theorem isSome_getElem? {l : List α} {n : Nat} : l[n]?.isSome ↔ n < l.length := by + simp - +@[deprecated _root_.isNone_getElem? (since := "2024-12-09")] +theorem isNone_getElem? {l : List α} {n : Nat} : l[n]?.isNone ↔ l.length ≤ n := by + simp end List
diff --git a/src/Init/Data/List/ToArray.lean b/src/Init/Data/List/ToArray.lean index 214364b..ffa2869 100644 --- a/src/Init/Data/List/ToArray.lean +++ b/src/Init/Data/List/ToArray.lean
@@ -1,23 +1,366 @@ /- -Copyright (c) 2024 Lean FRO. All rights reserved. +Copyright (c) 2022 Mario Carneiro. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Henrik Böving +Authors: Mario Carneiro -/ prelude -import Init.Data.List.Basic +import Init.Data.List.Impl +import Init.Data.List.Nat.Erase +import Init.Data.List.Monadic -/-- -Auxiliary definition for `List.toArray`. -`List.toArrayAux as r = r ++ as.toArray` +/-! ### Lemmas about `List.toArray`. + +We prefer to pull `List.toArray` outwards past `Array` operations. -/ -@[inline_if_reduce] -def List.toArrayAux : List α → Array α → Array α - | nil, r => r - | cons a as, r => toArrayAux as (r.push a) +namespace List -/-- Convert a `List α` into an `Array α`. This is O(n) in the length of the list. -/ --- This function is exported to C, where it is called by `Array.mk` --- (the constructor) to implement this functionality. -@[inline, match_pattern, pp_nodot, export lean_list_to_array] -def List.toArrayImpl (as : List α) : Array α := - as.toArrayAux (Array.mkEmpty as.length) +open Array + +theorem toArray_inj {a b : List α} (h : a.toArray = b.toArray) : a = b := by + cases a with + | nil => simpa using h + | cons a as => + cases b with + | nil => simp at h + | cons b bs => simpa using h + +@[simp] theorem size_toArrayAux {a : List α} {b : Array α} : + (a.toArrayAux b).size = b.size + a.length := by + simp [size] + +@[simp] theorem push_toArray (l : List α) (a : α) : l.toArray.push a = (l ++ [a]).toArray := by + apply ext' + simp + +/-- Unapplied variant of `push_toArray`, useful for monadic reasoning. -/ +@[simp] theorem push_toArray_fun (l : List α) : l.toArray.push = fun a => (l ++ [a]).toArray := by + funext a + simp + +@[simp] theorem isEmpty_toArray (l : List α) : l.toArray.isEmpty = l.isEmpty := by + cases l <;> simp + +@[simp] theorem toArray_singleton (a : α) : (List.singleton a).toArray = singleton a := rfl + +@[simp] theorem back!_toArray [Inhabited α] (l : List α) : l.toArray.back! = l.getLast! := by + simp only [back!, size_toArray, Array.get!_eq_getElem!, getElem!_toArray, getLast!_eq_getElem!] + +@[simp] theorem back?_toArray (l : List α) : l.toArray.back? = l.getLast? := by + simp [back?, List.getLast?_eq_getElem?] + +@[simp] theorem set_toArray (l : List α) (i : Nat) (a : α) (h : i < l.length) : + (l.toArray.set i a) = (l.set i a).toArray := rfl + +@[simp] theorem forIn'_loop_toArray [Monad m] (l : List α) (f : (a : α) → a ∈ l.toArray → β → m (ForInStep β)) (i : Nat) + (h : i ≤ l.length) (b : β) : + Array.forIn'.loop l.toArray f i h b = + forIn' (l.drop (l.length - i)) b (fun a m b => f a (by simpa using mem_of_mem_drop m) b) := by + induction i generalizing l b with + | zero => + simp [Array.forIn'.loop] + | succ i ih => + simp only [Array.forIn'.loop, size_toArray, getElem_toArray, ih] + have t : drop (l.length - (i + 1)) l = l[l.length - i - 1] :: drop (l.length - i) l := by + simp only [Nat.sub_add_eq] + rw [List.drop_sub_one (by omega), List.getElem?_eq_getElem (by omega)] + simp only [Option.toList_some, singleton_append] + simp [t] + have t : l.length - 1 - i = l.length - i - 1 := by omega + simp only [t] + congr + +@[simp] theorem forIn'_toArray [Monad m] (l : List α) (b : β) (f : (a : α) → a ∈ l.toArray → β → m (ForInStep β)) : + forIn' l.toArray b f = forIn' l b (fun a m b => f a (mem_toArray.mpr m) b) := by + change Array.forIn' _ _ _ = List.forIn' _ _ _ + rw [Array.forIn', forIn'_loop_toArray] + simp + +@[simp] theorem forIn_toArray [Monad m] (l : List α) (b : β) (f : α → β → m (ForInStep β)) : + forIn l.toArray b f = forIn l b f := by + simpa using forIn'_toArray l b fun a m b => f a b + +theorem foldrM_toArray [Monad m] (f : α → β → m β) (init : β) (l : List α) : + l.toArray.foldrM f init = l.foldrM f init := by + rw [foldrM_eq_reverse_foldlM_toList] + simp + +theorem foldlM_toArray [Monad m] (f : β → α → m β) (init : β) (l : List α) : + l.toArray.foldlM f init = l.foldlM f init := by + rw [foldlM_toList] + +theorem foldr_toArray (f : α → β → β) (init : β) (l : List α) : + l.toArray.foldr f init = l.foldr f init := by + rw [foldr_toList] + +theorem foldl_toArray (f : β → α → β) (init : β) (l : List α) : + l.toArray.foldl f init = l.foldl f init := by + rw [foldl_toList] + +/-- Variant of `foldrM_toArray` with a side condition for the `start` argument. -/ +@[simp] theorem foldrM_toArray' [Monad m] (f : α → β → m β) (init : β) (l : List α) + (h : start = l.toArray.size) : + l.toArray.foldrM f init start 0 = l.foldrM f init := by + subst h + rw [foldrM_eq_reverse_foldlM_toList] + simp + +/-- Variant of `foldlM_toArray` with a side condition for the `stop` argument. -/ +@[simp] theorem foldlM_toArray' [Monad m] (f : β → α → m β) (init : β) (l : List α) + (h : stop = l.toArray.size) : + l.toArray.foldlM f init 0 stop = l.foldlM f init := by + subst h + rw [foldlM_toList] + +/-- Variant of `foldr_toArray` with a side condition for the `start` argument. -/ +@[simp] theorem foldr_toArray' (f : α → β → β) (init : β) (l : List α) + (h : start = l.toArray.size) : + l.toArray.foldr f init start 0 = l.foldr f init := by + subst h + rw [foldr_toList] + +/-- Variant of `foldl_toArray` with a side condition for the `stop` argument. -/ +@[simp] theorem foldl_toArray' (f : β → α → β) (init : β) (l : List α) + (h : stop = l.toArray.size) : + l.toArray.foldl f init 0 stop = l.foldl f init := by + subst h + rw [foldl_toList] + +@[simp] theorem append_toArray (l₁ l₂ : List α) : + l₁.toArray ++ l₂.toArray = (l₁ ++ l₂).toArray := by + apply ext' + simp + +@[simp] theorem push_append_toArray {as : Array α} {a : α} {bs : List α} : as.push a ++ bs.toArray = as ++ (a ::bs).toArray := by + cases as + simp + +@[simp] theorem foldl_push {l : List α} {as : Array α} : l.foldl Array.push as = as ++ l.toArray := by + induction l generalizing as <;> simp [*] + +@[simp] theorem foldr_push {l : List α} {as : Array α} : l.foldr (fun a b => push b a) as = as ++ l.reverse.toArray := by + rw [foldr_eq_foldl_reverse, foldl_push] + +@[simp] theorem findSomeM?_toArray [Monad m] [LawfulMonad m] (f : α → m (Option β)) (l : List α) : + l.toArray.findSomeM? f = l.findSomeM? f := by + rw [Array.findSomeM?] + simp only [bind_pure_comp, map_pure, forIn_toArray] + induction l with + | nil => simp + | cons a l ih => + simp only [forIn_cons, LawfulMonad.bind_assoc, findSomeM?] + congr + ext1 (_|_) <;> simp [ih] + +theorem findSomeRevM?_find_toArray [Monad m] [LawfulMonad m] (f : α → m (Option β)) (l : List α) + (i : Nat) (h) : + findSomeRevM?.find f l.toArray i h = (l.take i).reverse.findSomeM? f := by + induction i generalizing l with + | zero => simp [Array.findSomeRevM?.find.eq_def] + | succ i ih => + rw [size_toArray] at h + rw [Array.findSomeRevM?.find, take_succ, getElem?_eq_getElem (by omega)] + simp only [ih, reverse_append] + congr + ext1 (_|_) <;> simp + +-- This is not marked as `@[simp]` as later we simplify all occurrences of `findSomeRevM?`. +theorem findSomeRevM?_toArray [Monad m] [LawfulMonad m] (f : α → m (Option β)) (l : List α) : + l.toArray.findSomeRevM? f = l.reverse.findSomeM? f := by + simp [Array.findSomeRevM?, findSomeRevM?_find_toArray] + +-- This is not marked as `@[simp]` as later we simplify all occurrences of `findRevM?`. +theorem findRevM?_toArray [Monad m] [LawfulMonad m] (f : α → m Bool) (l : List α) : + l.toArray.findRevM? f = l.reverse.findM? f := by + rw [Array.findRevM?, findSomeRevM?_toArray, findM?_eq_findSomeM?] + +@[simp] theorem findM?_toArray [Monad m] [LawfulMonad m] (f : α → m Bool) (l : List α) : + l.toArray.findM? f = l.findM? f := by + rw [Array.findM?] + simp only [bind_pure_comp, map_pure, forIn_toArray] + induction l with + | nil => simp + | cons a l ih => + simp only [forIn_cons, LawfulMonad.bind_assoc, findM?] + congr + ext1 (_|_) <;> simp [ih] + +@[simp] theorem findSome?_toArray (f : α → Option β) (l : List α) : + l.toArray.findSome? f = l.findSome? f := by + rw [Array.findSome?, ← findSomeM?_id, findSomeM?_toArray, Id.run] + +@[simp] theorem find?_toArray (f : α → Bool) (l : List α) : + l.toArray.find? f = l.find? f := by + rw [Array.find?] + simp only [Id.run, Id, Id.pure_eq, Id.bind_eq, forIn_toArray] + induction l with + | nil => simp + | cons a l ih => + simp only [forIn_cons, Id.pure_eq, Id.bind_eq, find?] + by_cases f a <;> simp_all + +theorem isPrefixOfAux_toArray_succ [BEq α] (l₁ l₂ : List α) (hle : l₁.length ≤ l₂.length) (i : Nat) : + Array.isPrefixOfAux l₁.toArray l₂.toArray hle (i + 1) = + Array.isPrefixOfAux l₁.tail.toArray l₂.tail.toArray (by simp; omega) i := by + rw [Array.isPrefixOfAux] + conv => rhs; rw [Array.isPrefixOfAux] + simp only [size_toArray, getElem_toArray, Bool.if_false_right, length_tail, getElem_tail] + split <;> rename_i h₁ <;> split <;> rename_i h₂ + · rw [isPrefixOfAux_toArray_succ] + · omega + · omega + · rfl + +theorem isPrefixOfAux_toArray_succ' [BEq α] (l₁ l₂ : List α) (hle : l₁.length ≤ l₂.length) (i : Nat) : + Array.isPrefixOfAux l₁.toArray l₂.toArray hle (i + 1) = + Array.isPrefixOfAux (l₁.drop (i+1)).toArray (l₂.drop (i+1)).toArray (by simp; omega) 0 := by + induction i generalizing l₁ l₂ with + | zero => simp [isPrefixOfAux_toArray_succ] + | succ i ih => + rw [isPrefixOfAux_toArray_succ, ih] + simp + +theorem isPrefixOfAux_toArray_zero [BEq α] (l₁ l₂ : List α) (hle : l₁.length ≤ l₂.length) : + Array.isPrefixOfAux l₁.toArray l₂.toArray hle 0 = + l₁.isPrefixOf l₂ := by + rw [Array.isPrefixOfAux] + match l₁, l₂ with + | [], _ => rw [dif_neg] <;> simp + | _::_, [] => simp at hle + | a::l₁, b::l₂ => + simp [isPrefixOf_cons₂, isPrefixOfAux_toArray_succ', isPrefixOfAux_toArray_zero] + +@[simp] theorem isPrefixOf_toArray [BEq α] (l₁ l₂ : List α) : + l₁.toArray.isPrefixOf l₂.toArray = l₁.isPrefixOf l₂ := by + rw [Array.isPrefixOf] + split <;> rename_i h + · simp [isPrefixOfAux_toArray_zero] + · simp only [Bool.false_eq] + induction l₁ generalizing l₂ with + | nil => simp at h + | cons a l₁ ih => + cases l₂ with + | nil => simp + | cons b l₂ => + simp only [isPrefixOf_cons₂, Bool.and_eq_false_imp] + intro w + rw [ih] + simp_all + +theorem zipWithAux_toArray_succ (as : List α) (bs : List β) (f : α → β → γ) (i : Nat) (cs : Array γ) : + zipWithAux as.toArray bs.toArray f (i + 1) cs = zipWithAux as.tail.toArray bs.tail.toArray f i cs := by + rw [zipWithAux] + conv => rhs; rw [zipWithAux] + simp only [size_toArray, getElem_toArray, length_tail, getElem_tail] + split <;> rename_i h₁ + · split <;> rename_i h₂ + · rw [dif_pos (by omega), dif_pos (by omega), zipWithAux_toArray_succ] + · rw [dif_pos (by omega)] + rw [dif_neg (by omega)] + · rw [dif_neg (by omega)] + +theorem zipWithAux_toArray_succ' (as : List α) (bs : List β) (f : α → β → γ) (i : Nat) (cs : Array γ) : + zipWithAux as.toArray bs.toArray f (i + 1) cs = zipWithAux (as.drop (i+1)).toArray (bs.drop (i+1)).toArray f 0 cs := by + induction i generalizing as bs cs with + | zero => simp [zipWithAux_toArray_succ] + | succ i ih => + rw [zipWithAux_toArray_succ, ih] + simp + +theorem zipWithAux_toArray_zero (f : α → β → γ) (as : List α) (bs : List β) (cs : Array γ) : + zipWithAux as.toArray bs.toArray f 0 cs = cs ++ (List.zipWith f as bs).toArray := by + rw [Array.zipWithAux] + match as, bs with + | [], _ => simp + | _, [] => simp + | a :: as, b :: bs => + simp [zipWith_cons_cons, zipWithAux_toArray_succ', zipWithAux_toArray_zero, push_append_toArray] + +@[simp] theorem zipWith_toArray (as : List α) (bs : List β) (f : α → β → γ) : + Array.zipWith as.toArray bs.toArray f = (List.zipWith f as bs).toArray := by + rw [Array.zipWith] + simp [zipWithAux_toArray_zero] + +@[simp] theorem zip_toArray (as : List α) (bs : List β) : + Array.zip as.toArray bs.toArray = (List.zip as bs).toArray := by + simp [Array.zip, zipWith_toArray, zip] + +theorem zipWithAll_go_toArray (as : List α) (bs : List β) (f : Option α → Option β → γ) (i : Nat) (cs : Array γ) : + zipWithAll.go f as.toArray bs.toArray i cs = cs ++ (List.zipWithAll f (as.drop i) (bs.drop i)).toArray := by + unfold zipWithAll.go + split <;> rename_i h + · rw [zipWithAll_go_toArray] + simp at h + simp only [getElem?_toArray, push_append_toArray] + if ha : i < as.length then + if hb : i < bs.length then + rw [List.drop_eq_getElem_cons ha, List.drop_eq_getElem_cons hb] + simp only [ha, hb, getElem?_eq_getElem, zipWithAll_cons_cons] + else + simp only [Nat.not_lt] at hb + rw [List.drop_eq_getElem_cons ha] + rw [(drop_eq_nil_iff (l := bs)).mpr (by omega), (drop_eq_nil_iff (l := bs)).mpr (by omega)] + simp only [zipWithAll_nil, map_drop, map_cons] + rw [getElem?_eq_getElem ha] + rw [getElem?_eq_none hb] + else + if hb : i < bs.length then + simp only [Nat.not_lt] at ha + rw [List.drop_eq_getElem_cons hb] + rw [(drop_eq_nil_iff (l := as)).mpr (by omega), (drop_eq_nil_iff (l := as)).mpr (by omega)] + simp only [nil_zipWithAll, map_drop, map_cons] + rw [getElem?_eq_getElem hb] + rw [getElem?_eq_none ha] + else + omega + · simp only [size_toArray, Nat.not_lt] at h + rw [drop_eq_nil_of_le (by omega), drop_eq_nil_of_le (by omega)] + simp + termination_by max as.length bs.length - i + decreasing_by simp_wf; decreasing_trivial_pre_omega + +@[simp] theorem zipWithAll_toArray (f : Option α → Option β → γ) (as : List α) (bs : List β) : + Array.zipWithAll as.toArray bs.toArray f = (List.zipWithAll f as bs).toArray := by + simp [Array.zipWithAll, zipWithAll_go_toArray] + +@[simp] theorem toArray_appendList (l₁ l₂ : List α) : + l₁.toArray ++ l₂ = (l₁ ++ l₂).toArray := by + apply ext' + simp + +@[simp] theorem pop_toArray (l : List α) : l.toArray.pop = l.dropLast.toArray := by + apply ext' + simp + +theorem takeWhile_go_succ (p : α → Bool) (a : α) (l : List α) (i : Nat) : + takeWhile.go p (a :: l).toArray (i+1) r = takeWhile.go p l.toArray i r := by + rw [takeWhile.go, takeWhile.go] + simp only [size_toArray, length_cons, Nat.add_lt_add_iff_right, Array.get_eq_getElem, + getElem_toArray, getElem_cons_succ] + split + rw [takeWhile_go_succ] + rfl + +theorem takeWhile_go_toArray (p : α → Bool) (l : List α) (i : Nat) : + Array.takeWhile.go p l.toArray i r = r ++ (takeWhile p (l.drop i)).toArray := by + induction l generalizing i r with + | nil => simp [takeWhile.go] + | cons a l ih => + rw [takeWhile.go] + cases i with + | zero => + simp [takeWhile_go_succ, ih, takeWhile_cons] + split <;> simp + | succ i => + simp only [size_toArray, length_cons, Nat.add_lt_add_iff_right, Array.get_eq_getElem, + getElem_toArray, getElem_cons_succ, drop_succ_cons] + split <;> rename_i h₁ + · rw [takeWhile_go_succ, ih] + rw [← getElem_cons_drop_succ_eq_drop h₁, takeWhile_cons] + split <;> simp_all + · simp_all [drop_eq_nil_of_le] + +@[simp] theorem takeWhile_toArray (p : α → Bool) (l : List α) : + l.toArray.takeWhile p = (l.takeWhile p).toArray := by + simp [Array.takeWhile, takeWhile_go_toArray] + +end List
diff --git a/src/Init/Data/List/ToArrayImpl.lean b/src/Init/Data/List/ToArrayImpl.lean new file mode 100644 index 0000000..214364b --- /dev/null +++ b/src/Init/Data/List/ToArrayImpl.lean
@@ -0,0 +1,23 @@ +/- +Copyright (c) 2024 Lean FRO. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Henrik Böving +-/ +prelude +import Init.Data.List.Basic + +/-- +Auxiliary definition for `List.toArray`. +`List.toArrayAux as r = r ++ as.toArray` +-/ +@[inline_if_reduce] +def List.toArrayAux : List α → Array α → Array α + | nil, r => r + | cons a as, r => toArrayAux as (r.push a) + +/-- Convert a `List α` into an `Array α`. This is O(n) in the length of the list. -/ +-- This function is exported to C, where it is called by `Array.mk` +-- (the constructor) to implement this functionality. +@[inline, match_pattern, pp_nodot, export lean_list_to_array] +def List.toArrayImpl (as : List α) : Array α := + as.toArrayAux (Array.mkEmpty as.length)
diff --git a/src/Init/GetElem.lean b/src/Init/GetElem.lean index 31bc54b..03ba857 100644 --- a/src/Init/GetElem.lean +++ b/src/Init/GetElem.lean
@@ -243,6 +243,12 @@ instance : GetElem (Array α) Nat α fun xs i => i < xs.size where getElem xs i h := xs.get i h +@[simp] theorem get_eq_getElem (a : Array α) (i : Nat) (h) : a.get i h = a[i] := rfl + +@[simp] theorem get!_eq_getElem! [Inhabited α] (a : Array α) (i : Nat) : a.get! i = a[i]! := by + simp only [get!, getD, get_eq_getElem, getElem!_def] + split <;> simp_all [getElem?_pos, getElem?_neg] + end Array namespace Lean.Syntax