feat: more iterator/range lemmas about toList and toArray (#10244)
This PR adds more lemmas about the `toList` and `toArray` functions on ranges and iterators. It also renames `Array.mem_toArray` into `List.mem_toArray`.
This commit is contained in:
Paul Reichert
GitHub
parent
b64111d5a8
commit
ae682ed225
16 changed files with 410 additions and 18 deletions
|
|
@ -121,7 +121,7 @@ theorem pmap_eq_map {p : α → Prop} {f : α → β} {xs : Array α} (H) :
|
|||
theorem pmap_congr_left {p q : α → Prop} {f : ∀ a, p a → β} {g : ∀ a, q a → β} (xs : Array α) {H₁ H₂}
|
||||
(h : ∀ a ∈ xs, ∀ (h₁ h₂), f a h₁ = g a h₂) : pmap f xs H₁ = pmap g xs H₂ := by
|
||||
cases xs
|
||||
simp only [mem_toArray] at h
|
||||
simp only [List.mem_toArray] at h
|
||||
simp only [List.pmap_toArray, mk.injEq]
|
||||
rw [List.pmap_congr_left _ h]
|
||||
|
||||
|
|
@ -346,7 +346,7 @@ theorem foldl_attach {xs : Array α} {f : β → α → β} {b : β} :
|
|||
xs.attach.foldl (fun acc t => f acc t.1) b = xs.foldl f b := by
|
||||
rcases xs with ⟨xs⟩
|
||||
simp only [List.attach_toArray, List.attachWith_mem_toArray, List.size_toArray,
|
||||
List.foldl_toArray', mem_toArray, List.foldl_subtype]
|
||||
List.foldl_toArray', List.mem_toArray, List.foldl_subtype]
|
||||
congr
|
||||
ext
|
||||
simpa using fun a => List.mem_of_getElem? a
|
||||
|
|
@ -365,7 +365,7 @@ theorem foldr_attach {xs : Array α} {f : α → β → β} {b : β} :
|
|||
xs.attach.foldr (fun t acc => f t.1 acc) b = xs.foldr f b := by
|
||||
rcases xs with ⟨xs⟩
|
||||
simp only [List.attach_toArray, List.attachWith_mem_toArray, List.size_toArray,
|
||||
List.foldr_toArray', mem_toArray, List.foldr_subtype]
|
||||
List.foldr_toArray', List.mem_toArray, List.foldr_subtype]
|
||||
congr
|
||||
ext
|
||||
simpa using fun a => List.mem_of_getElem? a
|
||||
|
|
|
|||
|
|
@ -108,9 +108,13 @@ instance : Membership α (Array α) where
|
|||
theorem mem_def {a : α} {as : Array α} : a ∈ as ↔ a ∈ as.toList :=
|
||||
⟨fun | .mk h => h, Array.Mem.mk⟩
|
||||
|
||||
@[simp, grind =] theorem mem_toArray {a : α} {l : List α} : a ∈ l.toArray ↔ a ∈ l := by
|
||||
@[simp, grind =] theorem _root_.List.mem_toArray {a : α} {l : List α} : a ∈ l.toArray ↔ a ∈ l := by
|
||||
simp [mem_def]
|
||||
|
||||
@[deprecated List.mem_toArray (since := "2025-09-04")]
|
||||
theorem mem_toArray {a : α} {l : List α} : a ∈ l.toArray ↔ a ∈ l :=
|
||||
List.mem_toArray
|
||||
|
||||
@[simp] theorem getElem_mem {xs : Array α} {i : Nat} (h : i < xs.size) : xs[i] ∈ xs := by
|
||||
rw [Array.mem_def, ← getElem_toList]
|
||||
apply List.getElem_mem
|
||||
|
|
|
|||
|
|
@ -271,7 +271,7 @@ theorem erase_append [LawfulBEq α] {a : α} {xs ys : Array α} :
|
|||
(xs ++ ys).erase a = if a ∈ xs then xs.erase a ++ ys else xs ++ ys.erase a := by
|
||||
rcases xs with ⟨xs⟩
|
||||
rcases ys with ⟨ys⟩
|
||||
simp only [List.append_toArray, List.erase_toArray, List.erase_append, mem_toArray]
|
||||
simp only [List.append_toArray, List.erase_toArray, List.erase_append, List.mem_toArray]
|
||||
split <;> simp
|
||||
|
||||
@[grind =]
|
||||
|
|
|
|||
|
|
@ -88,7 +88,7 @@ theorem eq_empty_iff_size_eq_zero : xs = #[] ↔ xs.size = 0 :=
|
|||
|
||||
theorem size_pos_of_mem {a : α} {xs : Array α} (h : a ∈ xs) : 0 < xs.size := by
|
||||
cases xs
|
||||
simp only [mem_toArray] at h
|
||||
simp only [List.mem_toArray] at h
|
||||
simpa using List.length_pos_of_mem h
|
||||
|
||||
grind_pattern size_pos_of_mem => a ∈ xs, xs.size
|
||||
|
|
@ -465,7 +465,7 @@ theorem mem_singleton_self (a : α) : a ∈ #[a] := by simp
|
|||
|
||||
theorem mem_of_mem_push_of_mem {a b : α} {xs : Array α} : a ∈ xs.push b → b ∈ xs → a ∈ xs := by
|
||||
cases xs
|
||||
simp only [List.push_toArray, mem_toArray, List.mem_append, List.mem_singleton]
|
||||
simp only [List.push_toArray, List.mem_toArray, List.mem_append, List.mem_singleton]
|
||||
rintro (h | rfl)
|
||||
· intro _
|
||||
exact h
|
||||
|
|
@ -2423,7 +2423,7 @@ abbrev mkArray_succ' := @replicate_succ'
|
|||
|
||||
@[simp, grind =] theorem mem_replicate {a b : α} {n} : b ∈ replicate n a ↔ n ≠ 0 ∧ b = a := by
|
||||
unfold replicate
|
||||
simp only [mem_toArray, List.mem_replicate]
|
||||
simp only [List.mem_toArray, List.mem_replicate]
|
||||
|
||||
@[deprecated mem_replicate (since := "2025-03-18")]
|
||||
abbrev mem_mkArray := @mem_replicate
|
||||
|
|
@ -4214,7 +4214,7 @@ variable [LawfulBEq α]
|
|||
(xs.replace a b)[i]? = if xs[i]? == some a then if a ∈ xs.take i then some a else some b else xs[i]? := by
|
||||
rcases xs with ⟨xs⟩
|
||||
simp only [List.replace_toArray, List.getElem?_toArray, List.getElem?_replace, take_eq_extract,
|
||||
List.extract_toArray, List.extract_eq_drop_take, Nat.sub_zero, List.drop_zero, mem_toArray]
|
||||
List.extract_toArray, List.extract_eq_drop_take, Nat.sub_zero, List.drop_zero, List.mem_toArray]
|
||||
|
||||
theorem getElem?_replace_of_ne {xs : Array α} {i : Nat} (h : xs[i]? ≠ some a) :
|
||||
(xs.replace a b)[i]? = xs[i]? := by
|
||||
|
|
@ -4235,7 +4235,7 @@ theorem getElem_replace_of_ne {xs : Array α} {i : Nat} {h : i < xs.size} (h' :
|
|||
(xs ++ ys).replace a b = if a ∈ xs then xs.replace a b ++ ys else xs ++ ys.replace a b := by
|
||||
rcases xs with ⟨xs⟩
|
||||
rcases ys with ⟨ys⟩
|
||||
simp only [List.append_toArray, List.replace_toArray, List.replace_append, mem_toArray]
|
||||
simp only [List.append_toArray, List.replace_toArray, List.replace_append, List.mem_toArray]
|
||||
split <;> simp
|
||||
|
||||
@[grind =] theorem replace_push {xs : Array α} {a b c : α} :
|
||||
|
|
|
|||
|
|
@ -167,7 +167,7 @@ theorem foldrM_filter [Monad m] [LawfulMonad m] {p : α → Bool} {g : α → β
|
|||
(h : ∀ a m b, f a (by simpa [w] using m) b = g a m b) :
|
||||
forIn' as b f = forIn' bs b' g := by
|
||||
cases as <;> cases bs
|
||||
simp only [mk.injEq, mem_toArray, List.forIn'_toArray] at w h ⊢
|
||||
simp only [mk.injEq, List.mem_toArray, List.forIn'_toArray] at w h ⊢
|
||||
exact List.forIn'_congr w hb h
|
||||
|
||||
/--
|
||||
|
|
|
|||
|
|
@ -116,7 +116,7 @@ theorem range'_eq_append_iff : range' s n = xs ++ ys ↔ ∃ k, k ≤ n ∧ xs =
|
|||
@[simp] theorem find?_range'_eq_some {s n : Nat} {i : Nat} {p : Nat → Bool} :
|
||||
(range' s n).find? p = some i ↔ p i ∧ i ∈ range' s n ∧ ∀ j, s ≤ j → j < i → !p j := by
|
||||
rw [← List.toArray_range']
|
||||
simp only [List.find?_toArray, mem_toArray]
|
||||
simp only [List.find?_toArray, List.mem_toArray]
|
||||
simp [List.find?_range'_eq_some]
|
||||
|
||||
@[simp] theorem find?_range'_eq_none {s n : Nat} {p : Nat → Bool} :
|
||||
|
|
|
|||
|
|
@ -139,7 +139,7 @@ def Iter.Partial.fold {α : Type w} {β : Type w} {γ : Type x} [Iterator α Id
|
|||
(init : γ) (it : Iter.Partial (α := α) β) : γ :=
|
||||
ForIn.forIn (m := Id) it init (fun x acc => ForInStep.yield (f acc x))
|
||||
|
||||
@[always_inline, inline, inherit_doc IterM.size]
|
||||
@[always_inline, inline, expose, inherit_doc IterM.size]
|
||||
def Iter.size {α : Type w} {β : Type w} [Iterator α Id β] [IteratorSize α Id]
|
||||
(it : Iter (α := α) β) : Nat :=
|
||||
(IteratorSize.size it.toIterM).run.down
|
||||
|
|
|
|||
|
|
@ -57,6 +57,6 @@ theorem IterM.map_unattach_toArray_attachWith [Iterator α m β] [Monad m] [Mona
|
|||
[LawfulMonad m] [LawfulIteratorCollect α m m] :
|
||||
(·.map Subtype.val) <$> (it.attachWith P hP).toArray = it.toArray := by
|
||||
rw [← toArray_toList, ← toArray_toList, ← map_unattach_toList_attachWith (it := it) (hP := hP)]
|
||||
simp [-map_unattach_toList_attachWith]
|
||||
simp [-map_unattach_toList_attachWith, -IterM.toArray_toList]
|
||||
|
||||
end Std.Iterators
|
||||
|
|
|
|||
|
|
@ -53,6 +53,6 @@ theorem Iter.toArray_uLift [Iterator α Id β] {it : Iter (α := α) β}
|
|||
[LawfulIteratorCollect α Id Id] :
|
||||
it.uLift.toArray = it.toArray.map ULift.up := by
|
||||
rw [← toArray_toList, ← toArray_toList, toList_uLift]
|
||||
simp
|
||||
simp [-toArray_toList]
|
||||
|
||||
end Std.Iterators
|
||||
|
|
|
|||
|
|
@ -44,11 +44,13 @@ theorem IterM.toListRev_toIter {α β} [Iterator α Id β] [Finite α Id]
|
|||
it.toIter.toListRev = it.toListRev.run :=
|
||||
(rfl)
|
||||
|
||||
@[simp]
|
||||
theorem Iter.toList_toArray {α β} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id]
|
||||
[LawfulIteratorCollect α Id Id] {it : Iter (α := α) β} :
|
||||
it.toArray.toList = it.toList := by
|
||||
simp [toArray_eq_toArray_toIterM, toList_eq_toList_toIterM, ← IterM.toList_toArray]
|
||||
|
||||
@[simp]
|
||||
theorem Iter.toArray_toList {α β} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id]
|
||||
[LawfulIteratorCollect α Id Id] {it : Iter (α := α) β} :
|
||||
it.toList.toArray = it.toArray := by
|
||||
|
|
|
|||
|
|
@ -14,6 +14,7 @@ public import Init.Data.Iterators.Consumers.Loop
|
|||
import all Init.Data.Iterators.Consumers.Loop
|
||||
public import Init.Data.Iterators.Consumers.Monadic.Collect
|
||||
import all Init.Data.Iterators.Consumers.Monadic.Collect
|
||||
import Init.Data.Array.Monadic
|
||||
|
||||
public section
|
||||
|
||||
|
|
@ -43,6 +44,20 @@ theorem Iter.forIn_eq {α β : Type w} [Iterator α Id β] [Finite α Id]
|
|||
f out acc) := by
|
||||
simp [ForIn.forIn, forIn'_eq, -forIn'_eq_forIn]
|
||||
|
||||
@[congr] theorem Iter.forIn'_congr {α β : Type w}
|
||||
[Iterator α Id β] [Finite α Id] [IteratorLoop α Id Id]
|
||||
{ita itb : Iter (α := α) β} (w : ita = itb)
|
||||
{b b' : γ} (hb : b = b')
|
||||
{f : (a' : β) → _ → γ → Id (ForInStep γ)}
|
||||
{g : (a' : β) → _ → γ → Id (ForInStep γ)}
|
||||
(h : ∀ a m b, f a (by simpa [w] using m) b = g a m b) :
|
||||
letI : ForIn' Id (Iter (α := α) β) β _ := Iter.instForIn'
|
||||
forIn' ita b f = forIn' itb b' g := by
|
||||
subst_eqs
|
||||
simp only [← funext_iff] at h
|
||||
rw [← h]
|
||||
rfl
|
||||
|
||||
theorem Iter.forIn'_eq_forIn'_toIterM {α β : Type w} [Iterator α Id β]
|
||||
[Finite α Id] {m : Type w → Type w''} [Monad m] [LawfulMonad m]
|
||||
[IteratorLoop α Id m] [LawfulIteratorLoop α Id m]
|
||||
|
|
@ -188,6 +203,13 @@ theorem Iter.mem_toList_iff_isPlausibleIndirectOutput {α β} [Iterator α Id β
|
|||
obtain ⟨step, h₁, rfl⟩ := h₁
|
||||
simp [heq, IterStep.successor] at h₁
|
||||
|
||||
theorem Iter.mem_toArray_iff_isPlausibleIndirectOutput {α β} [Iterator α Id β]
|
||||
[IteratorCollect α Id Id] [Finite α Id]
|
||||
[LawfulIteratorCollect α Id Id] [LawfulDeterministicIterator α Id]
|
||||
{it : Iter (α := α) β} {out : β} :
|
||||
out ∈ it.toArray ↔ it.IsPlausibleIndirectOutput out := by
|
||||
rw [← Iter.toArray_toList, List.mem_toArray, mem_toList_iff_isPlausibleIndirectOutput]
|
||||
|
||||
theorem Iter.forIn'_toList {α β : Type w} [Iterator α Id β]
|
||||
[Finite α Id] {m : Type x → Type x'} [Monad m] [LawfulMonad m]
|
||||
[IteratorLoop α Id m] [LawfulIteratorLoop α Id m]
|
||||
|
|
@ -222,6 +244,17 @@ theorem Iter.forIn'_toList {α β : Type w} [Iterator α Id β]
|
|||
simp only [ihs h (f := fun out h acc => f out (this ▸ h) acc)]
|
||||
· simp
|
||||
|
||||
theorem Iter.forIn'_toArray {α β : Type w} [Iterator α Id β]
|
||||
[Finite α Id] {m : Type x → Type x'} [Monad m] [LawfulMonad m]
|
||||
[IteratorLoop α Id m] [LawfulIteratorLoop α Id m]
|
||||
[IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id]
|
||||
[LawfulDeterministicIterator α Id]
|
||||
{γ : Type x} {it : Iter (α := α) β} {init : γ}
|
||||
{f : (out : β) → _ → γ → m (ForInStep γ)} :
|
||||
letI : ForIn' m (Iter (α := α) β) β _ := Iter.instForIn'
|
||||
ForIn'.forIn' it.toArray init f = ForIn'.forIn' it init (fun out h acc => f out (Iter.mem_toArray_iff_isPlausibleIndirectOutput.mpr h) acc) := by
|
||||
simp only [← Iter.toArray_toList (it := it), List.forIn'_toArray, Iter.forIn'_toList]
|
||||
|
||||
theorem Iter.forIn'_eq_forIn'_toList {α β : Type w} [Iterator α Id β]
|
||||
[Finite α Id] {m : Type x → Type x'} [Monad m] [LawfulMonad m]
|
||||
[IteratorLoop α Id m] [LawfulIteratorLoop α Id m]
|
||||
|
|
@ -234,6 +267,18 @@ theorem Iter.forIn'_eq_forIn'_toList {α β : Type w} [Iterator α Id β]
|
|||
simp only [forIn'_toList]
|
||||
congr
|
||||
|
||||
theorem Iter.forIn'_eq_forIn'_toArray {α β : Type w} [Iterator α Id β]
|
||||
[Finite α Id] {m : Type x → Type x'} [Monad m] [LawfulMonad m]
|
||||
[IteratorLoop α Id m] [LawfulIteratorLoop α Id m]
|
||||
[IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id]
|
||||
[LawfulDeterministicIterator α Id]
|
||||
{γ : Type x} {it : Iter (α := α) β} {init : γ}
|
||||
{f : (out : β) → _ → γ → m (ForInStep γ)} :
|
||||
letI : ForIn' m (Iter (α := α) β) β _ := Iter.instForIn'
|
||||
ForIn'.forIn' it init f = ForIn'.forIn' it.toArray init (fun out h acc => f out (Iter.mem_toArray_iff_isPlausibleIndirectOutput.mp h) acc) := by
|
||||
simp only [forIn'_toArray]
|
||||
congr
|
||||
|
||||
theorem Iter.forIn_toList {α β : Type w} [Iterator α Id β]
|
||||
[Finite α Id] {m : Type x → Type x'} [Monad m] [LawfulMonad m]
|
||||
[IteratorLoop α Id m] [LawfulIteratorLoop α Id m]
|
||||
|
|
@ -260,6 +305,15 @@ theorem Iter.forIn_toList {α β : Type w} [Iterator α Id β]
|
|||
rw [ihs h]
|
||||
· simp
|
||||
|
||||
theorem Iter.forIn_toArray {α β : Type w} [Iterator α Id β]
|
||||
[Finite α Id] {m : Type x → Type x'} [Monad m] [LawfulMonad m]
|
||||
[IteratorLoop α Id m] [LawfulIteratorLoop α Id m]
|
||||
[IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id]
|
||||
{γ : Type x} {it : Iter (α := α) β} {init : γ}
|
||||
{f : β → γ → m (ForInStep γ)} :
|
||||
ForIn.forIn it.toArray init f = ForIn.forIn it init f := by
|
||||
simp only [← Iter.toArray_toList, List.forIn_toArray, forIn_toList]
|
||||
|
||||
theorem Iter.foldM_eq_forIn {α β : Type w} {γ : Type x} [Iterator α Id β] [Finite α Id]
|
||||
{m : Type x → Type x'} [Monad m] [IteratorLoop α Id m] {f : γ → β → m γ}
|
||||
{init : γ} {it : Iter (α := α) β} :
|
||||
|
|
@ -301,6 +355,14 @@ theorem Iter.foldlM_toList {α β : Type w} {γ : Type x} [Iterator α Id β] [F
|
|||
rw [Iter.foldM_eq_forIn, ← Iter.forIn_toList]
|
||||
simp only [List.forIn_yield_eq_foldlM, id_map']
|
||||
|
||||
theorem Iter.foldlM_toArray {α β : Type w} {γ : Type x} [Iterator α Id β] [Finite α Id]
|
||||
{m : Type x → Type x'} [Monad m] [LawfulMonad m] [IteratorLoop α Id m]
|
||||
[LawfulIteratorLoop α Id m] [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id]
|
||||
{f : γ → β → m γ} {init : γ} {it : Iter (α := α) β} :
|
||||
it.toArray.foldlM (init := init) f = it.foldM (init := init) f := by
|
||||
rw [Iter.foldM_eq_forIn, ← Iter.forIn_toArray]
|
||||
simp only [Array.forIn_yield_eq_foldlM, id_map']
|
||||
|
||||
theorem IterM.forIn_eq_foldM {α β : Type w} [Iterator α Id β]
|
||||
[Finite α Id] {m : Type x → Type x'} [Monad m] [LawfulMonad m]
|
||||
[IteratorLoop α Id m] [LawfulIteratorLoop α Id m]
|
||||
|
|
@ -324,6 +386,12 @@ theorem Iter.fold_eq_foldM {α β : Type w} {γ : Type x} [Iterator α Id β]
|
|||
it.fold (init := init) f = (it.foldM (m := Id) (init := init) (pure <| f · ·)).run := by
|
||||
simp [foldM_eq_forIn, fold_eq_forIn]
|
||||
|
||||
theorem Iter.fold_eq_fold_toIterM {α β : Type w} {γ : Type w} [Iterator α Id β]
|
||||
[Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
|
||||
{f : γ → β → γ} {init : γ} {it : Iter (α := α) β} :
|
||||
it.fold (init := init) f = (it.toIterM.fold (init := init) f).run := by
|
||||
rw [fold_eq_foldM, foldM_eq_foldM_toIterM, IterM.fold_eq_foldM]
|
||||
|
||||
@[simp]
|
||||
theorem Iter.forIn_pure_yield_eq_fold {α β : Type w} {γ : Type x} [Iterator α Id β]
|
||||
[Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] {f : β → γ → γ} {init : γ}
|
||||
|
|
@ -344,6 +412,38 @@ theorem Iter.fold_eq_match_step {α β : Type w} {γ : Type x} [Iterator α Id
|
|||
generalize it.step = step
|
||||
cases step using PlausibleIterStep.casesOn <;> simp
|
||||
|
||||
-- The argument `f : γ₁ → γ₂` is intentionally explicit, as it is sometimes not found by unification.
|
||||
theorem Iter.fold_hom [Iterator α Id β] [Finite α Id]
|
||||
[IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
|
||||
{it : Iter (α := α) β}
|
||||
(f : γ₁ → γ₂) {g₁ : γ₁ → β → γ₁} {g₂ : γ₂ → β → γ₂} {init : γ₁}
|
||||
(H : ∀ x y, g₂ (f x) y = f (g₁ x y)) :
|
||||
it.fold g₂ (f init) = f (it.fold g₁ init) := by
|
||||
-- We cannot reduce to `IterM.fold_hom` because `IterM.fold` is necessarily more restrictive
|
||||
-- w.r.t. the universe of the output.
|
||||
induction it using Iter.inductSteps generalizing init with | step it ihy ihs =>
|
||||
rw [fold_eq_match_step, fold_eq_match_step]
|
||||
split
|
||||
· rw [H, ihy ‹_›]
|
||||
· rw [ihs ‹_›]
|
||||
· simp
|
||||
|
||||
theorem Iter.toList_eq_fold {α β : Type w} [Iterator α Id β]
|
||||
[Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
|
||||
[IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id]
|
||||
{it : Iter (α := α) β} :
|
||||
it.toList = it.fold (init := []) (fun l out => l ++ [out]) := by
|
||||
rw [Iter.toList_eq_toList_toIterM, IterM.toList_eq_fold, Iter.fold_eq_fold_toIterM]
|
||||
|
||||
theorem Iter.toArray_eq_fold {α β : Type w} [Iterator α Id β]
|
||||
[Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
|
||||
[IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id]
|
||||
{it : Iter (α := α) β} :
|
||||
it.toArray = it.fold (init := #[]) (fun xs out => xs.push out) := by
|
||||
simp only [← toArray_toList, toList_eq_fold]
|
||||
rw [← fold_hom (List.toArray)]
|
||||
simp
|
||||
|
||||
@[simp]
|
||||
theorem Iter.foldl_toList {α β : Type w} {γ : Type x} [Iterator α Id β] [Finite α Id]
|
||||
[IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
|
||||
|
|
@ -352,6 +452,14 @@ theorem Iter.foldl_toList {α β : Type w} {γ : Type x} [Iterator α Id β] [Fi
|
|||
it.toList.foldl (init := init) f = it.fold (init := init) f := by
|
||||
rw [fold_eq_foldM, List.foldl_eq_foldlM, ← Iter.foldlM_toList]
|
||||
|
||||
@[simp]
|
||||
theorem Iter.foldl_toArray {α β : Type w} {γ : Type x} [Iterator α Id β] [Finite α Id]
|
||||
[IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
|
||||
[IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id]
|
||||
{f : γ → β → γ} {init : γ} {it : Iter (α := α) β} :
|
||||
it.toArray.foldl (init := init) f = it.fold (init := init) f := by
|
||||
rw [fold_eq_foldM, Array.foldl_eq_foldlM, ← Iter.foldlM_toArray]
|
||||
|
||||
@[simp]
|
||||
theorem Iter.size_toArray_eq_size {α β : Type w} [Iterator α Id β] [Finite α Id]
|
||||
[IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id]
|
||||
|
|
|
|||
|
|
@ -67,15 +67,17 @@ theorem IterM.toArray_eq_match_step [Monad m] [LawfulMonad m] [Iterator α m β]
|
|||
rw [IterM.DefaultConsumers.toArrayMapped_eq_match_step]
|
||||
simp [bind_pure_comp, pure_bind]
|
||||
|
||||
@[simp]
|
||||
theorem IterM.toList_toArray [Monad m] [Iterator α m β] [Finite α m] [IteratorCollect α m m]
|
||||
{it : IterM (α := α) m β} :
|
||||
Array.toList <$> it.toArray = it.toList := by
|
||||
simp [IterM.toList]
|
||||
|
||||
@[simp]
|
||||
theorem IterM.toArray_toList [Monad m] [LawfulMonad m] [Iterator α m β] [Finite α m]
|
||||
[IteratorCollect α m m] {it : IterM (α := α) m β} :
|
||||
List.toArray <$> it.toList = it.toArray := by
|
||||
simp [IterM.toList]
|
||||
simp [IterM.toList, -toList_toArray]
|
||||
|
||||
theorem IterM.toList_eq_match_step [Monad m] [LawfulMonad m] [Iterator α m β] [Finite α m]
|
||||
[IteratorCollect α m m] [LawfulIteratorCollect α m m] {it : IterM (α := α) m β} :
|
||||
|
|
@ -153,6 +155,6 @@ theorem LawfulIteratorCollect.toList_eq {α β : Type w} {m : Type w → Type w'
|
|||
[hl : LawfulIteratorCollect α m m]
|
||||
{it : IterM (α := α) m β} :
|
||||
it.toList = (letI : IteratorCollect α m m := .defaultImplementation; it.toList) := by
|
||||
simp [IterM.toList, toArray_eq]
|
||||
simp [IterM.toList, toArray_eq, -IterM.toList_toArray]
|
||||
|
||||
end Std.Iterators
|
||||
|
|
|
|||
|
|
@ -60,6 +60,20 @@ theorem IterM.forIn_eq {α β : Type w} {m : Type w → Type w'} [Iterator α m
|
|||
IteratorLoop.wellFounded_of_finite it init _ (fun _ => id) (fun out _ acc => (⟨·, .intro⟩) <$> f out acc) := by
|
||||
simp only [ForIn.forIn, forIn'_eq]
|
||||
|
||||
@[congr] theorem IterM.forIn'_congr {α β : Type w} {m : Type w → Type w'} [Monad m]
|
||||
[Iterator α m β] [Finite α m] [IteratorLoop α m m]
|
||||
{ita itb : IterM (α := α) m β} (w : ita = itb)
|
||||
{b b' : γ} (hb : b = b')
|
||||
{f : (a' : β) → _ → γ → m (ForInStep γ)}
|
||||
{g : (a' : β) → _ → γ → m (ForInStep γ)}
|
||||
(h : ∀ a m b, f a (by simpa [w] using m) b = g a m b) :
|
||||
letI : ForIn' m (IterM (α := α) m β) β _ := IterM.instForIn'
|
||||
forIn' ita b f = forIn' itb b' g := by
|
||||
subst_eqs
|
||||
simp only [← funext_iff] at h
|
||||
rw [← h]
|
||||
rfl
|
||||
|
||||
theorem IterM.forIn'_eq_match_step {α β : Type w} {m : Type w → Type w'} [Iterator α m β]
|
||||
[Finite α m] {n : Type w → Type w''} [Monad m] [Monad n] [LawfulMonad n]
|
||||
[IteratorLoop α m n] [LawfulIteratorLoop α m n]
|
||||
|
|
@ -200,6 +214,23 @@ theorem IterM.fold_eq_match_step {α β γ : Type w} {m : Type w → Type w'} [I
|
|||
intro step
|
||||
cases step using PlausibleIterStep.casesOn <;> simp
|
||||
|
||||
-- The argument `f : γ₁ → γ₂` is intentionally explicit, as it is sometimes not found by unification.
|
||||
theorem IterM.fold_hom {m : Type w → Type w'} [Iterator α m β] [Finite α m]
|
||||
[Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m]
|
||||
{it : IterM (α := α) m β}
|
||||
(f : γ₁ → γ₂) {g₁ : γ₁ → β → γ₁} {g₂ : γ₂ → β → γ₂} {init : γ₁}
|
||||
(H : ∀ x y, g₂ (f x) y = f (g₁ x y)) :
|
||||
it.fold g₂ (f init) = f <$> (it.fold g₁ init) := by
|
||||
induction it using IterM.inductSteps generalizing init with | step it ihy ihs =>
|
||||
rw [fold_eq_match_step, fold_eq_match_step, map_eq_pure_bind, bind_assoc]
|
||||
apply bind_congr
|
||||
intro step
|
||||
rw [bind_pure_comp]
|
||||
split
|
||||
· rw [H, ihy ‹_›]
|
||||
· rw [ihs ‹_›]
|
||||
· simp
|
||||
|
||||
theorem IterM.toList_eq_fold {α β : Type w} {m : Type w → Type w'} [Iterator α m β]
|
||||
[Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m]
|
||||
[IteratorCollect α m m] [LawfulIteratorCollect α m m]
|
||||
|
|
@ -223,6 +254,15 @@ theorem IterM.toList_eq_fold {α β : Type w} {m : Type w → Type w'} [Iterator
|
|||
simp [ihs h]
|
||||
· simp
|
||||
|
||||
theorem IterM.toArray_eq_fold {α β : Type w} {m : Type w → Type w'} [Iterator α m β]
|
||||
[Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m]
|
||||
[IteratorCollect α m m] [LawfulIteratorCollect α m m]
|
||||
{it : IterM (α := α) m β} :
|
||||
it.toArray = it.fold (init := #[]) (fun xs out => xs.push out) := by
|
||||
simp only [← toArray_toList, toList_eq_fold]
|
||||
rw [← fold_hom]
|
||||
simp
|
||||
|
||||
theorem IterM.drain_eq_fold {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m]
|
||||
[Monad m] [IteratorLoop α m m] {it : IterM (α := α) m β} :
|
||||
it.drain = it.fold (init := PUnit.unit) (fun _ _ => .unit) :=
|
||||
|
|
|
|||
|
|
@ -27,7 +27,7 @@ def Internal.iter {sl su α} [UpwardEnumerable α] [BoundedUpwardEnumerable sl
|
|||
|
||||
/--
|
||||
Returns the elements of the given range as a list in ascending order, given that ranges of the given
|
||||
type and shape support this function and the range is finite.
|
||||
type and shape are finite and support this function.
|
||||
-/
|
||||
@[always_inline, inline, expose]
|
||||
def toList {sl su α} [UpwardEnumerable α] [BoundedUpwardEnumerable sl α]
|
||||
|
|
@ -37,6 +37,18 @@ def toList {sl su α} [UpwardEnumerable α] [BoundedUpwardEnumerable sl α]
|
|||
[IteratorCollect (RangeIterator su α) Id Id] : List α :=
|
||||
PRange.Internal.iter r |>.toList
|
||||
|
||||
/--
|
||||
Returns the elements of the given range as an array in ascending order, given that ranges of the
|
||||
given type and shape are finite and support this function.
|
||||
-/
|
||||
@[always_inline, inline, expose]
|
||||
def toArray {sl su α} [UpwardEnumerable α] [BoundedUpwardEnumerable sl α]
|
||||
[SupportsUpperBound su α]
|
||||
(r : PRange ⟨sl, su⟩ α)
|
||||
[Iterator (RangeIterator su α) Id α] [Finite (RangeIterator su α) Id]
|
||||
[IteratorCollect (RangeIterator su α) Id Id] : Array α :=
|
||||
PRange.Internal.iter r |>.toArray
|
||||
|
||||
/--
|
||||
Iterators for ranges implementing `RangeSize` support the `size` function.
|
||||
-/
|
||||
|
|
|
|||
|
|
@ -16,6 +16,7 @@ public import Init.Data.Range.Polymorphic.Iterators
|
|||
import all Init.Data.Range.Polymorphic.Iterators
|
||||
public import Init.Data.Iterators.Consumers.Loop
|
||||
import all Init.Data.Iterators.Consumers.Loop
|
||||
import Init.Data.Array.Monadic
|
||||
|
||||
public section
|
||||
|
||||
|
|
@ -44,6 +45,12 @@ private theorem Internal.toList_eq_toList_iter {sl su} [UpwardEnumerable α]
|
|||
r.toList = (Internal.iter r).toList := by
|
||||
rfl
|
||||
|
||||
private theorem Internal.toArray_eq_toArray_iter {sl su} [UpwardEnumerable α]
|
||||
[BoundedUpwardEnumerable sl α] [SupportsUpperBound su α] [HasFiniteRanges su α]
|
||||
[LawfulUpwardEnumerable α] {r : PRange ⟨sl, su⟩ α} :
|
||||
r.toArray = (Internal.iter r).toArray := by
|
||||
rfl
|
||||
|
||||
public theorem RangeIterator.toList_eq_match {su} [UpwardEnumerable α]
|
||||
[SupportsUpperBound su α] [HasFiniteRanges su α]
|
||||
[LawfulUpwardEnumerable α]
|
||||
|
|
@ -61,6 +68,35 @@ public theorem RangeIterator.toList_eq_match {su} [UpwardEnumerable α]
|
|||
· simp [*]
|
||||
· split <;> rename_i heq' <;> simp [*]
|
||||
|
||||
public theorem RangeIterator.toArray_eq_match {su} [UpwardEnumerable α]
|
||||
[SupportsUpperBound su α] [HasFiniteRanges su α]
|
||||
[LawfulUpwardEnumerable α]
|
||||
{it : Iter (α := RangeIterator su α) α} :
|
||||
it.toArray = match it.internalState.next with
|
||||
| none => #[]
|
||||
| some a => if SupportsUpperBound.IsSatisfied it.internalState.upperBound a then
|
||||
#[a] ++ (⟨⟨UpwardEnumerable.succ? a, it.internalState.upperBound⟩⟩ : Iter (α := RangeIterator su α) α).toArray
|
||||
else
|
||||
#[] := by
|
||||
rw [← Iter.toArray_toList, toList_eq_match]
|
||||
split
|
||||
· rfl
|
||||
· split <;> simp
|
||||
|
||||
@[simp]
|
||||
public theorem toList_toArray {sl su} [UpwardEnumerable α] [BoundedUpwardEnumerable sl α]
|
||||
[SupportsUpperBound su α] [HasFiniteRanges su α] [LawfulUpwardEnumerable α]
|
||||
{r : PRange ⟨sl, su⟩ α} :
|
||||
r.toArray.toList = r.toList := by
|
||||
simp [Internal.toArray_eq_toArray_iter, Internal.toList_eq_toList_iter]
|
||||
|
||||
@[simp]
|
||||
public theorem toArray_toList {sl su} [UpwardEnumerable α] [BoundedUpwardEnumerable sl α]
|
||||
[SupportsUpperBound su α] [HasFiniteRanges su α] [LawfulUpwardEnumerable α]
|
||||
{r : PRange ⟨sl, su⟩ α} :
|
||||
r.toList.toArray = r.toArray := by
|
||||
simp [Internal.toArray_eq_toArray_iter, Internal.toList_eq_toList_iter]
|
||||
|
||||
public theorem toList_eq_match {sl su} [UpwardEnumerable α] [BoundedUpwardEnumerable sl α]
|
||||
[SupportsUpperBound su α] [HasFiniteRanges su α]
|
||||
[LawfulUpwardEnumerable α]
|
||||
|
|
@ -73,6 +109,18 @@ public theorem toList_eq_match {sl su} [UpwardEnumerable α] [BoundedUpwardEnume
|
|||
[] := by
|
||||
rw [Internal.toList_eq_toList_iter, RangeIterator.toList_eq_match]; rfl
|
||||
|
||||
public theorem toArray_eq_match {sl su} [UpwardEnumerable α] [BoundedUpwardEnumerable sl α]
|
||||
[SupportsUpperBound su α] [HasFiniteRanges su α]
|
||||
[LawfulUpwardEnumerable α]
|
||||
{r : PRange ⟨sl, su⟩ α} :
|
||||
r.toArray = match init? r.lower with
|
||||
| none => #[]
|
||||
| some a => if SupportsUpperBound.IsSatisfied r.upper a then
|
||||
#[a] ++ (PRange.mk (shape := ⟨.open, su⟩) a r.upper).toArray
|
||||
else
|
||||
#[] := by
|
||||
rw [Internal.toArray_eq_toArray_iter, RangeIterator.toArray_eq_match]; rfl
|
||||
|
||||
public theorem toList_Rox_eq_toList_Rcx_of_isSome_succ? {su} [UpwardEnumerable α]
|
||||
[SupportsUpperBound su α] [HasFiniteRanges su α]
|
||||
[LawfulUpwardEnumerable α]
|
||||
|
|
@ -90,6 +138,14 @@ public theorem toList_open_eq_toList_closed_of_isSome_succ? {su} [UpwardEnumerab
|
|||
(PRange.mk (shape := ⟨.closed, su⟩) (UpwardEnumerable.succ? lo |>.get h) hi).toList :=
|
||||
toList_Rox_eq_toList_Rcx_of_isSome_succ? h
|
||||
|
||||
public theorem toArray_Rox_eq_toList_Rcx_of_isSome_succ? {su} [UpwardEnumerable α]
|
||||
[SupportsUpperBound su α] [HasFiniteRanges su α]
|
||||
[LawfulUpwardEnumerable α]
|
||||
{lo : Bound .open α} {hi} (h : (UpwardEnumerable.succ? lo).isSome) :
|
||||
(PRange.mk (shape := ⟨.open, su⟩) lo hi).toArray =
|
||||
(PRange.mk (shape := ⟨.closed, su⟩) (UpwardEnumerable.succ? lo |>.get h) hi).toArray := by
|
||||
simp [Internal.toArray_eq_toArray_iter, Internal.iter_Rox_eq_iter_Rcx_of_isSome_succ?, h]
|
||||
|
||||
public theorem toList_eq_nil_iff {sl su} [UpwardEnumerable α]
|
||||
[SupportsUpperBound su α] [HasFiniteRanges su α] [BoundedUpwardEnumerable sl α]
|
||||
[LawfulUpwardEnumerable α]
|
||||
|
|
@ -101,6 +157,14 @@ public theorem toList_eq_nil_iff {sl su} [UpwardEnumerable α]
|
|||
simp only
|
||||
split <;> rename_i heq <;> simp [heq]
|
||||
|
||||
public theorem toArray_eq_empty_iff {sl su} [UpwardEnumerable α]
|
||||
[SupportsUpperBound su α] [HasFiniteRanges su α] [BoundedUpwardEnumerable sl α]
|
||||
[LawfulUpwardEnumerable α]
|
||||
{r : PRange ⟨sl, su⟩ α} :
|
||||
r.toArray = #[] ↔
|
||||
¬ (∃ a, init? r.lower = some a ∧ SupportsUpperBound.IsSatisfied r.upper a) := by
|
||||
rw [← toArray_toList, List.toArray_eq_iff, Array.toList_empty, toList_eq_nil_iff]
|
||||
|
||||
public theorem mem_toList_iff_mem {sl su} [UpwardEnumerable α]
|
||||
[SupportsUpperBound su α] [SupportsLowerBound sl α] [HasFiniteRanges su α]
|
||||
[BoundedUpwardEnumerable sl α] [LawfulUpwardEnumerable α]
|
||||
|
|
@ -110,6 +174,15 @@ public theorem mem_toList_iff_mem {sl su} [UpwardEnumerable α]
|
|||
rw [Internal.toList_eq_toList_iter, Iter.mem_toList_iff_isPlausibleIndirectOutput,
|
||||
Internal.isPlausibleIndirectOutput_iter_iff]
|
||||
|
||||
public theorem mem_toArray_iff_mem {sl su} [UpwardEnumerable α]
|
||||
[SupportsUpperBound su α] [SupportsLowerBound sl α] [HasFiniteRanges su α]
|
||||
[BoundedUpwardEnumerable sl α] [LawfulUpwardEnumerable α]
|
||||
[LawfulUpwardEnumerableLowerBound sl α] [LawfulUpwardEnumerableUpperBound su α]
|
||||
{r : PRange ⟨sl, su⟩ α}
|
||||
{a : α} : a ∈ r.toArray ↔ a ∈ r := by
|
||||
rw [Internal.toArray_eq_toArray_iter, Iter.mem_toArray_iff_isPlausibleIndirectOutput,
|
||||
Internal.isPlausibleIndirectOutput_iter_iff]
|
||||
|
||||
public theorem BoundedUpwardEnumerable.init?_succ?_closed [UpwardEnumerable α]
|
||||
[LawfulUpwardEnumerable α] {lower lower' : Bound .closed α}
|
||||
(h : UpwardEnumerable.succ? lower = some lower') :
|
||||
|
|
@ -301,6 +374,17 @@ public theorem ClosedOpen.toList_succ_succ_eq_map [UpwardEnumerable α] [Support
|
|||
(lower...upper).toList.map succ :=
|
||||
toList_Rco_succ_succ_eq_map
|
||||
|
||||
public theorem toArray_Rco_succ_succ_eq_map [UpwardEnumerable α] [SupportsLowerBound .closed α]
|
||||
[LinearlyUpwardEnumerable α] [InfinitelyUpwardEnumerable α] [SupportsUpperBound .open α]
|
||||
[HasFiniteRanges .open α] [LawfulUpwardEnumerable α] [LawfulOpenUpperBound α]
|
||||
[LawfulUpwardEnumerableLowerBound .closed α] [LawfulUpwardEnumerableUpperBound .open α]
|
||||
{lower : Bound .closed α} {upper : Bound .open α} :
|
||||
((succ lower)...(succ upper)).toArray =
|
||||
(lower...upper).toArray.map succ := by
|
||||
simp only [← toArray_toList]
|
||||
rw [toList_Rco_succ_succ_eq_map]
|
||||
simp only [List.map_toArray]
|
||||
|
||||
private theorem Internal.forIn'_eq_forIn'_iter [UpwardEnumerable α]
|
||||
[SupportsUpperBound su α] [SupportsLowerBound sl α] [HasFiniteRanges su α]
|
||||
[BoundedUpwardEnumerable sl α] [LawfulUpwardEnumerable α]
|
||||
|
|
@ -324,6 +408,18 @@ public theorem forIn'_eq_forIn'_toList [UpwardEnumerable α]
|
|||
simp [Internal.forIn'_eq_forIn'_iter, Internal.toList_eq_toList_iter,
|
||||
Iter.forIn'_eq_forIn'_toList]
|
||||
|
||||
public theorem forIn'_eq_forIn'_toArray [UpwardEnumerable α]
|
||||
[SupportsUpperBound su α] [SupportsLowerBound sl α] [HasFiniteRanges su α]
|
||||
[BoundedUpwardEnumerable sl α] [LawfulUpwardEnumerable α]
|
||||
[LawfulUpwardEnumerableLowerBound sl α] [LawfulUpwardEnumerableUpperBound su α]
|
||||
{r : PRange ⟨sl, su⟩ α}
|
||||
{γ : Type u} {init : γ} {m : Type u → Type w} [Monad m] [LawfulMonad m]
|
||||
{f : (a : α) → a ∈ r → γ → m (ForInStep γ)} :
|
||||
ForIn'.forIn' r init f =
|
||||
ForIn'.forIn' r.toArray init (fun a ha acc => f a (mem_toArray_iff_mem.mp ha) acc) := by
|
||||
simp [Internal.forIn'_eq_forIn'_iter, Internal.toArray_eq_toArray_iter,
|
||||
Iter.forIn'_eq_forIn'_toArray]
|
||||
|
||||
public theorem forIn'_toList_eq_forIn' [UpwardEnumerable α]
|
||||
[SupportsUpperBound su α] [SupportsLowerBound sl α] [HasFiniteRanges su α]
|
||||
[BoundedUpwardEnumerable sl α] [LawfulUpwardEnumerable α]
|
||||
|
|
@ -335,6 +431,17 @@ public theorem forIn'_toList_eq_forIn' [UpwardEnumerable α]
|
|||
ForIn'.forIn' r init (fun a ha acc => f a (mem_toList_iff_mem.mpr ha) acc) := by
|
||||
simp [forIn'_eq_forIn'_toList]
|
||||
|
||||
public theorem forIn'_toArray_eq_forIn' [UpwardEnumerable α]
|
||||
[SupportsUpperBound su α] [SupportsLowerBound sl α] [HasFiniteRanges su α]
|
||||
[BoundedUpwardEnumerable sl α] [LawfulUpwardEnumerable α]
|
||||
[LawfulUpwardEnumerableLowerBound sl α] [LawfulUpwardEnumerableUpperBound su α]
|
||||
{r : PRange ⟨sl, su⟩ α}
|
||||
{γ : Type u} {init : γ} {m : Type u → Type w} [Monad m] [LawfulMonad m]
|
||||
{f : (a : α) → _ → γ → m (ForInStep γ)} :
|
||||
ForIn'.forIn' r.toArray init f =
|
||||
ForIn'.forIn' r init (fun a ha acc => f a (mem_toArray_iff_mem.mpr ha) acc) := by
|
||||
simp [forIn'_eq_forIn'_toArray]
|
||||
|
||||
public theorem mem_of_mem_open [UpwardEnumerable α]
|
||||
[SupportsUpperBound su α] [SupportsLowerBound sl α] [HasFiniteRanges su α]
|
||||
[BoundedUpwardEnumerable sl α] [LawfulUpwardEnumerable α]
|
||||
|
|
@ -431,6 +538,20 @@ public instance {su} [UpwardEnumerable α] [SupportsUpperBound su α] [RangeSize
|
|||
· have := LawfulRangeSize.size_eq_zero_of_not_isSatisfied _ _ h'
|
||||
simp [*] at this
|
||||
|
||||
public theorem length_toList {sl su} [UpwardEnumerable α] [SupportsUpperBound su α]
|
||||
[RangeSize su α] [LawfulUpwardEnumerable α] [BoundedUpwardEnumerable sl α]
|
||||
[HasFiniteRanges su α] [LawfulRangeSize su α]
|
||||
{r : PRange ⟨sl, su⟩ α} :
|
||||
r.toList.length = r.size := by
|
||||
simp [PRange.toList, PRange.size]
|
||||
|
||||
public theorem size_toArray {sl su} [UpwardEnumerable α] [SupportsUpperBound su α]
|
||||
[RangeSize su α] [LawfulUpwardEnumerable α] [BoundedUpwardEnumerable sl α]
|
||||
[HasFiniteRanges su α] [LawfulRangeSize su α]
|
||||
{r : PRange ⟨sl, su⟩ α} :
|
||||
r.toArray.size = r.size := by
|
||||
simp [PRange.toArray, PRange.size]
|
||||
|
||||
public theorem isEmpty_iff_forall_not_mem {sl su} [UpwardEnumerable α] [LawfulUpwardEnumerable α]
|
||||
[BoundedUpwardEnumerable sl α] [SupportsLowerBound sl α] [SupportsUpperBound su α]
|
||||
[LawfulUpwardEnumerableLowerBound sl α] [LawfulUpwardEnumerableUpperBound su α]
|
||||
|
|
@ -455,4 +576,94 @@ public theorem isEmpty_iff_forall_not_mem {sl su} [UpwardEnumerable α] [LawfulU
|
|||
(Option.some_get hi).symm
|
||||
exact h ((init? r.lower).get hi) ⟨hl, hu⟩
|
||||
|
||||
theorem Std.PRange.getElem?_toList_Rcx_eq [LE α] [UpwardEnumerable α] [LawfulUpwardEnumerable α]
|
||||
[SupportsUpperBound su α] [LawfulUpwardEnumerableUpperBound su α]
|
||||
[LawfulUpwardEnumerableLE α] [HasFiniteRanges su α]
|
||||
{r : PRange ⟨.closed, su⟩ α} {i} :
|
||||
r.toList[i]? = (UpwardEnumerable.succMany? i r.lower).filter (SupportsUpperBound.IsSatisfied r.upper) := by
|
||||
induction i generalizing r
|
||||
· rw [PRange.toList_eq_match, UpwardEnumerable.succMany?_zero]
|
||||
simp only [Option.filter_some, decide_eq_true_eq]
|
||||
split <;> simp
|
||||
· rename_i n ih
|
||||
rw [PRange.toList_eq_match]
|
||||
simp only
|
||||
split
|
||||
· simp [UpwardEnumerable.succMany?_succ?_eq_succ?_bind_succMany?]
|
||||
cases hs : UpwardEnumerable.succ? r.lower
|
||||
· rw [PRange.toList_eq_match]
|
||||
simp [BoundedUpwardEnumerable.init?, hs]
|
||||
· rw [toList_Rox_eq_toList_Rcx_of_isSome_succ? (by simp [hs])]
|
||||
rw [ih]
|
||||
simp [hs]
|
||||
· simp only [List.length_nil, Nat.not_lt_zero, not_false_eq_true, getElem?_neg]
|
||||
cases hs : UpwardEnumerable.succMany? (n + 1) r.lower
|
||||
· simp
|
||||
· rename_i hl a
|
||||
simp only [Option.filter_some, decide_eq_true_eq, right_eq_ite_iff]
|
||||
have : UpwardEnumerable.LE r.lower a := ⟨n + 1, hs⟩
|
||||
intro ha
|
||||
exact hl.elim <| LawfulUpwardEnumerableUpperBound.isSatisfied_of_le r.upper _ _ ha this (α := α)
|
||||
|
||||
theorem Std.PRange.getElem?_toArray_Rcx_eq [LE α] [UpwardEnumerable α] [LawfulUpwardEnumerable α]
|
||||
[SupportsUpperBound su α] [LawfulUpwardEnumerableUpperBound su α]
|
||||
[LawfulUpwardEnumerableLE α] [HasFiniteRanges su α]
|
||||
{r : PRange ⟨.closed, su⟩ α} {i} :
|
||||
r.toArray[i]? = (UpwardEnumerable.succMany? i r.lower).filter (SupportsUpperBound.IsSatisfied r.upper) := by
|
||||
rw [← toArray_toList, List.getElem?_toArray, getElem?_toList_Rcx_eq]
|
||||
|
||||
theorem Std.PRange.isSome_succMany?_of_lt_length_toList_Rcx [LE α] [UpwardEnumerable α]
|
||||
[LawfulUpwardEnumerable α] [SupportsUpperBound su α] [LawfulUpwardEnumerableUpperBound su α]
|
||||
[LawfulUpwardEnumerableLE α] [HasFiniteRanges su α]
|
||||
{r : PRange ⟨.closed, su⟩ α} {i} (h : i < r.toList.length) :
|
||||
(UpwardEnumerable.succMany? i r.lower).isSome := by
|
||||
have : r.toList[i]?.isSome := by simp [h]
|
||||
simp only [getElem?_toList_Rcx_eq, Option.isSome_filter] at this
|
||||
exact Option.isSome_of_any this
|
||||
|
||||
theorem Std.PRange.isSome_succMany?_of_lt_size_toArray_Rcx [LE α] [UpwardEnumerable α]
|
||||
[LawfulUpwardEnumerable α] [SupportsUpperBound su α] [LawfulUpwardEnumerableUpperBound su α]
|
||||
[LawfulUpwardEnumerableLE α] [HasFiniteRanges su α]
|
||||
{r : PRange ⟨.closed, su⟩ α} {i} (h : i < r.toArray.size) :
|
||||
(UpwardEnumerable.succMany? i r.lower).isSome := by
|
||||
have : r.toArray[i]?.isSome := by simp [h]
|
||||
simp only [getElem?_toArray_Rcx_eq, Option.isSome_filter] at this
|
||||
exact Option.isSome_of_any this
|
||||
|
||||
theorem Std.PRange.getElem_toList_Rcx_eq [LE α] [UpwardEnumerable α] [LawfulUpwardEnumerable α]
|
||||
[SupportsUpperBound su α] [LawfulUpwardEnumerableUpperBound su α]
|
||||
[LawfulUpwardEnumerableLE α] [HasFiniteRanges su α]
|
||||
{r : PRange ⟨.closed, su⟩ α} {i h} :
|
||||
r.toList[i]'h = (UpwardEnumerable.succMany? i r.lower).get
|
||||
(isSome_succMany?_of_lt_length_toList_Rcx h) := by
|
||||
simp [List.getElem_eq_getElem?_get, getElem?_toList_Rcx_eq]
|
||||
|
||||
theorem Std.PRange.getElem_toArray_Rcx_eq [LE α] [UpwardEnumerable α] [LawfulUpwardEnumerable α]
|
||||
[SupportsUpperBound su α] [LawfulUpwardEnumerableUpperBound su α]
|
||||
[LawfulUpwardEnumerableLE α] [HasFiniteRanges su α]
|
||||
{r : PRange ⟨.closed, su⟩ α} {i h} :
|
||||
r.toArray[i]'h = (UpwardEnumerable.succMany? i r.lower).get
|
||||
(isSome_succMany?_of_lt_size_toArray_Rcx h) := by
|
||||
simp [Array.getElem_eq_getElem?_get, getElem?_toArray_Rcx_eq]
|
||||
|
||||
theorem Std.PRange.eq_succMany?_of_toList_Rcx_eq_append_cons [LE α]
|
||||
[UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α]
|
||||
[SupportsUpperBound su α] [HasFiniteRanges su α] [LawfulUpwardEnumerableUpperBound su α]
|
||||
{r : PRange ⟨.closed, su⟩ α} {pref suff : List α} {cur : α} (h : r.toList = pref ++ cur :: suff) :
|
||||
cur = (UpwardEnumerable.succMany? pref.length r.lower).get
|
||||
(isSome_succMany?_of_lt_length_toList_Rcx (by simp [h])) := by
|
||||
have : cur = (pref ++ cur :: suff)[pref.length] := by simp
|
||||
simp only [← h] at this
|
||||
simp [this, getElem_toList_Rcx_eq]
|
||||
|
||||
theorem Std.PRange.eq_succMany?_of_toArray_Rcx_eq_append_append [LE α]
|
||||
[UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α]
|
||||
[SupportsUpperBound su α] [HasFiniteRanges su α] [LawfulUpwardEnumerableUpperBound su α]
|
||||
{r : PRange ⟨.closed, su⟩ α} {pref suff : Array α} {cur : α} (h : r.toArray = pref ++ #[cur] ++ suff) :
|
||||
cur = (UpwardEnumerable.succMany? pref.size r.lower).get
|
||||
(isSome_succMany?_of_lt_size_toArray_Rcx (by simp [h, Nat.add_assoc, Nat.add_comm 1])) := by
|
||||
have : cur = (pref ++ #[cur] ++ suff)[pref.size] := by simp
|
||||
simp only [← h] at this
|
||||
simp [this, getElem_toArray_Rcx_eq]
|
||||
|
||||
end Std.PRange
|
||||
|
|
|
|||
|
|
@ -25,4 +25,17 @@ theorem toList_Rco_succ_succ {m n : Nat} :
|
|||
theorem ClosedOpen.toList_succ_succ {m n : Nat} :
|
||||
((m+1)...(n+1)).toList = (m...n).toList.map (· + 1) := toList_Rco_succ_succ
|
||||
|
||||
@[simp]
|
||||
theorem Nat.size_Rco {a b : Nat} :
|
||||
(a...b).size = b - a := by
|
||||
simp only [size, Iterators.Iter.size, Iterators.IteratorSize.size, Iterators.Iter.toIterM,
|
||||
Internal.iter, init?, RangeSize.size, Id.run_pure]
|
||||
omega
|
||||
|
||||
@[simp]
|
||||
theorem Nat.size_Rcc {a b : Nat} :
|
||||
(a...=b).size = b + 1- a := by
|
||||
simp [Std.PRange.size, Std.Iterators.Iter.size, Std.Iterators.IteratorSize.size,
|
||||
Std.PRange.Internal.iter, Std.Iterators.Iter.toIterM, Std.PRange.RangeSize.size]
|
||||
|
||||
end Std.PRange.Nat
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue