feat: lemmas about List/Array/Vector.contains (#8175)
This PR adds simp/grind lemmas about `List`/`Array`/`Vector.contains`. In the presence of `LawfulBEq` these effectively already held, via simplifying `contains` to `mem`, but now these also fire without `LawfulBEq`.
This commit is contained in:
Kim Morrison
GitHub
parent
7ffeacf967
commit
a9f4170372
9 changed files with 586 additions and 399 deletions
|
|
@ -3742,6 +3742,56 @@ theorem contains_iff_mem [BEq α] [LawfulBEq α] {xs : Array α} {a : α} :
|
|||
xs.contains a ↔ a ∈ xs := by
|
||||
simp
|
||||
|
||||
@[simp, grind]
|
||||
theorem contains_toList [BEq α] {xs : Array α} {x : α} :
|
||||
xs.toList.contains x = xs.contains x := by
|
||||
rcases xs with ⟨xs⟩
|
||||
simp
|
||||
|
||||
@[simp, grind]
|
||||
theorem contains_map [BEq β] {xs : Array α} {x : β} {f : α → β} :
|
||||
(xs.map f).contains x = xs.any (fun a => x == f a) := by
|
||||
rcases xs with ⟨xs⟩
|
||||
simp
|
||||
|
||||
@[simp, grind]
|
||||
theorem contains_filter [BEq α] {xs : Array α} {x : α} {p : α → Bool} :
|
||||
(xs.filter p).contains x = xs.any (fun a => x == a && p a) := by
|
||||
rcases xs with ⟨xs⟩
|
||||
simp
|
||||
|
||||
@[simp, grind]
|
||||
theorem contains_filterMap [BEq β] {xs : Array α} {x : β} {f : α → Option β} :
|
||||
(xs.filterMap f).contains x = xs.any (fun a => (f a).any fun b => x == b) := by
|
||||
rcases xs with ⟨xs⟩
|
||||
simp
|
||||
|
||||
@[simp, grind _=_]
|
||||
theorem contains_append [BEq α] {xs ys : Array α} {x : α} :
|
||||
(xs ++ ys).contains x = (xs.contains x || ys.contains x) := by
|
||||
rcases xs with ⟨xs⟩
|
||||
rcases ys with ⟨ys⟩
|
||||
simp
|
||||
|
||||
@[simp, grind]
|
||||
theorem contains_flatten [BEq α] {xs : Array (Array α)} {x : α} :
|
||||
(xs.flatten).contains x = xs.any fun xs => xs.contains x := by
|
||||
rcases xs with ⟨xs⟩
|
||||
simp [Function.comp_def]
|
||||
|
||||
@[simp, grind]
|
||||
theorem contains_reverse [BEq α] {xs : Array α} {x : α} :
|
||||
(xs.reverse).contains x = xs.contains x := by
|
||||
rcases xs with ⟨xs⟩
|
||||
simp
|
||||
|
||||
@[simp, grind]
|
||||
theorem contains_flatMap [BEq β] {xs : Array α} {f : α → Array β} {x : β} :
|
||||
(xs.flatMap f).contains x = xs.any fun a => (f a).contains x := by
|
||||
rcases xs with ⟨xs⟩
|
||||
simp
|
||||
|
||||
|
||||
/-! ### more lemmas about `pop` -/
|
||||
|
||||
theorem pop_append {xs ys : Array α} :
|
||||
|
|
@ -3754,193 +3804,6 @@ theorem pop_append {xs ys : Array α} :
|
|||
@[deprecated pop_replicate (since := "2025-03-18")]
|
||||
abbrev pop_mkArray := @pop_replicate
|
||||
|
||||
/-! ### modify -/
|
||||
|
||||
@[simp] theorem size_modify {xs : Array α} {i : Nat} {f : α → α} : (xs.modify i f).size = xs.size := by
|
||||
unfold modify modifyM Id.run
|
||||
split <;> simp
|
||||
|
||||
theorem getElem_modify {xs : Array α} {j i} (h : i < (xs.modify j f).size) :
|
||||
(xs.modify j f)[i] = if j = i then f (xs[i]'(by simpa using h)) else xs[i]'(by simpa using h) := by
|
||||
simp only [modify, modifyM, Id.run, Id.pure_eq]
|
||||
split
|
||||
· simp only [Id.bind_eq, getElem_set]; split <;> simp [*]
|
||||
· rw [if_neg (mt (by rintro rfl; exact h) (by simp_all))]
|
||||
|
||||
@[simp] theorem toList_modify {xs : Array α} {f : α → α} {i : Nat} :
|
||||
(xs.modify i f).toList = xs.toList.modify i f := by
|
||||
apply List.ext_getElem
|
||||
· simp
|
||||
· simp [getElem_modify, List.getElem_modify]
|
||||
|
||||
theorem getElem_modify_self {xs : Array α} {i : Nat} (f : α → α) (h : i < (xs.modify i f).size) :
|
||||
(xs.modify i f)[i] = f (xs[i]'(by simpa using h)) := by
|
||||
simp [getElem_modify h]
|
||||
|
||||
theorem getElem_modify_of_ne {xs : Array α} {i : Nat} (h : i ≠ j)
|
||||
(f : α → α) (hj : j < (xs.modify i f).size) :
|
||||
(xs.modify i f)[j] = xs[j]'(by simpa using hj) := by
|
||||
simp [getElem_modify hj, h]
|
||||
|
||||
theorem getElem?_modify {xs : Array α} {i : Nat} {f : α → α} {j : Nat} :
|
||||
(xs.modify i f)[j]? = if i = j then xs[j]?.map f else xs[j]? := by
|
||||
simp only [getElem?_def, size_modify, getElem_modify, Option.map_dif]
|
||||
split <;> split <;> rfl
|
||||
|
||||
/-! ### swap -/
|
||||
|
||||
@[simp] theorem getElem_swap_right {xs : Array α} {i j : Nat} {hi hj} :
|
||||
(xs.swap i j hi hj)[j]'(by simpa using hj) = xs[i] := by
|
||||
simp [swap_def, getElem_set]
|
||||
|
||||
@[simp] theorem getElem_swap_left {xs : Array α} {i j : Nat} {hi hj} :
|
||||
(xs.swap i j hi hj)[i]'(by simpa using hi) = xs[j] := by
|
||||
simp +contextual [swap_def, getElem_set]
|
||||
|
||||
@[simp] theorem getElem_swap_of_ne {xs : Array α} {i j : Nat} {hi hj} (hp : k < xs.size)
|
||||
(hi' : k ≠ i) (hj' : k ≠ j) : (xs.swap i j hi hj)[k]'(xs.size_swap .. |>.symm ▸ hp) = xs[k] := by
|
||||
simp [swap_def, getElem_set, hi'.symm, hj'.symm]
|
||||
|
||||
theorem getElem_swap' {xs : Array α} {i j : Nat} {hi hj} {k : Nat} (hk : k < xs.size) :
|
||||
(xs.swap i j hi hj)[k]'(by simp_all) = if k = i then xs[j] else if k = j then xs[i] else xs[k] := by
|
||||
split
|
||||
· simp_all only [getElem_swap_left]
|
||||
· split <;> simp_all
|
||||
|
||||
theorem getElem_swap {xs : Array α} {i j : Nat} (hi hj) {k : Nat} (hk : k < (xs.swap i j hi hj).size) :
|
||||
(xs.swap i j hi hj)[k] = if k = i then xs[j] else if k = j then xs[i] else xs[k]'(by simp_all) := by
|
||||
apply getElem_swap'
|
||||
|
||||
@[simp] theorem swap_swap {xs : Array α} {i j : Nat} (hi hj) :
|
||||
(xs.swap i j hi hj).swap i j ((xs.size_swap ..).symm ▸ hi) ((xs.size_swap ..).symm ▸ hj) = xs := by
|
||||
apply ext
|
||||
· simp only [size_swap]
|
||||
· intros
|
||||
simp only [getElem_swap]
|
||||
split
|
||||
· simp_all
|
||||
· split <;> simp_all
|
||||
|
||||
theorem swap_comm {xs : Array α} {i j : Nat} (hi hj) : xs.swap i j hi hj = xs.swap j i hj hi := by
|
||||
apply ext
|
||||
· simp only [size_swap]
|
||||
· intros
|
||||
simp only [getElem_swap]
|
||||
split
|
||||
· split <;> simp_all
|
||||
· split <;> simp_all
|
||||
|
||||
@[simp] theorem size_swapIfInBounds {xs : Array α} {i j : Nat} :
|
||||
(xs.swapIfInBounds i j).size = xs.size := by unfold swapIfInBounds; split <;> (try split) <;> simp [size_swap]
|
||||
|
||||
@[deprecated size_swapIfInBounds (since := "2024-11-24")] abbrev size_swap! := @size_swapIfInBounds
|
||||
|
||||
/-! ### swapAt -/
|
||||
|
||||
@[simp] theorem swapAt_def {xs : Array α} {i : Nat} {v : α} (hi) :
|
||||
xs.swapAt i v hi = (xs[i], xs.set i v) := rfl
|
||||
|
||||
theorem size_swapAt {xs : Array α} {i : Nat} {v : α} (hi) :
|
||||
(xs.swapAt i v hi).2.size = xs.size := by simp
|
||||
|
||||
@[simp]
|
||||
theorem swapAt!_def {xs : Array α} {i : Nat} {v : α} (h : i < xs.size) :
|
||||
xs.swapAt! i v = (xs[i], xs.set i v) := by simp [swapAt!, h]
|
||||
|
||||
@[simp] theorem size_swapAt! {xs : Array α} {i : Nat} {v : α} :
|
||||
(xs.swapAt! i v).2.size = xs.size := by
|
||||
simp only [swapAt!]
|
||||
split
|
||||
· simp
|
||||
· rfl
|
||||
|
||||
/-! ### replace -/
|
||||
|
||||
section replace
|
||||
variable [BEq α]
|
||||
|
||||
@[simp, grind] theorem replace_empty : (#[] : Array α).replace a b = #[] := by rfl
|
||||
|
||||
@[simp, grind] theorem replace_singleton {a b c : α} : #[a].replace b c = #[if a == b then c else a] := by
|
||||
simp only [replace, List.finIdxOf?_toArray, List.finIdxOf?]
|
||||
by_cases h : a == b <;> simp [h]
|
||||
|
||||
@[simp, grind] theorem size_replace {xs : Array α} : (xs.replace a b).size = xs.size := by
|
||||
simp only [replace]
|
||||
split <;> simp
|
||||
|
||||
-- This hypothesis could probably be dropped from some of the lemmas below,
|
||||
-- by proving them direct from the definition rather than going via `List`.
|
||||
variable [LawfulBEq α]
|
||||
|
||||
@[simp] theorem replace_of_not_mem {xs : Array α} (h : ¬ a ∈ xs) : xs.replace a b = xs := by
|
||||
cases xs
|
||||
simp_all
|
||||
|
||||
@[grind] theorem getElem?_replace {xs : Array α} {i : Nat} :
|
||||
(xs.replace a b)[i]? = if xs[i]? == some a then if a ∈ xs.take i then some a else some b else xs[i]? := by
|
||||
rcases xs with ⟨xs⟩
|
||||
simp only [List.replace_toArray, List.getElem?_toArray, List.getElem?_replace, take_eq_extract,
|
||||
List.extract_toArray, List.extract_eq_drop_take, Nat.sub_zero, List.drop_zero, mem_toArray]
|
||||
|
||||
theorem getElem?_replace_of_ne {xs : Array α} {i : Nat} (h : xs[i]? ≠ some a) :
|
||||
(xs.replace a b)[i]? = xs[i]? := by
|
||||
simp_all [getElem?_replace]
|
||||
|
||||
@[grind] theorem getElem_replace {xs : Array α} {i : Nat} (h : i < xs.size) :
|
||||
(xs.replace a b)[i]'(by simpa) = if xs[i] == a then if a ∈ xs.take i then a else b else xs[i] := by
|
||||
apply Option.some.inj
|
||||
rw [← getElem?_eq_getElem, getElem?_replace]
|
||||
split <;> split <;> simp_all
|
||||
|
||||
theorem getElem_replace_of_ne {xs : Array α} {i : Nat} {h : i < xs.size} (h' : xs[i] ≠ a) :
|
||||
(xs.replace a b)[i]'(by simpa) = xs[i]'(h) := by
|
||||
rw [getElem_replace h]
|
||||
simp [h']
|
||||
|
||||
@[grind] theorem replace_append {xs ys : Array α} :
|
||||
(xs ++ ys).replace a b = if a ∈ xs then xs.replace a b ++ ys else xs ++ ys.replace a b := by
|
||||
rcases xs with ⟨xs⟩
|
||||
rcases ys with ⟨ys⟩
|
||||
simp only [List.append_toArray, List.replace_toArray, List.replace_append, mem_toArray]
|
||||
split <;> simp
|
||||
|
||||
@[grind] theorem replace_push {xs : Array α} {a b c : α} :
|
||||
(xs.push a).replace b c = if b ∈ xs then (xs.replace b c).push a else xs.push (if b == a then c else a) := by
|
||||
rcases xs with ⟨xs⟩
|
||||
simp [List.replace_append]
|
||||
split <;> simp
|
||||
|
||||
theorem replace_append_left {xs ys : Array α} (h : a ∈ xs) :
|
||||
(xs ++ ys).replace a b = xs.replace a b ++ ys := by
|
||||
simp [replace_append, h]
|
||||
|
||||
theorem replace_append_right {xs ys : Array α} (h : ¬ a ∈ xs) :
|
||||
(xs ++ ys).replace a b = xs ++ ys.replace a b := by
|
||||
simp [replace_append, h]
|
||||
|
||||
theorem replace_extract {xs : Array α} {i : Nat} :
|
||||
(xs.extract 0 i).replace a b = (xs.replace a b).extract 0 i := by
|
||||
rcases xs with ⟨xs⟩
|
||||
simp [List.replace_take]
|
||||
|
||||
@[simp] theorem replace_replicate_self {a : α} (h : 0 < n) :
|
||||
(replicate n a).replace a b = #[b] ++ replicate (n - 1) a := by
|
||||
cases n <;> simp_all [replicate_succ', replace_append]
|
||||
|
||||
@[deprecated replace_replicate_self (since := "2025-03-18")]
|
||||
abbrev replace_mkArray_self := @replace_replicate_self
|
||||
|
||||
@[simp] theorem replace_replicate_ne {a b c : α} (h : !b == a) :
|
||||
(replicate n a).replace b c = replicate n a := by
|
||||
rw [replace_of_not_mem]
|
||||
simp_all
|
||||
|
||||
@[deprecated replace_replicate_ne (since := "2025-03-18")]
|
||||
abbrev replace_mkArray_ne := @replace_replicate_ne
|
||||
|
||||
end replace
|
||||
|
||||
/-! ## Logic -/
|
||||
|
||||
/-! ### any / all -/
|
||||
|
|
@ -4180,6 +4043,193 @@ abbrev any_mkArray := @any_replicate
|
|||
@[deprecated all_replicate (since := "2025-03-18")]
|
||||
abbrev all_mkArray := @all_replicate
|
||||
|
||||
/-! ### modify -/
|
||||
|
||||
@[simp] theorem size_modify {xs : Array α} {i : Nat} {f : α → α} : (xs.modify i f).size = xs.size := by
|
||||
unfold modify modifyM Id.run
|
||||
split <;> simp
|
||||
|
||||
theorem getElem_modify {xs : Array α} {j i} (h : i < (xs.modify j f).size) :
|
||||
(xs.modify j f)[i] = if j = i then f (xs[i]'(by simpa using h)) else xs[i]'(by simpa using h) := by
|
||||
simp only [modify, modifyM, Id.run, Id.pure_eq]
|
||||
split
|
||||
· simp only [Id.bind_eq, getElem_set]; split <;> simp [*]
|
||||
· rw [if_neg (mt (by rintro rfl; exact h) (by simp_all))]
|
||||
|
||||
@[simp] theorem toList_modify {xs : Array α} {f : α → α} {i : Nat} :
|
||||
(xs.modify i f).toList = xs.toList.modify i f := by
|
||||
apply List.ext_getElem
|
||||
· simp
|
||||
· simp [getElem_modify, List.getElem_modify]
|
||||
|
||||
theorem getElem_modify_self {xs : Array α} {i : Nat} (f : α → α) (h : i < (xs.modify i f).size) :
|
||||
(xs.modify i f)[i] = f (xs[i]'(by simpa using h)) := by
|
||||
simp [getElem_modify h]
|
||||
|
||||
theorem getElem_modify_of_ne {xs : Array α} {i : Nat} (h : i ≠ j)
|
||||
(f : α → α) (hj : j < (xs.modify i f).size) :
|
||||
(xs.modify i f)[j] = xs[j]'(by simpa using hj) := by
|
||||
simp [getElem_modify hj, h]
|
||||
|
||||
theorem getElem?_modify {xs : Array α} {i : Nat} {f : α → α} {j : Nat} :
|
||||
(xs.modify i f)[j]? = if i = j then xs[j]?.map f else xs[j]? := by
|
||||
simp only [getElem?_def, size_modify, getElem_modify, Option.map_dif]
|
||||
split <;> split <;> rfl
|
||||
|
||||
/-! ### swap -/
|
||||
|
||||
@[simp] theorem getElem_swap_right {xs : Array α} {i j : Nat} {hi hj} :
|
||||
(xs.swap i j hi hj)[j]'(by simpa using hj) = xs[i] := by
|
||||
simp [swap_def, getElem_set]
|
||||
|
||||
@[simp] theorem getElem_swap_left {xs : Array α} {i j : Nat} {hi hj} :
|
||||
(xs.swap i j hi hj)[i]'(by simpa using hi) = xs[j] := by
|
||||
simp +contextual [swap_def, getElem_set]
|
||||
|
||||
@[simp] theorem getElem_swap_of_ne {xs : Array α} {i j : Nat} {hi hj} (hp : k < xs.size)
|
||||
(hi' : k ≠ i) (hj' : k ≠ j) : (xs.swap i j hi hj)[k]'(xs.size_swap .. |>.symm ▸ hp) = xs[k] := by
|
||||
simp [swap_def, getElem_set, hi'.symm, hj'.symm]
|
||||
|
||||
theorem getElem_swap' {xs : Array α} {i j : Nat} {hi hj} {k : Nat} (hk : k < xs.size) :
|
||||
(xs.swap i j hi hj)[k]'(by simp_all) = if k = i then xs[j] else if k = j then xs[i] else xs[k] := by
|
||||
split
|
||||
· simp_all only [getElem_swap_left]
|
||||
· split <;> simp_all
|
||||
|
||||
theorem getElem_swap {xs : Array α} {i j : Nat} (hi hj) {k : Nat} (hk : k < (xs.swap i j hi hj).size) :
|
||||
(xs.swap i j hi hj)[k] = if k = i then xs[j] else if k = j then xs[i] else xs[k]'(by simp_all) := by
|
||||
apply getElem_swap'
|
||||
|
||||
@[simp] theorem swap_swap {xs : Array α} {i j : Nat} (hi hj) :
|
||||
(xs.swap i j hi hj).swap i j ((xs.size_swap ..).symm ▸ hi) ((xs.size_swap ..).symm ▸ hj) = xs := by
|
||||
apply ext
|
||||
· simp only [size_swap]
|
||||
· intros
|
||||
simp only [getElem_swap]
|
||||
split
|
||||
· simp_all
|
||||
· split <;> simp_all
|
||||
|
||||
theorem swap_comm {xs : Array α} {i j : Nat} (hi hj) : xs.swap i j hi hj = xs.swap j i hj hi := by
|
||||
apply ext
|
||||
· simp only [size_swap]
|
||||
· intros
|
||||
simp only [getElem_swap]
|
||||
split
|
||||
· split <;> simp_all
|
||||
· split <;> simp_all
|
||||
|
||||
@[simp] theorem size_swapIfInBounds {xs : Array α} {i j : Nat} :
|
||||
(xs.swapIfInBounds i j).size = xs.size := by unfold swapIfInBounds; split <;> (try split) <;> simp [size_swap]
|
||||
|
||||
@[deprecated size_swapIfInBounds (since := "2024-11-24")] abbrev size_swap! := @size_swapIfInBounds
|
||||
|
||||
/-! ### swapAt -/
|
||||
|
||||
@[simp] theorem swapAt_def {xs : Array α} {i : Nat} {v : α} (hi) :
|
||||
xs.swapAt i v hi = (xs[i], xs.set i v) := rfl
|
||||
|
||||
theorem size_swapAt {xs : Array α} {i : Nat} {v : α} (hi) :
|
||||
(xs.swapAt i v hi).2.size = xs.size := by simp
|
||||
|
||||
@[simp]
|
||||
theorem swapAt!_def {xs : Array α} {i : Nat} {v : α} (h : i < xs.size) :
|
||||
xs.swapAt! i v = (xs[i], xs.set i v) := by simp [swapAt!, h]
|
||||
|
||||
@[simp] theorem size_swapAt! {xs : Array α} {i : Nat} {v : α} :
|
||||
(xs.swapAt! i v).2.size = xs.size := by
|
||||
simp only [swapAt!]
|
||||
split
|
||||
· simp
|
||||
· rfl
|
||||
|
||||
/-! ### replace -/
|
||||
|
||||
section replace
|
||||
variable [BEq α]
|
||||
|
||||
@[simp, grind] theorem replace_empty : (#[] : Array α).replace a b = #[] := by rfl
|
||||
|
||||
@[simp, grind] theorem replace_singleton {a b c : α} : #[a].replace b c = #[if a == b then c else a] := by
|
||||
simp only [replace, List.finIdxOf?_toArray, List.finIdxOf?]
|
||||
by_cases h : a == b <;> simp [h]
|
||||
|
||||
@[simp, grind] theorem size_replace {xs : Array α} : (xs.replace a b).size = xs.size := by
|
||||
simp only [replace]
|
||||
split <;> simp
|
||||
|
||||
-- This hypothesis could probably be dropped from some of the lemmas below,
|
||||
-- by proving them direct from the definition rather than going via `List`.
|
||||
variable [LawfulBEq α]
|
||||
|
||||
@[simp] theorem replace_of_not_mem {xs : Array α} (h : ¬ a ∈ xs) : xs.replace a b = xs := by
|
||||
cases xs
|
||||
simp_all
|
||||
|
||||
@[grind] theorem getElem?_replace {xs : Array α} {i : Nat} :
|
||||
(xs.replace a b)[i]? = if xs[i]? == some a then if a ∈ xs.take i then some a else some b else xs[i]? := by
|
||||
rcases xs with ⟨xs⟩
|
||||
simp only [List.replace_toArray, List.getElem?_toArray, List.getElem?_replace, take_eq_extract,
|
||||
List.extract_toArray, List.extract_eq_drop_take, Nat.sub_zero, List.drop_zero, mem_toArray]
|
||||
|
||||
theorem getElem?_replace_of_ne {xs : Array α} {i : Nat} (h : xs[i]? ≠ some a) :
|
||||
(xs.replace a b)[i]? = xs[i]? := by
|
||||
simp_all [getElem?_replace]
|
||||
|
||||
@[grind] theorem getElem_replace {xs : Array α} {i : Nat} (h : i < xs.size) :
|
||||
(xs.replace a b)[i]'(by simpa) = if xs[i] == a then if a ∈ xs.take i then a else b else xs[i] := by
|
||||
apply Option.some.inj
|
||||
rw [← getElem?_eq_getElem, getElem?_replace]
|
||||
split <;> split <;> simp_all
|
||||
|
||||
theorem getElem_replace_of_ne {xs : Array α} {i : Nat} {h : i < xs.size} (h' : xs[i] ≠ a) :
|
||||
(xs.replace a b)[i]'(by simpa) = xs[i]'(h) := by
|
||||
rw [getElem_replace h]
|
||||
simp [h']
|
||||
|
||||
@[grind] theorem replace_append {xs ys : Array α} :
|
||||
(xs ++ ys).replace a b = if a ∈ xs then xs.replace a b ++ ys else xs ++ ys.replace a b := by
|
||||
rcases xs with ⟨xs⟩
|
||||
rcases ys with ⟨ys⟩
|
||||
simp only [List.append_toArray, List.replace_toArray, List.replace_append, mem_toArray]
|
||||
split <;> simp
|
||||
|
||||
@[grind] theorem replace_push {xs : Array α} {a b c : α} :
|
||||
(xs.push a).replace b c = if b ∈ xs then (xs.replace b c).push a else xs.push (if b == a then c else a) := by
|
||||
rcases xs with ⟨xs⟩
|
||||
simp [List.replace_append]
|
||||
split <;> simp
|
||||
|
||||
theorem replace_append_left {xs ys : Array α} (h : a ∈ xs) :
|
||||
(xs ++ ys).replace a b = xs.replace a b ++ ys := by
|
||||
simp [replace_append, h]
|
||||
|
||||
theorem replace_append_right {xs ys : Array α} (h : ¬ a ∈ xs) :
|
||||
(xs ++ ys).replace a b = xs ++ ys.replace a b := by
|
||||
simp [replace_append, h]
|
||||
|
||||
theorem replace_extract {xs : Array α} {i : Nat} :
|
||||
(xs.extract 0 i).replace a b = (xs.replace a b).extract 0 i := by
|
||||
rcases xs with ⟨xs⟩
|
||||
simp [List.replace_take]
|
||||
|
||||
@[simp] theorem replace_replicate_self {a : α} (h : 0 < n) :
|
||||
(replicate n a).replace a b = #[b] ++ replicate (n - 1) a := by
|
||||
cases n <;> simp_all [replicate_succ', replace_append]
|
||||
|
||||
@[deprecated replace_replicate_self (since := "2025-03-18")]
|
||||
abbrev replace_mkArray_self := @replace_replicate_self
|
||||
|
||||
@[simp] theorem replace_replicate_ne {a b c : α} (h : !b == a) :
|
||||
(replicate n a).replace b c = replicate n a := by
|
||||
rw [replace_of_not_mem]
|
||||
simp_all
|
||||
|
||||
@[deprecated replace_replicate_ne (since := "2025-03-18")]
|
||||
abbrev replace_mkArray_ne := @replace_replicate_ne
|
||||
|
||||
end replace
|
||||
|
||||
/-! ### toListRev -/
|
||||
|
||||
/--
|
||||
|
|
|
|||
|
|
@ -1539,7 +1539,7 @@ Examples:
|
|||
* `[1, 2, 3].insert 2 = [1, 2, 3]`
|
||||
-/
|
||||
@[inline] protected def insert [BEq α] (a : α) (l : List α) : List α :=
|
||||
if l.elem a then l else a :: l
|
||||
if l.contains a then l else a :: l
|
||||
|
||||
/--
|
||||
Inserts an element into a list at the specified index. If the index is greater than the length of
|
||||
|
|
|
|||
|
|
@ -2972,7 +2972,10 @@ theorem leftpad_suffix {n : Nat} {a : α} {l : List α} : l <:+ (leftpad n a l)
|
|||
|
||||
/-! ## List membership -/
|
||||
|
||||
/-! ### elem / contains -/
|
||||
/-! ### contains / elem
|
||||
|
||||
Recall that the preferred simp normal form is `contains` rather than `elem`.
|
||||
-/
|
||||
|
||||
theorem elem_cons_self [BEq α] [LawfulBEq α] {a : α} : (a::as).elem a = true := by simp
|
||||
|
||||
|
|
@ -2987,6 +2990,57 @@ theorem contains_iff_mem [BEq α] [LawfulBEq α] {l : List α} {a : α} :
|
|||
l.contains a ↔ a ∈ l := by
|
||||
simp
|
||||
|
||||
@[simp, grind]
|
||||
theorem contains_map [BEq β] {l : List α} {x : β} {f : α → β} :
|
||||
(l.map f).contains x = l.any (fun a => x == f a) := by
|
||||
induction l with simp_all
|
||||
|
||||
@[simp, grind]
|
||||
theorem contains_filter [BEq α] {l : List α} {x : α} {p : α → Bool} :
|
||||
(l.filter p).contains x = l.any (fun a => x == a && p a) := by
|
||||
induction l with
|
||||
| nil => simp
|
||||
| cons a l ih =>
|
||||
simp only [filter_cons, any_cons]
|
||||
split <;> simp_all
|
||||
|
||||
@[simp, grind]
|
||||
theorem contains_filterMap [BEq β] {l : List α} {x : β} {f : α → Option β} :
|
||||
(l.filterMap f).contains x = l.any (fun a => (f a).any fun b => x == b) := by
|
||||
induction l with
|
||||
| nil => simp
|
||||
| cons a l ih =>
|
||||
simp only [filterMap_cons, any_cons]
|
||||
split <;> simp_all
|
||||
|
||||
@[simp, grind _=_]
|
||||
theorem contains_append [BEq α] {l₁ l₂ : List α} {x : α} :
|
||||
(l₁ ++ l₂).contains x = (l₁.contains x || l₂.contains x) := by
|
||||
induction l₁ with
|
||||
| nil => simp
|
||||
| cons a l ih => simp [ih, Bool.or_assoc]
|
||||
|
||||
@[simp, grind]
|
||||
theorem contains_flatten [BEq α] {l : List (List α)} {x : α} :
|
||||
l.flatten.contains x = l.any fun l => l.contains x := by
|
||||
induction l with
|
||||
| nil => simp
|
||||
| cons _ l ih => simp [ih]
|
||||
|
||||
@[simp, grind]
|
||||
theorem contains_reverse [BEq α] {l : List α} {x : α} :
|
||||
(l.reverse).contains x = l.contains x := by
|
||||
induction l with
|
||||
| nil => simp
|
||||
| cons a l ih => simp [ih, Bool.or_comm]
|
||||
|
||||
@[simp, grind]
|
||||
theorem contains_flatMap [BEq β] {l : List α} {f : α → List β} {x : β} :
|
||||
(l.flatMap f).contains x = l.any fun a => (f a).contains x := by
|
||||
induction l with
|
||||
| nil => simp
|
||||
| cons a l ih => simp [ih]
|
||||
|
||||
/-! ## Sublists -/
|
||||
|
||||
/-! ### partition
|
||||
|
|
@ -3138,6 +3192,137 @@ theorem splitAt_go {i : Nat} {l acc : List α} :
|
|||
singleton_append, length_cons]
|
||||
simp only [Nat.succ_lt_succ_iff]
|
||||
|
||||
/-! ## Logic -/
|
||||
|
||||
/-! ### any / all -/
|
||||
|
||||
theorem not_any_eq_all_not {l : List α} {p : α → Bool} : (!l.any p) = l.all fun a => !p a := by
|
||||
induction l with simp | cons _ _ ih => rw [ih]
|
||||
|
||||
theorem not_all_eq_any_not {l : List α} {p : α → Bool} : (!l.all p) = l.any fun a => !p a := by
|
||||
induction l with simp | cons _ _ ih => rw [ih]
|
||||
|
||||
theorem and_any_distrib_left {l : List α} {p : α → Bool} {q : Bool} :
|
||||
(q && l.any p) = l.any fun a => q && p a := by
|
||||
induction l with simp | cons _ _ ih => rw [Bool.and_or_distrib_left, ih]
|
||||
|
||||
theorem and_any_distrib_right {l : List α} {p : α → Bool} {q : Bool} :
|
||||
(l.any p && q) = l.any fun a => p a && q := by
|
||||
induction l with simp | cons _ _ ih => rw [Bool.and_or_distrib_right, ih]
|
||||
|
||||
theorem or_all_distrib_left {l : List α} {p : α → Bool} {q : Bool} :
|
||||
(q || l.all p) = l.all fun a => q || p a := by
|
||||
induction l with simp | cons _ _ ih => rw [Bool.or_and_distrib_left, ih]
|
||||
|
||||
theorem or_all_distrib_right {l : List α} {p : α → Bool} {q : Bool} :
|
||||
(l.all p || q) = l.all fun a => p a || q := by
|
||||
induction l with simp | cons _ _ ih => rw [Bool.or_and_distrib_right, ih]
|
||||
|
||||
theorem any_eq_not_all_not {l : List α} {p : α → Bool} : l.any p = !l.all (!p .) := by
|
||||
simp only [not_all_eq_any_not, Bool.not_not]
|
||||
|
||||
theorem all_eq_not_any_not {l : List α} {p : α → Bool} : l.all p = !l.any (!p .) := by
|
||||
simp only [not_any_eq_all_not, Bool.not_not]
|
||||
|
||||
@[simp] theorem any_map {l : List α} {p : β → Bool} : (l.map f).any p = l.any (p ∘ f) := by
|
||||
induction l with simp | cons _ _ ih => rw [ih]
|
||||
|
||||
@[simp] theorem all_map {l : List α} {p : β → Bool} : (l.map f).all p = l.all (p ∘ f) := by
|
||||
induction l with simp | cons _ _ ih => rw [ih]
|
||||
|
||||
@[simp] theorem any_filter {l : List α} {p q : α → Bool} :
|
||||
(filter p l).any q = l.any fun a => p a && q a := by
|
||||
induction l with
|
||||
| nil => rfl
|
||||
| cons h t ih =>
|
||||
simp only [filter_cons]
|
||||
split <;> simp_all
|
||||
|
||||
@[simp] theorem all_filter {l : List α} {p q : α → Bool} :
|
||||
(filter p l).all q = l.all fun a => !(p a) || q a := by
|
||||
induction l with
|
||||
| nil => rfl
|
||||
| cons h t ih =>
|
||||
simp only [filter_cons]
|
||||
split <;> simp_all
|
||||
|
||||
@[simp] theorem any_filterMap {l : List α} {f : α → Option β} {p : β → Bool} :
|
||||
(filterMap f l).any p = l.any fun a => match f a with | some b => p b | none => false := by
|
||||
induction l with
|
||||
| nil => rfl
|
||||
| cons h t ih =>
|
||||
simp only [filterMap_cons]
|
||||
split <;> simp_all
|
||||
|
||||
@[simp] theorem all_filterMap {l : List α} {f : α → Option β} {p : β → Bool} :
|
||||
(filterMap f l).all p = l.all fun a => match f a with | some b => p b | none => true := by
|
||||
induction l with
|
||||
| nil => rfl
|
||||
| cons h t ih =>
|
||||
simp only [filterMap_cons]
|
||||
split <;> simp_all
|
||||
|
||||
@[simp, grind _=_] theorem any_append {xs ys : List α} : (xs ++ ys).any f = (xs.any f || ys.any f) := by
|
||||
induction xs with
|
||||
| nil => rfl
|
||||
| cons h t ih => simp_all [Bool.or_assoc]
|
||||
|
||||
@[simp, grind _=_] theorem all_append {xs ys : List α} : (xs ++ ys).all f = (xs.all f && ys.all f) := by
|
||||
induction xs with
|
||||
| nil => rfl
|
||||
| cons h t ih => simp_all [Bool.and_assoc]
|
||||
|
||||
@[simp, grind] theorem any_flatten {l : List (List α)} : l.flatten.any f = l.any (any · f) := by
|
||||
induction l <;> simp_all
|
||||
|
||||
@[deprecated any_flatten (since := "2024-10-14")] abbrev any_join := @any_flatten
|
||||
|
||||
@[simp, grind] theorem all_flatten {l : List (List α)} : l.flatten.all f = l.all (all · f) := by
|
||||
induction l <;> simp_all
|
||||
|
||||
@[deprecated all_flatten (since := "2024-10-14")] abbrev all_join := @all_flatten
|
||||
|
||||
@[simp, grind] theorem any_flatMap {l : List α} {f : α → List β} :
|
||||
(l.flatMap f).any p = l.any fun a => (f a).any p := by
|
||||
induction l <;> simp_all
|
||||
|
||||
@[simp, grind] theorem all_flatMap {l : List α} {f : α → List β} :
|
||||
(l.flatMap f).all p = l.all fun a => (f a).all p := by
|
||||
induction l <;> simp_all
|
||||
|
||||
@[simp, grind] theorem any_reverse {l : List α} : l.reverse.any f = l.any f := by
|
||||
induction l <;> simp_all [Bool.or_comm]
|
||||
|
||||
@[simp, grind] theorem all_reverse {l : List α} : l.reverse.all f = l.all f := by
|
||||
induction l <;> simp_all [Bool.and_comm]
|
||||
|
||||
@[simp] theorem any_replicate {n : Nat} {a : α} :
|
||||
(replicate n a).any f = if n = 0 then false else f a := by
|
||||
cases n <;> simp [replicate_succ]
|
||||
|
||||
@[simp] theorem all_replicate {n : Nat} {a : α} :
|
||||
(replicate n a).all f = if n = 0 then true else f a := by
|
||||
cases n <;> simp +contextual [replicate_succ]
|
||||
|
||||
theorem any_congr {l₁ l₂ : List α} (w : l₁ = l₂) {p q : α → Bool} (h : ∀ a, p a = q a) :
|
||||
l₁.any p = l₂.any q := by
|
||||
subst w
|
||||
induction l₁ with
|
||||
| nil => rfl
|
||||
| cons a l ih => simp [ih, h]
|
||||
|
||||
theorem all_congr {l₁ l₂ : List α} (w : l₁ = l₂) {p q : α → Bool} (h : ∀ a, p a = q a) :
|
||||
l₁.all p = l₂.all q := by
|
||||
subst w
|
||||
induction l₁ with
|
||||
| nil => rfl
|
||||
| cons a l ih => simp [ih, h]
|
||||
|
||||
theorem contains_congr [BEq α] [PartialEquivBEq α] {l : List α} {x y : α} (h : x == y) :
|
||||
l.contains x = l.contains y := by
|
||||
simp only [contains_eq_any_beq]
|
||||
exact any_congr rfl fun a => BEq.congr_left h
|
||||
|
||||
/-! ## Manipulating elements -/
|
||||
|
||||
/-! ### replace -/
|
||||
|
|
@ -3253,6 +3438,15 @@ variable [BEq α]
|
|||
|
||||
@[simp, grind] theorem insert_nil (a : α) : [].insert a = [a] := rfl
|
||||
|
||||
@[simp, grind] theorem contains_insert [PartialEquivBEq α] {l : List α} {a : α} {x : α} :
|
||||
(l.insert a).contains x = (x == a || l.contains x) := by
|
||||
simp only [List.insert]
|
||||
split <;> rename_i h
|
||||
· simp only [Bool.eq_or_self]
|
||||
intro h'
|
||||
simpa [contains_congr h']
|
||||
· simp
|
||||
|
||||
variable [LawfulBEq α]
|
||||
|
||||
@[simp] theorem insert_of_mem {l : List α} (h : a ∈ l) : l.insert a = l := by
|
||||
|
|
@ -3369,128 +3563,16 @@ theorem insert_append_of_not_mem_left {l₁ l₂ : List α} (h : ¬ a ∈ l₂)
|
|||
rw [insert_of_not_mem]
|
||||
simp_all
|
||||
|
||||
end insert
|
||||
|
||||
/-! ## Logic -/
|
||||
|
||||
/-! ### any / all -/
|
||||
|
||||
theorem not_any_eq_all_not {l : List α} {p : α → Bool} : (!l.any p) = l.all fun a => !p a := by
|
||||
induction l with simp | cons _ _ ih => rw [ih]
|
||||
|
||||
theorem not_all_eq_any_not {l : List α} {p : α → Bool} : (!l.all p) = l.any fun a => !p a := by
|
||||
induction l with simp | cons _ _ ih => rw [ih]
|
||||
|
||||
theorem and_any_distrib_left {l : List α} {p : α → Bool} {q : Bool} :
|
||||
(q && l.any p) = l.any fun a => q && p a := by
|
||||
induction l with simp | cons _ _ ih => rw [Bool.and_or_distrib_left, ih]
|
||||
|
||||
theorem and_any_distrib_right {l : List α} {p : α → Bool} {q : Bool} :
|
||||
(l.any p && q) = l.any fun a => p a && q := by
|
||||
induction l with simp | cons _ _ ih => rw [Bool.and_or_distrib_right, ih]
|
||||
|
||||
theorem or_all_distrib_left {l : List α} {p : α → Bool} {q : Bool} :
|
||||
(q || l.all p) = l.all fun a => q || p a := by
|
||||
induction l with simp | cons _ _ ih => rw [Bool.or_and_distrib_left, ih]
|
||||
|
||||
theorem or_all_distrib_right {l : List α} {p : α → Bool} {q : Bool} :
|
||||
(l.all p || q) = l.all fun a => p a || q := by
|
||||
induction l with simp | cons _ _ ih => rw [Bool.or_and_distrib_right, ih]
|
||||
|
||||
theorem any_eq_not_all_not {l : List α} {p : α → Bool} : l.any p = !l.all (!p .) := by
|
||||
simp only [not_all_eq_any_not, Bool.not_not]
|
||||
|
||||
theorem all_eq_not_any_not {l : List α} {p : α → Bool} : l.all p = !l.any (!p .) := by
|
||||
simp only [not_any_eq_all_not, Bool.not_not]
|
||||
|
||||
@[simp] theorem any_map {l : List α} {p : β → Bool} : (l.map f).any p = l.any (p ∘ f) := by
|
||||
induction l with simp | cons _ _ ih => rw [ih]
|
||||
|
||||
@[simp] theorem all_map {l : List α} {p : β → Bool} : (l.map f).all p = l.all (p ∘ f) := by
|
||||
induction l with simp | cons _ _ ih => rw [ih]
|
||||
|
||||
@[simp] theorem any_filter {l : List α} {p q : α → Bool} :
|
||||
(filter p l).any q = l.any fun a => p a && q a := by
|
||||
induction l with
|
||||
| nil => rfl
|
||||
| cons h t ih =>
|
||||
simp only [filter_cons]
|
||||
split <;> simp_all
|
||||
|
||||
@[simp] theorem all_filter {l : List α} {p q : α → Bool} :
|
||||
(filter p l).all q = l.all fun a => !(p a) || q a := by
|
||||
induction l with
|
||||
| nil => rfl
|
||||
| cons h t ih =>
|
||||
simp only [filter_cons]
|
||||
split <;> simp_all
|
||||
|
||||
@[simp] theorem any_filterMap {l : List α} {f : α → Option β} {p : β → Bool} :
|
||||
(filterMap f l).any p = l.any fun a => match f a with | some b => p b | none => false := by
|
||||
induction l with
|
||||
| nil => rfl
|
||||
| cons h t ih =>
|
||||
simp only [filterMap_cons]
|
||||
split <;> simp_all
|
||||
|
||||
@[simp] theorem all_filterMap {l : List α} {f : α → Option β} {p : β → Bool} :
|
||||
(filterMap f l).all p = l.all fun a => match f a with | some b => p b | none => true := by
|
||||
induction l with
|
||||
| nil => rfl
|
||||
| cons h t ih =>
|
||||
simp only [filterMap_cons]
|
||||
split <;> simp_all
|
||||
|
||||
@[simp, grind _=_] theorem any_append {xs ys : List α} : (xs ++ ys).any f = (xs.any f || ys.any f) := by
|
||||
induction xs with
|
||||
| nil => rfl
|
||||
| cons h t ih => simp_all [Bool.or_assoc]
|
||||
|
||||
@[simp, grind _=_] theorem all_append {xs ys : List α} : (xs ++ ys).all f = (xs.all f && ys.all f) := by
|
||||
induction xs with
|
||||
| nil => rfl
|
||||
| cons h t ih => simp_all [Bool.and_assoc]
|
||||
|
||||
@[simp, grind] theorem any_flatten {l : List (List α)} : l.flatten.any f = l.any (any · f) := by
|
||||
induction l <;> simp_all
|
||||
|
||||
@[deprecated any_flatten (since := "2024-10-14")] abbrev any_join := @any_flatten
|
||||
|
||||
@[simp, grind] theorem all_flatten {l : List (List α)} : l.flatten.all f = l.all (all · f) := by
|
||||
induction l <;> simp_all
|
||||
|
||||
@[deprecated all_flatten (since := "2024-10-14")] abbrev all_join := @all_flatten
|
||||
|
||||
@[simp, grind] theorem any_flatMap {l : List α} {f : α → List β} :
|
||||
(l.flatMap f).any p = l.any fun a => (f a).any p := by
|
||||
induction l <;> simp_all
|
||||
|
||||
@[simp, grind] theorem all_flatMap {l : List α} {f : α → List β} :
|
||||
(l.flatMap f).all p = l.all fun a => (f a).all p := by
|
||||
induction l <;> simp_all
|
||||
|
||||
@[simp, grind] theorem any_reverse {l : List α} : l.reverse.any f = l.any f := by
|
||||
induction l <;> simp_all [Bool.or_comm]
|
||||
|
||||
@[simp, grind] theorem all_reverse {l : List α} : l.reverse.all f = l.all f := by
|
||||
induction l <;> simp_all [Bool.and_comm]
|
||||
|
||||
@[simp] theorem any_replicate {n : Nat} {a : α} :
|
||||
(replicate n a).any f = if n = 0 then false else f a := by
|
||||
cases n <;> simp [replicate_succ]
|
||||
|
||||
@[simp] theorem all_replicate {n : Nat} {a : α} :
|
||||
(replicate n a).all f = if n = 0 then true else f a := by
|
||||
cases n <;> simp +contextual [replicate_succ]
|
||||
|
||||
@[simp] theorem any_insert [BEq α] [LawfulBEq α] {l : List α} {a : α} :
|
||||
@[simp] theorem any_insert {l : List α} {a : α} :
|
||||
(l.insert a).any f = (f a || l.any f) := by
|
||||
simp [any_eq]
|
||||
|
||||
@[simp] theorem all_insert [BEq α] [LawfulBEq α] {l : List α} {a : α} :
|
||||
@[simp] theorem all_insert {l : List α} {a : α} :
|
||||
(l.insert a).all f = (f a && l.all f) := by
|
||||
simp [all_eq]
|
||||
|
||||
end insert
|
||||
|
||||
/-! ### `removeAll` -/
|
||||
|
||||
@[simp] theorem removeAll_nil [BEq α] {xs : List α} : xs.removeAll [] = xs := by
|
||||
|
|
|
|||
|
|
@ -2679,6 +2679,61 @@ theorem contains_iff_mem [BEq α] [LawfulBEq α] {xs : Vector α n} {a : α} :
|
|||
xs.contains a ↔ a ∈ xs := by
|
||||
simp
|
||||
|
||||
@[simp, grind]
|
||||
theorem contains_toList [BEq α] {xs : Vector α n} {x : α} :
|
||||
xs.toList.contains x = xs.contains x := by
|
||||
rcases xs with ⟨xs, rfl⟩
|
||||
simp
|
||||
|
||||
@[simp, grind]
|
||||
theorem contains_toArray [BEq α] {xs : Vector α n} {x : α} :
|
||||
xs.toArray.contains x = xs.contains x := by
|
||||
rcases xs with ⟨xs, rfl⟩
|
||||
simp
|
||||
|
||||
@[simp, grind]
|
||||
theorem contains_map [BEq β] {xs : Vector α n} {x : β} {f : α → β} :
|
||||
(xs.map f).contains x = xs.any (fun a => x == f a) := by
|
||||
rcases xs with ⟨xs⟩
|
||||
simp
|
||||
|
||||
@[simp, grind]
|
||||
theorem contains_filter [BEq α] {xs : Vector α n} {x : α} {p : α → Bool} :
|
||||
(xs.filter p).contains x = xs.any (fun a => x == a && p a) := by
|
||||
rcases xs with ⟨xs, rfl⟩
|
||||
simp
|
||||
|
||||
@[simp, grind]
|
||||
theorem contains_filterMap [BEq β] {xs : Vector α n} {x : β} {f : α → Option β} :
|
||||
(xs.filterMap f).contains x = xs.any (fun a => (f a).any fun b => x == b) := by
|
||||
rcases xs with ⟨xs, rfl⟩
|
||||
simp
|
||||
|
||||
@[simp, grind _=_]
|
||||
theorem contains_append [BEq α] {xs : Vector α n} {ys : Vector α m} {x : α} :
|
||||
(xs ++ ys).contains x = (xs.contains x || ys.contains x) := by
|
||||
rcases xs with ⟨xs, rfl⟩
|
||||
rcases ys with ⟨ys, rfl⟩
|
||||
simp
|
||||
|
||||
@[simp, grind]
|
||||
theorem contains_flatten [BEq α] {xs : Vector (Vector α n) m} {x : α} :
|
||||
(xs.flatten).contains x = xs.any fun xs => xs.contains x := by
|
||||
rcases xs with ⟨xs, rfl⟩
|
||||
simp [Function.comp_def]
|
||||
|
||||
@[simp, grind]
|
||||
theorem contains_reverse [BEq α] {xs : Vector α n} {x : α} :
|
||||
(xs.reverse).contains x = xs.contains x := by
|
||||
rcases xs with ⟨xs, rfl⟩
|
||||
simp
|
||||
|
||||
@[simp, grind]
|
||||
theorem contains_flatMap [BEq β] {xs : Vector α n} {f : α → Vector β m} {x : β} :
|
||||
(xs.flatMap f).contains x = xs.any fun a => (f a).contains x := by
|
||||
rcases xs with ⟨xs, rfl⟩
|
||||
simp
|
||||
|
||||
/-! ### more lemmas about `pop` -/
|
||||
|
||||
@[simp] theorem pop_empty : (#v[] : Vector α 0).pop = #v[] := rfl
|
||||
|
|
@ -2737,93 +2792,6 @@ theorem pop_append {xs : Vector α n} {ys : Vector α m} :
|
|||
@[deprecated pop_replicate (since := "2025-03-18")]
|
||||
abbrev pop_mkVector := @pop_replicate
|
||||
|
||||
/-! ### replace -/
|
||||
|
||||
section replace
|
||||
variable [BEq α]
|
||||
|
||||
@[simp] theorem replace_cast {xs : Vector α n} {a b : α} :
|
||||
(xs.cast h).replace a b = (xs.replace a b).cast (by simp [h]) := by
|
||||
rcases xs with ⟨xs, rfl⟩
|
||||
simp
|
||||
|
||||
@[simp, grind] theorem replace_empty : (#v[] : Vector α 0).replace a b = #v[] := by rfl
|
||||
|
||||
@[grind] theorem replace_singleton {a b c : α} : #v[a].replace b c = #v[if a == b then c else a] := by
|
||||
simp
|
||||
|
||||
-- This hypothesis could probably be dropped from some of the lemmas below,
|
||||
-- by proving them direct from the definition rather than going via `List`.
|
||||
variable [LawfulBEq α]
|
||||
|
||||
@[simp] theorem replace_of_not_mem {xs : Vector α n} (h : ¬ a ∈ xs) : xs.replace a b = xs := by
|
||||
rcases xs with ⟨xs, rfl⟩
|
||||
simp_all
|
||||
|
||||
@[grind] theorem getElem?_replace {xs : Vector α n} {i : Nat} :
|
||||
(xs.replace a b)[i]? = if xs[i]? == some a then if a ∈ xs.take i then some a else some b else xs[i]? := by
|
||||
rcases xs with ⟨xs, rfl⟩
|
||||
simp [Array.getElem?_replace, -beq_iff_eq]
|
||||
|
||||
theorem getElem?_replace_of_ne {xs : Vector α n} {i : Nat} (h : xs[i]? ≠ some a) :
|
||||
(xs.replace a b)[i]? = xs[i]? := by
|
||||
simp_all [getElem?_replace]
|
||||
|
||||
@[grind] theorem getElem_replace {xs : Vector α n} {i : Nat} (h : i < n) :
|
||||
(xs.replace a b)[i] = if xs[i] == a then if a ∈ xs.take i then a else b else xs[i] := by
|
||||
apply Option.some.inj
|
||||
rw [← getElem?_eq_getElem, getElem?_replace]
|
||||
split <;> split <;> simp_all
|
||||
|
||||
theorem getElem_replace_of_ne {xs : Vector α n} {i : Nat} {h : i < n} (h' : xs[i] ≠ a) :
|
||||
(xs.replace a b)[i]'(by simpa) = xs[i]'(h) := by
|
||||
rw [getElem_replace h]
|
||||
simp [h']
|
||||
|
||||
@[grind] theorem replace_append {xs : Vector α n} {ys : Vector α m} :
|
||||
(xs ++ ys).replace a b = if a ∈ xs then xs.replace a b ++ ys else xs ++ ys.replace a b := by
|
||||
rcases xs with ⟨xs, rfl⟩
|
||||
rcases ys with ⟨ys, rfl⟩
|
||||
simp only [mk_append_mk, replace_mk, eq_mk, Array.replace_append]
|
||||
split <;> simp_all
|
||||
|
||||
theorem replace_append_left {xs : Vector α n} {ys : Vector α m} (h : a ∈ xs) :
|
||||
(xs ++ ys).replace a b = xs.replace a b ++ ys := by
|
||||
simp [replace_append, h]
|
||||
|
||||
theorem replace_append_right {xs : Vector α n} {ys : Vector α m} (h : ¬ a ∈ xs) :
|
||||
(xs ++ ys).replace a b = xs ++ ys.replace a b := by
|
||||
simp [replace_append, h]
|
||||
|
||||
@[grind] theorem replace_push {xs : Vector α n} {a b c : α} :
|
||||
(xs.push a).replace b c = if b ∈ xs then (xs.replace b c).push a else xs.push (if b == a then c else a) := by
|
||||
rcases xs with ⟨xs, rfl⟩
|
||||
simp only [push_mk, replace_mk, Array.replace_push, mem_mk]
|
||||
split <;> simp
|
||||
|
||||
theorem replace_extract {xs : Vector α n} {i : Nat} :
|
||||
(xs.extract 0 i).replace a b = (xs.replace a b).extract 0 i := by
|
||||
rcases xs with ⟨xs, rfl⟩
|
||||
simp [Array.replace_extract]
|
||||
|
||||
@[simp] theorem replace_replicate_self {a : α} (h : 0 < n) :
|
||||
(replicate n a).replace a b = (#v[b] ++ replicate (n - 1) a).cast (by omega) := by
|
||||
match n, h with
|
||||
| n + 1, _ => simp_all [replicate_succ', replace_append]
|
||||
|
||||
@[deprecated replace_replicate_self (since := "2025-03-18")]
|
||||
abbrev replace_mkArray_self := @replace_replicate_self
|
||||
|
||||
@[simp] theorem replace_replicate_ne {a b c : α} (h : !b == a) :
|
||||
(replicate n a).replace b c = replicate n a := by
|
||||
rw [replace_of_not_mem]
|
||||
simp_all
|
||||
|
||||
@[deprecated replace_replicate_ne (since := "2025-03-18")]
|
||||
abbrev replace_mkArray_ne := @replace_replicate_ne
|
||||
|
||||
end replace
|
||||
|
||||
/-! ## Logic -/
|
||||
|
||||
/-! ### any / all -/
|
||||
|
|
@ -2985,6 +2953,93 @@ abbrev any_mkVector := @any_replicate
|
|||
@[deprecated all_replicate (since := "2025-03-18")]
|
||||
abbrev all_mkVector := @all_replicate
|
||||
|
||||
/-! ### replace -/
|
||||
|
||||
section replace
|
||||
variable [BEq α]
|
||||
|
||||
@[simp] theorem replace_cast {xs : Vector α n} {a b : α} :
|
||||
(xs.cast h).replace a b = (xs.replace a b).cast (by simp [h]) := by
|
||||
rcases xs with ⟨xs, rfl⟩
|
||||
simp
|
||||
|
||||
@[simp, grind] theorem replace_empty : (#v[] : Vector α 0).replace a b = #v[] := by rfl
|
||||
|
||||
@[grind] theorem replace_singleton {a b c : α} : #v[a].replace b c = #v[if a == b then c else a] := by
|
||||
simp
|
||||
|
||||
-- This hypothesis could probably be dropped from some of the lemmas below,
|
||||
-- by proving them direct from the definition rather than going via `List`.
|
||||
variable [LawfulBEq α]
|
||||
|
||||
@[simp] theorem replace_of_not_mem {xs : Vector α n} (h : ¬ a ∈ xs) : xs.replace a b = xs := by
|
||||
rcases xs with ⟨xs, rfl⟩
|
||||
simp_all
|
||||
|
||||
@[grind] theorem getElem?_replace {xs : Vector α n} {i : Nat} :
|
||||
(xs.replace a b)[i]? = if xs[i]? == some a then if a ∈ xs.take i then some a else some b else xs[i]? := by
|
||||
rcases xs with ⟨xs, rfl⟩
|
||||
simp [Array.getElem?_replace, -beq_iff_eq]
|
||||
|
||||
theorem getElem?_replace_of_ne {xs : Vector α n} {i : Nat} (h : xs[i]? ≠ some a) :
|
||||
(xs.replace a b)[i]? = xs[i]? := by
|
||||
simp_all [getElem?_replace]
|
||||
|
||||
@[grind] theorem getElem_replace {xs : Vector α n} {i : Nat} (h : i < n) :
|
||||
(xs.replace a b)[i] = if xs[i] == a then if a ∈ xs.take i then a else b else xs[i] := by
|
||||
apply Option.some.inj
|
||||
rw [← getElem?_eq_getElem, getElem?_replace]
|
||||
split <;> split <;> simp_all
|
||||
|
||||
theorem getElem_replace_of_ne {xs : Vector α n} {i : Nat} {h : i < n} (h' : xs[i] ≠ a) :
|
||||
(xs.replace a b)[i]'(by simpa) = xs[i]'(h) := by
|
||||
rw [getElem_replace h]
|
||||
simp [h']
|
||||
|
||||
@[grind] theorem replace_append {xs : Vector α n} {ys : Vector α m} :
|
||||
(xs ++ ys).replace a b = if a ∈ xs then xs.replace a b ++ ys else xs ++ ys.replace a b := by
|
||||
rcases xs with ⟨xs, rfl⟩
|
||||
rcases ys with ⟨ys, rfl⟩
|
||||
simp only [mk_append_mk, replace_mk, eq_mk, Array.replace_append]
|
||||
split <;> simp_all
|
||||
|
||||
theorem replace_append_left {xs : Vector α n} {ys : Vector α m} (h : a ∈ xs) :
|
||||
(xs ++ ys).replace a b = xs.replace a b ++ ys := by
|
||||
simp [replace_append, h]
|
||||
|
||||
theorem replace_append_right {xs : Vector α n} {ys : Vector α m} (h : ¬ a ∈ xs) :
|
||||
(xs ++ ys).replace a b = xs ++ ys.replace a b := by
|
||||
simp [replace_append, h]
|
||||
|
||||
@[grind] theorem replace_push {xs : Vector α n} {a b c : α} :
|
||||
(xs.push a).replace b c = if b ∈ xs then (xs.replace b c).push a else xs.push (if b == a then c else a) := by
|
||||
rcases xs with ⟨xs, rfl⟩
|
||||
simp only [push_mk, replace_mk, Array.replace_push, mem_mk]
|
||||
split <;> simp
|
||||
|
||||
theorem replace_extract {xs : Vector α n} {i : Nat} :
|
||||
(xs.extract 0 i).replace a b = (xs.replace a b).extract 0 i := by
|
||||
rcases xs with ⟨xs, rfl⟩
|
||||
simp [Array.replace_extract]
|
||||
|
||||
@[simp] theorem replace_replicate_self {a : α} (h : 0 < n) :
|
||||
(replicate n a).replace a b = (#v[b] ++ replicate (n - 1) a).cast (by omega) := by
|
||||
match n, h with
|
||||
| n + 1, _ => simp_all [replicate_succ', replace_append]
|
||||
|
||||
@[deprecated replace_replicate_self (since := "2025-03-18")]
|
||||
abbrev replace_mkArray_self := @replace_replicate_self
|
||||
|
||||
@[simp] theorem replace_replicate_ne {a b c : α} (h : !b == a) :
|
||||
(replicate n a).replace b c = replicate n a := by
|
||||
rw [replace_of_not_mem]
|
||||
simp_all
|
||||
|
||||
@[deprecated replace_replicate_ne (since := "2025-03-18")]
|
||||
abbrev replace_mkArray_ne := @replace_replicate_ne
|
||||
|
||||
end replace
|
||||
|
||||
/-! Content below this point has not yet been aligned with `List` and `Array`. -/
|
||||
|
||||
set_option linter.indexVariables false in
|
||||
|
|
|
|||
|
|
@ -1795,7 +1795,7 @@ theorem size_insertMany_list [EquivBEq α] [LawfulHashable α] (h : m.WF)
|
|||
(distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)) :
|
||||
(∀ (a : α), a ∈ m → (l.map Prod.fst).contains a = false) →
|
||||
(insertMany m l).size = m.size + l.length := by
|
||||
simp [← contains_iff_mem]
|
||||
simp only [← contains_iff_mem]
|
||||
simp_to_raw using Raw₀.Const.size_insertMany_list
|
||||
|
||||
theorem size_le_size_insertMany_list [EquivBEq α] [LawfulHashable α] (h : m.WF)
|
||||
|
|
|
|||
|
|
@ -2380,7 +2380,7 @@ theorem get!_insertMany!_list_of_contains_eq_false [TransOrd α] [BEq α] [Lawfu
|
|||
(h' : (l.map Prod.fst).contains k = false) :
|
||||
get! (insertMany! t l).1 k = get! t k := by
|
||||
simpa only [insertMany_eq_insertMany!] using
|
||||
get!_insertMany_list_of_contains_eq_false h (h' := by simpa [insertMany_eq_insertMany!])
|
||||
get!_insertMany_list_of_contains_eq_false h (h' := by simpa [insertMany_eq_insertMany!] using h')
|
||||
|
||||
theorem get!_insertMany_list_of_mem [TransOrd α] [Inhabited β] (h : t.WF)
|
||||
{l : List (α × β)} {k k' : α} {v : β} : (k_beq : compare k k' = .eq) →
|
||||
|
|
|
|||
|
|
@ -1769,7 +1769,7 @@ theorem ofList_cons {k : α} {v : β k} {tl : List ((a : α) × (β a))} :
|
|||
theorem contains_ofList [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
|
||||
{l : List ((a : α) × β a)} {k : α} :
|
||||
(ofList l cmp).contains k = (l.map Sigma.fst).contains k := by
|
||||
simp [ofList, contains, Impl.ofList]
|
||||
simp only [contains, ofList, Impl.ofList]
|
||||
exact Impl.contains_insertMany_empty_list (instOrd := ⟨cmp⟩) (k := k) (l := l)
|
||||
|
||||
@[simp]
|
||||
|
|
|
|||
|
|
@ -1776,7 +1776,7 @@ theorem ofList_cons {k : α} {v : β k} {tl : List ((a : α) × (β a))} :
|
|||
theorem contains_ofList [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
|
||||
{l : List ((a : α) × β a)} {k : α} :
|
||||
(ofList l cmp).contains k = (l.map Sigma.fst).contains k := by
|
||||
simp [ofList, contains, Impl.ofList]
|
||||
simp only [contains, ofList, Impl.ofList]
|
||||
exact Impl.contains_insertMany_empty_list (instOrd := ⟨cmp⟩) (k := k) (l := l)
|
||||
|
||||
@[simp]
|
||||
|
|
|
|||
|
|
@ -3008,7 +3008,7 @@ theorem containsKey_of_containsKey_insertListConst [BEq α] [PartialEquivBEq α]
|
|||
(h₂ : (toInsert.map Prod.fst).contains k = false) : containsKey k l := by
|
||||
unfold insertListConst at h₁
|
||||
apply containsKey_of_containsKey_insertList h₁
|
||||
simpa
|
||||
simpa using h₂
|
||||
|
||||
theorem getKey?_insertListConst_of_contains_eq_false [BEq α] [EquivBEq α]
|
||||
{l : List ((_ : α) × β)} {toInsert : List (α × β)} {k : α}
|
||||
|
|
@ -3016,7 +3016,7 @@ theorem getKey?_insertListConst_of_contains_eq_false [BEq α] [EquivBEq α]
|
|||
getKey? k (insertListConst l toInsert) = getKey? k l := by
|
||||
unfold insertListConst
|
||||
apply getKey?_insertList_of_contains_eq_false
|
||||
simpa
|
||||
simpa using not_contains
|
||||
|
||||
theorem getKey?_insertListConst_of_mem [BEq α] [EquivBEq α]
|
||||
{l : List ((_ : α) × β)} {toInsert : List (α × β)}
|
||||
|
|
@ -3125,7 +3125,7 @@ theorem getValue?_insertListConst_of_contains_eq_false [BEq α] [PartialEquivBEq
|
|||
unfold insertListConst
|
||||
rw [getValue?_eq_getEntry?, getValue?_eq_getEntry?, getEntry?_insertList_of_contains_eq_false]
|
||||
rw [containsKey_eq_contains_map_fst]
|
||||
simpa
|
||||
simpa using not_contains
|
||||
|
||||
theorem getValue?_insertListConst_of_mem [BEq α] [EquivBEq α]
|
||||
{l : List ((_ : α) × β)} {toInsert : List (α × β)}
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue