max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: rename Array.data to Array.toList

Browse source
This commit is contained in:
Kim Morrison 2024-09-09 13:37:28 +10:00
parent b1a03a471f
commit e41e305479
32 changed files with 465 additions and 367 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Init/Data/Array/Attach.lean
View file

@ -20,7 +20,7 @@ Unsafe implementation of `attachWith`, taking advantage of the fact that the rep
with the same elements but in the type `{x // P x}`. -/
@[implemented_by attachWithImpl] def attachWith
(xs : Array α) (P : α → Prop) (H : ∀ x ∈ xs, P x) : Array {x // P x} :=
⟨xs.data.attachWith P fun x h => H x (Array.Mem.mk h)⟩
⟨xs.toList.attachWith P fun x h => H x (Array.Mem.mk h)⟩
/-- `O(1)`. "Attach" the proof that the elements of `xs` are in `xs` to produce a new array
with the same elements but in the type `{x // x ∈ xs}`. -/

32
src/Init/Data/Array/Basic.lean
View file

@ -16,10 +16,11 @@ universe u v w
namespace Array
variable {α : Type u}
@[deprecated Array.toList (since := "2024-09-10")] abbrev Array.data := @Array.toList
@[extern "lean_mk_array"]
def mkArray {α : Type u} (n : Nat) (v : α) : Array α := {
data := List.replicate n v
}
def mkArray {α : Type u} (n : Nat) (v : α) : Array α where
toList := List.replicate n v
/--
`ofFn f` with `f : Fin n → α` returns the list whose ith element is `f i`.
@ -134,9 +135,8 @@ def swapAt! (a : Array α) (i : Nat) (v : α) : α × Array α :=
panic! ("index " ++ toString i ++ " out of bounds")
@[extern "lean_array_pop"]
def pop (a : Array α) : Array α := {
data := a.data.dropLast
}
def pop (a : Array α) : Array α where
toList := a.toList.dropLast
def shrink (a : Array α) (n : Nat) : Array α :=
let rec loop
@ -499,10 +499,10 @@ def elem [BEq α] (a : α) (as : Array α) : Bool :=
(true, r)
/-- Convert a `Array α` into an `List α`. This is O(n) in the size of the array. -/
-- This function is exported to C, where it is called by `Array.data`
-- This function is exported to C, where it is called by `Array.toList`
-- (the projection) to implement this functionality.
@[export lean_array_to_list]
def toList (as : Array α) : List α :=
@[export lean_array_to_list_impl]
def toListImpl (as : Array α) : List α :=
as.foldr List.cons []
/-- Prepends an `Array α` onto the front of a list. Equivalent to `as.toList ++ l`. -/
@ -793,30 +793,32 @@ def toListLitAux (a : Array α) (n : Nat) (hsz : a.size = n) : ∀ (i : Nat), i
def toArrayLit (a : Array α) (n : Nat) (hsz : a.size = n) : Array α :=
List.toArray <| toListLitAux a n hsz n (hsz ▸ Nat.le_refl _) []
theorem ext' {as bs : Array α} (h : as.data = bs.data) : as = bs := by
theorem ext' {as bs : Array α} (h : as.toList = bs.toList) : as = bs := by
cases as; cases bs; simp at h; rw [h]
@[simp] theorem toArrayAux_eq (as : List α) (acc : Array α) : (as.toArrayAux acc).data = acc.data ++ as := by
@[simp] theorem toArrayAux_eq (as : List α) (acc : Array α) : (as.toArrayAux acc).toList = acc.toList ++ as := by
induction as generalizing acc <;> simp [*, List.toArrayAux, Array.push, List.append_assoc, List.concat_eq_append]
@[simp] theorem data_toArray (as : List α) : as.toArray.data = as := by
@[simp] theorem toList_toArray (as : List α) : as.toArray.toList = as := by
simp [List.toArray, Array.mkEmpty]
@[deprecated toList_toArray (since := "2024-09-09")] abbrev data_toArray := @toList_toArray
@[simp] theorem size_toArray (as : List α) : as.toArray.size = as.length := by simp [size]
theorem toArrayLit_eq (as : Array α) (n : Nat) (hsz : as.size = n) : as = toArrayLit as n hsz := by
apply ext'
simp [toArrayLit, data_toArray]
simp [toArrayLit, toList_toArray]
have hle : n ≤ as.size := hsz ▸ Nat.le_refl _
have hge : as.size ≤ n := hsz ▸ Nat.le_refl _
have := go n hle
rw [List.drop_eq_nil_of_le hge] at this
rw [this]
where
getLit_eq (as : Array α) (i : Nat) (h₁ : as.size = n) (h₂ : i < n) : as.getLit i h₁ h₂ = getElem as.data i ((id (α := as.data.length = n) h₁) ▸ h₂) :=
getLit_eq (as : Array α) (i : Nat) (h₁ : as.size = n) (h₂ : i < n) : as.getLit i h₁ h₂ = getElem as.toList i ((id (α := as.toList.length = n) h₁) ▸ h₂) :=
rfl
go (i : Nat) (hi : i ≤ as.size) : toListLitAux as n hsz i hi (as.data.drop i) = as.data := by
go (i : Nat) (hi : i ≤ as.size) : toListLitAux as n hsz i hi (as.toList.drop i) = as.toList := by
induction i <;> simp [getLit_eq, List.get_drop_eq_drop, toListLitAux, List.drop, *]
def isPrefixOfAux [BEq α] (as bs : Array α) (hle : as.size ≤ bs.size) (i : Nat) : Bool :=

94
src/Init/Data/Array/Bootstrap.lean
View file

@ -15,76 +15,106 @@ This file contains some theorems about `Array` and `List` needed for `Init.Data.
namespace Array
theorem foldlM_eq_foldlM_data.aux [Monad m]
theorem foldlM_eq_foldlM_toList.aux [Monad m]
(f : β → α → m β) (arr : Array α) (i j) (H : arr.size ≤ i + j) (b) :
foldlM.loop f arr arr.size (Nat.le_refl _) i j b = (arr.data.drop j).foldlM f b := by
foldlM.loop f arr arr.size (Nat.le_refl _) i j b = (arr.toList.drop j).foldlM f b := by
unfold foldlM.loop
split; split
· cases Nat.not_le_of_gt ‹_› (Nat.zero_add _ ▸ H)
· rename_i i; rw [Nat.succ_add] at H
simp [foldlM_eq_foldlM_data.aux f arr i (j+1) H]
simp [foldlM_eq_foldlM_toList.aux f arr i (j+1) H]
rw (config := {occs := .pos [2]}) [← List.get_drop_eq_drop _ _ ‹_›]
rfl
· rw [List.drop_of_length_le (Nat.ge_of_not_lt ‹_›)]; rfl
theorem foldlM_eq_foldlM_data [Monad m]
theorem foldlM_eq_foldlM_toList [Monad m]
(f : β → α → m β) (init : β) (arr : Array α) :
arr.foldlM f init = arr.data.foldlM f init := by
simp [foldlM, foldlM_eq_foldlM_data.aux]
arr.foldlM f init = arr.toList.foldlM f init := by
simp [foldlM, foldlM_eq_foldlM_toList.aux]
theorem foldl_eq_foldl_data (f : β → α → β) (init : β) (arr : Array α) :
arr.foldl f init = arr.data.foldl f init :=
List.foldl_eq_foldlM .. ▸ foldlM_eq_foldlM_data ..
theorem foldl_eq_foldl_toList (f : β → α → β) (init : β) (arr : Array α) :
arr.foldl f init = arr.toList.foldl f init :=
List.foldl_eq_foldlM .. ▸ foldlM_eq_foldlM_toList ..
theorem foldrM_eq_reverse_foldlM_data.aux [Monad m]
theorem foldrM_eq_reverse_foldlM_toList.aux [Monad m]
(f : α → β → m β) (arr : Array α) (init : β) (i h) :
(arr.data.take i).reverse.foldlM (fun x y => f y x) init = foldrM.fold f arr 0 i h init := by
(arr.toList.take i).reverse.foldlM (fun x y => f y x) init = foldrM.fold f arr 0 i h init := by
unfold foldrM.fold
match i with
| 0 => simp [List.foldlM, List.take]
| i+1 => rw [← List.take_concat_get _ _ h]; simp [← (aux f arr · i)]; rfl
theorem foldrM_eq_reverse_foldlM_data [Monad m] (f : α → β → m β) (init : β) (arr : Array α) :
arr.foldrM f init = arr.data.reverse.foldlM (fun x y => f y x) init := by
theorem foldrM_eq_reverse_foldlM_toList [Monad m] (f : α → β → m β) (init : β) (arr : Array α) :
arr.foldrM f init = arr.toList.reverse.foldlM (fun x y => f y x) init := by
have : arr = #[] ∨ 0 < arr.size :=
match arr with | ⟨[]⟩ => .inl rfl | ⟨a::l⟩ => .inr (Nat.zero_lt_succ _)
match arr, this with | _, .inl rfl => rfl | arr, .inr h => ?_
simp [foldrM, h, ← foldrM_eq_reverse_foldlM_data.aux, List.take_length]
simp [foldrM, h, ← foldrM_eq_reverse_foldlM_toList.aux, List.take_length]
theorem foldrM_eq_foldrM_data [Monad m]
theorem foldrM_eq_foldrM_toList [Monad m]
(f : α → β → m β) (init : β) (arr : Array α) :
arr.foldrM f init = arr.data.foldrM f init := by
rw [foldrM_eq_reverse_foldlM_data, List.foldlM_reverse]
arr.foldrM f init = arr.toList.foldrM f init := by
rw [foldrM_eq_reverse_foldlM_toList, List.foldlM_reverse]
theorem foldr_eq_foldr_data (f : α → β → β) (init : β) (arr : Array α) :
arr.foldr f init = arr.data.foldr f init :=
List.foldr_eq_foldrM .. ▸ foldrM_eq_foldrM_data ..
theorem foldr_eq_foldr_toList (f : α → β → β) (init : β) (arr : Array α) :
arr.foldr f init = arr.toList.foldr f init :=
List.foldr_eq_foldrM .. ▸ foldrM_eq_foldrM_toList ..
@[simp] theorem push_data (arr : Array α) (a : α) : (arr.push a).data = arr.data ++ [a] := by
@[simp] theorem push_toList (arr : Array α) (a : α) : (arr.push a).toList = arr.toList ++ [a] := by
simp [push, List.concat_eq_append]
@[simp] theorem toListAppend_eq (arr : Array α) (l) : arr.toListAppend l = arr.data ++ l := by
simp [toListAppend, foldr_eq_foldr_data]
@[simp] theorem toListAppend_eq (arr : Array α) (l) : arr.toListAppend l = arr.toList ++ l := by
simp [toListAppend, foldr_eq_foldr_toList]
@[simp] theorem toList_eq (arr : Array α) : arr.toList = arr.data := by
simp [toList, foldr_eq_foldr_data]
@[simp] theorem toListImpl_eq (arr : Array α) : arr.toListImpl = arr.toList := by
simp [toListImpl, foldr_eq_foldr_toList]
@[simp] theorem pop_data (arr : Array α) : arr.pop.data = arr.data.dropLast := rfl
@[simp] theorem pop_toList (arr : Array α) : arr.pop.toList = arr.toList.dropLast := rfl
@[simp] theorem append_eq_append (arr arr' : Array α) : arr.append arr' = arr ++ arr' := rfl
@[simp] theorem append_data (arr arr' : Array α) :
(arr ++ arr').data = arr.data ++ arr'.data := by
@[simp] theorem append_toList (arr arr' : Array α) :
(arr ++ arr').toList = arr.toList ++ arr'.toList := by
rw [← append_eq_append]; unfold Array.append
rw [foldl_eq_foldl_data]
induction arr'.data generalizing arr <;> simp [*]
rw [foldl_eq_foldl_toList]
induction arr'.toList generalizing arr <;> simp [*]
@[simp] theorem appendList_eq_append
(arr : Array α) (l : List α) : arr.appendList l = arr ++ l := rfl
@[simp] theorem appendList_data (arr : Array α) (l : List α) :
(arr ++ l).data = arr.data ++ l := by
@[simp] theorem appendList_toList (arr : Array α) (l : List α) :
(arr ++ l).toList = arr.toList ++ l := by
rw [← appendList_eq_append]; unfold Array.appendList
induction l generalizing arr <;> simp [*]
@[deprecated foldlM_eq_foldlM_toList (since := "2024-09-09")]
abbrev foldlM_eq_foldlM_data := @foldlM_eq_foldlM_toList
@[deprecated foldl_eq_foldl_toList (since := "2024-09-09")]
abbrev foldl_eq_foldl_data := @foldl_eq_foldl_toList
@[deprecated foldrM_eq_reverse_foldlM_toList (since := "2024-09-09")]
abbrev foldrM_eq_reverse_foldlM_data := @foldrM_eq_reverse_foldlM_toList
@[deprecated foldrM_eq_foldrM_toList (since := "2024-09-09")]
abbrev foldrM_eq_foldrM_data := @foldrM_eq_foldrM_toList
@[deprecated foldr_eq_foldr_toList (since := "2024-09-09")]
abbrev foldr_eq_foldr_data := @foldr_eq_foldr_toList
@[deprecated push_toList (since := "2024-09-09")]
abbrev push_data := @push_toList
@[deprecated toListImpl_eq (since := "2024-09-09")]
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 appendList_toList (since := "2024-09-09")]
abbrev appendList_data := @appendList_toList
end Array

251
src/Init/Data/Array/Lemmas.lean
View file

@ -23,25 +23,34 @@ attribute [simp] data_toArray uset
@[simp] theorem singleton_def (v : α) : singleton v = #[v] := rfl
@[simp] theorem toArray_data : (a : Array α) → a.data.toArray = a
| ⟨l⟩ => ext' (data_toArray l)
@[simp] theorem toArray_toList : (a : Array α) → a.toList.toArray = a
| ⟨l⟩ => ext' (toList_toArray l)
@[simp] theorem data_length {l : Array α} : l.data.length = l.size := rfl
@[deprecated toArray_toList (since := "2024-09-09")]
abbrev toArray_data := @toArray_toList
@[simp] theorem toList_length {l : Array α} : l.toList.length = l.size := rfl
@[deprecated toList_length (since := "2024-09-09")]
abbrev data_length := @toList_length
@[simp] theorem mkEmpty_eq (α n) : @mkEmpty α n = #[] := rfl
@[simp] theorem size_mk (as : List α) : (Array.mk as).size = as.length := by simp [size]
theorem getElem_eq_data_getElem (a : Array α) (h : i < a.size) : a[i] = a.data[i] := by
theorem getElem_eq_toList_getElem (a : Array α) (h : i < a.size) : a[i] = a.toList[i] := by
by_cases i < a.size <;> (try simp [*]) <;> rfl
@[deprecated getElem_eq_data_getElem (since := "2024-06-12")]
theorem getElem_eq_data_get (a : Array α) (h : i < a.size) : a[i] = a.data.get ⟨i, h⟩ := by
simp [getElem_eq_data_getElem]
@[deprecated getElem_eq_toList_getElem (since := "2024-09-09")]
abbrev getElem_eq_data_getElem := @getElem_eq_toList_getElem
@[deprecated getElem_eq_toList_getElem (since := "2024-06-12")]
theorem getElem_eq_toList_get (a : Array α) (h : i < a.size) : a[i] = a.toList.get ⟨i, h⟩ := by
simp [getElem_eq_toList_getElem]
theorem foldrM_push [Monad m] (f : α → β → m β) (init : β) (arr : Array α) (a : α) :
(arr.push a).foldrM f init = f a init >>= arr.foldrM f := by
simp [foldrM_eq_reverse_foldlM_data, -size_push]
simp [foldrM_eq_reverse_foldlM_toList, -size_push]
@[simp] theorem foldrM_push' [Monad m] (f : α → β → m β) (init : β) (arr : Array α) (a : α) :
(arr.push a).foldrM f init (start := arr.size + 1) = f a init >>= arr.foldrM f := by
@ -56,17 +65,17 @@ theorem foldr_push (f : α → β → β) (init : β) (arr : Array α) (a : α)
/-- A more efficient version of `arr.toList.reverse`. -/
@[inline] def toListRev (arr : Array α) : List α := arr.foldl (fun l t => t :: l) []
@[simp] theorem toListRev_eq (arr : Array α) : arr.toListRev = arr.data.reverse := by
rw [toListRev, foldl_eq_foldl_data, ← List.foldr_reverse, List.foldr_cons_nil]
@[simp] theorem toListRev_eq (arr : Array α) : arr.toListRev = arr.toList.reverse := by
rw [toListRev, foldl_eq_foldl_toList, ← List.foldr_reverse, List.foldr_cons_nil]
theorem get_push_lt (a : Array α) (x : α) (i : Nat) (h : i < a.size) :
have : i < (a.push x).size := by simp [*, Nat.lt_succ_of_le, Nat.le_of_lt]
(a.push x)[i] = a[i] := by
simp only [push, getElem_eq_data_getElem, List.concat_eq_append, List.getElem_append_left, h]
simp only [push, getElem_eq_toList_getElem, List.concat_eq_append, List.getElem_append_left, h]
@[simp] theorem get_push_eq (a : Array α) (x : α) : (a.push x)[a.size] = x := by
simp only [push, getElem_eq_data_getElem, List.concat_eq_append]
rw [List.getElem_append_right] <;> simp [getElem_eq_data_getElem, Nat.zero_lt_one]
simp only [push, getElem_eq_toList_getElem, List.concat_eq_append]
rw [List.getElem_append_right] <;> simp [getElem_eq_toList_getElem, Nat.zero_lt_one]
theorem get_push (a : Array α) (x : α) (i : Nat) (h : i < (a.push x).size) :
(a.push x)[i] = if h : i < a.size then a[i] else x := by
@ -77,27 +86,31 @@ theorem get_push (a : Array α) (x : α) (i : Nat) (h : i < (a.push x).size) :
theorem mapM_eq_foldlM [Monad m] [LawfulMonad m] (f : α → m β) (arr : Array α) :
arr.mapM f = arr.foldlM (fun bs a => bs.push <$> f a) #[] := by
rw [mapM, aux, foldlM_eq_foldlM_data]; rfl
rw [mapM, aux, foldlM_eq_foldlM_toList]; rfl
where
aux (i r) :
mapM.map f arr i r = (arr.data.drop i).foldlM (fun bs a => bs.push <$> f a) r := by
mapM.map f arr i r = (arr.toList.drop i).foldlM (fun bs a => bs.push <$> f a) r := by
unfold mapM.map; split
· rw [← List.get_drop_eq_drop _ i ‹_›]
simp only [aux (i + 1), map_eq_pure_bind, data_length, List.foldlM_cons, bind_assoc, pure_bind]
simp only [aux (i + 1), map_eq_pure_bind, toList_length, List.foldlM_cons, bind_assoc,
pure_bind]
rfl
· rw [List.drop_of_length_le (Nat.ge_of_not_lt ‹_›)]; rfl
termination_by arr.size - i
decreasing_by decreasing_trivial_pre_omega
@[simp] theorem map_data (f : α → β) (arr : Array α) : (arr.map f).data = arr.data.map f := by
@[simp] theorem map_toList (f : α → β) (arr : Array α) : (arr.map f).toList = arr.toList.map f := by
rw [map, mapM_eq_foldlM]
apply congrArg data (foldl_eq_foldl_data (fun bs a => push bs (f a)) #[] arr) |>.trans
have H (l arr) : List.foldl (fun bs a => push bs (f a)) arr l = ⟨arr.data ++ l.map f⟩ := by
apply congrArg toList (foldl_eq_foldl_toList (fun bs a => push bs (f a)) #[] arr) |>.trans
have H (l arr) : List.foldl (fun bs a => push bs (f a)) arr l = ⟨arr.toList ++ l.map f⟩ := by
induction l generalizing arr <;> simp [*]
simp [H]
@[deprecated map_toList (since := "2024-09-09")]
abbrev map_data := @map_toList
@[simp] theorem size_map (f : α → β) (arr : Array α) : (arr.map f).size = arr.size := by
simp only [← data_length]
simp only [← toList_length]
simp
@[simp] theorem appendList_nil (arr : Array α) : arr ++ ([] : List α) = arr := Array.ext' (by simp)
@ -105,16 +118,22 @@ where
@[simp] theorem appendList_cons (arr : Array α) (a : α) (l : List α) :
arr ++ (a :: l) = arr.push a ++ l := Array.ext' (by simp)
theorem foldl_data_eq_bind (l : List α) (acc : Array β)
theorem foldl_toList_eq_bind (l : List α) (acc : Array β)
(F : Array β → α → Array β) (G : α → List β)
(H : ∀ acc a, (F acc a).data = acc.data ++ G a) :
(l.foldl F acc).data = acc.data ++ l.bind G := by
(H : ∀ acc a, (F acc a).toList = acc.toList ++ G a) :
(l.foldl F acc).toList = acc.toList ++ l.bind G := by
induction l generalizing acc <;> simp [*, List.bind]
theorem foldl_data_eq_map (l : List α) (acc : Array β) (G : α → β) :
(l.foldl (fun acc a => acc.push (G a)) acc).data = acc.data ++ l.map G := by
@[deprecated foldl_toList_eq_bind (since := "2024-09-09")]
abbrev foldl_data_eq_bind := @foldl_toList_eq_bind
theorem foldl_toList_eq_map (l : List α) (acc : Array β) (G : α → β) :
(l.foldl (fun acc a => acc.push (G a)) acc).toList = acc.toList ++ l.map G := by
induction l generalizing acc <;> simp [*]
@[deprecated foldl_toList_eq_map (since := "2024-09-09")]
abbrev foldl_data_eq_map := @foldl_toList_eq_map
theorem size_uset (a : Array α) (v i h) : (uset a i v h).size = a.size := by simp
theorem anyM_eq_anyM_loop [Monad m] (p : α → m Bool) (as : Array α) (start stop) :
@ -125,7 +144,7 @@ theorem anyM_stop_le_start [Monad m] (p : α → m Bool) (as : Array α) (start
(h : min stop as.size ≤ start) : anyM p as start stop = pure false := by
rw [anyM_eq_anyM_loop, anyM.loop, dif_neg (Nat.not_lt.2 h)]
theorem mem_def {a : α} {as : Array α} : a ∈ as ↔ a ∈ as.data :=
theorem mem_def {a : α} {as : Array α} : a ∈ as ↔ a ∈ as.toList :=
⟨fun | .mk h => h, Array.Mem.mk⟩
/-! # get -/
@ -164,11 +183,11 @@ theorem get!_eq_getD [Inhabited α] (a : Array α) : a.get! n = a.getD n default
@[simp] theorem getElem_set_eq (a : Array α) (i : Fin a.size) (v : α) {j : Nat}
(eq : i.val = j) (p : j < (a.set i v).size) :
(a.set i v)[j]'p = v := by
simp [set, getElem_eq_data_getElem, ←eq]
simp [set, getElem_eq_toList_getElem, ←eq]
@[simp] theorem getElem_set_ne (a : Array α) (i : Fin a.size) (v : α) {j : Nat} (pj : j < (a.set i v).size)
(h : i.val ≠ j) : (a.set i v)[j]'pj = a[j]'(size_set a i v ▸ pj) := by
simp only [set, getElem_eq_data_getElem, List.getElem_set_ne h]
simp only [set, getElem_eq_toList_getElem, List.getElem_set_ne h]
theorem getElem_set (a : Array α) (i : Fin a.size) (v : α) (j : Nat)
(h : j < (a.set i v).size) :
@ -249,14 +268,20 @@ termination_by n - i
/-- # mkArray -/
@[simp] theorem mkArray_data (n : Nat) (v : α) : (mkArray n v).data = List.replicate n v := rfl
@[simp] theorem toList_mkArray (n : Nat) (v : α) : (mkArray n v).toList = List.replicate n v := rfl
@[deprecated toList_mkArray (since := "2024-09-09")]
abbrev mkArray_data := @toList_mkArray
@[simp] theorem getElem_mkArray (n : Nat) (v : α) (h : i < (mkArray n v).size) :
(mkArray n v)[i] = v := by simp [Array.getElem_eq_data_getElem]
(mkArray n v)[i] = v := by simp [Array.getElem_eq_toList_getElem]
/-- # mem -/
theorem mem_data {a : α} {l : Array α} : a ∈ l.data ↔ a ∈ l := mem_def.symm
theorem mem_toList {a : α} {l : Array α} : a ∈ l.toList ↔ a ∈ l := mem_def.symm
@[deprecated mem_toList (since := "2024-09-09")]
abbrev mem_data := @mem_toList
theorem not_mem_nil (a : α) : ¬ a ∈ #[] := nofun
@ -290,10 +315,13 @@ theorem lt_of_getElem {x : α} {a : Array α} {idx : Nat} {hidx : idx < a.size}
hidx
theorem getElem?_mem {l : Array α} {i : Fin l.size} : l[i] ∈ l := by
erw [Array.mem_def, getElem_eq_data_getElem]
erw [Array.mem_def, getElem_eq_toList_getElem]
apply List.get_mem
theorem getElem_fin_eq_data_get (a : Array α) (i : Fin _) : a[i] = a.data.get i := rfl
theorem getElem_fin_eq_toList_get (a : Array α) (i : Fin _) : a[i] = a.toList.get i := rfl
@[deprecated getElem_fin_eq_toList_get (since := "2024-09-09")]
abbrev getElem_fin_eq_data_get := @getElem_fin_eq_toList_get
@[simp] theorem ugetElem_eq_getElem (a : Array α) {i : USize} (h : i.toNat < a.size) :
a[i] = a[i.toNat] := rfl
@ -304,14 +332,23 @@ theorem getElem?_eq_getElem (a : Array α) (i : Nat) (h : i < a.size) : a[i]? =
theorem get?_len_le (a : Array α) (i : Nat) (h : a.size ≤ i) : a[i]? = none := by
simp [getElem?_neg, h]
theorem getElem_mem_data (a : Array α) (h : i < a.size) : a[i] ∈ a.data := by
simp only [getElem_eq_data_getElem, List.getElem_mem]
theorem getElem_mem_toList (a : Array α) (h : i < a.size) : a[i] ∈ a.toList := by
simp only [getElem_eq_toList_getElem, List.getElem_mem]
theorem getElem?_eq_data_get? (a : Array α) (i : Nat) : a[i]? = a.data.get? i := by
@[deprecated getElem_mem_toList (since := "2024-09-09")]
abbrev getElem_mem_data := @getElem_mem_toList
theorem getElem?_eq_toList_get? (a : Array α) (i : Nat) : a[i]? = a.toList.get? i := by
by_cases i < a.size <;> simp_all [getElem?_pos, getElem?_neg, List.get?_eq_get, eq_comm]; rfl
theorem get?_eq_data_get? (a : Array α) (i : Nat) : a.get? i = a.data.get? i :=
getElem?_eq_data_get? ..
@[deprecated getElem?_eq_toList_get? (since := "2024-09-09")]
abbrev getElem?_eq_data_get? := @getElem?_eq_toList_get?
theorem get?_eq_toList_get? (a : Array α) (i : Nat) : a.get? i = a.toList.get? i :=
getElem?_eq_toList_get? ..
@[deprecated get?_eq_toList_get? (since := "2024-09-09")]
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]
@ -320,7 +357,7 @@ theorem get!_eq_get? [Inhabited α] (a : Array α) : a.get! n = (a.get? n).getD
simp [back, back?]
@[simp] theorem back?_push (a : Array α) : (a.push x).back? = some x := by
simp [back?, getElem?_eq_data_get?]
simp [back?, getElem?_eq_toList_get?]
theorem back_push [Inhabited α] (a : Array α) : (a.push x).back = x := by simp
@ -349,11 +386,14 @@ theorem get?_push {a : Array α} : (a.push x)[i]? = if i = a.size then some x el
@[simp] theorem get?_size {a : Array α} : a[a.size]? = none := by
simp only [getElem?_def, Nat.lt_irrefl, dite_false]
@[simp] theorem data_set (a : Array α) (i v) : (a.set i v).data = a.data.set i.1 v := rfl
@[simp] theorem toList_set (a : Array α) (i v) : (a.set i v).toList = a.toList.set i.1 v := rfl
@[deprecated toList_set (since := "2024-09-09")]
abbrev data_set := @toList_set
theorem get_set_eq (a : Array α) (i : Fin a.size) (v : α) :
(a.set i v)[i.1] = v := by
simp only [set, getElem_eq_data_getElem, List.getElem_set_self]
simp only [set, getElem_eq_toList_getElem, List.getElem_set_self]
theorem get?_set_eq (a : Array α) (i : Fin a.size) (v : α) :
(a.set i v)[i.1]? = v := by simp [getElem?_pos, i.2]
@ -372,7 +412,7 @@ theorem get_set (a : Array α) (i : Fin a.size) (j : Nat) (hj : j < a.size) (v :
@[simp] theorem get_set_ne (a : Array α) (i : Fin a.size) {j : Nat} (v : α) (hj : j < a.size)
(h : i.1 ≠ j) : (a.set i v)[j]'(by simp [*]) = a[j] := by
simp only [set, getElem_eq_data_getElem, List.getElem_set_ne h]
simp only [set, getElem_eq_toList_getElem, List.getElem_set_ne h]
theorem getElem_setD (a : Array α) (i : Nat) (v : α) (h : i < (setD a i v).size) :
(setD a i v)[i] = v := by
@ -388,12 +428,15 @@ theorem swap_def (a : Array α) (i j : Fin a.size) :
a.swap i j = (a.set i (a.get j)).set ⟨j.1, by simp [j.2]⟩ (a.get i) := by
simp [swap, fin_cast_val]
theorem data_swap (a : Array α) (i j : Fin a.size) :
(a.swap i j).data = (a.data.set i (a.get j)).set j (a.get i) := by simp [swap_def]
theorem toList_swap (a : Array α) (i j : Fin a.size) :
(a.swap i j).toList = (a.toList.set i (a.get j)).set j (a.get i) := by simp [swap_def]
@[deprecated toList_swap (since := "2024-09-09")]
abbrev data_swap := @toList_swap
theorem get?_swap (a : Array α) (i j : Fin a.size) (k : Nat) : (a.swap i j)[k]? =
if j = k then some a[i.1] else if i = k then some a[j.1] else a[k]? := by
simp [swap_def, get?_set, ← getElem_fin_eq_data_get]
simp [swap_def, get?_set, ← getElem_fin_eq_toList_get]
@[simp] theorem swapAt_def (a : Array α) (i : Fin a.size) (v : α) :
a.swapAt i v = (a[i.1], a.set i v) := rfl
@ -402,7 +445,10 @@ theorem get?_swap (a : Array α) (i j : Fin a.size) (k : Nat) : (a.swap i j)[k]?
theorem swapAt!_def (a : Array α) (i : Nat) (v : α) (h : i < a.size) :
a.swapAt! i v = (a[i], a.set ⟨i, h⟩ v) := by simp [swapAt!, h]
@[simp] theorem data_pop (a : Array α) : a.pop.data = a.data.dropLast := by simp [pop]
@[simp] theorem toList_pop (a : Array α) : a.pop.toList = a.toList.dropLast := by simp [pop]
@[deprecated toList_pop (since := "2024-09-09")]
abbrev data_pop := @toList_pop
@[simp] theorem pop_empty : (#[] : Array α).pop = #[] := rfl
@ -434,7 +480,10 @@ theorem eq_push_of_size_ne_zero {as : Array α} (h : as.size ≠ 0) :
let _ : Inhabited α := ⟨as[0]⟩
⟨as.pop, as.back, eq_push_pop_back_of_size_ne_zero h⟩
theorem size_eq_length_data (as : Array α) : as.size = as.data.length := rfl
theorem size_eq_length_toList (as : Array α) : as.size = as.toList.length := rfl
@[deprecated size_eq_length_toList (since := "2024-09-09")]
abbrev size_eq_length_data := @size_eq_length_toList
@[simp] theorem size_swap! (a : Array α) (i j) :
(a.swap! i j).size = a.size := by unfold swap!; split <;> (try split) <;> simp [size_swap]
@ -458,19 +507,22 @@ theorem size_eq_length_data (as : Array α) : as.size = as.data.length := rfl
simp only [mkEmpty_eq, size_push] at *
omega
@[simp] theorem data_range (n : Nat) : (range n).data = List.range n := by
@[simp] theorem toList_range (n : Nat) : (range n).toList = List.range n := by
induction n <;> simp_all [range, Nat.fold, flip, List.range_succ]
@[deprecated toList_range (since := "2024-09-09")]
abbrev data_range := @toList_range
@[simp]
theorem getElem_range {n : Nat} {x : Nat} (h : x < (Array.range n).size) : (Array.range n)[x] = x := by
simp [getElem_eq_data_getElem]
simp [getElem_eq_toList_getElem]
set_option linter.deprecated false in
@[simp] theorem reverse_data (a : Array α) : a.reverse.data = a.data.reverse := by
@[simp] theorem reverse_toList (a : Array α) : a.reverse.toList = a.toList.reverse := by
let rec go (as : Array α) (i j hj)
(h : i + j + 1 = a.size) (h₂ : as.size = a.size)
(H : ∀ k, as.data.get? k = if i ≤ k ∧ k ≤ j then a.data.get? k else a.data.reverse.get? k)
(k) : (reverse.loop as i ⟨j, hj⟩).data.get? k = a.data.reverse.get? k := by
(H : ∀ k, as.toList.get? k = if i ≤ k ∧ k ≤ j then a.toList.get? k else a.toList.reverse.get? k)
(k) : (reverse.loop as i ⟨j, hj⟩).toList.get? k = a.toList.reverse.get? k := by
rw [reverse.loop]; dsimp; split <;> rename_i h₁
· have p := reverse.termination h₁
match j with | j+1 => ?_
@ -479,8 +531,9 @@ set_option linter.deprecated false in
· rwa [Nat.add_right_comm i]
· simp [size_swap, h₂]
· intro k
rw [← getElem?_eq_data_get?, get?_swap]
simp only [H, getElem_eq_data_get, ← List.get?_eq_get, Nat.le_of_lt h₁, getElem?_eq_data_get?]
rw [← getElem?_eq_toList_get?, get?_swap]
simp only [H, getElem_eq_toList_get, ← List.get?_eq_get, Nat.le_of_lt h₁,
getElem?_eq_toList_get?]
split <;> rename_i h₂
· simp only [← h₂, Nat.not_le.2 (Nat.lt_succ_self _), Nat.le_refl, and_false]
exact (List.get?_reverse' (j+1) i (Eq.trans (by simp_arith) h)).symm
@ -505,7 +558,7 @@ set_option linter.deprecated false in
· rename_i h
simp only [← show k < _ + 1 ↔ _ from Nat.lt_succ (n := a.size - 1), this, Nat.zero_le,
true_and, Nat.not_lt] at h
rw [List.get?_eq_none.2 ‹_›, List.get?_eq_none.2 (a.data.length_reverse ▸ ‹_›)]
rw [List.get?_eq_none.2 ‹_›, List.get?_eq_none.2 (a.toList.length_reverse ▸ ‹_›)]
/-! ### foldl / foldr -/
@ -545,16 +598,19 @@ theorem foldr_induction
/-! ### map -/
@[simp] theorem mem_map {f : α → β} {l : Array α} : b ∈ l.map f ↔ ∃ a, a ∈ l ∧ f a = b := by
simp only [mem_def, map_data, List.mem_map]
simp only [mem_def, map_toList, List.mem_map]
theorem mapM_eq_mapM_data [Monad m] [LawfulMonad m] (f : α → m β) (arr : Array α) :
arr.mapM f = return mk (← arr.data.mapM f) := by
rw [mapM_eq_foldlM, foldlM_eq_foldlM_data, ← List.foldrM_reverse]
conv => rhs; rw [← List.reverse_reverse arr.data]
induction arr.data.reverse with
theorem mapM_eq_mapM_toList [Monad m] [LawfulMonad m] (f : α → m β) (arr : Array α) :
arr.mapM f = return mk (← 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; rfl
| cons a l ih => simp [ih]; simp [map_eq_pure_bind, push]
@[deprecated mapM_eq_mapM_toList (since := "2024-09-09")]
abbrev mapM_eq_mapM_data := @mapM_eq_mapM_toList
theorem mapM_map_eq_foldl (as : Array α) (f : α → β) (i) :
mapM.map (m := Id) f as i b = as.foldl (start := i) (fun r a => r.push (f a)) b := by
unfold mapM.map
@ -691,86 +747,95 @@ theorem get_modify {arr : Array α} {x i} (h : i < arr.size) :
/-! ### filter -/
@[simp] theorem filter_data (p : α → Bool) (l : Array α) :
(l.filter p).data = l.data.filter p := by
@[simp] theorem filter_toList (p : α → Bool) (l : Array α) :
(l.filter p).toList = l.toList.filter p := by
dsimp only [filter]
rw [foldl_eq_foldl_data]
generalize l.data = l
suffices ∀ a, (List.foldl (fun r a => if p a = true then push r a else r) a l).data =
a.data ++ List.filter p l by
rw [foldl_eq_foldl_toList]
generalize l.toList = l
suffices ∀ a, (List.foldl (fun r a => if p a = true then push r a else r) a l).toList =
a.toList ++ List.filter p l by
simpa using this #[]
induction l with simp
| cons => split <;> simp [*]
@[deprecated filter_toList (since := "2024-09-09")]
abbrev filter_data := @filter_toList
@[simp] theorem filter_filter (q) (l : Array α) :
filter p (filter q l) = filter (fun a => p a && q a) l := by
apply ext'
simp only [filter_data, List.filter_filter]
simp only [filter_toList, List.filter_filter]
@[simp] theorem mem_filter : x ∈ filter p as ↔ x ∈ as ∧ p x := by
simp only [mem_def, filter_data, List.mem_filter]
simp only [mem_def, filter_toList, List.mem_filter]
theorem mem_of_mem_filter {a : α} {l} (h : a ∈ filter p l) : a ∈ l :=
(mem_filter.mp h).1
/-! ### filterMap -/
@[simp] theorem filterMap_data (f : α → Option β) (l : Array α) :
(l.filterMap f).data = l.data.filterMap f := by
@[simp] theorem filterMap_toList (f : α → Option β) (l : Array α) :
(l.filterMap f).toList = l.toList.filterMap f := by
dsimp only [filterMap, filterMapM]
rw [foldlM_eq_foldlM_data]
generalize l.data = l
have this : ∀ a : Array β, (Id.run (List.foldlM (m := Id) ?_ a l)).data =
a.data ++ List.filterMap f l := ?_
rw [foldlM_eq_foldlM_toList]
generalize l.toList = l
have this : ∀ a : Array β, (Id.run (List.foldlM (m := Id) ?_ a l)).toList =
a.toList ++ List.filterMap f l := ?_
exact this #[]
induction l
· simp_all [Id.run]
· simp_all [Id.run, List.filterMap_cons]
split <;> simp_all
@[deprecated filterMap_toList (since := "2024-09-09")]
abbrev filterMap_data := @filterMap_toList
@[simp] theorem mem_filterMap {f : α → Option β} {l : Array α} {b : β} :
b ∈ filterMap f l ↔ ∃ a, a ∈ l ∧ f a = some b := by
simp only [mem_def, filterMap_data, List.mem_filterMap]
simp only [mem_def, filterMap_toList, List.mem_filterMap]
/-! ### empty -/
theorem size_empty : (#[] : Array α).size = 0 := rfl
theorem empty_data : (#[] : Array α).data = [] := rfl
theorem toList_empty : (#[] : Array α).toList = [] := rfl
@[deprecated toList_empty (since := "2024-09-09")]
abbrev empty_data := @toList_empty
/-! ### append -/
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_data, List.mem_append]
simp only [mem_def, append_toList, List.mem_append]
theorem size_append (as bs : Array α) : (as ++ bs).size = as.size + bs.size := by
simp only [size, append_data, List.length_append]
simp only [size, append_toList, List.length_append]
theorem get_append_left {as bs : Array α} {h : i < (as ++ bs).size} (hlt : i < as.size) :
(as ++ bs)[i] = as[i] := by
simp only [getElem_eq_data_getElem]
have h' : i < (as.data ++ bs.data).length := by rwa [← data_length, append_data] at h
conv => rhs; rw [← List.getElem_append_left (bs := bs.data) (h' := h')]
apply List.get_of_eq; rw [append_data]
simp only [getElem_eq_toList_getElem]
have h' : i < (as.toList ++ bs.toList).length := by rwa [← toList_length, append_toList] at h
conv => rhs; rw [← List.getElem_append_left (bs := bs.toList) (h' := h')]
apply List.get_of_eq; rw [append_toList]
theorem get_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_data_getElem]
have h' : i < (as.data ++ bs.data).length := by rwa [← data_length, append_data] at h
simp only [getElem_eq_toList_getElem]
have h' : i < (as.toList ++ bs.toList).length := by rwa [← toList_length, append_toList] at h
conv => rhs; rw [← List.getElem_append_right (h' := h') (h := Nat.not_lt_of_ge hle)]
apply List.get_of_eq; rw [append_data]
apply List.get_of_eq; rw [append_toList]
@[simp] theorem append_nil (as : Array α) : as ++ #[] = as := by
apply ext'; simp only [append_data, empty_data, List.append_nil]
apply ext'; simp only [append_toList, toList_empty, List.append_nil]
@[simp] theorem nil_append (as : Array α) : #[] ++ as = as := by
apply ext'; simp only [append_data, empty_data, List.nil_append]
apply ext'; simp only [append_toList, toList_empty, List.nil_append]
theorem append_assoc (as bs cs : Array α) : as ++ bs ++ cs = as ++ (bs ++ cs) := by
apply ext'; simp only [append_data, List.append_assoc]
apply ext'; simp only [append_toList, List.append_assoc]
/-! ### extract -/
@ -944,7 +1009,7 @@ 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.data.any p := by
theorem any_def {p : α → Bool} (as : Array α) : as.any p = as.toList.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⟩⟩
@ -967,14 +1032,14 @@ 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.data.all p := by
theorem all_def {p : α → Bool} (as : Array α) : as.all p = as.toList.all p := by
rw [Bool.eq_iff_iff, all_eq_true, List.all_eq_true]; simp only [List.mem_iff_getElem]
constructor
· rintro w x ⟨r, h, rfl⟩
rw [← getElem_eq_data_getElem]
rw [← getElem_eq_toList_getElem]
exact w ⟨r, h⟩
· intro w i
exact w as[i] ⟨i, i.2, (getElem_eq_data_getElem as i.2).symm⟩
exact w as[i] ⟨i, i.2, (getElem_eq_toList_getElem as i.2).symm⟩
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]

2
src/Init/Data/Array/Mem.lean
View file

@ -14,7 +14,7 @@ namespace Array
-- NB: This is defined as a structure rather than a plain def so that a lemma
-- like `sizeOf_lt_of_mem` will not apply with no actual arrays around.
structure Mem (as : Array α) (a : α) : Prop where
val : a ∈ as.data
val : a ∈ as.toList
instance : Membership α (Array α) where
mem := Mem

6
src/Init/Data/Array/TakeDrop.lean
View file

@ -10,8 +10,8 @@ import Init.Data.List.Nat.TakeDrop
namespace Array
theorem exists_of_uset (self : Array α) (i d h) :
∃ l₁ l₂, self.data = l₁ ++ self[i] :: l₂ ∧ List.length l₁ = i.toNat ∧
(self.uset i d h).data = l₁ ++ d :: l₂ := by
simpa [Array.getElem_eq_data_getElem] using List.exists_of_set _
∃ l₁ l₂, self.toList = l₁ ++ self[i] :: l₂ ∧ List.length l₁ = i.toNat ∧
(self.uset i d h).toList = l₁ ++ d :: l₂ := by
simpa [Array.getElem_eq_toList_getElem] using List.exists_of_set _
end Array

39
src/Init/Data/List/Impl.lean
View file

@ -57,8 +57,8 @@ The following operations are given `@[csimp]` replacements below:
@[csimp] theorem set_eq_setTR : @set = @setTR := by
funext α l n a; simp [setTR]
let rec go (acc) : ∀ xs n, l = acc.data ++ xs →
setTR.go l a xs n acc = acc.data ++ xs.set n a
let rec go (acc) : ∀ xs n, l = acc.toList ++ xs →
setTR.go l a xs n acc = acc.toList ++ xs.set n a
| [], _ => fun h => by simp [setTR.go, set, h]
| x::xs, 0 => by simp [setTR.go, set]
| x::xs, n+1 => fun h => by simp only [setTR.go, set]; rw [go _ xs] <;> simp [h]
@ -77,10 +77,11 @@ The following operations are given `@[csimp]` replacements below:
@[csimp] theorem filterMap_eq_filterMapTR : @List.filterMap = @filterMapTR := by
funext α β f l
let rec go : ∀ as acc, filterMapTR.go f as acc = acc.data ++ as.filterMap f
let rec go : ∀ as acc, filterMapTR.go f as acc = acc.toList ++ as.filterMap f
| [], acc => by simp [filterMapTR.go, filterMap]
| a::as, acc => by
simp only [filterMapTR.go, go as, Array.push_data, append_assoc, singleton_append, filterMap]
simp only [filterMapTR.go, go as, Array.push_toList, append_assoc, singleton_append,
filterMap]
split <;> simp [*]
exact (go l #[]).symm
@ -90,7 +91,7 @@ The following operations are given `@[csimp]` replacements below:
@[specialize] def foldrTR (f : α → β → β) (init : β) (l : List α) : β := l.toArray.foldr f init
@[csimp] theorem foldr_eq_foldrTR : @foldr = @foldrTR := by
funext α β f init l; simp [foldrTR, Array.foldr_eq_foldr_data, -Array.size_toArray]
funext α β f init l; simp [foldrTR, Array.foldr_eq_foldr_toList, -Array.size_toArray]
/-! ### bind -/
@ -103,7 +104,7 @@ The following operations are given `@[csimp]` replacements below:
@[csimp] theorem bind_eq_bindTR : @List.bind = @bindTR := by
funext α β as f
let rec go : ∀ as acc, bindTR.go f as acc = acc.data ++ as.bind f
let rec go : ∀ as acc, bindTR.go f as acc = acc.toList ++ as.bind f
| [], acc => by simp [bindTR.go, bind]
| x::xs, acc => by simp [bindTR.go, bind, go xs]
exact (go as #[]).symm
@ -131,7 +132,7 @@ The following operations are given `@[csimp]` replacements below:
@[csimp] theorem take_eq_takeTR : @take = @takeTR := by
funext α n l; simp [takeTR]
suffices ∀ xs acc, l = acc.data ++ xs → takeTR.go l xs n acc = acc.data ++ xs.take n from
suffices ∀ xs acc, l = acc.toList ++ xs → takeTR.go l xs n acc = acc.toList ++ xs.take n from
(this l #[] (by simp)).symm
intro xs; induction xs generalizing n with intro acc
| nil => cases n <;> simp [take, takeTR.go]
@ -152,13 +153,13 @@ The following operations are given `@[csimp]` replacements below:
@[csimp] theorem takeWhile_eq_takeWhileTR : @takeWhile = @takeWhileTR := by
funext α p l; simp [takeWhileTR]
suffices ∀ xs acc, l = acc.data ++ xs →
takeWhileTR.go p l xs acc = acc.data ++ xs.takeWhile p from
suffices ∀ xs acc, l = acc.toList ++ xs →
takeWhileTR.go p l xs acc = acc.toList ++ xs.takeWhile p from
(this l #[] (by simp)).symm
intro xs; induction xs with intro acc
| nil => simp [takeWhile, takeWhileTR.go]
| cons x xs IH =>
simp only [takeWhileTR.go, Array.toList_eq, takeWhile]
simp only [takeWhileTR.go, Array.toListImpl_eq, takeWhile]
split
· intro h; rw [IH] <;> simp_all
· simp [*]
@ -185,8 +186,8 @@ The following operations are given `@[csimp]` replacements below:
@[csimp] theorem replace_eq_replaceTR : @List.replace = @replaceTR := by
funext α _ l b c; simp [replaceTR]
suffices ∀ xs acc, l = acc.data ++ xs →
replaceTR.go l b c xs acc = acc.data ++ xs.replace b c from
suffices ∀ xs acc, l = acc.toList ++ xs →
replaceTR.go l b c xs acc = acc.toList ++ xs.replace b c from
(this l #[] (by simp)).symm
intro xs; induction xs with intro acc
| nil => simp [replace, replaceTR.go]
@ -208,7 +209,7 @@ The following operations are given `@[csimp]` replacements below:
@[csimp] theorem erase_eq_eraseTR : @List.erase = @eraseTR := by
funext α _ l a; simp [eraseTR]
suffices ∀ xs acc, l = acc.data ++ xs → eraseTR.go l a xs acc = acc.data ++ xs.erase a from
suffices ∀ xs acc, l = acc.toList ++ xs → eraseTR.go l a xs acc = acc.toList ++ xs.erase a from
(this l #[] (by simp)).symm
intro xs; induction xs with intro acc h
| nil => simp [List.erase, eraseTR.go, h]
@ -228,8 +229,8 @@ The following operations are given `@[csimp]` replacements below:
@[csimp] theorem eraseP_eq_erasePTR : @eraseP = @erasePTR := by
funext α p l; simp [erasePTR]
let rec go (acc) : ∀ xs, l = acc.data ++ xs →
erasePTR.go p l xs acc = acc.data ++ xs.eraseP p
let rec go (acc) : ∀ xs, l = acc.toList ++ xs →
erasePTR.go p l xs acc = acc.toList ++ xs.eraseP p
| [] => fun h => by simp [erasePTR.go, eraseP, h]
| x::xs => by
simp [erasePTR.go, eraseP]; cases p x <;> simp
@ -249,7 +250,7 @@ The following operations are given `@[csimp]` replacements below:
@[csimp] theorem eraseIdx_eq_eraseIdxTR : @eraseIdx = @eraseIdxTR := by
funext α l n; simp [eraseIdxTR]
suffices ∀ xs acc, l = acc.data ++ xs → eraseIdxTR.go l xs n acc = acc.data ++ xs.eraseIdx n from
suffices ∀ xs acc, l = acc.toList ++ xs → eraseIdxTR.go l xs n acc = acc.toList ++ xs.eraseIdx n from
(this l #[] (by simp)).symm
intro xs; induction xs generalizing n with intro acc h
| nil => simp [eraseIdx, eraseIdxTR.go, h]
@ -273,7 +274,7 @@ The following operations are given `@[csimp]` replacements below:
@[csimp] theorem zipWith_eq_zipWithTR : @zipWith = @zipWithTR := by
funext α β γ f as bs
let rec go : ∀ as bs acc, zipWithTR.go f as bs acc = acc.data ++ as.zipWith f bs
let rec go : ∀ as bs acc, zipWithTR.go f as bs acc = acc.toList ++ as.zipWith f bs
| [], _, acc | _::_, [], acc => by simp [zipWithTR.go, zipWith]
| a::as, b::bs, acc => by simp [zipWithTR.go, zipWith, go as bs]
exact (go as bs #[]).symm
@ -295,7 +296,7 @@ def enumFromTR (n : Nat) (l : List α) : List (Nat × α) :=
| a::as, n => by
rw [← show _ + as.length = n + (a::as).length from Nat.succ_add .., foldr, go as]
simp [enumFrom, f]
rw [Array.foldr_eq_foldr_data]
rw [Array.foldr_eq_foldr_toList]
simp [go]
/-! ## Other list operations -/
@ -321,7 +322,7 @@ where
| [_] => simp
| x::y::xs =>
let rec go {acc x} : ∀ xs,
intercalateTR.go sep.toArray x xs acc = acc.data ++ join (intersperse sep (x::xs))
intercalateTR.go sep.toArray x xs acc = acc.toList ++ join (intersperse sep (x::xs))
| [] => by simp [intercalateTR.go]
| _::_ => by simp [intercalateTR.go, go]
simp [intersperse, go]

16
src/Init/Prelude.lean
View file

@ -2568,17 +2568,17 @@ structure Array (α : Type u) where
/--
Converts a `Array α` into an `List α`.
At runtime, this projection is implemented by `Array.toList` and is O(n) in the length of the
At runtime, this projection is implemented by `Array.toListImpl` and is O(n) in the length of the
array. -/
data : List α
toList : List α
attribute [extern "lean_array_data"] Array.data
attribute [extern "lean_array_to_list"] Array.toList
attribute [extern "lean_array_mk"] Array.mk
/-- Construct a new empty array with initial capacity `c`. -/
@[extern "lean_mk_empty_array_with_capacity"]
def Array.mkEmpty {α : Type u} (c : @& Nat) : Array α where
data := List.nil
toList := List.nil
/-- Construct a new empty array. -/
def Array.empty {α : Type u} : Array α := mkEmpty 0
@ -2586,12 +2586,12 @@ def Array.empty {α : Type u} : Array α := mkEmpty 0
/-- Get the size of an array. This is a cached value, so it is O(1) to access. -/
@[reducible, extern "lean_array_get_size"]
def Array.size {α : Type u} (a : @& Array α) : Nat :=
a.data.length
a.toList.length
/-- Access an element from an array without bounds checks, using a `Fin` index. -/
@[extern "lean_array_fget"]
def Array.get {α : Type u} (a : @& Array α) (i : @& Fin a.size) : α :=
a.data.get i
a.toList.get i
/-- Access an element from an array, or return `v₀` if the index is out of bounds. -/
@[inline] abbrev Array.getD (a : Array α) (i : Nat) (v₀ : α) : α :=
@ -2608,7 +2608,7 @@ Push an element onto the end of an array. This is amortized O(1) because
-/
@[extern "lean_array_push"]
def Array.push {α : Type u} (a : Array α) (v : α) : Array α where
data := List.concat a.data v
toList := List.concat a.toList v
/-- Create array `#[]` -/
def Array.mkArray0 {α : Type u} : Array α :=
@ -2654,7 +2654,7 @@ count of 1 when called.
-/
@[extern "lean_array_fset"]
def Array.set (a : Array α) (i : @& Fin a.size) (v : α) : Array α where
data := a.data.set i.val v
toList := a.toList.set i.val v
/--
Set an element in an array, or do nothing if the index is out of bounds.

2
src/Std/Data/DHashMap/Internal/Defs.lean
View file

@ -156,7 +156,7 @@ namespace DHashMap.Internal
/-- Internal implementation detail of the hash map -/
def toListModel (buckets : Array (AssocList α β)) : List ((a : α) × β a) :=
buckets.data.bind AssocList.toList
buckets.toList.bind AssocList.toList
/-- Internal implementation detail of the hash map -/
@[inline] def computeSize (buckets : Array (AssocList α β)) : Nat :=

6
src/Std/Data/DHashMap/Internal/Model.lean
View file

@ -121,7 +121,7 @@ theorem exists_bucket_of_update [BEq α] [Hashable α] (m : Array (AssocList α
theorem exists_bucket' [BEq α] [Hashable α]
(self : Array (AssocList α β)) (i : USize) (hi : i.toNat < self.size) :
∃ l, Perm (self.data.bind AssocList.toList) (self[i.toNat].toList ++ l) ∧
∃ l, Perm (self.toList.bind AssocList.toList) (self[i.toNat].toList ++ l) ∧
(∀ [LawfulHashable α], IsHashSelf self → ∀ k,
(mkIdx self.size (by omega) (hash k)).1.toNat = i.toNat → containsKey k l = false) := by
obtain ⟨l, h₁, -, h₂⟩ := exists_bucket_of_uset self i hi .nil
@ -186,13 +186,13 @@ theorem toListModel_updateAllBuckets {m : Raw₀ α β} {f : AssocList α β →
have := (hg (l := []) (l' := [])).length_eq
rw [List.length_append, List.append_nil] at this
omega
rw [updateAllBuckets, toListModel, Array.map_data, List.bind_eq_foldl, List.foldl_map,
rw [updateAllBuckets, toListModel, Array.map_toList, List.bind_eq_foldl, List.foldl_map,
toListModel, List.bind_eq_foldl]
suffices ∀ (l : List (AssocList α β)) (l' : List ((a: α) × δ a)) (l'' : List ((a : α) × β a)),
Perm (g l'') l' →
Perm (l.foldl (fun acc a => acc ++ (f a).toList) l')
(g (l.foldl (fun acc a => acc ++ a.toList) l'')) by
simpa using this m.1.buckets.data [] [] (by simp [hg₀])
simpa using this m.1.buckets.toList [] [] (by simp [hg₀])
rintro l l' l'' h
induction l generalizing l' l''
· simpa using h.symm

12
src/Std/Data/DHashMap/Internal/WF.lean
View file

@ -38,11 +38,11 @@ theorem toListModel_mkArray_nil {c} :
@[simp]
theorem computeSize_eq {buckets : Array (AssocList α β)} :
computeSize buckets = (toListModel buckets).length := by
rw [computeSize, toListModel, List.bind_eq_foldl, Array.foldl_eq_foldl_data]
rw [computeSize, toListModel, List.bind_eq_foldl, Array.foldl_eq_foldl_toList]
suffices ∀ (l : List (AssocList α β)) (l' : List ((a : α) × β a)),
l.foldl (fun d b => d + b.toList.length) l'.length =
(l.foldl (fun acc a => acc ++ a.toList) l').length
by simpa using this buckets.data []
by simpa using this buckets.toList []
intro l l'
induction l generalizing l'
· simp
@ -129,7 +129,7 @@ theorem expand.go_eq [BEq α] [Hashable α] [PartialEquivBEq α] (source : Array
(target : {d : Array (AssocList α β) // 0 < d.size}) : expand.go 0 source target =
(toListModel source).foldl (fun acc p => reinsertAux hash acc p.1 p.2) target := by
suffices ∀ i, expand.go i source target =
((source.data.drop i).bind AssocList.toList).foldl
((source.toList.drop i).bind AssocList.toList).foldl
(fun acc p => reinsertAux hash acc p.1 p.2) target by
simpa using this 0
intro i
@ -138,12 +138,12 @@ theorem expand.go_eq [BEq α] [Hashable α] [PartialEquivBEq α] (source : Array
simp only [newSource, newTarget, es] at *
rw [expand.go_pos hi]
refine ih.trans ?_
simp only [Array.get_eq_getElem, AssocList.foldl_eq, Array.data_set]
simp only [Array.get_eq_getElem, AssocList.foldl_eq, Array.toList_set]
rw [List.drop_eq_getElem_cons hi, List.bind_cons, List.foldl_append,
List.drop_set_of_lt _ _ (by omega), Array.getElem_eq_data_getElem]
List.drop_set_of_lt _ _ (by omega), Array.getElem_eq_toList_getElem]
· next i source target hi =>
rw [expand.go_neg hi, List.drop_eq_nil_of_le, bind_nil, foldl_nil]
rwa [Array.size_eq_length_data, Nat.not_lt] at hi
rwa [Array.size_eq_length_toList, Nat.not_lt] at hi
theorem isHashSelf_expand [BEq α] [Hashable α] [LawfulHashable α] [EquivBEq α]
{buckets : {d : Array (AssocList α β) // 0 < d.size}} : IsHashSelf (expand buckets).1 := by

2
src/Std/Sat/AIG/Lemmas.lean
View file

@ -277,7 +277,7 @@ theorem denote_congr (assign1 assign2 : α → Bool) (aig : AIG α) (idx : Nat)
simp only [denote_idx_atom heq]
apply h
rw [mem_def, ← heq, Array.mem_def]
apply Array.getElem_mem_data
apply Array.getElem_mem_toList
· intro lhs rhs linv rinv heq
simp only [denote_idx_gate heq]
have := aig.invariant hidx heq

2
src/Std/Tactic/BVDecide/LRAT/Checker.lean
View file

@ -62,7 +62,7 @@ theorem check_sound (lratProof : Array IntAction) (cnf : CNF Nat) :
_
(by
intro action h
simp only [Array.toList_eq, List.filterMap_map, List.mem_filterMap, Function.comp_apply] at h
simp only [List.filterMap_map, List.mem_filterMap, Function.comp_apply] at h
rcases h with ⟨WellFormedActions, _, h2⟩
split at h2
. contradiction

2
src/Std/Tactic/BVDecide/LRAT/Internal/CNF.lean
View file

@ -113,7 +113,7 @@ theorem limplies_insert [Clause α β] [Entails α σ] [Formula α β σ] {c :
simp only [formulaEntails_def, List.all_eq_true, decide_eq_true_eq]
intro h c' c'_in_f
have c'_in_fc : c' ∈ toList (insert f c) := by
simp only [insert_iff, Array.toList_eq, Array.data_toArray, List.mem_singleton]
simp only [insert_iff, Array.toList_toArray, List.mem_singleton]
exact Or.inr c'_in_f
exact h c' c'_in_fc

8
src/Std/Tactic/BVDecide/LRAT/Internal/Clause.lean
View file

@ -223,7 +223,7 @@ theorem ofArray_eq (arr : Array (Literal (PosFin n)))
ofArray arr = some c → toList c = Array.toList arr := by
intro h
simp only [ofArray] at h
rw [toList, Array.toList_eq]
rw [toList]
let motive (idx : Nat) (acc : Option (DefaultClause n)) : Prop :=
∃ idx_le_arr_size : idx ≤ arr.size, ∀ c' : DefaultClause n, acc = some c' →
∃ hsize : c'.clause.length = arr.size - idx, ∀ i : Fin c'.clause.length,
@ -293,13 +293,13 @@ theorem ofArray_eq (arr : Array (Literal (PosFin n)))
next i l =>
by_cases i_in_bounds : i < c.clause.length
· specialize h ⟨i, i_in_bounds⟩
have i_in_bounds' : i < arr.data.length := by
have i_in_bounds' : i < arr.toList.length := by
dsimp; omega
rw [List.getElem?_eq_getElem i_in_bounds, List.getElem?_eq_getElem i_in_bounds']
simp only [List.get_eq_getElem, Nat.zero_add] at h
rw [← Array.getElem_eq_data_getElem]
rw [← Array.getElem_eq_toList_getElem]
simp [h]
· have arr_data_length_le_i : arr.data.length ≤ i := by
· have arr_data_length_le_i : arr.toList.length ≤ i := by
dsimp; omega
simp only [Nat.not_lt, ← List.getElem?_eq_none_iff] at i_in_bounds arr_data_length_le_i
rw [i_in_bounds, arr_data_length_le_i]

8
src/Std/Tactic/BVDecide/LRAT/Internal/Convert.lean
View file

@ -61,7 +61,7 @@ theorem CNF.Clause.mem_lrat_of_mem (clause : CNF.Clause (PosFin n)) (h1 : l ∈
| nil => cases h1
| cons hd tl ih =>
unfold DefaultClause.ofArray at h2
rw [Array.foldr_eq_foldr_data, Array.toArray_data] at h2
rw [Array.foldr_eq_foldr_toList, Array.toArray_toList] at h2
dsimp only [List.foldr] at h2
split at h2
· cases h2
@ -77,7 +77,7 @@ theorem CNF.Clause.mem_lrat_of_mem (clause : CNF.Clause (PosFin n)) (h1 : l ∈
· assumption
· next heq _ _ =>
unfold DefaultClause.ofArray
rw [Array.foldr_eq_foldr_data, Array.toArray_data]
rw [Array.foldr_eq_foldr_toList, Array.toArray_toList]
exact heq
· cases h1
· simp only [← Option.some.inj h2]
@ -89,7 +89,7 @@ theorem CNF.Clause.mem_lrat_of_mem (clause : CNF.Clause (PosFin n)) (h1 : l ∈
apply ih
assumption
unfold DefaultClause.ofArray
rw [Array.foldr_eq_foldr_data, Array.toArray_data]
rw [Array.foldr_eq_foldr_toList, Array.toArray_toList]
exact heq
theorem CNF.Clause.convertLRAT_sat_of_sat (clause : CNF.Clause (PosFin n))
@ -155,7 +155,7 @@ theorem CNF.unsat_of_convertLRAT_unsat (cnf : CNF Nat) :
simp only [Formula.formulaEntails_def, List.all_eq_true, decide_eq_true_eq]
intro lratClause hlclause
simp only [Formula.toList, DefaultFormula.toList, DefaultFormula.ofArray,
CNF.convertLRAT', Array.size_toArray, List.length_map, Array.toList_eq, Array.data_toArray,
CNF.convertLRAT', Array.size_toArray, List.length_map, Array.toList_toArray,
List.map_nil, List.append_nil, List.mem_filterMap, List.mem_map, id_eq, exists_eq_right] at hlclause
rcases hlclause with ⟨reflectClause, ⟨hrclause1, hrclause2⟩⟩
simp only [CNF.eval, List.all_eq_true] at h2

130
src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean
View file

@ -106,11 +106,11 @@ theorem readyForRupAdd_ofArray {n : Nat} (arr : Array (Option (DefaultClause n))
constructor
· simp only [ofArray]
· have hsize : (ofArray arr).assignments.size = n := by
simp only [ofArray, Array.foldl_eq_foldl_data]
simp only [ofArray, Array.foldl_eq_foldl_toList]
have hb : (mkArray n unassigned).size = n := by simp only [Array.size_mkArray]
have hl (acc : Array Assignment) (ih : acc.size = n) (cOpt : Option (DefaultClause n)) (_cOpt_in_arr : cOpt ∈ arr.data) :
have hl (acc : Array Assignment) (ih : acc.size = n) (cOpt : Option (DefaultClause n)) (_cOpt_in_arr : cOpt ∈ arr.toList) :
(ofArray_fold_fn acc cOpt).size = n := by rw [size_ofArray_fold_fn acc cOpt, ih]
exact List.foldlRecOn arr.data ofArray_fold_fn (mkArray n unassigned) hb hl
exact List.foldlRecOn arr.toList ofArray_fold_fn (mkArray n unassigned) hb hl
apply Exists.intro hsize
let ModifiedAssignmentsInvariant (assignments : Array Assignment) : Prop :=
∃ hsize : assignments.size = n,
@ -122,7 +122,7 @@ theorem readyForRupAdd_ofArray {n : Nat} (arr : Array (Option (DefaultClause n))
intro i b h
by_cases hb : b <;> simp [hasAssignment, hb, hasPosAssignment, hasNegAssignment] at h
have hl (acc : Array Assignment) (ih : ModifiedAssignmentsInvariant acc) (cOpt : Option (DefaultClause n))
(cOpt_in_arr : cOpt ∈ arr.data) : ModifiedAssignmentsInvariant (ofArray_fold_fn acc cOpt) := by
(cOpt_in_arr : cOpt ∈ arr.toList) : ModifiedAssignmentsInvariant (ofArray_fold_fn acc cOpt) := by
have hsize : (ofArray_fold_fn acc cOpt).size = n := by rw [size_ofArray_fold_fn, ih.1]
apply Exists.intro hsize
intro i b h
@ -145,7 +145,7 @@ theorem readyForRupAdd_ofArray {n : Nat} (arr : Array (Option (DefaultClause n))
by_cases b
· next b_eq_true =>
rw [isUnit_iff, DefaultClause.toList] at heq
simp only [toList, ofArray, Array.toList_eq, List.map, List.append_nil, List.mem_filterMap, id_eq, exists_eq_right]
simp only [toList, ofArray, List.map, List.append_nil, List.mem_filterMap, id_eq, exists_eq_right]
have i_eq_l : i = l := Subtype.ext i_eq_l
simp only [unit, b_eq_true, i_eq_l]
have c_def : c = ⟨c.clause, c.nodupkey, c.nodup⟩ := rfl
@ -179,7 +179,7 @@ theorem readyForRupAdd_ofArray {n : Nat} (arr : Array (Option (DefaultClause n))
exact ih h
· next b_eq_false =>
rw [isUnit_iff, DefaultClause.toList] at heq
simp only [toList, ofArray, Array.toList_eq, List.map, List.append_nil, List.mem_filterMap, id_eq, exists_eq_right]
simp only [toList, ofArray, List.map, List.append_nil, List.mem_filterMap, id_eq, exists_eq_right]
have i_eq_l : i = l := Subtype.ext i_eq_l
simp only [unit, b_eq_false, i_eq_l]
have c_def : c = ⟨c.clause, c.nodupkey, c.nodup⟩ := rfl
@ -189,9 +189,9 @@ theorem readyForRupAdd_ofArray {n : Nat} (arr : Array (Option (DefaultClause n))
· next i_ne_l =>
simp only [Array.getElem_modify_of_ne i_in_bounds _ (Ne.symm i_ne_l)] at h
exact ih i b h
rcases List.foldlRecOn arr.data ofArray_fold_fn (mkArray n unassigned) hb hl with ⟨_h_size, h'⟩
rcases List.foldlRecOn arr.toList ofArray_fold_fn (mkArray n unassigned) hb hl with ⟨_h_size, h'⟩
intro i b h
simp only [ofArray, Array.foldl_eq_foldl_data] at h
simp only [ofArray, Array.foldl_eq_foldl_toList] at h
exact h' i b h
theorem readyForRatAdd_ofArray {n : Nat} (arr : Array (Option (DefaultClause n))) :
@ -202,7 +202,7 @@ theorem readyForRatAdd_ofArray {n : Nat} (arr : Array (Option (DefaultClause n))
theorem insert_iff {n : Nat} (f : DefaultFormula n) (c1 : DefaultClause n) (c2 : DefaultClause n) :
c2 ∈ toList (insert f c1) ↔ c2 = c1 ∨ c2 ∈ toList f := by
simp only [toList, Array.toList_eq, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq, exists_eq_right,
simp only [toList, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq, exists_eq_right,
List.mem_map, Prod.exists, Bool.exists_bool]
by_cases c2 = c1
· next c2_eq_c1 =>
@ -222,7 +222,7 @@ theorem insert_iff {n : Nat} (f : DefaultFormula n) (c1 : DefaultClause n) (c2 :
simp only [insert] at h
split at h
all_goals
simp only [Array.push_data, List.mem_append, List.mem_singleton, Option.some.injEq] at h
simp only [Array.push_toList, List.mem_append, List.mem_singleton, Option.some.injEq] at h
rcases h with h | h
· exact h
· exact False.elim <| c2_ne_c1 h
@ -237,7 +237,7 @@ theorem insert_iff {n : Nat} (f : DefaultFormula n) (c1 : DefaultClause n) (c2 :
simp only [insert]
split
all_goals
simp only [Array.push_data, List.mem_append, List.mem_singleton, Option.some.injEq]
simp only [Array.push_toList, List.mem_append, List.mem_singleton, Option.some.injEq]
exact Or.inl h
· rw [rupUnits_insert]
exact Or.inr <| Or.inl h
@ -250,7 +250,7 @@ theorem limplies_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClause n) :
simp only [formulaEntails_def, List.all_eq_true, decide_eq_true_eq]
intro h c' c'_in_f
have c'_in_fc : c' ∈ toList (insert f c) := by
simp only [insert_iff, Array.toList_eq, Array.data_toArray, List.mem_singleton]
simp only [insert_iff, Array.toList_toArray, List.mem_singleton]
exact Or.inr c'_in_f
exact h c' c'_in_fc
@ -267,9 +267,9 @@ theorem readyForRupAdd_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClaus
· refine ⟨f_readyForRupAdd.1, f_readyForRupAdd.2.1, ?_⟩
intro i b hb
have hf := f_readyForRupAdd.2.2 i b hb
simp only [toList, Array.toList_eq, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq, exists_eq_right,
simp only [toList, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq, exists_eq_right,
List.mem_map, Prod.exists, Bool.exists_bool] at hf
simp only [toList, Array.toList_eq, Array.push_data, List.append_assoc, List.mem_append, List.mem_filterMap,
simp only [toList, Array.push_toList, List.append_assoc, List.mem_append, List.mem_filterMap,
List.mem_singleton, id_eq, exists_eq_right, Option.some.injEq, List.mem_map, Prod.exists, Bool.exists_bool]
rcases hf with hf | hf
· exact (Or.inl ∘ Or.inl) hf
@ -285,7 +285,7 @@ theorem readyForRupAdd_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClaus
simp only at hb
by_cases (i, b) = (l, true)
· next ib_eq_c =>
simp only [toList, Array.toList_eq, Array.push_data, List.append_assoc, List.mem_append, List.mem_filterMap,
simp only [toList, Array.push_toList, List.append_assoc, List.mem_append, List.mem_filterMap,
List.mem_singleton, id_eq, exists_eq_right, Option.some.injEq, List.mem_map, Prod.exists, Bool.exists_bool]
apply Or.inl ∘ Or.inr
rw [isUnit_iff, DefaultClause.toList, ← ib_eq_c] at hc
@ -308,9 +308,9 @@ theorem readyForRupAdd_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClaus
simp only [Array.getElem_modify_of_ne i_in_bounds _ l_ne_i] at hb
exact hb
specialize hf hb'
simp only [toList, Array.toList_eq, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
simp only [toList, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
exists_eq_right, List.mem_map, Prod.exists, Bool.exists_bool] at hf
simp only [toList, Array.toList_eq, Array.push_data, List.append_assoc, List.mem_append, List.mem_filterMap,
simp only [toList, Array.push_toList, List.append_assoc, List.mem_append, List.mem_filterMap,
List.mem_singleton, id_eq, exists_eq_right, Option.some.injEq, List.mem_map, Prod.exists, Bool.exists_bool]
rcases hf with hf | hf
· exact Or.inl <| Or.inl hf
@ -326,7 +326,7 @@ theorem readyForRupAdd_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClaus
simp only at hb
by_cases (i, b) = (l, false)
· next ib_eq_c =>
simp only [toList, Array.toList_eq, Array.push_data, List.append_assoc, List.mem_append, List.mem_filterMap,
simp only [toList, Array.push_toList, List.append_assoc, List.mem_append, List.mem_filterMap,
List.mem_singleton, id_eq, exists_eq_right, Option.some.injEq, List.mem_map, Prod.exists, Bool.exists_bool]
apply Or.inl ∘ Or.inr
rw [isUnit_iff, DefaultClause.toList, ← ib_eq_c] at hc
@ -347,9 +347,9 @@ theorem readyForRupAdd_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClaus
simp only [Array.getElem_modify_of_ne i_in_bounds _ l_ne_i] at hb
exact hb
specialize hf hb'
simp only [toList, Array.toList_eq, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
simp only [toList, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
exists_eq_right, List.mem_map, Prod.exists, Bool.exists_bool] at hf
simp only [toList, Array.toList_eq, Array.push_data, List.append_assoc, List.mem_append, List.mem_filterMap,
simp only [toList, Array.push_toList, List.append_assoc, List.mem_append, List.mem_filterMap,
List.mem_singleton, id_eq, exists_eq_right, Option.some.injEq, List.mem_map, Prod.exists, Bool.exists_bool]
rcases hf with hf | hf
· exact Or.inl <| Or.inl hf
@ -365,22 +365,22 @@ theorem readyForRatAdd_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClaus
theorem mem_of_insertRupUnits {n : Nat} (f : DefaultFormula n) (units : CNF.Clause (PosFin n))
(c : DefaultClause n) :
c ∈ toList (insertRupUnits f units).1 → c ∈ units.map Clause.unit ∨ c ∈ toList f := by
simp only [toList, insertRupUnits, Array.toList_eq, List.append_assoc, List.mem_append,
simp only [toList, insertRupUnits, List.append_assoc, List.mem_append,
List.mem_filterMap, id_eq, exists_eq_right, List.mem_map, Prod.exists, Bool.exists_bool]
intro h
have hb : ∀ l : Literal (PosFin n), l ∈ (f.rupUnits, f.assignments, false).1.data → (l ∈ f.rupUnits.data ∨ l ∈ units) := by
have hb : ∀ l : Literal (PosFin n), l ∈ (f.rupUnits, f.assignments, false).1.toList → (l ∈ f.rupUnits.toList ∨ l ∈ units) := by
intro l hl
exact Or.inl hl
have hl (acc : Array (Literal (PosFin n)) × Array Assignment × Bool)
(ih : ∀ l : Literal (PosFin n), l ∈ acc.1.data → l ∈ f.rupUnits.data ∨ l ∈ units)
(ih : ∀ l : Literal (PosFin n), l ∈ acc.1.toList → l ∈ f.rupUnits.toList ∨ l ∈ units)
(unit : Literal (PosFin n)) (unit_in_units : unit ∈ units) :
∀ l : Literal (PosFin n), l ∈ (insertUnit acc unit).1.data → (l ∈ f.rupUnits.data ∨ l ∈ units) := by
∀ l : Literal (PosFin n), l ∈ (insertUnit acc unit).1.toList → (l ∈ f.rupUnits.toList ∨ l ∈ units) := by
intro l hl
rw [insertUnit.eq_def] at hl
dsimp at hl
split at hl
· exact ih l hl
· simp only [Array.push_data, List.mem_append, List.mem_singleton] at hl
· simp only [Array.push_toList, List.mem_append, List.mem_singleton] at hl
rcases hl with l_in_acc | l_eq_unit
· exact ih l l_in_acc
· rw [l_eq_unit]
@ -403,21 +403,21 @@ theorem mem_of_insertRupUnits {n : Nat} (f : DefaultFormula n) (units : CNF.Clau
theorem mem_of_insertRatUnits {n : Nat} (f : DefaultFormula n) (units : CNF.Clause (PosFin n))
(c : DefaultClause n) :
c ∈ toList (insertRatUnits f units).1 → c ∈ units.map Clause.unit ∨ c ∈ toList f := by
simp only [toList, insertRatUnits, Array.toList_eq, List.append_assoc, List.mem_append,
simp only [toList, insertRatUnits, List.append_assoc, List.mem_append,
List.mem_filterMap, id_eq, exists_eq_right, List.mem_map, Prod.exists, Bool.exists_bool]
intro h
have hb : ∀ l : Literal (PosFin n), l ∈ (f.ratUnits, f.assignments, false).1.data → (l ∈ f.ratUnits.data ∨ l ∈ units) :=
have hb : ∀ l : Literal (PosFin n), l ∈ (f.ratUnits, f.assignments, false).1.toList → (l ∈ f.ratUnits.toList ∨ l ∈ units) :=
fun _ => Or.inl
have hl (acc : Array (Literal (PosFin n)) × Array Assignment × Bool)
(ih : ∀ l : Literal (PosFin n), l ∈ acc.1.data → l ∈ f.ratUnits.data ∨ l ∈ units)
(ih : ∀ l : Literal (PosFin n), l ∈ acc.1.toList → l ∈ f.ratUnits.toList ∨ l ∈ units)
(unit : Literal (PosFin n)) (unit_in_units : unit ∈ units) :
∀ l : Literal (PosFin n), l ∈ (insertUnit acc unit).1.data → (l ∈ f.ratUnits.data ∨ l ∈ units) := by
∀ l : Literal (PosFin n), l ∈ (insertUnit acc unit).1.toList → (l ∈ f.ratUnits.toList ∨ l ∈ units) := by
intro l hl
rw [insertUnit.eq_def] at hl
dsimp at hl
split at hl
· exact ih l hl
· simp only [Array.push_data, List.mem_append, List.mem_singleton] at hl
· simp only [Array.push_toList, List.mem_append, List.mem_singleton] at hl
rcases hl with l_in_acc | l_eq_unit
· exact ih l l_in_acc
· rw [l_eq_unit]
@ -481,18 +481,18 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
rw [l_ne_b] at hb
have hb := has_remove_irrelevant f.assignments[i.1] b hb
specialize hf i b hb
simp only [toList, Array.toList_eq, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
simp only [toList, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
exists_eq_right, List.mem_map, Prod.exists, Bool.exists_bool] at hf
simp only [toList, Array.toList_eq, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
simp only [toList, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
exists_eq_right, List.mem_map, Prod.exists, Bool.exists_bool]
rcases hf with hf | hf
· apply Or.inl
simp only [Array.set!, Array.setD]
split
· rcases List.getElem_of_mem hf with ⟨idx, hbound, hidx⟩
simp only [← hidx, Array.data_set]
simp only [← hidx, Array.toList_set]
rw [List.mem_iff_get]
have idx_in_bounds : idx < List.length (List.set f.clauses.data id none) := by
have idx_in_bounds : idx < List.length (List.set f.clauses.toList id none) := by
simp only [List.length_set]
exact hbound
apply Exists.intro ⟨idx, idx_in_bounds⟩
@ -500,11 +500,11 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
· next id_eq_idx =>
exfalso
have idx_in_bounds2 : idx < f.clauses.size := by
have f_clauses_rw : f.clauses = { data := f.clauses.data } := rfl
have f_clauses_rw : f.clauses = { toList := f.clauses.toList } := rfl
conv => rhs; rw [f_clauses_rw, Array.size_mk]
exact hbound
simp only [getElem!, id_eq_idx, Array.data_length, idx_in_bounds2, ↓reduceDIte,
Fin.eta, Array.get_eq_getElem, Array.getElem_eq_data_getElem, decidableGetElem?] at heq
simp only [getElem!, id_eq_idx, Array.toList_length, idx_in_bounds2, ↓reduceDIte,
Fin.eta, Array.get_eq_getElem, Array.getElem_eq_toList_getElem, decidableGetElem?] at heq
rw [hidx, hl] at heq
simp only [unit, Option.some.injEq, DefaultClause.mk.injEq, List.cons.injEq, and_true] at heq
simp only [← heq, not] at l_ne_b
@ -515,18 +515,18 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
· next l_ne_i =>
simp only [Array.getElem_modify_of_ne i_in_bounds _ l_ne_i] at hb
specialize hf i b hb
simp only [toList, Array.toList_eq, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
simp only [toList, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
exists_eq_right, List.mem_map, Prod.exists, Bool.exists_bool] at hf
simp only [toList, Array.toList_eq, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
simp only [toList, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
exists_eq_right, List.mem_map, Prod.exists, Bool.exists_bool]
rcases hf with hf | hf
· apply Or.inl
simp only [Array.set!, Array.setD]
split
· rcases List.getElem_of_mem hf with ⟨idx, hbound, hidx⟩
simp only [← hidx, Array.data_set]
simp only [← hidx, Array.toList_set]
rw [List.mem_iff_get]
have idx_in_bounds : idx < List.length (List.set f.clauses.data id none) := by
have idx_in_bounds : idx < List.length (List.set f.clauses.toList id none) := by
simp only [List.length_set]
exact hbound
apply Exists.intro ⟨idx, idx_in_bounds⟩
@ -534,11 +534,11 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
· next id_eq_idx =>
exfalso
have idx_in_bounds2 : idx < f.clauses.size := by
have f_clauses_rw : f.clauses = { data := f.clauses.data } := rfl
have f_clauses_rw : f.clauses = { toList := f.clauses.toList } := rfl
conv => rhs; rw [f_clauses_rw, Array.size_mk]
exact hbound
simp only [getElem!, id_eq_idx, Array.data_length, idx_in_bounds2, ↓reduceDIte,
Fin.eta, Array.get_eq_getElem, Array.getElem_eq_data_getElem, decidableGetElem?] at heq
simp only [getElem!, id_eq_idx, Array.toList_length, idx_in_bounds2, ↓reduceDIte,
Fin.eta, Array.get_eq_getElem, Array.getElem_eq_toList_getElem, decidableGetElem?] at heq
rw [hidx, hl] at heq
simp only [unit, Option.some.injEq, DefaultClause.mk.injEq, List.cons.injEq, and_true] at heq
have i_eq_l : i = l.1 := by rw [← heq]
@ -576,18 +576,18 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
· rfl
simp only [deleteOne_f_rw] at hb
specialize hf i b hb
simp only [toList, Array.toList_eq, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
simp only [toList, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
exists_eq_right, List.mem_map, Prod.exists, Bool.exists_bool] at hf
simp only [toList, Array.toList_eq, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
simp only [toList, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
exists_eq_right, List.mem_map, Prod.exists, Bool.exists_bool]
rcases hf with hf | hf
· apply Or.inl
simp only [Array.set!, Array.setD]
split
· rcases List.getElem_of_mem hf with ⟨idx, hbound, hidx⟩
simp only [← hidx, Array.data_set]
simp only [← hidx, Array.toList_set]
rw [List.mem_iff_get]
have idx_in_bounds : idx < List.length (List.set f.clauses.data id none) := by
have idx_in_bounds : idx < List.length (List.set f.clauses.toList id none) := by
simp only [List.length_set]
exact hbound
apply Exists.intro ⟨idx, idx_in_bounds⟩
@ -595,11 +595,11 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
· next id_eq_idx =>
exfalso
have idx_in_bounds2 : idx < f.clauses.size := by
have f_clauses_rw : f.clauses = { data := f.clauses.data } := rfl
have f_clauses_rw : f.clauses = { toList := f.clauses.toList } := rfl
conv => rhs; rw [f_clauses_rw, Array.size_mk]
exact hbound
simp only [getElem!, id_eq_idx, Array.data_length, idx_in_bounds2, ↓reduceDIte,
Fin.eta, Array.get_eq_getElem, Array.getElem_eq_data_getElem, decidableGetElem?] at heq
simp only [getElem!, id_eq_idx, Array.toList_length, idx_in_bounds2, ↓reduceDIte,
Fin.eta, Array.get_eq_getElem, Array.getElem_eq_toList_getElem, decidableGetElem?] at heq
rw [hidx] at heq
simp only [Option.some.injEq] at heq
rw [← heq] at hl
@ -614,16 +614,16 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
theorem readyForRupAdd_delete {n : Nat} (f : DefaultFormula n) (arr : Array Nat) :
ReadyForRupAdd f → ReadyForRupAdd (delete f arr) := by
intro h
rw [delete, Array.foldl_eq_foldl_data]
rw [delete, Array.foldl_eq_foldl_toList]
constructor
· have hb : f.rupUnits = #[] := h.1
have hl (acc : DefaultFormula n) (ih : acc.rupUnits = #[]) (id : Nat) (_id_in_arr : id ∈ arr.data) :
have hl (acc : DefaultFormula n) (ih : acc.rupUnits = #[]) (id : Nat) (_id_in_arr : id ∈ arr.toList) :
(deleteOne acc id).rupUnits = #[] := by rw [deleteOne_preserves_rupUnits, ih]
exact List.foldlRecOn arr.data deleteOne f hb hl
exact List.foldlRecOn arr.toList deleteOne f hb hl
· have hb : StrongAssignmentsInvariant f := h.2
have hl (acc : DefaultFormula n) (ih : StrongAssignmentsInvariant acc) (id : Nat) (_id_in_arr : id ∈ arr.data) :
have hl (acc : DefaultFormula n) (ih : StrongAssignmentsInvariant acc) (id : Nat) (_id_in_arr : id ∈ arr.toList) :
StrongAssignmentsInvariant (deleteOne acc id) := deleteOne_preserves_strongAssignmentsInvariant acc id ih
exact List.foldlRecOn arr.data deleteOne f hb hl
exact List.foldlRecOn arr.toList deleteOne f hb hl
theorem deleteOne_preserves_ratUnits {n : Nat} (f : DefaultFormula n) (id : Nat) :
(deleteOne f id).ratUnits = f.ratUnits := by
@ -634,11 +634,11 @@ theorem readyForRatAdd_delete {n : Nat} (f : DefaultFormula n) (arr : Array Nat)
ReadyForRatAdd f → ReadyForRatAdd (delete f arr) := by
intro h
constructor
· rw [delete, Array.foldl_eq_foldl_data]
· rw [delete, Array.foldl_eq_foldl_toList]
have hb : f.ratUnits = #[] := h.1
have hl (acc : DefaultFormula n) (ih : acc.ratUnits = #[]) (id : Nat) (_id_in_arr : id ∈ arr.data) :
have hl (acc : DefaultFormula n) (ih : acc.ratUnits = #[]) (id : Nat) (_id_in_arr : id ∈ arr.toList) :
(deleteOne acc id).ratUnits = #[] := by rw [deleteOne_preserves_ratUnits, ih]
exact List.foldlRecOn arr.data deleteOne f hb hl
exact List.foldlRecOn arr.toList deleteOne f hb hl
· exact readyForRupAdd_delete f arr h.2
theorem deleteOne_subset (f : DefaultFormula n) (id : Nat) (c : DefaultClause n) :
@ -651,11 +651,11 @@ theorem deleteOne_subset (f : DefaultFormula n) (id : Nat) (c : DefaultClause n)
rw [toList, List.mem_append, List.mem_append, or_assoc]
rcases h1 with h1 | h1 | h1
· apply Or.inl
simp only [Array.toList_eq, List.mem_filterMap, id_eq, exists_eq_right] at h1
simp only [Array.toList_eq, List.mem_filterMap, id_eq, exists_eq_right]
simp only [List.mem_filterMap, id_eq, exists_eq_right] at h1
simp only [List.mem_filterMap, id_eq, exists_eq_right]
rw [Array.set!, Array.setD] at h1
split at h1
· simp only [Array.data_set] at h1
· simp only [Array.toList_set] at h1
rcases List.getElem_of_mem h1 with ⟨i, h, h4⟩
rw [List.getElem_set] at h4
split at h4
@ -668,11 +668,11 @@ theorem deleteOne_subset (f : DefaultFormula n) (id : Nat) (c : DefaultClause n)
theorem delete_subset (f : DefaultFormula n) (arr : Array Nat) (c : DefaultClause n) :
c ∈ toList (delete f arr) → c ∈ toList f := by
simp only [delete, Array.foldl_eq_foldl_data]
simp only [delete, Array.foldl_eq_foldl_toList]
have hb : c ∈ toList f → c ∈ toList f := id
have hl (f' : DefaultFormula n) (ih : c ∈ toList f' → c ∈ toList f) (id : Nat) (_ : id ∈ arr.data) :
have hl (f' : DefaultFormula n) (ih : c ∈ toList f' → c ∈ toList f) (id : Nat) (_ : id ∈ arr.toList) :
c ∈ toList (deleteOne f' id) → c ∈ toList f := by intro h; exact ih <| deleteOne_subset f' id c h
exact List.foldlRecOn arr.data deleteOne f hb hl
exact List.foldlRecOn arr.toList deleteOne f hb hl
end DefaultFormula

58
src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean
View file

@ -80,12 +80,12 @@ theorem assignmentsInvariant_insertRatUnits {n : Nat} (f : DefaultFormula n)
apply Exists.intro hsize
intro i b hb p hp
simp only [(· ⊨ ·), Clause.eval] at hp
simp only [toList, Array.toList_eq, List.append_assoc,
simp only [toList, List.append_assoc,
Entails.eval, List.any_eq_true, Prod.exists, Bool.exists_bool, Bool.decide_coe,
List.all_eq_true, List.mem_append, List.mem_filterMap, id_eq, exists_eq_right, List.mem_map] at hp
have pf : p ⊨ f := by
simp only [(· ⊨ ·), Clause.eval]
simp only [toList, Array.toList_eq, List.append_assoc,
simp only [toList, List.append_assoc,
Entails.eval, List.any_eq_true, Prod.exists, Bool.exists_bool,
Bool.decide_coe, List.all_eq_true, List.mem_append, List.mem_filterMap, id_eq, exists_eq_right, List.mem_map]
intro c cf
@ -105,8 +105,8 @@ theorem assignmentsInvariant_insertRatUnits {n : Nat} (f : DefaultFormula n)
have j_unit_def : j_unit = unit (insertRatUnits f units).1.ratUnits[j] := rfl
have j_unit_in_insertRatUnits_res :
∃ i : PosFin n,
(i, false) ∈ (insertRatUnits f units).1.ratUnits.data ∧ unit (i, false) = j_unit ∨
(i, true) ∈ (insertRatUnits f units).1.ratUnits.data ∧ unit (i, true) = j_unit := by
(i, false) ∈ (insertRatUnits f units).1.ratUnits.toList ∧ unit (i, false) = j_unit ∨
(i, true) ∈ (insertRatUnits f units).1.ratUnits.toList ∧ unit (i, true) = j_unit := by
apply Exists.intro i
rw [j_unit_def, h1]
by_cases hb' : b'
@ -118,7 +118,7 @@ theorem assignmentsInvariant_insertRatUnits {n : Nat} (f : DefaultFormula n)
simp only [h1, Prod.mk.injEq, and_true]
rfl
rw [← h1]
apply Array.getElem_mem_data
apply Array.getElem_mem_toList
· rfl
· simp only [Bool.not_eq_true] at hb'
rw [hb']
@ -129,7 +129,7 @@ theorem assignmentsInvariant_insertRatUnits {n : Nat} (f : DefaultFormula n)
simp only [h1, Prod.mk.injEq, and_true]
rfl
rw [← h1]
apply Array.getElem_mem_data
apply Array.getElem_mem_toList
· rfl
specialize hp j_unit ((Or.inr ∘ Or.inr) j_unit_in_insertRatUnits_res)
simp only [List.any_eq_true, Prod.exists, Bool.exists_bool, Bool.decide_coe, Fin.getElem_fin, List.find?, j_unit] at hp
@ -151,8 +151,8 @@ theorem assignmentsInvariant_insertRatUnits {n : Nat} (f : DefaultFormula n)
have j1_unit_def : j1_unit = unit (insertRatUnits f units).1.ratUnits[j1] := rfl
have j1_unit_in_insertRatUnits_res :
∃ i : PosFin n,
(i, false) ∈ (insertRatUnits f units).1.ratUnits.data ∧ unit (i, false) = j1_unit ∨
(i, true) ∈ (insertRatUnits f units).1.ratUnits.data ∧ unit (i, true) = j1_unit := by
(i, false) ∈ (insertRatUnits f units).1.ratUnits.toList ∧ unit (i, false) = j1_unit ∨
(i, true) ∈ (insertRatUnits f units).1.ratUnits.toList ∧ unit (i, true) = j1_unit := by
apply Exists.intro i ∘ Or.inr
rw [j1_unit_def, h1]
constructor
@ -161,14 +161,14 @@ theorem assignmentsInvariant_insertRatUnits {n : Nat} (f : DefaultFormula n)
simp only [Prod.mk.injEq, and_true]
rfl
rw [← h1]
apply Array.getElem_mem_data
apply Array.getElem_mem_toList
· rfl
let j2_unit := unit (insertRatUnits f units).1.ratUnits[j2]
have j2_unit_def : j2_unit = unit (insertRatUnits f units).1.ratUnits[j2] := rfl
have j2_unit_in_insertRatUnits_res :
∃ i : PosFin n,
(i, false) ∈ (insertRatUnits f units).1.ratUnits.data ∧ unit (i, false) = j2_unit ∨
(i, true) ∈ (insertRatUnits f units).1.ratUnits.data ∧ unit (i, true) = j2_unit := by
(i, false) ∈ (insertRatUnits f units).1.ratUnits.toList ∧ unit (i, false) = j2_unit ∨
(i, true) ∈ (insertRatUnits f units).1.ratUnits.toList ∧ unit (i, true) = j2_unit := by
apply Exists.intro i ∘ Or.inl
rw [j2_unit_def, h2]
constructor
@ -177,7 +177,7 @@ theorem assignmentsInvariant_insertRatUnits {n : Nat} (f : DefaultFormula n)
simp only [Prod.mk.injEq, and_true]
rfl
rw [← h2]
apply Array.getElem_mem_data
apply Array.getElem_mem_toList
· rfl
have hp1 := hp j1_unit ((Or.inr ∘ Or.inr) j1_unit_in_insertRatUnits_res)
have hp2 := hp j2_unit ((Or.inr ∘ Or.inr) j2_unit_in_insertRatUnits_res)
@ -219,7 +219,7 @@ theorem sat_of_confirmRupHint_of_insertRat_fold {n : Nat} (f : DefaultFormula n)
not_imp] at fc_unsat
rcases fc_unsat with ⟨unsat_c, unsat_c_in_fc, p_unsat_c⟩
have unsat_c_in_fc := mem_of_insertRatUnits f (negate c) unsat_c unsat_c_in_fc
simp only [Array.toList_eq, List.mem_map, Prod.exists, Bool.exists_bool] at unsat_c_in_fc
simp only [List.mem_map, Prod.exists, Bool.exists_bool] at unsat_c_in_fc
rcases unsat_c_in_fc with ⟨v, ⟨v_in_neg_c, unsat_c_eq⟩ | ⟨v_in_neg_c, unsat_c_eq⟩⟩ | unsat_c_in_f
· simp only [negate_eq, List.mem_map, Prod.exists, Bool.exists_bool] at v_in_neg_c
rcases v_in_neg_c with ⟨v', ⟨_, v'_eq_v⟩ | ⟨v'_in_c, v'_eq_v⟩⟩
@ -285,13 +285,13 @@ theorem sat_of_insertRat {n : Nat} (f : DefaultFormula n)
simp [p_entails_i_true] at p_entails_i_false
· simp only [(· ⊨ ·), Clause.eval, List.any_eq_true, Prod.exists, Bool.exists_bool, Bool.decide_coe]
apply Exists.intro i
have ib_in_insertUnit_fold : (i, b) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) (negate c)).1.data := by
have ib_in_insertUnit_fold : (i, b) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) (negate c)).1.toList := by
have i_rw : i = ⟨i.1, i.2⟩ := rfl
rw [i_rw, ← h1]
apply List.get_mem
have ib_in_insertUnit_fold := mem_insertUnit_fold_units f.ratUnits f.assignments false (negate c) (i, b) ib_in_insertUnit_fold
simp only [negate, Literal.negate, List.mem_map, Prod.mk.injEq, Prod.exists, Bool.exists_bool,
Bool.not_false, Bool.not_true, hf.1, Array.data_toArray, List.find?, List.not_mem_nil, or_false]
Bool.not_false, Bool.not_true, hf.1, Array.toList_toArray, List.find?, List.not_mem_nil, or_false]
at ib_in_insertUnit_fold
rw [hboth] at h2
rcases ib_in_insertUnit_fold with ⟨i', ⟨i_false_in_c, i'_eq_i, b_eq_true⟩ | ⟨i_true_in_c, i'_eq_i, b_eq_false⟩⟩
@ -330,11 +330,11 @@ theorem sat_of_insertRat {n : Nat} (f : DefaultFormula n)
exact h3 (has_both b)
· simp at h2
· exfalso
have i_true_in_insertUnit_fold : (i, true) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) (negate c)).1.data := by
have i_true_in_insertUnit_fold : (i, true) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) (negate c)).1.toList := by
have i_rw : i = ⟨i.1, i.2⟩ := rfl
rw [i_rw, ← h1]
apply List.get_mem
have i_false_in_insertUnit_fold : (i, false) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) (negate c)).1.data := by
have i_false_in_insertUnit_fold : (i, false) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) (negate c)).1.toList := by
have i_rw : i = ⟨i.1, i.2⟩ := rfl
rw [i_rw, ← h2]
apply List.get_mem
@ -344,7 +344,7 @@ theorem sat_of_insertRat {n : Nat} (f : DefaultFormula n)
have i_false_in_insertUnit_fold :=
mem_insertUnit_fold_units #[] f.assignments false (c.clause.map Literal.negate) (i, false) i_false_in_insertUnit_fold
simp only [Literal.negate, List.mem_map, Prod.mk.injEq, Bool.not_eq_true', Prod.exists,
exists_eq_right_right, exists_eq_right, Array.data_toArray, List.find?, List.not_mem_nil, or_false,
exists_eq_right_right, exists_eq_right, Array.toList_toArray, List.find?, List.not_mem_nil, or_false,
Bool.not_eq_false'] at i_true_in_insertUnit_fold i_false_in_insertUnit_fold
have c_not_tautology := Clause.not_tautology c (i, true)
simp only [Clause.toList] at c_not_tautology
@ -440,7 +440,7 @@ theorem existsRatHint_of_ratHintsExhaustive {n : Nat} (f : DefaultFormula n)
(ratHintsExhaustive_eq_true : ratHintsExhaustive f pivot ratHints = true) (c' : DefaultClause n)
(c'_in_f : c' ∈ toList f) (negPivot_in_c' : Literal.negate pivot ∈ Clause.toList c') :
∃ i : Fin ratHints.size, f.clauses[ratHints[i].1]! = some c' := by
simp only [toList, Array.toList_eq, f_readyForRatAdd.2.1, Array.data_toArray, List.map, List.append_nil, f_readyForRatAdd.1,
simp only [toList, f_readyForRatAdd.2.1, Array.toList_toArray, List.map, List.append_nil, f_readyForRatAdd.1,
List.mem_filterMap, id_eq, exists_eq_right] at c'_in_f
rw [List.mem_iff_getElem] at c'_in_f
rcases c'_in_f with ⟨i, hi, c'_in_f⟩
@ -451,29 +451,29 @@ theorem existsRatHint_of_ratHintsExhaustive {n : Nat} (f : DefaultFormula n)
have i_lt_f_clauses_size : i < f.clauses.size := by
rw [Array.size_range] at i_in_bounds
exact i_in_bounds
have h : i ∈ (ratHints.map (fun x => x.1)).data := by
have h : i ∈ (ratHints.map (fun x => x.1)).toList := by
rw [← of_decide_eq_true ratHintsExhaustive_eq_true]
have i_eq_range_i : i = (Array.range f.clauses.size)[i]'i_in_bounds := by
rw [Array.getElem_range]
rw [i_eq_range_i]
rw [Array.mem_data]
rw [Array.mem_toList]
rw [Array.mem_filter]
constructor
· rw [← Array.mem_data]
apply Array.getElem_mem_data
· rw [← Array.getElem_eq_data_getElem] at c'_in_f
· rw [← Array.mem_toList]
apply Array.getElem_mem_toList
· rw [← Array.getElem_eq_toList_getElem] at c'_in_f
simp only [getElem!, Array.getElem_range, i_lt_f_clauses_size, dite_true,
c'_in_f, DefaultClause.contains_iff, Array.get_eq_getElem, decidableGetElem?]
simpa [Clause.toList] using negPivot_in_c'
rcases List.get_of_mem h with ⟨j, h'⟩
have j_in_bounds : j < ratHints.size := by
have j_property := j.2
simp only [Array.map_data, List.length_map] at j_property
simp only [Array.map_toList, List.length_map] at j_property
dsimp at *
omega
simp only [List.get_eq_getElem, Array.map_data, Array.data_length, List.getElem_map] at h'
rw [← Array.getElem_eq_data_getElem] at h'
rw [← Array.getElem_eq_data_getElem] at c'_in_f
simp only [List.get_eq_getElem, Array.map_toList, Array.toList_length, List.getElem_map] at h'
rw [← Array.getElem_eq_toList_getElem] at h'
rw [← Array.getElem_eq_toList_getElem] at c'_in_f
exists ⟨j.1, j_in_bounds⟩
simp [getElem!, h', i_lt_f_clauses_size, dite_true, c'_in_f, decidableGetElem?]
@ -559,7 +559,7 @@ theorem safe_insert_of_performRatCheck_fold_success {n : Nat} (f : DefaultFormul
simp only [formulaEntails_def, List.all_eq_true, decide_eq_true_eq, Classical.not_forall,
not_imp] at fc_unsat
rcases fc_unsat with ⟨c', c'_in_fc, p'_not_entails_c'⟩
simp only [insert_iff, Array.toList_eq, Array.data_toArray, List.mem_singleton] at c'_in_fc
simp only [insert_iff, Array.toList_toArray, List.mem_singleton] at c'_in_fc
rcases c'_in_fc with c'_eq_c | c'_in_f
· rw [← c'_eq_c] at p'_entails_c
exact p'_not_entails_c' p'_entails_c

56
src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean
View file

@ -746,13 +746,13 @@ theorem size_assignemnts_confirmRupHint {n : Nat} (clauses : Array (Option (Defa
theorem size_assignments_performRupCheck {n : Nat} (f : DefaultFormula n) (rupHints : Array Nat) :
(performRupCheck f rupHints).1.assignments.size = f.assignments.size := by
simp only [performRupCheck]
rw [Array.foldl_eq_foldl_data]
rw [Array.foldl_eq_foldl_toList]
have hb : (f.assignments, ([] : CNF.Clause (PosFin n)), false, false).1.size = f.assignments.size := rfl
have hl (acc : Array Assignment × CNF.Clause (PosFin n) × Bool × Bool) (hsize : acc.1.size = f.assignments.size)
(id : Nat) (_ : id ∈ rupHints.data) : (confirmRupHint f.clauses acc id).1.size = f.assignments.size := by
(id : Nat) (_ : id ∈ rupHints.toList) : (confirmRupHint f.clauses acc id).1.size = f.assignments.size := by
have h := size_assignemnts_confirmRupHint f.clauses acc.1 acc.2.1 acc.2.2.1 acc.2.2.2 id
rw [h, hsize]
exact List.foldlRecOn rupHints.data (confirmRupHint f.clauses) (f.assignments, [], false, false) hb hl
exact List.foldlRecOn rupHints.toList (confirmRupHint f.clauses) (f.assignments, [], false, false) hb hl
def DerivedLitsInvariant {n : Nat} (f : DefaultFormula n)
(fassignments_size : f.assignments.size = n) (assignments : Array Assignment)
@ -1112,13 +1112,13 @@ theorem nodup_derivedLits {n : Nat} (f : DefaultFormula n)
(derivedLits : CNF.Clause (PosFin n))
(derivedLits_satisfies_invariant:
DerivedLitsInvariant f f_assignments_size (performRupCheck f rupHints).fst.assignments f'_assignments_size derivedLits)
(derivedLits_arr : Array (Literal (PosFin n))) (derivedLits_arr_def: derivedLits_arr = { data := derivedLits })
(derivedLits_arr : Array (Literal (PosFin n))) (derivedLits_arr_def: derivedLits_arr = { toList := derivedLits })
(i j : Fin (Array.size derivedLits_arr)) (i_ne_j : i ≠ j) :
derivedLits_arr[i] ≠ derivedLits_arr[j] := by
intro li_eq_lj
let li := derivedLits_arr[i]
have li_in_derivedLits : li ∈ derivedLits := by
rw [Array.mem_data, ← derivedLits_arr_def]
rw [Array.mem_toList, ← derivedLits_arr_def]
simp only [li, Array.getElem?_mem]
have i_in_bounds : i.1 < derivedLits.length := by
have i_property := i.2
@ -1140,25 +1140,25 @@ theorem nodup_derivedLits {n : Nat} (f : DefaultFormula n)
specialize h3 ⟨j.1, j_in_bounds⟩ j_ne_k
simp only [derivedLits_arr_def, Fin.getElem_fin] at li_eq_lj
simp only [Fin.getElem_fin, derivedLits_arr_def, ne_eq, li, li_eq_lj] at h3
simp only [List.get_eq_getElem, Array.getElem_eq_data_getElem, not_true_eq_false] at h3
simp only [List.get_eq_getElem, Array.getElem_eq_toList_getElem, not_true_eq_false] at h3
· next k_ne_i =>
have i_ne_k : ⟨i.1, i_in_bounds⟩ ≠ k := by intro i_eq_k; simp only [← i_eq_k, not_true] at k_ne_i
specialize h3 ⟨i.1, i_in_bounds⟩ i_ne_k
simp (config := { decide := true }) [Fin.getElem_fin, derivedLits_arr_def, ne_eq,
Array.getElem_eq_data_getElem, li] at h3
Array.getElem_eq_toList_getElem, li] at h3
· by_cases li.2 = true
· next li_eq_true =>
have i_ne_k2 : ⟨i.1, i_in_bounds⟩ ≠ k2 := by
intro i_eq_k2
rw [← i_eq_k2] at k2_eq_false
simp only [List.get_eq_getElem] at k2_eq_false
simp [derivedLits_arr_def, Array.getElem_eq_data_getElem, k2_eq_false, li] at li_eq_true
simp [derivedLits_arr_def, Array.getElem_eq_toList_getElem, k2_eq_false, li] at li_eq_true
have j_ne_k2 : ⟨j.1, j_in_bounds⟩ ≠ k2 := by
intro j_eq_k2
rw [← j_eq_k2] at k2_eq_false
simp only [List.get_eq_getElem] at k2_eq_false
simp only [derivedLits_arr_def, Fin.getElem_fin, Array.getElem_eq_data_getElem] at li_eq_lj
simp [derivedLits_arr_def, Array.getElem_eq_data_getElem, k2_eq_false, li_eq_lj, li] at li_eq_true
simp only [derivedLits_arr_def, Fin.getElem_fin, Array.getElem_eq_toList_getElem] at li_eq_lj
simp [derivedLits_arr_def, Array.getElem_eq_toList_getElem, k2_eq_false, li_eq_lj, li] at li_eq_true
by_cases ⟨i.1, i_in_bounds⟩ = k1
· next i_eq_k1 =>
have j_ne_k1 : ⟨j.1, j_in_bounds⟩ ≠ k1 := by
@ -1167,11 +1167,11 @@ theorem nodup_derivedLits {n : Nat} (f : DefaultFormula n)
simp only [Fin.mk.injEq] at i_eq_k1
exact i_ne_j (Fin.eq_of_val_eq i_eq_k1)
specialize h3 ⟨j.1, j_in_bounds⟩ j_ne_k1 j_ne_k2
simp [li, li_eq_lj, derivedLits_arr_def, Array.getElem_eq_data_getElem] at h3
simp [li, li_eq_lj, derivedLits_arr_def, Array.getElem_eq_toList_getElem] at h3
· next i_ne_k1 =>
specialize h3 ⟨i.1, i_in_bounds⟩ i_ne_k1 i_ne_k2
apply h3
simp (config := { decide := true }) only [Fin.getElem_fin, Array.getElem_eq_data_getElem,
simp (config := { decide := true }) only [Fin.getElem_fin, Array.getElem_eq_toList_getElem,
ne_eq, derivedLits_arr_def, li]
rfl
· next li_eq_false =>
@ -1180,13 +1180,13 @@ theorem nodup_derivedLits {n : Nat} (f : DefaultFormula n)
intro i_eq_k1
rw [← i_eq_k1] at k1_eq_true
simp only [List.get_eq_getElem] at k1_eq_true
simp [derivedLits_arr_def, Array.getElem_eq_data_getElem, k1_eq_true, li] at li_eq_false
simp [derivedLits_arr_def, Array.getElem_eq_toList_getElem, k1_eq_true, li] at li_eq_false
have j_ne_k1 : ⟨j.1, j_in_bounds⟩ ≠ k1 := by
intro j_eq_k1
rw [← j_eq_k1] at k1_eq_true
simp only [List.get_eq_getElem] at k1_eq_true
simp only [derivedLits_arr_def, Fin.getElem_fin, Array.getElem_eq_data_getElem] at li_eq_lj
simp [derivedLits_arr_def, Array.getElem_eq_data_getElem, k1_eq_true, li_eq_lj, li] at li_eq_false
simp only [derivedLits_arr_def, Fin.getElem_fin, Array.getElem_eq_toList_getElem] at li_eq_lj
simp [derivedLits_arr_def, Array.getElem_eq_toList_getElem, k1_eq_true, li_eq_lj, li] at li_eq_false
by_cases ⟨i.1, i_in_bounds⟩ = k2
· next i_eq_k2 =>
have j_ne_k2 : ⟨j.1, j_in_bounds⟩ ≠ k2 := by
@ -1195,17 +1195,17 @@ theorem nodup_derivedLits {n : Nat} (f : DefaultFormula n)
simp only [Fin.mk.injEq] at i_eq_k2
exact i_ne_j (Fin.eq_of_val_eq i_eq_k2)
specialize h3 ⟨j.1, j_in_bounds⟩ j_ne_k1 j_ne_k2
simp [li, li_eq_lj, derivedLits_arr_def, Array.getElem_eq_data_getElem] at h3
simp [li, li_eq_lj, derivedLits_arr_def, Array.getElem_eq_toList_getElem] at h3
· next i_ne_k2 =>
specialize h3 ⟨i.1, i_in_bounds⟩ i_ne_k1 i_ne_k2
simp (config := { decide := true }) [Array.getElem_eq_data_getElem, derivedLits_arr_def, li] at h3
simp (config := { decide := true }) [Array.getElem_eq_toList_getElem, derivedLits_arr_def, li] at h3
theorem restoreAssignments_performRupCheck_base_case {n : Nat} (f : DefaultFormula n)
(f_assignments_size : f.assignments.size = n)
(f' : DefaultFormula n) (_f'_def : f' = (performRupCheck f rupHints).1)
(f'_assignments_size : f'.assignments.size = n) (derivedLits : CNF.Clause (PosFin n))
(derivedLits_arr : Array (Literal (PosFin n)))
(derivedLits_arr_def : derivedLits_arr = {data := derivedLits})
(derivedLits_arr_def : derivedLits_arr = {toList := derivedLits})
(derivedLits_satisfies_invariant :
DerivedLitsInvariant f f_assignments_size f'.assignments f'_assignments_size derivedLits)
(_derivedLits_arr_nodup : ∀ (i j : Fin (Array.size derivedLits_arr)), i ≠ j → derivedLits_arr[i] ≠ derivedLits_arr[j]) :
@ -1221,7 +1221,7 @@ theorem restoreAssignments_performRupCheck_base_case {n : Nat} (f : DefaultFormu
· intro j _
have idx_in_list : derivedLits_arr[j] ∈ derivedLits := by
simp only [derivedLits_arr_def, Fin.getElem_fin]
apply Array.getElem_mem_data
apply Array.getElem_mem_toList
exact h2 derivedLits_arr[j] idx_in_list
· apply Or.inr ∘ Or.inl
have j_lt_derivedLits_arr_size : j.1 < derivedLits_arr.size := by
@ -1232,7 +1232,7 @@ theorem restoreAssignments_performRupCheck_base_case {n : Nat} (f : DefaultFormu
constructor
· apply Nat.zero_le
· constructor
· simp only [derivedLits_arr_def, Fin.getElem_fin, Array.getElem_eq_data_getElem, ← j_eq_i]
· simp only [derivedLits_arr_def, Fin.getElem_fin, Array.getElem_eq_toList_getElem, ← j_eq_i]
rfl
· apply And.intro h1 ∘ And.intro h2
intro k _ k_ne_j
@ -1244,7 +1244,7 @@ theorem restoreAssignments_performRupCheck_base_case {n : Nat} (f : DefaultFormu
apply Fin.ne_of_val_ne
simp only
exact Fin.val_ne_of_ne k_ne_j
simp only [Fin.getElem_fin, Array.getElem_eq_data_getElem, ne_eq, derivedLits_arr_def]
simp only [Fin.getElem_fin, Array.getElem_eq_toList_getElem, ne_eq, derivedLits_arr_def]
exact h3 ⟨k.1, k_in_bounds⟩ k_ne_j
· apply Or.inr ∘ Or.inr
have j1_lt_derivedLits_arr_size : j1.1 < derivedLits_arr.size := by
@ -1258,11 +1258,11 @@ theorem restoreAssignments_performRupCheck_base_case {n : Nat} (f : DefaultFormu
⟨j2.1, j2_lt_derivedLits_arr_size⟩,
i_gt_zero, Nat.zero_le j1.1, Nat.zero_le j2.1, ?_⟩
constructor
· simp only [derivedLits_arr_def, Fin.getElem_fin, Array.getElem_eq_data_getElem, ← j1_eq_i]
· simp only [derivedLits_arr_def, Fin.getElem_fin, Array.getElem_eq_toList_getElem, ← j1_eq_i]
rw [← j1_eq_true]
rfl
· constructor
· simp only [derivedLits_arr_def, Fin.getElem_fin, Array.getElem_eq_data_getElem, ← j2_eq_i]
· simp only [derivedLits_arr_def, Fin.getElem_fin, Array.getElem_eq_toList_getElem, ← j2_eq_i]
rw [← j2_eq_false]
rfl
· apply And.intro h1 ∘ And.intro h2
@ -1279,7 +1279,7 @@ theorem restoreAssignments_performRupCheck_base_case {n : Nat} (f : DefaultFormu
apply Fin.ne_of_val_ne
simp only
exact Fin.val_ne_of_ne k_ne_j2
simp only [Fin.getElem_fin, Array.getElem_eq_data_getElem, ne_eq, derivedLits_arr_def]
simp only [Fin.getElem_fin, Array.getElem_eq_toList_getElem, ne_eq, derivedLits_arr_def]
exact h3 ⟨k.1, k_in_bounds⟩ k_ne_j1 k_ne_j2
theorem restoreAssignments_performRupCheck {n : Nat} (f : DefaultFormula n) (f_assignments_size : f.assignments.size = n)
@ -1295,9 +1295,9 @@ theorem restoreAssignments_performRupCheck {n : Nat} (f : DefaultFormula n) (f_a
have derivedLits_satisfies_invariant := derivedLitsInvariant_performRupCheck f f_assignments_size rupHints f'_assignments_size
simp only at derivedLits_satisfies_invariant
generalize (performRupCheck f rupHints).2.1 = derivedLits at *
rw [← f'_def, ← Array.foldl_eq_foldl_data]
let derivedLits_arr : Array (Literal (PosFin n)) := {data := derivedLits}
have derivedLits_arr_def : derivedLits_arr = {data := derivedLits} := rfl
rw [← f'_def, ← Array.foldl_eq_foldl_toList]
let derivedLits_arr : Array (Literal (PosFin n)) := {toList := derivedLits}
have derivedLits_arr_def : derivedLits_arr = {toList := derivedLits} := rfl
have derivedLits_arr_nodup := nodup_derivedLits f f_assignments_size rupHints f'_assignments_size derivedLits
derivedLits_satisfies_invariant derivedLits_arr derivedLits_arr_def
let motive := ClearInsertInductionMotive f f_assignments_size derivedLits_arr
@ -1308,7 +1308,7 @@ theorem restoreAssignments_performRupCheck {n : Nat} (f : DefaultFormula n) (f_a
clear_insert_inductive_case f f_assignments_size derivedLits_arr derivedLits_arr_nodup idx assignments ih
rcases Array.foldl_induction motive h_base h_inductive with ⟨h_size, h⟩
apply Array.ext
· rw [Array.foldl_eq_foldl_data, size_clearUnit_foldl f'.assignments clearUnit size_clearUnit derivedLits,
· rw [Array.foldl_eq_foldl_toList, size_clearUnit_foldl f'.assignments clearUnit size_clearUnit derivedLits,
f'_assignments_size, f_assignments_size]
· intro i hi1 hi2
rw [f_assignments_size] at hi2

66
src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean
View file

@ -92,25 +92,25 @@ theorem contradiction_of_insertUnit_fold_success {n : Nat} (assignments : Array
theorem mem_insertUnit_units {n : Nat} (units : Array (Literal (PosFin n))) (assignments : Array Assignment)
(foundContradiction : Bool) (l : Literal (PosFin n)) :
let insertUnit_res := insertUnit (units, assignments, foundContradiction) l
∀ l' : Literal (PosFin n), l' ∈ insertUnit_res.1.data → l' = l ∨ l' ∈ units.data := by
∀ l' : Literal (PosFin n), l' ∈ insertUnit_res.1.toList → l' = l ∨ l' ∈ units.toList := by
intro insertUnit_res l' l'_in_insertUnit_res
simp only [insertUnit_res] at *
simp only [insertUnit] at l'_in_insertUnit_res
split at l'_in_insertUnit_res
· exact Or.inr l'_in_insertUnit_res
· simp only [Array.push_data, List.mem_append, List.mem_singleton] at l'_in_insertUnit_res
· simp only [Array.push_toList, List.mem_append, List.mem_singleton] at l'_in_insertUnit_res
exact Or.symm l'_in_insertUnit_res
theorem mem_insertUnit_fold_units {n : Nat} (units : Array (Literal (PosFin n))) (assignments : Array Assignment)
(foundContradiction : Bool) (l : CNF.Clause (PosFin n)) :
let insertUnit_fold_res := List.foldl insertUnit (units, assignments, foundContradiction) l
∀ l' : Literal (PosFin n), l' ∈ insertUnit_fold_res.1.data → l' ∈ l ∨ l' ∈ units.data := by
have hb (l' : Literal (PosFin n)) : l' ∈ (units, assignments, foundContradiction).1.data → l' ∈ l ∨ l' ∈ units.data := by
∀ l' : Literal (PosFin n), l' ∈ insertUnit_fold_res.1.toList → l' ∈ l ∨ l' ∈ units.toList := by
have hb (l' : Literal (PosFin n)) : l' ∈ (units, assignments, foundContradiction).1.toList → l' ∈ l ∨ l' ∈ units.toList := by
intro h
exact Or.inr h
have hl (acc : Array (Literal (PosFin n)) × Array Assignment × Bool)
(h : ∀ l' : Literal (PosFin n), l' ∈ acc.1.data → l' ∈ l ∨ l' ∈ units.data) (l'' : Literal (PosFin n))
(l''_in_l : l'' ∈ l) : ∀ l' : Literal (PosFin n), l' ∈ (insertUnit acc l'').1.data → l' ∈ l ∨ l' ∈ units.data := by
(h : ∀ l' : Literal (PosFin n), l' ∈ acc.1.toList → l' ∈ l ∨ l' ∈ units.toList) (l'' : Literal (PosFin n))
(l''_in_l : l'' ∈ l) : ∀ l' : Literal (PosFin n), l' ∈ (insertUnit acc l'').1.toList → l' ∈ l ∨ l' ∈ units.toList := by
intro l' l'_in_res
rcases mem_insertUnit_units acc.1 acc.2.1 acc.2.2 l'' l' l'_in_res with l'_eq_l'' | l'_in_acc
· rw [l'_eq_l'']
@ -150,13 +150,13 @@ theorem sat_of_insertRup {n : Nat} (f : DefaultFormula n) (f_readyForRupAdd : Re
simp [p_entails_i_true] at p_entails_i_false
· simp only [(· ⊨ ·), Clause.eval, List.any_eq_true, Prod.exists, Bool.exists_bool, Bool.decide_coe]
apply Exists.intro i
have ib_in_insertUnit_fold : (i, b) ∈ (List.foldl insertUnit (f.rupUnits, f.assignments, false) (negate c)).1.data := by
have ib_in_insertUnit_fold : (i, b) ∈ (List.foldl insertUnit (f.rupUnits, f.assignments, false) (negate c)).1.toList := by
have i_rw : i = ⟨i.1, i.2⟩ := rfl
rw [i_rw, ← h1]
apply List.get_mem
have ib_in_insertUnit_fold := mem_insertUnit_fold_units f.rupUnits f.assignments false (negate c) (i, b) ib_in_insertUnit_fold
simp only [negate, Literal.negate, List.mem_map, Prod.mk.injEq, Prod.exists, Bool.exists_bool,
Bool.not_false, Bool.not_true, f_readyForRupAdd.1, Array.data_toArray, List.find?, List.not_mem_nil, or_false]
Bool.not_false, Bool.not_true, f_readyForRupAdd.1, Array.toList_toArray, List.find?, List.not_mem_nil, or_false]
at ib_in_insertUnit_fold
rw [hboth] at h2
rcases ib_in_insertUnit_fold with ⟨i', ⟨i_false_in_c, i'_eq_i, b_eq_true⟩ | ⟨i_true_in_c, i'_eq_i, b_eq_false⟩⟩
@ -196,11 +196,11 @@ theorem sat_of_insertRup {n : Nat} (f : DefaultFormula n) (f_readyForRupAdd : Re
exact h3 (has_both b)
· simp at h2
· exfalso
have i_true_in_insertUnit_fold : (i, true) ∈ (List.foldl insertUnit (f.rupUnits, f.assignments, false) (negate c)).1.data := by
have i_true_in_insertUnit_fold : (i, true) ∈ (List.foldl insertUnit (f.rupUnits, f.assignments, false) (negate c)).1.toList := by
have i_rw : i = ⟨i.1, i.2⟩ := rfl
rw [i_rw, ← h1]
apply List.get_mem
have i_false_in_insertUnit_fold : (i, false) ∈ (List.foldl insertUnit (f.rupUnits, f.assignments, false) (negate c)).1.data := by
have i_false_in_insertUnit_fold : (i, false) ∈ (List.foldl insertUnit (f.rupUnits, f.assignments, false) (negate c)).1.toList := by
have i_rw : i = ⟨i.1, i.2⟩ := rfl
rw [i_rw, ← h2]
apply List.get_mem
@ -210,7 +210,7 @@ theorem sat_of_insertRup {n : Nat} (f : DefaultFormula n) (f_readyForRupAdd : Re
have i_false_in_insertUnit_fold :=
mem_insertUnit_fold_units #[] f.assignments false (c.clause.map Literal.negate) (i, false) i_false_in_insertUnit_fold
simp only [Literal.negate, List.mem_map, Prod.mk.injEq, Bool.not_eq_true', Prod.exists,
exists_eq_right_right, exists_eq_right, Array.data_toArray, List.find?, List.not_mem_nil, or_false,
exists_eq_right_right, exists_eq_right, Array.toList_toArray, List.find?, List.not_mem_nil, or_false,
Bool.not_eq_false'] at i_true_in_insertUnit_fold i_false_in_insertUnit_fold
have c_not_tautology := Clause.not_tautology c (i, true)
simp only [Clause.toList, (· ⊨ ·)] at c_not_tautology
@ -240,18 +240,18 @@ theorem assignmentsInvariant_insertRupUnits_of_assignmentsInvariant {n : Nat} (f
apply Exists.intro hsize
intro i b hb p hp
simp only [(· ⊨ ·), Clause.eval] at hp
simp only [toList, Array.toList_eq, List.append_assoc, List.any_eq_true, Prod.exists,
simp only [toList, List.append_assoc, List.any_eq_true, Prod.exists,
Bool.exists_bool, Bool.decide_coe, List.all_eq_true, List.mem_append, List.mem_filterMap, id_eq,
exists_eq_right, List.mem_map] at hp
have pf : p ⊨ f := by
simp only [(· ⊨ ·), Clause.eval]
simp only [toList, Array.toList_eq, List.append_assoc, List.any_eq_true, Prod.exists, Bool.exists_bool,
simp only [toList, List.append_assoc, List.any_eq_true, Prod.exists, Bool.exists_bool,
Bool.decide_coe, List.all_eq_true, List.mem_append, List.mem_filterMap, id_eq, exists_eq_right, List.mem_map]
intro c cf
rcases cf with cf | cf | cf
· specialize hp c (Or.inl cf)
exact hp
· simp only [f_readyForRupAdd.1, Array.data_toArray, List.find?, List.not_mem_nil, false_and, or_self, exists_false] at cf
· simp only [f_readyForRupAdd.1, Array.toList_toArray, List.find?, List.not_mem_nil, false_and, or_self, exists_false] at cf
· specialize hp c <| (Or.inr ∘ Or.inr) cf
exact hp
rcases h ⟨i.1, i.2.2⟩ with ⟨h1, h2⟩ | ⟨j, b', i_gt_zero, h1, h2, h3, h4⟩ | ⟨j1, j2, i_gt_zero, h1, h2, _, _, _⟩
@ -264,8 +264,8 @@ theorem assignmentsInvariant_insertRupUnits_of_assignmentsInvariant {n : Nat} (f
have j_unit_def : j_unit = unit (insertRupUnits f units).1.rupUnits[j] := rfl
have j_unit_in_insertRupUnits_res :
∃ i : PosFin n,
(i, false) ∈ (insertRupUnits f units).1.rupUnits.data ∧ unit (i, false) = j_unit ∨
(i, true) ∈ (insertRupUnits f units).1.rupUnits.data ∧ unit (i, true) = j_unit := by
(i, false) ∈ (insertRupUnits f units).1.rupUnits.toList ∧ unit (i, false) = j_unit ∨
(i, true) ∈ (insertRupUnits f units).1.rupUnits.toList ∧ unit (i, true) = j_unit := by
apply Exists.intro i
rw [j_unit_def, h1]
by_cases hb' : b'
@ -278,7 +278,7 @@ theorem assignmentsInvariant_insertRupUnits_of_assignmentsInvariant {n : Nat} (f
simp only [Prod.mk.injEq, and_true]
rfl
rw [← h1]
apply Array.getElem_mem_data
apply Array.getElem_mem_toList
· rfl
· simp only [Bool.not_eq_true] at hb'
rw [hb']
@ -290,7 +290,7 @@ theorem assignmentsInvariant_insertRupUnits_of_assignmentsInvariant {n : Nat} (f
simp only [Prod.mk.injEq, and_true]
rfl
rw [← h1]
apply Array.getElem_mem_data
apply Array.getElem_mem_toList
· rfl
specialize hp j_unit ((Or.inr ∘ Or.inl) j_unit_in_insertRupUnits_res)
simp only [List.any_eq_true, Prod.exists, Bool.exists_bool, Bool.decide_coe, Fin.getElem_fin, List.find?, j_unit] at hp
@ -314,8 +314,8 @@ theorem assignmentsInvariant_insertRupUnits_of_assignmentsInvariant {n : Nat} (f
have j1_unit_def : j1_unit = unit (insertRupUnits f units).1.rupUnits[j1] := rfl
have j1_unit_in_insertRupUnits_res :
∃ i : PosFin n,
(i, false) ∈ (insertRupUnits f units).1.rupUnits.data ∧ unit (i, false) = j1_unit ∨
(i, true) ∈ (insertRupUnits f units).1.rupUnits.data ∧ unit (i, true) = j1_unit := by
(i, false) ∈ (insertRupUnits f units).1.rupUnits.toList ∧ unit (i, false) = j1_unit ∨
(i, true) ∈ (insertRupUnits f units).1.rupUnits.toList ∧ unit (i, true) = j1_unit := by
apply Exists.intro i ∘ Or.inr
rw [j1_unit_def, h1]
constructor
@ -324,14 +324,14 @@ theorem assignmentsInvariant_insertRupUnits_of_assignmentsInvariant {n : Nat} (f
simp only [Prod.mk.injEq, and_true]
rfl
rw [← h1]
apply Array.getElem_mem_data
apply Array.getElem_mem_toList
· rfl
let j2_unit := unit (insertRupUnits f units).1.rupUnits[j2]
have j2_unit_def : j2_unit = unit (insertRupUnits f units).1.rupUnits[j2] := rfl
have j2_unit_in_insertRupUnits_res :
∃ i : PosFin n,
(i, false) ∈ (insertRupUnits f units).1.rupUnits.data ∧ unit (i, false) = j2_unit ∨
(i, true) ∈ (insertRupUnits f units).1.rupUnits.data ∧ unit (i, true) = j2_unit := by
(i, false) ∈ (insertRupUnits f units).1.rupUnits.toList ∧ unit (i, false) = j2_unit ∨
(i, true) ∈ (insertRupUnits f units).1.rupUnits.toList ∧ unit (i, true) = j2_unit := by
apply Exists.intro i ∘ Or.inl
rw [j2_unit_def, h2]
constructor
@ -340,7 +340,7 @@ theorem assignmentsInvariant_insertRupUnits_of_assignmentsInvariant {n : Nat} (f
simp only [Prod.mk.injEq, and_true]
rfl
rw [← h2]
apply Array.getElem_mem_data
apply Array.getElem_mem_toList
· rfl
have hp1 := hp j1_unit ((Or.inr ∘ Or.inl) j1_unit_in_insertRupUnits_res)
have hp2 := hp j2_unit ((Or.inr ∘ Or.inl) j2_unit_in_insertRupUnits_res)
@ -544,8 +544,8 @@ theorem reduce_postcondition {n : Nat} (c : DefaultClause n) (assignment : Array
(reduce c assignment = reducedToEmpty → Incompatible (PosFin n) c assignment) ∧
(∀ l : Literal (PosFin n), reduce c assignment = reducedToUnit l → ∀ (p : (PosFin n) → Bool), p ⊨ assignment → p ⊨ c → p ⊨ l) := by
let c_arr := Array.mk c.clause
have c_clause_rw : c.clause = c_arr.data := rfl
rw [reduce, c_clause_rw, ← Array.foldl_eq_foldl_data]
have c_clause_rw : c.clause = c_arr.toList := rfl
rw [reduce, c_clause_rw, ← Array.foldl_eq_foldl_toList]
let motive := ReducePostconditionInductionMotive c_arr assignment
have h_base : motive 0 reducedToEmpty := by
have : ∀ (a : PosFin n) (b : Bool), (reducedToEmpty = reducedToUnit (a, b)) = False := by intros; simp
@ -571,7 +571,7 @@ theorem reduce_postcondition {n : Nat} (c : DefaultClause n) (assignment : Array
rw [c_clause_rw] at pc1
have idx_exists : ∃ idx : Fin c_arr.size, c_arr[idx] = (i, false) := by
rcases List.get_of_mem pc1 with ⟨idx, hidx⟩
rw [← Array.getElem_fin_eq_data_get] at hidx
rw [← Array.getElem_fin_eq_toList_get] at hidx
exact Exists.intro idx hidx
rcases idx_exists with ⟨idx, hidx⟩
specialize h1 idx idx.2
@ -581,7 +581,7 @@ theorem reduce_postcondition {n : Nat} (c : DefaultClause n) (assignment : Array
rw [c_clause_rw] at pc1
have idx_exists : ∃ idx : Fin c_arr.size, c_arr[idx] = (i, true) := by
rcases List.get_of_mem pc1 with ⟨idx, hidx⟩
rw [← Array.getElem_fin_eq_data_get] at hidx
rw [← Array.getElem_fin_eq_toList_get] at hidx
exact Exists.intro idx hidx
rcases idx_exists with ⟨idx, hidx⟩
specialize h1 idx idx.2
@ -596,7 +596,7 @@ theorem reduce_postcondition {n : Nat} (c : DefaultClause n) (assignment : Array
rw [c_clause_rw] at pc1
have idx_exists : ∃ idx : Fin c_arr.size, c_arr[idx] = (i, false) := by
rcases List.get_of_mem pc1 with ⟨idx, hidx⟩
rw [← Array.getElem_fin_eq_data_get] at hidx
rw [← Array.getElem_fin_eq_toList_get] at hidx
exact Exists.intro idx hidx
rcases idx_exists with ⟨idx, hidx⟩
apply Exists.intro idx ∘ And.intro idx.2
@ -607,7 +607,7 @@ theorem reduce_postcondition {n : Nat} (c : DefaultClause n) (assignment : Array
rw [c_clause_rw] at pc1
have idx_exists : ∃ idx : Fin c_arr.size, c_arr[idx] = (i, true) := by
rcases List.get_of_mem pc1 with ⟨idx, hidx⟩
rw [← Array.getElem_fin_eq_data_get] at hidx
rw [← Array.getElem_fin_eq_toList_get] at hidx
exact Exists.intro idx hidx
rcases idx_exists with ⟨idx, hidx⟩
apply Exists.intro idx ∘ And.intro idx.2
@ -638,14 +638,14 @@ theorem confirmRupHint_preserves_motive {n : Nat} (f : DefaultFormula n) (rupHin
split
· next c hc =>
have c_in_f : c ∈ toList f := by
simp only [toList, Array.toList_eq, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
simp only [toList, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
exists_eq_right, List.mem_map, Prod.exists, Bool.exists_bool]
apply Or.inl
simp only [getElem?, decidableGetElem?] at hc
split at hc
· simp only [Option.some.injEq] at hc
rw [← hc]
apply Array.getElem_mem_data
apply Array.getElem_mem_toList
· simp at hc
split
· next heq =>
@ -745,7 +745,7 @@ theorem sat_of_confirmRupHint_insertRup_fold {n : Nat} (f : DefaultFormula n)
not_imp] at fc_unsat
rcases fc_unsat with ⟨unsat_c, unsat_c_in_fc, p_unsat_c⟩
have unsat_c_in_fc := mem_of_insertRupUnits f (negate c) unsat_c unsat_c_in_fc
simp only [Array.toList_eq, List.mem_map, Prod.exists, Bool.exists_bool] at unsat_c_in_fc
simp only [List.mem_map, Prod.exists, Bool.exists_bool] at unsat_c_in_fc
rcases unsat_c_in_fc with ⟨v, ⟨v_in_neg_c, unsat_c_eq⟩ | ⟨v_in_neg_c, unsat_c_eq⟩⟩ | unsat_c_in_f
· simp only [negate_eq, List.mem_map, Prod.exists, Bool.exists_bool] at v_in_neg_c
rcases v_in_neg_c with ⟨v', ⟨_, v'_eq_v⟩ | ⟨v'_in_c, v'_eq_v⟩⟩

2
src/include/lean/lean.h
View file

@ -703,7 +703,7 @@ static inline void lean_array_set_core(u_lean_obj_arg o, size_t i, lean_obj_arg
lean_to_array(o)->m_data[i] = v;
}
LEAN_EXPORT lean_object * lean_array_mk(lean_obj_arg l);
LEAN_EXPORT lean_object * lean_array_data(lean_obj_arg a);
LEAN_EXPORT lean_object * lean_array_to_list(lean_obj_arg a);
/* Arrays of objects (high level API) */

2
src/lake/Lake/CLI/Actions.lean
View file

@ -78,7 +78,7 @@ def Package.lint (pkg : Package) (args : List String := []) (buildConfig : Build
let cfgArgs := pkg.lintDriverArgs
let (pkg, driver) ← pkg.resolveDriver "lint" pkg.lintDriver
if let some script := pkg.scripts.find? driver.toName then
script.run (cfgArgs.data ++ args)
script.run (cfgArgs.toList ++ args)
else if let some exe := pkg.findLeanExe? driver.toName then
let exeFile ← runBuild exe.fetch buildConfig
env exeFile.toString (cfgArgs ++ args.toArray)

2
src/library/compiler/erase_irrelevant.cpp
View file

@ -215,7 +215,7 @@ class erase_irrelevant_fn {
expr minor = visit_minor(args[3]);
lean_always_assert(is_lambda(minor));
return
::lean::mk_let(next_name(), mk_enf_object_type(), mk_app(mk_constant(get_array_data_name()), mk_enf_neutral(), major),
::lean::mk_let(next_name(), mk_enf_object_type(), mk_app(mk_constant(get_array_to_list_name()), mk_enf_neutral(), major),
binding_body(minor));
}

10
src/library/constants.cpp
View file

@ -12,7 +12,7 @@ name const * g_and_rec = nullptr;
name const * g_and_cases_on = nullptr;
name const * g_array = nullptr;
name const * g_array_sz = nullptr;
name const * g_array_data = nullptr;
name const * g_array_to_list = nullptr;
name const * g_auto_param = nullptr;
name const * g_bit0 = nullptr;
name const * g_bit1 = nullptr;
@ -127,8 +127,8 @@ void initialize_constants() {
mark_persistent(g_array->raw());
g_array_sz = new name{"Array", "sz"};
mark_persistent(g_array_sz->raw());
g_array_data = new name{"Array", "data"};
mark_persistent(g_array_data->raw());
g_array_to_list = new name{"Array", "toList"};
mark_persistent(g_array_to_list->raw());
g_auto_param = new name{"autoParam"};
mark_persistent(g_auto_param->raw());
g_bit0 = new name{"bit0"};
@ -330,7 +330,7 @@ void finalize_constants() {
delete g_and_cases_on;
delete g_array;
delete g_array_sz;
delete g_array_data;
delete g_array_to_list;
delete g_auto_param;
delete g_bit0;
delete g_bit1;
@ -436,7 +436,7 @@ name const & get_and_rec_name() { return *g_and_rec; }
name const & get_and_cases_on_name() { return *g_and_cases_on; }
name const & get_array_name() { return *g_array; }
name const & get_array_sz_name() { return *g_array_sz; }
name const & get_array_data_name() { return *g_array_data; }
name const & get_array_to_list_name() { return *g_array_to_list; }
name const & get_auto_param_name() { return *g_auto_param; }
name const & get_bit0_name() { return *g_bit0; }
name const & get_bit1_name() { return *g_bit1; }

2
src/library/constants.h
View file

@ -14,7 +14,7 @@ name const & get_and_rec_name();
name const & get_and_cases_on_name();
name const & get_array_name();
name const & get_array_sz_name();
name const & get_array_data_name();
name const & get_array_to_list_name();
name const & get_auto_param_name();
name const & get_bit0_name();
name const & get_bit1_name();

2
src/library/constants.txt
View file

@ -7,7 +7,7 @@ And.rec
And.casesOn
Array
Array.sz
Array.data
Array.toList
autoParam
bit0
bit1

6
src/runtime/object.cpp
View file

@ -364,14 +364,14 @@ object * array_mk_empty() {
}
extern "C" object * lean_list_to_array(object *, object *);
extern "C" object * lean_array_to_list(object *, object *);
extern "C" object * lean_array_to_list_impl(object *, object *);
extern "C" LEAN_EXPORT object * lean_array_mk(lean_obj_arg lst) {
return lean_list_to_array(lean_box(0), lst);
}
extern "C" LEAN_EXPORT lean_object * lean_array_data(lean_obj_arg a) {
return lean_array_to_list(lean_box(0), a);
extern "C" LEAN_EXPORT lean_object * lean_array_to_list(lean_obj_arg a) {
return lean_array_to_list_impl(lean_box(0), a);
}
extern "C" LEAN_EXPORT lean_obj_res lean_array_get_panic(lean_obj_arg def_val) {

2
tests/bench/liasolver.lean
View file

@ -392,5 +392,5 @@ def main (args : List String) : IO UInt32 := do
IO.println "UNSAT"
| Solution.sat assignment =>
IO.println "SAT"
IO.println <| String.intercalate " " <| assignment.data.map toString
IO.println <| String.intercalate " " <| assignment.toList.map toString
return 0

2
tests/compiler/array.lean
View file

@ -2,7 +2,7 @@
Array.casesOn (motive := fun _ => Nat) a (fun data => data.length)
@[noinline] def g (a : Array Nat) : List Nat :=
a.data
a.toList
@[noinline] def h (a : List Nat) : List Nat :=
g (Array.mk a)

4
tests/lean/run/PPTopDownAnalyze.lean
View file

@ -275,8 +275,8 @@ set_option pp.proofs.withType false in
end proofs
#testDelab ∀ (α : Type u) (vals vals_1 : List α), { data := vals : Array α } = { data := vals_1 : Array α }
expecting ∀ (α : Type u) (vals vals_1 : List α), { data := vals : Array α } = { data := vals_1 }
#testDelab ∀ (α : Type u) (vals vals_1 : List α), { toList := vals : Array α } = { toList := vals_1 : Array α }
expecting ∀ (α : Type u) (vals vals_1 : List α), { toList := vals : Array α } = { toList := vals_1 }
#testDelab (do let ctxCore ← readThe Core.Context; pure ctxCore.currNamespace : MetaM Name)
expecting do

2
tests/lean/run/structInstFast.lean
View file

@ -63,7 +63,7 @@ where go (val : TSyntax `ident) (width depth : Nat) (cmds : Array <| TSyntax `co
let cmd : TSyntax `command := ⟨mkNullNode cmds⟩
`($cmd:command)
| m+1 =>
let len := cmds.data.length
let len := cmds.toList.length
let newTerm (s : String) := if len = 1 then baseTypeIdent else mkIdent' s (m+1)
let newTerm' (s : String) := if len = 1 then baseIdent else mkIdent' s (m+1)
let fieldsStx ← mkFieldsStx type (s!"x{m}_") width

2
tests/lean/run/structuralMutual.lean
View file

@ -696,7 +696,7 @@ info: WithTuple.Tree.map.induct {α β : Type} (f : α → β) (motive_1 : WithT
info: WithArray.Tree.map.induct {α β : Type} (f : α → β) (motive_1 : WithArray.Tree α → Prop)
(motive_2 : Array (WithArray.Tree α) → Prop) (motive_3 : List (WithArray.Tree α) → Prop)
(case1 : ∀ (x : α) (arr₁ : Array (WithArray.Tree α)), motive_2 arr₁ → motive_1 (WithArray.Tree.node x arr₁))
(case2 : ∀ (arr₁ : List (WithArray.Tree α)), motive_3 arr₁ → motive_2 { data := arr₁ }) (case3 : motive_3 [])
(case2 : ∀ (arr₁ : List (WithArray.Tree α)), motive_3 arr₁ → motive_2 { toList := arr₁ }) (case3 : motive_3 [])
(case4 : ∀ (h₁ : WithArray.Tree α) (t₁ : List (WithArray.Tree α)), motive_1 h₁ → motive_3 t₁ → motive_3 (h₁ :: t₁))
(x : WithArray.Tree α) : motive_1 x
-/