chore: cleanup of Array GetElem lemmas (#5534)
This commit is contained in:
Kim Morrison
GitHub
parent
56ba39d68a
commit
4f2c4c7bd1
3 changed files with 130 additions and 64 deletions
|
|
@ -73,7 +73,7 @@ theorem foldr_eq_foldr_toList (f : α → β → β) (init : β) (arr : Array α
|
|||
|
||||
@[simp] theorem append_eq_append (arr arr' : Array α) : arr.append arr' = arr ++ arr' := rfl
|
||||
|
||||
@[simp] theorem append_toList (arr arr' : Array α) :
|
||||
@[simp] theorem toList_append (arr arr' : Array α) :
|
||||
(arr ++ arr').toList = arr.toList ++ arr'.toList := by
|
||||
rw [← append_eq_append]; unfold Array.append
|
||||
rw [foldl_eq_foldl_toList]
|
||||
|
|
@ -111,8 +111,8 @@ abbrev toList_eq := @toListImpl_eq
|
|||
@[deprecated pop_toList (since := "2024-09-09")]
|
||||
abbrev pop_data := @pop_toList
|
||||
|
||||
@[deprecated append_toList (since := "2024-09-09")]
|
||||
abbrev append_data := @append_toList
|
||||
@[deprecated toList_append (since := "2024-09-09")]
|
||||
abbrev append_data := @toList_append
|
||||
|
||||
@[deprecated appendList_toList (since := "2024-09-09")]
|
||||
abbrev appendList_data := @appendList_toList
|
||||
|
|
|
|||
|
|
@ -91,6 +91,8 @@ abbrev toArray_data := @toArray_toList
|
|||
@[simp] theorem getElem_toArray {a : List α} {i : Nat} (h : i < a.toArray.size) :
|
||||
a.toArray[i] = a[i]'(by simpa using h) := rfl
|
||||
|
||||
@[simp] theorem getElem?_toArray {a : List α} {i : Nat} : a.toArray[i]? = a[i]? := rfl
|
||||
|
||||
@[deprecated "Use the reverse direction of `List.push_toArray`." (since := "2024-09-27")]
|
||||
theorem toArray_concat {as : List α} {x : α} :
|
||||
(as ++ [x]).toArray = as.toArray.push x := by
|
||||
|
|
@ -123,6 +125,11 @@ theorem toArray_concat {as : List α} {x : α} :
|
|||
l.toArray.foldl f init = l.foldl f init := by
|
||||
rw [foldl_eq_foldl_toList]
|
||||
|
||||
@[simp] theorem append_toArray (l₁ l₂ : List α) :
|
||||
l₁.toArray ++ l₂.toArray = (l₁ ++ l₂).toArray := by
|
||||
apply ext'
|
||||
simp
|
||||
|
||||
end List
|
||||
|
||||
namespace Array
|
||||
|
|
@ -450,6 +457,10 @@ abbrev get?_eq_data_get? := @get?_eq_toList_get?
|
|||
theorem get!_eq_get? [Inhabited α] (a : Array α) : a.get! n = (a.get? n).getD default := by
|
||||
simp [get!_eq_getD]
|
||||
|
||||
theorem getElem?_eq_some_iff {as : Array α} : as[n]? = some a ↔ ∃ h : n < as.size, as[n] = a := by
|
||||
cases as
|
||||
simp [List.getElem?_eq_some_iff]
|
||||
|
||||
@[simp] theorem back_eq_back? [Inhabited α] (a : Array α) : a.back = a.back?.getD default := by
|
||||
simp [back, back?]
|
||||
|
||||
|
|
@ -725,13 +736,17 @@ theorem foldr_induction
|
|||
simp only [mem_def, toList_map, List.mem_map]
|
||||
|
||||
theorem mapM_eq_mapM_toList [Monad m] [LawfulMonad m] (f : α → m β) (arr : Array α) :
|
||||
arr.mapM f = return mk (← arr.toList.mapM f) := by
|
||||
arr.mapM f = List.toArray <$> (arr.toList.mapM f) := by
|
||||
rw [mapM_eq_foldlM, foldlM_eq_foldlM_toList, ← List.foldrM_reverse]
|
||||
conv => rhs; rw [← List.reverse_reverse arr.toList]
|
||||
induction arr.toList.reverse with
|
||||
| nil => simp
|
||||
| cons a l ih => simp [ih]
|
||||
|
||||
@[simp] theorem toList_mapM [Monad m] [LawfulMonad m] (f : α → m β) (arr : Array α) :
|
||||
toList <$> arr.mapM f = arr.toList.mapM f := by
|
||||
simp [mapM_eq_mapM_toList]
|
||||
|
||||
@[deprecated mapM_eq_mapM_toList (since := "2024-09-09")]
|
||||
abbrev mapM_eq_mapM_data := @mapM_eq_mapM_toList
|
||||
|
||||
|
|
@ -788,16 +803,20 @@ theorem map_spec (as : Array α) (f : α → β) (p : Fin as.size → β → Pro
|
|||
simpa using map_induction as f (fun _ => True) trivial p (by simp_all)
|
||||
|
||||
@[simp] theorem getElem_map (f : α → β) (as : Array α) (i : Nat) (h) :
|
||||
((as.map f)[i]) = f (as[i]'(size_map .. ▸ h)) := by
|
||||
(as.map f)[i] = f (as[i]'(size_map .. ▸ h)) := by
|
||||
have := map_spec as f (fun i b => b = f (as[i]))
|
||||
simp only [implies_true, true_implies] at this
|
||||
obtain ⟨eq, w⟩ := this
|
||||
apply w
|
||||
simp_all
|
||||
|
||||
@[simp] theorem getElem?_map (f : α → β) (as : Array α) (i : Nat) :
|
||||
(as.map f)[i]? = as[i]?.map f := by
|
||||
simp [getElem?_def]
|
||||
|
||||
/-! ### mapIdx -/
|
||||
|
||||
-- This could also be prove from `SatisfiesM_mapIdxM`.
|
||||
-- This could also be proved from `SatisfiesM_mapIdxM` in Batteries.
|
||||
theorem mapIdx_induction (as : Array α) (f : Fin as.size → α → β)
|
||||
(motive : Nat → Prop) (h0 : motive 0)
|
||||
(p : Fin as.size → β → Prop)
|
||||
|
|
@ -837,10 +856,15 @@ theorem mapIdx_spec (as : Array α) (f : Fin as.size → α → β)
|
|||
|
||||
@[simp] theorem getElem_mapIdx (a : Array α) (f : Fin a.size → α → β) (i : Nat)
|
||||
(h : i < (mapIdx a f).size) :
|
||||
haveI : i < a.size := by simp_all
|
||||
(a.mapIdx f)[i] = f ⟨i, this⟩ a[i] :=
|
||||
(a.mapIdx f)[i] = f ⟨i, by simp_all⟩ (a[i]'(by simp_all)) :=
|
||||
(mapIdx_spec _ _ (fun i b => b = f i a[i]) fun _ => rfl).2 i _
|
||||
|
||||
@[simp] theorem getElem?_mapIdx (a : Array α) (f : Fin a.size → α → β) (i : Nat) :
|
||||
(a.mapIdx f)[i]? =
|
||||
a[i]?.pbind fun b h => f ⟨i, (getElem?_eq_some_iff.1 h).1⟩ b := by
|
||||
simp only [getElem?_def, size_mapIdx, getElem_mapIdx]
|
||||
split <;> simp_all
|
||||
|
||||
/-! ### modify -/
|
||||
|
||||
@[simp] theorem size_modify (a : Array α) (i : Nat) (f : α → α) : (a.modify i f).size = a.size := by
|
||||
|
|
@ -932,34 +956,45 @@ abbrev empty_data := @toList_empty
|
|||
theorem push_eq_append_singleton (as : Array α) (x) : as.push x = as ++ #[x] := rfl
|
||||
|
||||
@[simp] theorem mem_append {a : α} {s t : Array α} : a ∈ s ++ t ↔ a ∈ s ∨ a ∈ t := by
|
||||
simp only [mem_def, append_toList, List.mem_append]
|
||||
simp only [mem_def, toList_append, List.mem_append]
|
||||
|
||||
theorem size_append (as bs : Array α) : (as ++ bs).size = as.size + bs.size := by
|
||||
simp only [size, append_toList, List.length_append]
|
||||
@[simp] theorem size_append (as bs : Array α) : (as ++ bs).size = as.size + bs.size := by
|
||||
simp only [size, toList_append, List.length_append]
|
||||
|
||||
theorem get_append_left {as bs : Array α} {h : i < (as ++ bs).size} (hlt : i < as.size) :
|
||||
theorem getElem_append {as bs : Array α} (h : i < (as ++ bs).size) :
|
||||
(as ++ bs)[i] = if h' : i < as.size then as[i] else bs[i - as.size]'(by simp at h; omega) := by
|
||||
cases as; cases bs
|
||||
simp [List.getElem_append]
|
||||
|
||||
theorem getElem_append_left {as bs : Array α} {h : i < (as ++ bs).size} (hlt : i < as.size) :
|
||||
(as ++ bs)[i] = as[i] := by
|
||||
simp only [getElem_eq_getElem_toList]
|
||||
have h' : i < (as.toList ++ bs.toList).length := by rwa [← length_toList, append_toList] at h
|
||||
have h' : i < (as.toList ++ bs.toList).length := by rwa [← length_toList, toList_append] at h
|
||||
conv => rhs; rw [← List.getElem_append_left (bs := bs.toList) (h' := h')]
|
||||
apply List.get_of_eq; rw [append_toList]
|
||||
apply List.get_of_eq; rw [toList_append]
|
||||
|
||||
theorem get_append_right {as bs : Array α} {h : i < (as ++ bs).size} (hle : as.size ≤ i)
|
||||
@[deprecated getElem_append_left (since := "2024-09-30")]
|
||||
abbrev get_append_left := @getElem_append_left
|
||||
|
||||
theorem getElem_append_right {as bs : Array α} {h : i < (as ++ bs).size} (hle : as.size ≤ i)
|
||||
(hlt : i - as.size < bs.size := Nat.sub_lt_left_of_lt_add hle (size_append .. ▸ h)) :
|
||||
(as ++ bs)[i] = bs[i - as.size] := by
|
||||
simp only [getElem_eq_getElem_toList]
|
||||
have h' : i < (as.toList ++ bs.toList).length := by rwa [← length_toList, append_toList] at h
|
||||
have h' : i < (as.toList ++ bs.toList).length := by rwa [← length_toList, toList_append] at h
|
||||
conv => rhs; rw [← List.getElem_append_right (h₁ := hle) (h₂ := h')]
|
||||
apply List.get_of_eq; rw [append_toList]
|
||||
apply List.get_of_eq; rw [toList_append]
|
||||
|
||||
@[deprecated getElem_append_right (since := "2024-09-30")]
|
||||
abbrev get_append_right := @getElem_append_right
|
||||
|
||||
@[simp] theorem append_nil (as : Array α) : as ++ #[] = as := by
|
||||
apply ext'; simp only [append_toList, toList_empty, List.append_nil]
|
||||
apply ext'; simp only [toList_append, toList_empty, List.append_nil]
|
||||
|
||||
@[simp] theorem nil_append (as : Array α) : #[] ++ as = as := by
|
||||
apply ext'; simp only [append_toList, toList_empty, List.nil_append]
|
||||
apply ext'; simp only [toList_append, toList_empty, List.nil_append]
|
||||
|
||||
theorem append_assoc (as bs cs : Array α) : as ++ bs ++ cs = as ++ (bs ++ cs) := by
|
||||
apply ext'; simp only [append_toList, List.append_assoc]
|
||||
apply ext'; simp only [toList_append, List.append_assoc]
|
||||
|
||||
/-! ### extract -/
|
||||
|
||||
|
|
@ -1009,20 +1044,20 @@ theorem size_extract_loop (as bs : Array α) (size start : Nat) :
|
|||
simp [extract]; rw [size_extract_loop, size_empty, Nat.zero_add, Nat.sub_min_sub_right,
|
||||
Nat.min_assoc, Nat.min_self]
|
||||
|
||||
theorem get_extract_loop_lt_aux (as bs : Array α) (size start : Nat) (hlt : i < bs.size) :
|
||||
theorem getElem_extract_loop_lt_aux (as bs : Array α) (size start : Nat) (hlt : i < bs.size) :
|
||||
i < (extract.loop as size start bs).size := by
|
||||
rw [size_extract_loop]
|
||||
apply Nat.lt_of_lt_of_le hlt
|
||||
exact Nat.le_add_right ..
|
||||
|
||||
theorem get_extract_loop_lt (as bs : Array α) (size start : Nat) (hlt : i < bs.size)
|
||||
(h := get_extract_loop_lt_aux as bs size start hlt) :
|
||||
theorem getElem_extract_loop_lt (as bs : Array α) (size start : Nat) (hlt : i < bs.size)
|
||||
(h := getElem_extract_loop_lt_aux as bs size start hlt) :
|
||||
(extract.loop as size start bs)[i] = bs[i] := by
|
||||
apply Eq.trans _ (get_append_left (bs:=extract.loop as size start #[]) hlt)
|
||||
apply Eq.trans _ (getElem_append_left (bs:=extract.loop as size start #[]) hlt)
|
||||
· rw [size_append]; exact Nat.lt_of_lt_of_le hlt (Nat.le_add_right ..)
|
||||
· congr; rw [extract_loop_eq_aux]
|
||||
|
||||
theorem get_extract_loop_ge_aux (as bs : Array α) (size start : Nat) (hge : i ≥ bs.size)
|
||||
theorem getElem_extract_loop_ge_aux (as bs : Array α) (size start : Nat) (hge : i ≥ bs.size)
|
||||
(h : i < (extract.loop as size start bs).size) : start + i - bs.size < as.size := by
|
||||
have h : i < bs.size + (as.size - start) := by
|
||||
apply Nat.lt_of_lt_of_le h
|
||||
|
|
@ -1033,9 +1068,9 @@ theorem get_extract_loop_ge_aux (as bs : Array α) (size start : Nat) (hge : i
|
|||
apply Nat.add_lt_of_lt_sub'
|
||||
exact Nat.sub_lt_left_of_lt_add hge h
|
||||
|
||||
theorem get_extract_loop_ge (as bs : Array α) (size start : Nat) (hge : i ≥ bs.size)
|
||||
theorem getElem_extract_loop_ge (as bs : Array α) (size start : Nat) (hge : i ≥ bs.size)
|
||||
(h : i < (extract.loop as size start bs).size)
|
||||
(h' := get_extract_loop_ge_aux as bs size start hge h) :
|
||||
(h' := getElem_extract_loop_ge_aux as bs size start hge h) :
|
||||
(extract.loop as size start bs)[i] = as[start + i - bs.size] := by
|
||||
induction size using Nat.recAux generalizing start bs with
|
||||
| zero =>
|
||||
|
|
@ -1057,28 +1092,37 @@ theorem get_extract_loop_ge (as bs : Array α) (size start : Nat) (hge : i ≥ b
|
|||
have h₂ : bs.size < (extract.loop as size (start+1) (bs.push as[start])).size := by
|
||||
rw [size_extract_loop]; apply Nat.lt_of_lt_of_le h₁; exact Nat.le_add_right ..
|
||||
have h : (extract.loop as size (start + 1) (push bs as[start]))[bs.size] = as[start] := by
|
||||
rw [get_extract_loop_lt as (bs.push as[start]) size (start+1) h₁ h₂, get_push_eq]
|
||||
rw [getElem_extract_loop_lt as (bs.push as[start]) size (start+1) h₁ h₂, get_push_eq]
|
||||
rw [h]; congr; rw [Nat.add_sub_cancel]
|
||||
else
|
||||
have hge : bs.size + 1 ≤ i := Nat.lt_of_le_of_ne hge hi
|
||||
rw [ih (bs.push as[start]) (start+1) ((size_push ..).symm ▸ hge)]
|
||||
congr 1; rw [size_push, Nat.add_right_comm, Nat.add_sub_add_right]
|
||||
|
||||
theorem get_extract_aux {as : Array α} {start stop : Nat} (h : i < (as.extract start stop).size) :
|
||||
theorem getElem_extract_aux {as : Array α} {start stop : Nat} (h : i < (as.extract start stop).size) :
|
||||
start + i < as.size := by
|
||||
rw [size_extract] at h; apply Nat.add_lt_of_lt_sub'; apply Nat.lt_of_lt_of_le h
|
||||
apply Nat.sub_le_sub_right; apply Nat.min_le_right
|
||||
|
||||
@[simp] theorem get_extract {as : Array α} {start stop : Nat}
|
||||
@[simp] theorem getElem_extract {as : Array α} {start stop : Nat}
|
||||
(h : i < (as.extract start stop).size) :
|
||||
(as.extract start stop)[i] = as[start + i]'(get_extract_aux h) :=
|
||||
(as.extract start stop)[i] = as[start + i]'(getElem_extract_aux h) :=
|
||||
show (extract.loop as (min stop as.size - start) start #[])[i]
|
||||
= as[start + i]'(get_extract_aux h) by rw [get_extract_loop_ge]; rfl; exact Nat.zero_le _
|
||||
= as[start + i]'(getElem_extract_aux h) by rw [getElem_extract_loop_ge]; rfl; exact Nat.zero_le _
|
||||
|
||||
theorem getElem?_extract {as : Array α} {start stop : Nat} :
|
||||
(as.extract start stop)[i]? = if i < min stop as.size - start then as[start + i]? else none := by
|
||||
simp only [getElem?_def, size_extract, getElem_extract]
|
||||
split
|
||||
· split
|
||||
· rfl
|
||||
· omega
|
||||
· rfl
|
||||
|
||||
@[simp] theorem extract_all (as : Array α) : as.extract 0 as.size = as := by
|
||||
apply ext
|
||||
· rw [size_extract, Nat.min_self, Nat.sub_zero]
|
||||
· intros; rw [get_extract]; congr; rw [Nat.zero_add]
|
||||
· intros; rw [getElem_extract]; congr; rw [Nat.zero_add]
|
||||
|
||||
theorem extract_empty_of_stop_le_start (as : Array α) {start stop : Nat} (h : stop ≤ start) :
|
||||
as.extract start stop = #[] := by
|
||||
|
|
@ -1160,9 +1204,12 @@ theorem any_iff_exists {p : α → Bool} {as : Array α} {start stop} :
|
|||
theorem any_eq_true {p : α → Bool} {as : Array α} :
|
||||
any as p ↔ ∃ i : Fin as.size, p as[i] := by simp [any_iff_exists, Fin.isLt]
|
||||
|
||||
theorem any_def {p : α → Bool} (as : Array α) : as.any p = as.toList.any p := by
|
||||
theorem any_toList {p : α → Bool} (as : Array α) : as.toList.any p = as.any p := by
|
||||
rw [Bool.eq_iff_iff, any_eq_true, List.any_eq_true]; simp only [List.mem_iff_get]
|
||||
exact ⟨fun ⟨i, h⟩ => ⟨_, ⟨i, rfl⟩, h⟩, fun ⟨_, ⟨i, rfl⟩, h⟩ => ⟨i, h⟩⟩
|
||||
exact ⟨fun ⟨_, ⟨i, rfl⟩, h⟩ => ⟨i, h⟩, fun ⟨i, h⟩ => ⟨_, ⟨i, rfl⟩, h⟩⟩
|
||||
|
||||
@[deprecated "Use the reverse direction of `Array.any_toList`" (since := "2024-09-30")]
|
||||
abbrev any_def := @any_toList
|
||||
|
||||
/-! ### all -/
|
||||
|
||||
|
|
@ -1194,22 +1241,25 @@ theorem all_iff_forall {p : α → Bool} {as : Array α} {start stop} :
|
|||
theorem all_eq_true {p : α → Bool} {as : Array α} : all as p ↔ ∀ i : Fin as.size, p as[i] := by
|
||||
simp [all_iff_forall, Fin.isLt]
|
||||
|
||||
theorem all_def {p : α → Bool} (as : Array α) : as.all p = as.toList.all p := by
|
||||
theorem all_toList {p : α → Bool} (as : Array α) : as.toList.all p = as.all p := by
|
||||
rw [Bool.eq_iff_iff, all_eq_true, List.all_eq_true]; simp only [List.mem_iff_getElem]
|
||||
constructor
|
||||
· intro w i
|
||||
exact w as[i] ⟨i, i.2, (getElem_eq_getElem_toList i.2).symm⟩
|
||||
· rintro w x ⟨r, h, rfl⟩
|
||||
rw [← getElem_eq_getElem_toList]
|
||||
exact w ⟨r, h⟩
|
||||
· intro w i
|
||||
exact w as[i] ⟨i, i.2, (getElem_eq_getElem_toList i.2).symm⟩
|
||||
|
||||
@[deprecated "Use the reverse direction of `Array.all_toList`" (since := "2024-09-30")]
|
||||
abbrev all_def := @all_toList
|
||||
|
||||
theorem all_eq_true_iff_forall_mem {l : Array α} : l.all p ↔ ∀ x, x ∈ l → p x := by
|
||||
simp only [all_def, List.all_eq_true, mem_def]
|
||||
simp only [← all_toList, List.all_eq_true, mem_def]
|
||||
|
||||
/-! ### contains -/
|
||||
|
||||
theorem contains_def [DecidableEq α] {a : α} {as : Array α} : as.contains a ↔ a ∈ as := by
|
||||
rw [mem_def, contains, any_def, List.any_eq_true]; simp [and_comm]
|
||||
rw [mem_def, contains, ← any_toList, List.any_eq_true]; simp [and_comm]
|
||||
|
||||
instance [DecidableEq α] (a : α) (as : Array α) : Decidable (a ∈ as) :=
|
||||
decidable_of_iff _ contains_def
|
||||
|
|
@ -1218,12 +1268,12 @@ instance [DecidableEq α] (a : α) (as : Array α) : Decidable (a ∈ as) :=
|
|||
|
||||
open Fin
|
||||
|
||||
@[simp] theorem get_swap_right (a : Array α) {i j : Fin a.size} : (a.swap i j)[j.val] = a[i] :=
|
||||
@[simp] theorem getElem_swap_right (a : Array α) {i j : Fin a.size} : (a.swap i j)[j.val] = a[i] :=
|
||||
by simp only [swap, fin_cast_val, get_eq_getElem, getElem_set_eq, getElem_fin]
|
||||
|
||||
@[simp] theorem get_swap_left (a : Array α) {i j : Fin a.size} : (a.swap i j)[i.val] = a[j] :=
|
||||
@[simp] theorem getElem_swap_left (a : Array α) {i j : Fin a.size} : (a.swap i j)[i.val] = a[j] :=
|
||||
if he : ((Array.size_set _ _ _).symm ▸ j).val = i.val then by
|
||||
simp only [←he, fin_cast_val, get_swap_right, getElem_fin]
|
||||
simp only [←he, fin_cast_val, getElem_swap_right, getElem_fin]
|
||||
else by
|
||||
apply Eq.trans
|
||||
· apply Array.get_set_ne
|
||||
|
|
@ -1231,7 +1281,7 @@ open Fin
|
|||
· assumption
|
||||
· simp [get_set_ne]
|
||||
|
||||
@[simp] theorem get_swap_of_ne (a : Array α) {i j : Fin a.size} (hp : p < a.size)
|
||||
@[simp] theorem getElem_swap_of_ne (a : Array α) {i j : Fin a.size} (hp : p < a.size)
|
||||
(hi : p ≠ i) (hj : p ≠ j) : (a.swap i j)[p]'(a.size_swap .. |>.symm ▸ hp) = a[p] := by
|
||||
apply Eq.trans
|
||||
· have : ((a.size_set i (a.get j)).symm ▸ j).val = j.val := by simp only [fin_cast_val]
|
||||
|
|
@ -1243,22 +1293,22 @@ open Fin
|
|||
· apply Ne.symm
|
||||
· assumption
|
||||
|
||||
theorem get_swap (a : Array α) (i j : Fin a.size) (k : Nat) (hk: k < a.size) :
|
||||
theorem getElem_swap' (a : Array α) (i j : Fin a.size) (k : Nat) (hk : k < a.size) :
|
||||
(a.swap i j)[k]'(by simp_all) = if k = i then a[j] else if k = j then a[i] else a[k] := by
|
||||
split
|
||||
· simp_all only [get_swap_left]
|
||||
· simp_all only [getElem_swap_left]
|
||||
· split <;> simp_all
|
||||
|
||||
theorem get_swap' (a : Array α) (i j : Fin a.size) (k : Nat) (hk' : k < (a.swap i j).size) :
|
||||
theorem getElem_swap (a : Array α) (i j : Fin a.size) (k : Nat) (hk : k < (a.swap i j).size) :
|
||||
(a.swap i j)[k] = if k = i then a[j] else if k = j then a[i] else a[k]'(by simp_all) := by
|
||||
apply get_swap
|
||||
apply getElem_swap'
|
||||
|
||||
@[simp] theorem swap_swap (a : Array α) {i j : Fin a.size} :
|
||||
(a.swap i j).swap ⟨i.1, (a.size_swap ..).symm ▸i.2⟩ ⟨j.1, (a.size_swap ..).symm ▸j.2⟩ = a := by
|
||||
apply ext
|
||||
· simp only [size_swap]
|
||||
· intros
|
||||
simp only [get_swap']
|
||||
simp only [getElem_swap]
|
||||
split
|
||||
· simp_all
|
||||
· split <;> simp_all
|
||||
|
|
@ -1267,11 +1317,35 @@ theorem swap_comm (a : Array α) {i j : Fin a.size} : a.swap i j = a.swap j i :=
|
|||
apply ext
|
||||
· simp only [size_swap]
|
||||
· intros
|
||||
simp only [get_swap']
|
||||
simp only [getElem_swap]
|
||||
split
|
||||
· split <;> simp_all
|
||||
· split <;> simp_all
|
||||
|
||||
@[deprecated getElem_extract_loop_lt_aux (since := "2024-09-30")]
|
||||
abbrev get_extract_loop_lt_aux := @getElem_extract_loop_lt_aux
|
||||
@[deprecated getElem_extract_loop_lt (since := "2024-09-30")]
|
||||
abbrev get_extract_loop_lt := @getElem_extract_loop_lt
|
||||
@[deprecated getElem_extract_loop_ge_aux (since := "2024-09-30")]
|
||||
abbrev get_extract_loop_ge_aux := @getElem_extract_loop_ge_aux
|
||||
@[deprecated getElem_extract_loop_ge (since := "2024-09-30")]
|
||||
abbrev get_extract_loop_ge := @getElem_extract_loop_ge
|
||||
@[deprecated getElem_extract_aux (since := "2024-09-30")]
|
||||
abbrev get_extract_aux := @getElem_extract_aux
|
||||
@[deprecated getElem_extract (since := "2024-09-30")]
|
||||
abbrev get_extract := @getElem_extract
|
||||
|
||||
@[deprecated getElem_swap_right (since := "2024-09-30")]
|
||||
abbrev get_swap_right := @getElem_swap_right
|
||||
@[deprecated getElem_swap_left (since := "2024-09-30")]
|
||||
abbrev get_swap_left := @getElem_swap_left
|
||||
@[deprecated getElem_swap_of_ne (since := "2024-09-30")]
|
||||
abbrev get_swap_of_ne := @getElem_swap_of_ne
|
||||
@[deprecated getElem_swap (since := "2024-09-30")]
|
||||
abbrev get_swap := @getElem_swap
|
||||
@[deprecated getElem_swap' (since := "2024-09-30")]
|
||||
abbrev get_swap' := @getElem_swap'
|
||||
|
||||
end Array
|
||||
|
||||
|
||||
|
|
@ -1288,9 +1362,6 @@ Our goal is to have `simp` "pull `List.toArray` outwards" as much as possible.
|
|||
@[simp] theorem mem_toArray {a : α} {l : List α} : a ∈ l.toArray ↔ a ∈ l := by
|
||||
simp [mem_def]
|
||||
|
||||
@[simp] theorem getElem?_toArray (l : List α) (i : Nat) : l.toArray[i]? = l[i]? := by
|
||||
simp [getElem?_eq_getElem?_toList]
|
||||
|
||||
@[simp] theorem toListRev_toArray (l : List α) : l.toArray.toListRev = l.reverse := by
|
||||
simp
|
||||
|
||||
|
|
@ -1345,14 +1416,14 @@ Our goal is to have `simp` "pull `List.toArray` outwards" as much as possible.
|
|||
rw [← anyM_toList]
|
||||
|
||||
@[simp] theorem any_toArray (p : α → Bool) (l : List α) : l.toArray.any p = l.any p := by
|
||||
rw [Array.any_def]
|
||||
rw [any_toList]
|
||||
|
||||
@[simp] theorem allM_toArray [Monad m] [LawfulMonad m] (p : α → m Bool) (l : List α) :
|
||||
l.toArray.allM p = l.allM p := by
|
||||
rw [← allM_toList]
|
||||
|
||||
@[simp] theorem all_toArray (p : α → Bool) (l : List α) : l.toArray.all p = l.all p := by
|
||||
rw [Array.all_def]
|
||||
rw [all_toList]
|
||||
|
||||
@[simp] theorem swap_toArray (l : List α) (i j : Fin l.toArray.size) :
|
||||
l.toArray.swap i j = ((l.set i l[j]).set j l[i]).toArray := by
|
||||
|
|
@ -1377,11 +1448,6 @@ Our goal is to have `simp` "pull `List.toArray` outwards" as much as possible.
|
|||
apply ext'
|
||||
erw [toList_filterMap] -- `erw` required to unify `l.length` with `l.toArray.size`.
|
||||
|
||||
@[simp] theorem append_toArray (l₁ l₂ : List α) :
|
||||
l₁.toArray ++ l₂.toArray = (l₁ ++ l₂).toArray := by
|
||||
apply ext'
|
||||
simp
|
||||
|
||||
@[simp] theorem toArray_range (n : Nat) : (range n).toArray = Array.range n := by
|
||||
apply ext'
|
||||
simp
|
||||
|
|
|
|||
|
|
@ -104,10 +104,10 @@ def append (lhs : RefVec aig lw) (rhs : RefVec aig rw) : RefVec aig (lw + rw) :=
|
|||
by
|
||||
intro i h
|
||||
by_cases hsplit : i < lrefs.size
|
||||
· rw [Array.get_append_left]
|
||||
· rw [Array.getElem_append_left]
|
||||
apply hl2
|
||||
omega
|
||||
· rw [Array.get_append_right]
|
||||
· rw [Array.getElem_append_right]
|
||||
· apply hr2
|
||||
omega
|
||||
· omega
|
||||
|
|
@ -124,9 +124,9 @@ theorem get_append (lhs : RefVec aig lw) (rhs : RefVec aig rw) (idx : Nat)
|
|||
simp only [get, append]
|
||||
split
|
||||
· simp [Ref.mk.injEq]
|
||||
rw [Array.get_append_left]
|
||||
rw [Array.getElem_append_left]
|
||||
· simp only [Ref.mk.injEq]
|
||||
rw [Array.get_append_right]
|
||||
rw [Array.getElem_append_right]
|
||||
· simp [lhs.hlen]
|
||||
· rw [lhs.hlen]
|
||||
omega
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue