@@ -61,7 +61,7 @@ theorem toArray_eq : List.toArray as = xs ↔ as = xs.toList := by
@[ simp ] theorem empty_eq { xs : Array α } : # [ ] = xs ↔ xs = # [ ] : = by
cases xs < ; > simp
@[ grind ] theorem size_empty : ( # [ ] : Array α ) . size = 0 : = rfl
@[ grind = ] theorem size_empty : ( # [ ] : Array α ) . size = 0 : = rfl
/- ! ### size -/
@@ -196,7 +196,7 @@ theorem getElem?_push_size {xs : Array α
theorem getElem_singleton { a : α } { i : Nat } ( h : i < 1 ) : # [ a ] [ i ] = a : = by
simp
@[ grind ]
@[ grind = ]
theorem getElem?_singleton { a : α } { i : Nat } : # [ a ] [ i ] ? = if i = 0 then some a else none : = by
simp [ List . getElem?_singleton ]
@@ -211,12 +211,12 @@ theorem ext_getElem? {xs ys : Array α
@[ simp ] theorem pop_push { xs : Array α } { x : α } : ( xs . push x ) . pop = xs : = by simp [ pop ]
@[ simp , grind ] theorem getElem_pop { xs : Array α } { i : Nat } ( h : i < xs . pop . size ) :
@[ simp , grind = ] theorem getElem_pop { xs : Array α } { i : Nat } ( h : i < xs . pop . size ) :
xs . pop [ i ] = xs [ i ] ' ( by simp at h ; omega ) : = by
rcases xs with ⟨ xs ⟩
simp [ List . getElem_dropLast ]
@[ grind ] theorem getElem?_pop { xs : Array α } { i : Nat } :
@[ grind = ] theorem getElem?_pop { xs : Array α } { i : Nat } :
xs . pop [ i ] ? = if i < xs . size - 1 then xs [ i ] ? else none : = by
rcases xs with ⟨ xs ⟩
simp [ List . getElem?_dropLast ]
@@ -331,7 +331,7 @@ theorem singleton_inj : #[a] = #[b] ↔ a = b := by
/- ! ### replicate -/
@[ simp , grind ] theorem size_replicate { n : Nat } { v : α } : ( replicate n v ) . size = n : =
@[ simp , grind = ] theorem size_replicate { n : Nat } { v : α } : ( replicate n v ) . size = n : =
List . length_replicate . .
@[ deprecated size_replicate ( since : = " 2025-03-18 " ) ]
@@ -343,12 +343,12 @@ abbrev size_mkArray := @size_replicate
@[ deprecated toList_replicate ( since : = " 2025-03-18 " ) ]
abbrev toList_mkArray : = @ toList_replicate
@[ simp , grind ] theorem replicate_zero : replicate 0 a = # [ ] : = rfl
@[ simp , grind = ] theorem replicate_zero : replicate 0 a = # [ ] : = rfl
@[ deprecated replicate_zero ( since : = " 2025-03-18 " ) ]
abbrev mkArray_zero : = @ replicate_zero
@[ grind ]
@[ grind = ]
theorem replicate_succ : replicate ( n + 1 ) a = ( replicate n a ) . push a : = by
apply toList_inj . 1
simp [ List . replicate_succ' ]
@@ -356,13 +356,13 @@ theorem replicate_succ : replicate (n + 1) a = (replicate n a).push a := by
@[ deprecated replicate_succ ( since : = " 2025-03-18 " ) ]
abbrev mkArray_succ : = @ replicate_succ
@[ simp , grind ] theorem getElem_replicate { n : Nat } { v : α } { i : Nat } ( h : i < ( replicate n v ) . size ) :
@[ simp , grind = ] theorem getElem_replicate { n : Nat } { v : α } { i : Nat } ( h : i < ( replicate n v ) . size ) :
( replicate n v ) [ i ] = v : = by simp [ ← getElem_toList ]
@[ deprecated getElem_replicate ( since : = " 2025-03-18 " ) ]
abbrev getElem_mkArray : = @ getElem_replicate
@[ grind ] theorem getElem?_replicate { n : Nat } { v : α } { i : Nat } :
@[ grind = ] theorem getElem?_replicate { n : Nat } { v : α } { i : Nat } :
( replicate n v ) [ i ] ? = if i < n then some v else none : = by
simp [ getElem?_def ]
@@ -520,8 +520,8 @@ theorem forall_getElem {xs : Array α α
/- ! ### isEmpty -/
@[ grind ] theorem isEmpty_empty : ( # [ ] : Array α ) . isEmpty = true : = rfl
@[ simp , grind ] theorem isEmpty_push { xs : Array α } : ( xs . push x ) . isEmpty = false : = by
@[ grind = ] theorem isEmpty_empty : ( # [ ] : Array α ) . isEmpty = true : = rfl
@[ simp , grind = ] theorem isEmpty_push { xs : Array α } : ( xs . push x ) . isEmpty = false : = by
rcases xs with ⟨ xs ⟩
simp
@@ -728,18 +728,18 @@ theorem all_eq_true_iff_forall_mem {xs : Array α
subst h
rw [ all_toList ]
@[ grind ] theorem _ root_ . List . anyM_toArray [ Monad m ] [ LawfulMonad m ] { p : α → m Bool } { l : List α } :
@[ grind = ] theorem _ root_ . List . anyM_toArray [ Monad m ] [ LawfulMonad m ] { p : α → m Bool } { l : List α } :
l . toArray . anyM p = l . anyM p : = by
rw [ ← anyM_toList ]
@[ grind ] theorem _ root_ . List . any_toArray { p : α → Bool } { l : List α } : l . toArray . any p = l . any p : = by
@[ grind = ] theorem _ root_ . List . any_toArray { p : α → Bool } { l : List α } : l . toArray . any p = l . any p : = by
rw [ any_toList ]
@[ grind ] theorem _ root_ . List . allM_toArray [ Monad m ] [ LawfulMonad m ] { p : α → m Bool } { l : List α } :
@[ grind = ] theorem _ root_ . List . allM_toArray [ Monad m ] [ LawfulMonad m ] { p : α → m Bool } { l : List α } :
l . toArray . allM p = l . allM p : = by
rw [ ← allM_toList ]
@[ grind ] theorem _ root_ . List . all_toArray { p : α → Bool } { l : List α } : l . toArray . all p = l . all p : = by
@[ grind = ] theorem _ root_ . List . all_toArray { p : α → Bool } { l : List α } : l . toArray . all p = l . all p : = by
rw [ all_toList ]
/-- Variant of `any_eq_true` in terms of membership rather than an array index. -/
@@ -851,7 +851,7 @@ abbrev elem_eq_true_of_mem := @contains_eq_true_of_mem
elem a xs = xs . contains a : = by
simp [ elem ]
@[ grind ] theorem contains_empty [ BEq α ] : ( # [ ] : Array α ) . contains a = false : = by simp
@[ grind = ] theorem contains_empty [ BEq α ] : ( # [ ] : Array α ) . contains a = false : = by simp
theorem elem_iff [ BEq α ] [ LawfulBEq α ] { a : α } { xs : Array α } :
elem a xs = true ↔ a ∈ xs : = ⟨ mem_of_contains_eq_true , contains_eq_true_of_mem ⟩
@@ -865,14 +865,14 @@ instance [BEq α α α α
theorem elem_eq_mem [ BEq α ] [ LawfulBEq α ] { a : α } { xs : Array α } :
elem a xs = decide ( a ∈ xs ) : = by rw [ Bool . eq_iff_iff , elem_iff , decide_eq_true_iff ]
@[ simp , grind ] theorem contains_eq_mem [ BEq α ] [ LawfulBEq α ] { a : α } { xs : Array α } :
@[ simp , grind = ] theorem contains_eq_mem [ BEq α ] [ LawfulBEq α ] { a : α } { xs : Array α } :
xs . contains a = decide ( a ∈ xs ) : = by rw [ ← elem_eq_contains , elem_eq_mem ]
@[ grind ] theorem any_empty [ BEq α ] { p : α → Bool } : ( # [ ] : Array α ) . any p = false : = by simp
@[ grind ] theorem all_empty [ BEq α ] { p : α → Bool } : ( # [ ] : Array α ) . all p = true : = by simp
@[ grind = ] theorem any_empty [ BEq α ] { p : α → Bool } : ( # [ ] : Array α ) . any p = false : = by simp
@[ grind = ] theorem all_empty [ BEq α ] { p : α → Bool } : ( # [ ] : Array α ) . all p = true : = by simp
/-- Variant of `any_push` with a side condition on `stop`. -/
@[ simp , grind ] theorem any_push' { xs : Array α } { a : α } { p : α → Bool } ( h : stop = xs . size + 1 ) :
@[ simp , grind = ] theorem any_push' { xs : Array α } { a : α } { p : α → Bool } ( h : stop = xs . size + 1 ) :
( xs . push a ) . any p 0 stop = ( xs . any p | | p a ) : = by
cases xs
rw [ List . push_toArray ]
@@ -883,7 +883,7 @@ theorem any_push {xs : Array α α α
any_push' ( by simp )
/-- Variant of `all_push` with a side condition on `stop`. -/
@[ simp , grind ] theorem all_push' { xs : Array α } { a : α } { p : α → Bool } ( h : stop = xs . size + 1 ) :
@[ simp , grind = ] theorem all_push' { xs : Array α } { a : α } { p : α → Bool } ( h : stop = xs . size + 1 ) :
( xs . push a ) . all p 0 stop = ( xs . all p & & p a ) : = by
cases xs
rw [ List . push_toArray ]
@@ -922,13 +922,13 @@ abbrev getElem?_set_eq := @getElem?_set_self
( ne : i ≠ j ) : ( xs . set i v ) [ j ] ? = xs [ j ] ? : = by
by_cases h : j < xs . size < ; > simp [ ne , h ]
@[ grind ] theorem getElem_set { xs : Array α } { i : Nat } ( h' : i < xs . size ) { v : α } { j : Nat }
@[ grind = ] theorem getElem_set { xs : Array α } { i : Nat } ( h' : i < xs . size ) { v : α } { j : Nat }
( h : j < ( xs . set i v ) . size ) :
( xs . set i v ) [ j ] = if i = j then v else xs [ j ] ' ( by simpa using h ) : = by
simp at h
by_cases p : i = j < ; > simp [ p , h ]
@[ grind ] theorem getElem?_set { xs : Array α } { i : Nat } ( h : i < xs . size ) { v : α } { j : Nat } :
@[ grind = ] theorem getElem?_set { xs : Array α } { i : Nat } ( h : i < xs . size ) { v : α } { j : Nat } :
( xs . set i v ) [ j ] ? = if i = j then some v else xs [ j ] ? : = by
split < ; > simp_all
@@ -994,26 +994,26 @@ grind_pattern mem_or_eq_of_mem_set => a ∈ xs.set i b
/- ! ### setIfInBounds -/
@[ simp , grind ] theorem setIfInBounds_empty { i : Nat } { a : α } :
@[ simp , grind = ] theorem setIfInBounds_empty { i : Nat } { a : α } :
# [ ] . setIfInBounds i a = # [ ] : = rfl
@[ simp , grind = ] theorem set!_eq_setIfInBounds : set! xs i v = setIfInBounds xs i v : = rfl
@[ grind ]
@[ grind = ]
theorem setIfInBounds_def ( xs : Array α ) ( i : Nat ) ( a : α ) :
xs . setIfInBounds i a = if h : i < xs . size then xs . set i a else xs : = rfl
@[ deprecated set!_eq_setIfInBounds ( since : = " 2024-12-12 " ) ]
abbrev set!_is_setIfInBounds : = @ set!_eq_setIfInBounds
@[ simp , grind ] theorem size_setIfInBounds { xs : Array α } { i : Nat } { a : α } :
@[ simp , grind = ] theorem size_setIfInBounds { xs : Array α } { i : Nat } { a : α } :
( xs . setIfInBounds i a ) . size = xs . size : = by
if h : i < xs . size then
simp [ setIfInBounds , h ]
else
simp [ setIfInBounds , h ]
@[ grind ] theorem getElem_setIfInBounds { xs : Array α } { i : Nat } { a : α } { j : Nat }
@[ grind = ] theorem getElem_setIfInBounds { xs : Array α } { i : Nat } { a : α } { j : Nat }
( hj : j < xs . size ) :
( xs . setIfInBounds i a ) [ j ] ' ( by simp [ hj ] ) = if i = j then a else xs [ j ] : = by
simp only [ setIfInBounds ]
@@ -1035,7 +1035,7 @@ abbrev getElem_setIfInBounds_eq := @getElem_setIfInBounds_self
( xs . setIfInBounds i a ) [ j ] ' ( by simpa using hj ) = xs [ j ] : = by
simp [ getElem_setIfInBounds , hj , h ]
@[ grind ] theorem getElem?_setIfInBounds { xs : Array α } { i j : Nat } { a : α } :
@[ grind = ] theorem getElem?_setIfInBounds { xs : Array α } { i j : Nat } { a : α } :
( xs . setIfInBounds i a ) [ j ] ? = if i = j then if i < xs . size then some a else none else xs [ j ] ? : = by
cases xs
simp [ List . getElem?_set ]
@@ -1102,11 +1102,11 @@ theorem mem_or_eq_of_mem_setIfInBounds
/- ! ### BEq -/
@[ simp , grind ] theorem beq_empty_eq [ BEq α ] { xs : Array α } : ( xs = = # [ ] ) = xs . isEmpty : = by
@[ simp , grind = ] theorem beq_empty_eq [ BEq α ] { xs : Array α } : ( xs = = # [ ] ) = xs . isEmpty : = by
cases xs
simp
@[ simp , grind ] theorem empty_beq_eq [ BEq α ] { xs : Array α } : ( # [ ] = = xs ) = xs . isEmpty : = by
@[ simp , grind = ] theorem empty_beq_eq [ BEq α ] { xs : Array α } : ( # [ ] = = xs ) = xs . isEmpty : = by
cases xs
simp
@@ -1116,7 +1116,7 @@ abbrev beq_empty_iff := @beq_empty_eq
@[ deprecated empty_beq_eq ( since : = " 2025-04-04 " ) ]
abbrev empty_beq_iff : = @ empty_beq_eq
@[ simp , grind ] theorem push_beq_push [ BEq α ] { a b : α } { xs ys : Array α } :
@[ simp , grind = ] theorem push_beq_push [ BEq α ] { a b : α } { xs ys : Array α } :
( xs . push a = = ys . push b ) = ( xs = = ys & & a = = b ) : = by
cases xs
cases ys
@@ -1176,16 +1176,16 @@ private theorem beq_of_beq_singleton [BEq α α
/- ! ### back -/
@[ grind ] theorem back_singleton { a : α } : # [ a ] . back = a : = by simp
@[ grind = ] theorem back_singleton { a : α } : # [ a ] . back = a : = by simp
@[ grind ]
@[ grind = ]
theorem back_eq_getElem { xs : Array α } ( h : 0 < xs . size ) : xs . back = xs [ xs . size - 1 ] : = by
cases xs
simp [ List . getLast_eq_getElem ]
@[ grind ] theorem back?_empty : ( # [ ] : Array α ) . back? = none : = by simp
@[ grind = ] theorem back?_empty : ( # [ ] : Array α ) . back? = none : = by simp
@[ grind ] theorem back?_eq_getElem? { xs : Array α } : xs . back? = xs [ xs . size - 1 ] ? : = by
@[ grind = ] theorem back?_eq_getElem? { xs : Array α } : xs . back? = xs [ xs . size - 1 ] ? : = by
cases xs
simp [ List . getLast?_eq_getElem? ]
@@ -1222,17 +1222,17 @@ where
apply ext'
simp
@[ simp , grind ] theorem size_map { f : α → β } { xs : Array α } : ( xs . map f ) . size = xs . size : = by
@[ simp , grind = ] theorem size_map { f : α → β } { xs : Array α } : ( xs . map f ) . size = xs . size : = by
simp only [ ← length_toList ]
simp
-- The argument `f : α
@[ simp , grind ] theorem getElem_map ( f : α → β ) { xs : Array α } { i : Nat } ( hi : i < ( xs . map f ) . size ) :
@[ simp , grind = ] theorem getElem_map ( f : α → β ) { xs : Array α } { i : Nat } ( hi : i < ( xs . map f ) . size ) :
( xs . map f ) [ i ] = f ( xs [ i ] ' ( by simpa using hi ) ) : = by
cases xs
simp
@[ simp , grind ] theorem getElem?_map { f : α → β } { xs : Array α } { i : Nat } :
@[ simp , grind = ] theorem getElem?_map { f : α → β } { xs : Array α } { i : Nat } :
( xs . map f ) [ i ] ? = xs [ i ] ? . map f : = by
simp [ getElem?_def ]
@@ -1240,9 +1240,9 @@ where
@[ simp ] theorem mapM_empty [ Monad m ] ( f : α → m β ) : mapM f # [ ] = pure # [ ] : = by
rw [ mapM , mapM . map ] ; rfl
@[ grind ] theorem map_empty { f : α → β } : map f # [ ] = # [ ] : = by simp
@[ grind = ] theorem map_empty { f : α → β } : map f # [ ] = # [ ] : = by simp
@[ simp , grind ] theorem map_push { f : α → β } { as : Array α } { x : α } :
@[ simp , grind = ] theorem map_push { f : α → β } { as : Array α } { x : α } :
( as . push x ) . map f = ( as . map f ) . push ( f x ) : = by
ext
· simp
@@ -1420,7 +1420,7 @@ theorem array₃_induction (P : Array (Array (Array α
/- ! ### filter -/
@[ grind ] theorem filter_empty { p : α → Bool } : # [ ] . filter p = # [ ] : = rfl
@[ grind = ] theorem filter_empty { p : α → Bool } : # [ ] . filter p = # [ ] : = rfl
@[ congr ]
theorem filter_congr { xs ys : Array α } ( h : xs = ys )
@@ -1441,7 +1441,7 @@ theorem filter_congr {xs ys : Array α
induction xs with simp
| cons = > split < ; > simp [ * ]
@[ grind ] theorem toList_filter { p : α → Bool } { xs : Array α } :
@[ grind = ] theorem toList_filter { p : α → Bool } { xs : Array α } :
( xs . filter p ) . toList = xs . toList . filter p : = by
simp
@@ -1450,7 +1450,7 @@ theorem filter_congr {xs ys : Array α
apply ext'
simp [ h ]
@[ grind ] theorem _ root_ . List . filter_toArray { p : α → Bool } { l : List α } :
@[ grind = ] theorem _ root_ . List . filter_toArray { p : α → Bool } { l : List α } :
l . toArray . filter p = ( l . filter p ) . toArray : = by
simp
@@ -1468,7 +1468,7 @@ theorem filter_congr {xs ys : Array α
rcases xs with ⟨ xs ⟩
simp [ h ]
@[ grind ] theorem filter_push { p : α → Bool } { a : α } { xs : Array α } :
@[ grind = ] theorem filter_push { p : α → Bool } { a : α } { xs : Array α } :
( xs . push a ) . filter p = if p a then ( xs . filter p ) . push a else xs . filter p : = by
split < ; > simp [ * ]
@@ -1489,7 +1489,7 @@ grind_pattern Array.size_filter_le => (xs.filter p).size
rcases xs with ⟨ xs ⟩
simp
@[ simp , grind ] theorem mem_filter { p : α → Bool } { xs : Array α } { a : α } :
@[ simp , grind = ] theorem mem_filter { p : α → Bool } { xs : Array α } { a : α } :
a ∈ xs . filter p ↔ a ∈ xs ∧ p a : = by
rcases xs with ⟨ xs ⟩
simp
@@ -1551,7 +1551,7 @@ theorem map_filter_eq_foldl {f : α α α
simp only [ List . filter_cons , List . foldr_cons ]
split < ; > simp_all
@[ simp , grind ] theorem filter_append { p : α → Bool } { xs ys : Array α } { stop : Nat } ( w : stop = xs . size + ys . size ) :
@[ simp , grind = ] theorem filter_append { p : α → Bool } { xs ys : Array α } { stop : Nat } ( w : stop = xs . size + ys . size ) :
filter p ( xs + + ys ) 0 stop = filter p xs + + filter p ys : = by
subst w
rcases xs with ⟨ xs ⟩
@@ -1605,7 +1605,7 @@ theorem size_filter_lt_size_iff_exists {xs : Array α α
/- ! ### filterMap -/
@[ simp , grind ] theorem filterMap_empty { f : α → Option β } : filterMap f # [ ] = # [ ] : = rfl
@[ simp , grind = ] theorem filterMap_empty { f : α → Option β } : filterMap f # [ ] = # [ ] : = rfl
@[ congr ]
theorem filterMap_congr { as bs : Array α } ( h : as = bs )
@@ -1628,7 +1628,7 @@ theorem filterMap_congr {as bs : Array α
· simp_all [ List . filterMap_cons ]
split < ; > simp_all
@[ grind ] theorem toList_filterMap { f : α → Option β } { xs : Array α } :
@[ grind = ] theorem toList_filterMap { f : α → Option β } { xs : Array α } :
( xs . filterMap f ) . toList = xs . toList . filterMap f : = by
simp [ toList_filterMap' ]
@@ -1638,7 +1638,7 @@ theorem filterMap_congr {as bs : Array α
apply ext'
simp [ h ]
@[ grind ] theorem _ root_ . List . filterMap_toArray { f : α → Option β } { l : List α } :
@[ grind = ] theorem _ root_ . List . filterMap_toArray { f : α → Option β } { l : List α } :
l . toArray . filterMap f = ( l . filterMap f ) . toArray : = by
simp
@@ -1656,7 +1656,7 @@ theorem filterMap_congr {as bs : Array α
rcases xs with ⟨ xs ⟩
simp [ h ]
@[ grind ] theorem filterMap_push { f : α → Option β } { a : α } { xs : Array α }
@[ grind = ] theorem filterMap_push { f : α → Option β } { a : α } { xs : Array α }
( w : stop = xs . size + 1 ) :
filterMap f ( xs . push a ) 0 stop =
match f a with
@@ -1681,7 +1681,7 @@ theorem filterMap_eq_map' {f : α
cases xs
simp
@[ grind ] theorem filterMap_some { xs : Array α } : filterMap some xs = xs : = by
@[ grind = ] theorem filterMap_some { xs : Array α } : filterMap some xs = xs : = by
cases xs
simp
@@ -1709,19 +1709,19 @@ theorem filterMap_eq_filter {p : α
cases as
simp
@[ grind ]
@[ grind = ]
theorem filterMap_filterMap { f : α → Option β } { g : β → Option γ } { xs : Array α } :
filterMap g ( filterMap f xs ) = filterMap ( fun x = > ( f x ) . bind g ) xs : = by
cases xs
simp [ List . filterMap_filterMap ]
@[ grind ]
@[ grind = ]
theorem map_filterMap { f : α → Option β } { g : β → γ } { xs : Array α } :
map g ( filterMap f xs ) = filterMap ( fun x = > ( f x ) . map g ) xs : = by
cases xs
simp [ List . map_filterMap ]
@[ simp , grind ] theorem filterMap_map { f : α → β } { g : β → Option γ } { xs : Array α } :
@[ simp , grind = ] theorem filterMap_map { f : α → β } { g : β → Option γ } { xs : Array α } :
filterMap g ( map f xs ) = filterMap ( g ∘ f ) xs : = by
cases xs
simp [ List . filterMap_map ]
@@ -1736,7 +1736,7 @@ theorem filterMap_filter {p : α α α
cases xs
simp [ List . filterMap_filter ]
@[ simp , grind ] theorem mem_filterMap { f : α → Option β } { xs : Array α } { b : β } :
@[ simp , grind = ] theorem mem_filterMap { f : α → Option β } { xs : Array α } { b : β } :
b ∈ filterMap f xs ↔ ∃ a , a ∈ xs ∧ f a = some b : = by
simp only [ mem_def , toList_filterMap , List . mem_filterMap ]
@@ -1748,7 +1748,7 @@ theorem forall_mem_filterMap {f : α α
intro a
rw [ forall_comm ]
@[ simp , grind ] theorem filterMap_append { α β : Type _ } { xs ys : Array α } { f : α → Option β }
@[ simp , grind = ] theorem filterMap_append { α β : Type _ } { xs ys : Array α } { f : α → Option β }
{ stop : Nat } ( w : stop = xs . size + ys . size ) :
filterMap f ( xs + + ys ) 0 stop = filterMap f xs + + filterMap f ys : = by
subst w
@@ -1807,7 +1807,7 @@ theorem size_filterMap_lt_size_iff_exists {xs : Array α α
/- ! ### append -/
@[ simp , grind ] theorem size_append { xs ys : Array α } : ( xs + + ys ) . size = xs . size + ys . size : = by
@[ simp , grind = ] theorem size_append { xs ys : Array α } : ( xs + + ys ) . size = xs . size + ys . size : = by
simp only [ size , toList_append , List . length_append ]
@[ simp , grind _ = _ ] theorem push_append { a : α } { xs ys : Array α } : ( xs + + ys ) . push a = xs + + ys . push a : = by
@@ -1844,7 +1844,7 @@ theorem empty_append_fun : ((#[] : Array α
funext ⟨ l ⟩
simp
@[ simp , grind ] theorem mem_append { a : α } { xs ys : Array α } : a ∈ xs + + ys ↔ a ∈ xs ∨ a ∈ ys : = by
@[ simp , grind = ] theorem mem_append { a : α } { xs ys : Array α } : a ∈ xs + + ys ↔ a ∈ xs ∨ a ∈ ys : = by
simp only [ mem_def , toList_append , List . mem_append ]
theorem mem_append_left { a : α } { xs : Array α } ( ys : Array α ) ( h : a ∈ xs ) : a ∈ xs + + ys : =
@@ -1872,7 +1872,7 @@ theorem forall_mem_append {p : α α
( ∀ ( x ) ( _ : x ∈ xs + + ys ) , p x ) ↔ ( ∀ ( x ) ( _ : x ∈ xs ) , p x ) ∧ ( ∀ ( x ) ( _ : x ∈ ys ) , p x ) : = by
simp only [ mem_append , or_imp , forall_and ]
@[ grind ] theorem getElem_append { xs ys : Array α } ( h : i < ( xs + + ys ) . size ) :
@[ grind = ] theorem getElem_append { xs ys : Array α } ( h : i < ( xs + + ys ) . size ) :
( xs + + ys ) [ i ] = if h' : i < xs . size then xs [ i ] else ys [ i - xs . size ] ' ( by simp at h ; omega ) : = by
cases xs ; cases ys
simp [ List . getElem_append ]
@@ -1906,7 +1906,7 @@ theorem getElem?_append_right {xs ys : Array α
simp at h
simp [ List . getElem?_append_right , h ]
@[ grind ] theorem getElem?_append { xs ys : Array α } { i : Nat } :
@[ grind = ] theorem getElem?_append { xs ys : Array α } { i : Nat } :
( xs + + ys ) [ i ] ? = if i < xs . size then xs [ i ] ? else ys [ i - xs . size ] ? : = by
split < ; > rename_i h
· exact getElem?_append_left h
@@ -2049,7 +2049,7 @@ theorem append_eq_append_iff {ws xs ys zs : Array α
· left ; exact ⟨ as . toList , by simp ⟩
· right ; exact ⟨ cs . toList , by simp ⟩
@[ grind ] theorem set_append { xs ys : Array α } { i : Nat } { x : α } ( h : i < ( xs + + ys ) . size ) :
@[ grind = ] theorem set_append { xs ys : Array α } { i : Nat } { x : α } ( h : i < ( xs + + ys ) . size ) :
( xs + + ys ) . set i x =
if h' : i < xs . size then
xs . set i x + + ys
@@ -2069,7 +2069,7 @@ theorem append_eq_append_iff {ws xs ys zs : Array α
( xs + + ys ) . set i x = xs + + ys . set ( i - xs . size ) x ( by simp at h' ; omega ) : = by
rw [ set_append , dif_neg ( by omega ) ]
@[ grind ] theorem setIfInBounds_append { xs ys : Array α } { i : Nat } { x : α } :
@[ grind = ] theorem setIfInBounds_append { xs ys : Array α } { i : Nat } { x : α } :
( xs + + ys ) . setIfInBounds i x =
if i < xs . size then
xs . setIfInBounds i x + + ys
@@ -2106,7 +2106,7 @@ theorem append_eq_filterMap_iff {f : α
∃ as bs , zs = as + + bs ∧ filterMap f as = xs ∧ filterMap f bs = ys : = by
rw [ eq_comm , filterMap_eq_append_iff ]
@[ simp , grind ] theorem map_append { f : α → β } { xs ys : Array α } :
@[ simp , grind = ] theorem map_append { f : α → β } { xs ys : Array α } :
map f ( xs + + ys ) = map f xs + + map f ys : = by
rcases xs with ⟨ xs ⟩
rcases ys with ⟨ ys ⟩
@@ -2122,9 +2122,9 @@ theorem append_eq_map_iff {f : α
/- ! ### flatten -/
@[ simp , grind ] theorem flatten_empty : ( # [ ] : Array ( Array α ) ) . flatten = # [ ] : = by simp [ flatten ] ; rfl
@[ simp , grind = ] theorem flatten_empty : ( # [ ] : Array ( Array α ) ) . flatten = # [ ] : = by simp [ flatten ] ; rfl
@[ simp , grind ] theorem toList_flatten { xss : Array ( Array α ) } :
@[ simp , grind = ] theorem toList_flatten { xss : Array ( Array α ) } :
xss . flatten . toList = ( xss . toList . map toList ) . flatten : = by
dsimp [ flatten ]
simp only [ ← foldl_toList ]
@@ -2150,11 +2150,11 @@ theorem flatten_map_toArray {L : List (List α
apply ext'
simp
@[ simp , grind ] theorem size_flatten { xss : Array ( Array α ) } : xss . flatten . size = ( xss . map size ) . sum : = by
@[ simp , grind = ] theorem size_flatten { xss : Array ( Array α ) } : xss . flatten . size = ( xss . map size ) . sum : = by
cases xss using array₂_induction
simp [ Function . comp_def ]
@[ simp , grind ] theorem flatten_singleton { xs : Array α } : # [ xs ] . flatten = xs : = by simp [ flatten ] ; rfl
@[ simp , grind = ] theorem flatten_singleton { xs : Array α } : # [ xs ] . flatten = xs : = by simp [ flatten ] ; rfl
theorem mem_flatten : ∀ { xss : Array ( Array α ) } , a ∈ xss . flatten ↔ ∃ xs , xs ∈ xss ∧ a ∈ xs : = by
simp only [ mem_def , toList_flatten , List . mem_flatten , List . mem_map ]
@@ -2197,7 +2197,7 @@ theorem flatten_eq_flatMap {xss : Array (Array α
Function . comp_def ]
rw [ ← Function . comp_def , ← List . map_map , flatten_toArray_map ]
@[ simp , grind ] theorem filterMap_flatten { f : α → Option β } { xss : Array ( Array α ) } { stop : Nat } ( w : stop = xss . flatten . size ) :
@[ simp , grind = ] theorem filterMap_flatten { f : α → Option β } { xss : Array ( Array α ) } { stop : Nat } ( w : stop = xss . flatten . size ) :
filterMap f ( flatten xss ) 0 stop = flatten ( map ( filterMap f ) xss ) : = by
subst w
induction xss using array₂_induction
