refactor: small iterator improvements (#11175)
This PR removes duplicated instance parameters in the standard library and flips lemmas of the form `toList_eq_toListIter` into a form that is suitable for `simp`.
This commit is contained in:
Paul Reichert
GitHub
parent
1f807969b7
commit
1a4c3ca35d
4 changed files with 324 additions and 135 deletions
|
|
@ -490,7 +490,7 @@ public theorem Rxi.Iterator.toArray_eq_match
|
|||
|
||||
public theorem Rxc.Iterator.pairwise_toList_upwardEnumerableLt [LE α] [DecidableLE α]
|
||||
[UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α]
|
||||
[Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α]
|
||||
[Rxc.IsAlwaysFinite α]
|
||||
(it : Iter (α := Rxc.Iterator α) α) :
|
||||
it.toList.Pairwise (fun a b => UpwardEnumerable.LT a b) := by
|
||||
induction it using Iter.inductSteps with | step it ihy ihs
|
||||
|
|
@ -513,7 +513,7 @@ public theorem Rxc.Iterator.pairwise_toList_upwardEnumerableLt [LE α] [Decidabl
|
|||
|
||||
public theorem Rxo.Iterator.pairwise_toList_upwardEnumerableLt [LT α] [DecidableLT α]
|
||||
[UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α]
|
||||
[Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α]
|
||||
[Rxo.IsAlwaysFinite α]
|
||||
(it : Iter (α := Rxo.Iterator α) α) :
|
||||
it.toList.Pairwise (fun a b => UpwardEnumerable.LT a b) := by
|
||||
induction it using Iter.inductSteps with | step it ihy ihs
|
||||
|
|
@ -536,7 +536,7 @@ public theorem Rxo.Iterator.pairwise_toList_upwardEnumerableLt [LT α] [Decidabl
|
|||
|
||||
public theorem Rxi.Iterator.pairwise_toList_upwardEnumerableLt
|
||||
[UpwardEnumerable α] [LawfulUpwardEnumerable α]
|
||||
[Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α]
|
||||
[Rxi.IsAlwaysFinite α]
|
||||
(it : Iter (α := Rxi.Iterator α) α) :
|
||||
it.toList.Pairwise (fun a b => UpwardEnumerable.LT a b) := by
|
||||
induction it using Iter.inductSteps with | step it ihy ihs
|
||||
|
|
@ -589,8 +589,7 @@ public theorem toList_eq_if_roc [LE α] [DecidableLE α] [UpwardEnumerable α]
|
|||
def toList_eq_match := @toList_eq_if_roc
|
||||
|
||||
public theorem toArray_eq_if_roc [LE α] [DecidableLE α] [UpwardEnumerable α]
|
||||
[LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α]
|
||||
[LawfulUpwardEnumerable α] :
|
||||
[LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] :
|
||||
r.toArray = if r.lower ≤ r.upper then
|
||||
#[r.lower] ++ (r.lower<...=r.upper).toArray
|
||||
else
|
||||
|
|
@ -613,53 +612,51 @@ public theorem toList_toArray [LE α] [DecidableLE α] [UpwardEnumerable α]
|
|||
simp [Internal.toList_eq_toList_iter, Internal.toArray_eq_toArray_iter]
|
||||
|
||||
public theorem toList_eq_nil_iff [LE α] [DecidableLE α] [UpwardEnumerable α]
|
||||
[LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α]
|
||||
[LawfulUpwardEnumerable α] :
|
||||
[LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] :
|
||||
r.toList = [] ↔ ¬ (r.lower ≤ r.upper) := by
|
||||
rw [Internal.toList_eq_toList_iter, Rxc.Iterator.toList_eq_match, Internal.iter]
|
||||
simp only
|
||||
split <;> rename_i heq <;> simp [heq]
|
||||
|
||||
public theorem toArray_eq_empty_iff [LE α] [DecidableLE α] [UpwardEnumerable α]
|
||||
[LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α]
|
||||
[LawfulUpwardEnumerable α] :
|
||||
[LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] :
|
||||
r.toArray = #[] ↔ ¬ (r.lower ≤ r.upper) := by
|
||||
simp [← toArray_toList, toList_eq_nil_iff]
|
||||
|
||||
public theorem mem_toList_iff_mem [LE α] [DecidableLE α] [UpwardEnumerable α]
|
||||
[LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α]
|
||||
[LawfulUpwardEnumerable α] {a : α} : a ∈ r.toList ↔ a ∈ r := by
|
||||
{a : α} : a ∈ r.toList ↔ a ∈ r := by
|
||||
rw [Internal.toList_eq_toList_iter, Iter.mem_toList_iff_isPlausibleIndirectOutput,
|
||||
Internal.isPlausibleIndirectOutput_iter_iff]
|
||||
|
||||
public theorem mem_toArray_iff_mem [LE α] [DecidableLE α] [UpwardEnumerable α]
|
||||
[LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α]
|
||||
[LawfulUpwardEnumerable α] {a : α} : a ∈ r.toArray ↔ a ∈ r := by
|
||||
{a : α} : a ∈ r.toArray ↔ a ∈ r := by
|
||||
simp [← toArray_toList, mem_toList_iff_mem]
|
||||
|
||||
public theorem pairwise_toList_upwardEnumerableLt [LE α] [DecidableLE α]
|
||||
[UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α]
|
||||
[Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
|
||||
[Rxc.IsAlwaysFinite α] :
|
||||
r.toList.Pairwise (fun a b => UpwardEnumerable.LT a b) := by
|
||||
rw [Internal.toList_eq_toList_iter]
|
||||
apply Rxc.Iterator.pairwise_toList_upwardEnumerableLt
|
||||
|
||||
public theorem pairwise_toList_ne [LE α] [DecidableLE α]
|
||||
[UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α]
|
||||
[Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
|
||||
[Rxc.IsAlwaysFinite α] :
|
||||
r.toList.Pairwise (fun a b => a ≠ b) :=
|
||||
List.Pairwise.imp (fun hlt => UpwardEnumerable.ne_of_lt hlt) pairwise_toList_upwardEnumerableLt
|
||||
|
||||
public theorem pairwise_toList_lt [LE α] [DecidableLE α] [LT α]
|
||||
[UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α]
|
||||
[LawfulUpwardEnumerableLT α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
|
||||
[LawfulUpwardEnumerableLT α] [Rxc.IsAlwaysFinite α] :
|
||||
r.toList.Pairwise (fun a b => a < b) :=
|
||||
List.Pairwise.imp
|
||||
(fun hlt => (LawfulUpwardEnumerableLT.lt_iff ..).mpr hlt) pairwise_toList_upwardEnumerableLt
|
||||
|
||||
public theorem pairwise_toList_le [LE α] [DecidableLE α] [LT α]
|
||||
[UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α]
|
||||
[Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
|
||||
[Rxc.IsAlwaysFinite α] :
|
||||
r.toList.Pairwise (fun a b => a ≤ b) :=
|
||||
pairwise_toList_upwardEnumerableLt
|
||||
|> List.Pairwise.imp UpwardEnumerable.le_of_lt
|
||||
|
|
@ -852,54 +849,52 @@ public theorem toList_toArray [LT α] [DecidableLT α] [UpwardEnumerable α]
|
|||
simp [Internal.toList_eq_toList_iter, Internal.toArray_eq_toArray_iter]
|
||||
|
||||
public theorem toList_eq_nil_iff [LT α] [DecidableLT α] [UpwardEnumerable α]
|
||||
[LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α]
|
||||
[LawfulUpwardEnumerable α] :
|
||||
[LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] :
|
||||
r.toList = [] ↔ ¬ (r.lower < r.upper) := by
|
||||
rw [Internal.toList_eq_toList_iter, Rxo.Iterator.toList_eq_match, Internal.iter]
|
||||
simp only
|
||||
split <;> rename_i heq <;> simp [heq]
|
||||
|
||||
public theorem toArray_eq_empty_iff [LT α] [DecidableLT α] [UpwardEnumerable α]
|
||||
[LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α]
|
||||
[LawfulUpwardEnumerable α] :
|
||||
[LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] :
|
||||
r.toArray = #[] ↔ ¬ (r.lower < r.upper) := by
|
||||
simp [← toArray_toList, toList_eq_nil_iff]
|
||||
|
||||
public theorem mem_toList_iff_mem [LE α] [LT α] [DecidableLT α] [UpwardEnumerable α]
|
||||
[LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] [LawfulUpwardEnumerableLE α]
|
||||
[Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {a : α} : a ∈ r.toList ↔ a ∈ r := by
|
||||
[Rxo.IsAlwaysFinite α] {a : α} : a ∈ r.toList ↔ a ∈ r := by
|
||||
rw [Internal.toList_eq_toList_iter, Iter.mem_toList_iff_isPlausibleIndirectOutput,
|
||||
Internal.isPlausibleIndirectOutput_iter_iff]
|
||||
|
||||
public theorem mem_toArray_iff_mem [LE α] [LT α] [DecidableLT α] [UpwardEnumerable α]
|
||||
[LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] [LawfulUpwardEnumerableLE α]
|
||||
[Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {a : α} : a ∈ r.toArray ↔ a ∈ r := by
|
||||
[Rxo.IsAlwaysFinite α] {a : α} : a ∈ r.toArray ↔ a ∈ r := by
|
||||
rw [Internal.toArray_eq_toArray_iter, Iter.mem_toArray_iff_isPlausibleIndirectOutput,
|
||||
Internal.isPlausibleIndirectOutput_iter_iff]
|
||||
|
||||
public theorem pairwise_toList_upwardEnumerableLt [LE α] [LT α] [DecidableLT α]
|
||||
[UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α]
|
||||
[Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
|
||||
[Rxo.IsAlwaysFinite α] :
|
||||
r.toList.Pairwise (fun a b => UpwardEnumerable.LT a b) := by
|
||||
rw [Internal.toList_eq_toList_iter]
|
||||
apply Rxo.Iterator.pairwise_toList_upwardEnumerableLt
|
||||
|
||||
public theorem pairwise_toList_ne [LE α] [LT α] [DecidableLT α]
|
||||
[UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α]
|
||||
[Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
|
||||
[Rxo.IsAlwaysFinite α] :
|
||||
r.toList.Pairwise (fun a b => a ≠ b) :=
|
||||
List.Pairwise.imp (fun hlt => UpwardEnumerable.ne_of_lt hlt) pairwise_toList_upwardEnumerableLt
|
||||
|
||||
public theorem pairwise_toList_lt [LE α] [LT α] [DecidableLT α]
|
||||
[UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α]
|
||||
[Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
|
||||
[Rxo.IsAlwaysFinite α] :
|
||||
r.toList.Pairwise (fun a b => a < b) :=
|
||||
List.Pairwise.imp
|
||||
(fun hlt => (LawfulUpwardEnumerableLT.lt_iff ..).mpr hlt) pairwise_toList_upwardEnumerableLt
|
||||
|
||||
public theorem pairwise_toList_le [LE α] [LT α] [DecidableLT α]
|
||||
[UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α]
|
||||
[LawfulUpwardEnumerableLE α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
|
||||
[LawfulUpwardEnumerableLE α] [Rxo.IsAlwaysFinite α] :
|
||||
r.toList.Pairwise (fun a b => a ≤ b) :=
|
||||
pairwise_toList_upwardEnumerableLt
|
||||
|> List.Pairwise.imp UpwardEnumerable.le_of_lt
|
||||
|
|
@ -1039,7 +1034,7 @@ namespace Rci
|
|||
variable {r : Rci α}
|
||||
|
||||
public theorem toList_eq_toList_roi [UpwardEnumerable α]
|
||||
[LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
|
||||
[LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] :
|
||||
r.toList = r.lower :: (r.lower<...*).toList := by
|
||||
rw [Internal.toList_eq_toList_iter, Rxi.Iterator.toList_eq_match]; rfl
|
||||
|
||||
|
|
@ -1047,7 +1042,7 @@ public theorem toList_eq_toList_roi [UpwardEnumerable α]
|
|||
def toList_eq_toList_Roi := @toList_eq_toList_roi
|
||||
|
||||
public theorem toArray_eq_toArray_roi [UpwardEnumerable α]
|
||||
[LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
|
||||
[LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] :
|
||||
r.toArray = #[r.lower] ++ (r.lower<...*).toArray := by
|
||||
rw [Internal.toArray_eq_toArray_iter, Rxi.Iterator.toArray_eq_match]; rfl
|
||||
|
||||
|
|
@ -1067,51 +1062,49 @@ public theorem toList_toArray [UpwardEnumerable α] [LawfulUpwardEnumerable α]
|
|||
simp [Internal.toList_eq_toList_iter, Internal.toArray_eq_toArray_iter]
|
||||
|
||||
public theorem toList_ne_nil [UpwardEnumerable α]
|
||||
[LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α]
|
||||
[LawfulUpwardEnumerable α] :
|
||||
[LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] :
|
||||
r.toList ≠ [] := by
|
||||
rw [Internal.toList_eq_toList_iter, Rxi.Iterator.toList_eq_match, Internal.iter]
|
||||
simp
|
||||
|
||||
public theorem toArray_ne_nil [UpwardEnumerable α]
|
||||
[LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α]
|
||||
[LawfulUpwardEnumerable α] :
|
||||
[LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] :
|
||||
r.toArray ≠ #[] := by
|
||||
simp [← toArray_toList, toList_ne_nil]
|
||||
|
||||
public theorem mem_toList_iff_mem [LE α] [UpwardEnumerable α]
|
||||
[LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α]
|
||||
[Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {a : α} : a ∈ r.toList ↔ a ∈ r := by
|
||||
[Rxi.IsAlwaysFinite α] {a : α} : a ∈ r.toList ↔ a ∈ r := by
|
||||
rw [Internal.toList_eq_toList_iter, Iter.mem_toList_iff_isPlausibleIndirectOutput,
|
||||
Internal.isPlausibleIndirectOutput_iter_iff]
|
||||
|
||||
public theorem mem_toArray_iff_mem [LE α] [UpwardEnumerable α]
|
||||
[LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α]
|
||||
[Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {a : α} : a ∈ r.toArray ↔ a ∈ r := by
|
||||
[Rxi.IsAlwaysFinite α] {a : α} : a ∈ r.toArray ↔ a ∈ r := by
|
||||
rw [Internal.toArray_eq_toArray_iter, Iter.mem_toArray_iff_isPlausibleIndirectOutput,
|
||||
Internal.isPlausibleIndirectOutput_iter_iff]
|
||||
|
||||
public theorem pairwise_toList_upwardEnumerableLt [LE α]
|
||||
[UpwardEnumerable α] [LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
|
||||
[UpwardEnumerable α] [LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] :
|
||||
r.toList.Pairwise (fun a b => UpwardEnumerable.LT a b) := by
|
||||
rw [Internal.toList_eq_toList_iter]
|
||||
apply Rxi.Iterator.pairwise_toList_upwardEnumerableLt
|
||||
|
||||
public theorem pairwise_toList_ne [LE α]
|
||||
[UpwardEnumerable α] [LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
|
||||
[UpwardEnumerable α] [LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] :
|
||||
r.toList.Pairwise (fun a b => a ≠ b) :=
|
||||
List.Pairwise.imp (fun hlt => UpwardEnumerable.ne_of_lt hlt) pairwise_toList_upwardEnumerableLt
|
||||
|
||||
public theorem pairwise_toList_lt [LE α] [LT α]
|
||||
[UpwardEnumerable α] [LawfulUpwardEnumerable α]
|
||||
[LawfulUpwardEnumerableLT α] [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
|
||||
[LawfulUpwardEnumerableLT α] [Rxi.IsAlwaysFinite α] :
|
||||
r.toList.Pairwise (fun a b => a < b) :=
|
||||
List.Pairwise.imp
|
||||
(fun hlt => (LawfulUpwardEnumerableLT.lt_iff ..).mpr hlt) pairwise_toList_upwardEnumerableLt
|
||||
|
||||
public theorem pairwise_toList_le [LE α]
|
||||
[UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α]
|
||||
[Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
|
||||
[Rxi.IsAlwaysFinite α] :
|
||||
r.toList.Pairwise (fun a b => a ≤ b) :=
|
||||
pairwise_toList_upwardEnumerableLt
|
||||
|> List.Pairwise.imp UpwardEnumerable.le_of_lt
|
||||
|
|
@ -1293,7 +1286,7 @@ public theorem toList_toArray [LE α] [DecidableLE α] [UpwardEnumerable α] [La
|
|||
|
||||
public theorem toList_eq_nil_iff [LE α] [DecidableLE α] [LT α] [UpwardEnumerable α]
|
||||
[LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [LawfulUpwardEnumerableLT α]
|
||||
[Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
|
||||
[Rxc.IsAlwaysFinite α] :
|
||||
r.toList = [] ↔ ¬ (r.lower < r.upper) := by
|
||||
rw [Internal.toList_eq_toList_iter, Rxc.Iterator.toList_eq_match, Internal.iter]
|
||||
simp only
|
||||
|
|
@ -1304,45 +1297,45 @@ public theorem toList_eq_nil_iff [LE α] [DecidableLE α] [LT α] [UpwardEnumera
|
|||
|
||||
public theorem toArray_eq_empty_iff [LE α] [DecidableLE α] [LT α] [UpwardEnumerable α]
|
||||
[LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [LawfulUpwardEnumerableLT α]
|
||||
[Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
|
||||
[Rxc.IsAlwaysFinite α] :
|
||||
r.toArray = #[] ↔ ¬ (r.lower < r.upper) := by
|
||||
simp [← toArray_toList, toList_eq_nil_iff]
|
||||
|
||||
public theorem mem_toList_iff_mem [LE α] [DecidableLE α] [LT α] [UpwardEnumerable α]
|
||||
[LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [LawfulUpwardEnumerableLT α]
|
||||
[Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {a : α} : a ∈ r.toList ↔ a ∈ r := by
|
||||
[Rxc.IsAlwaysFinite α] {a : α} : a ∈ r.toList ↔ a ∈ r := by
|
||||
rw [Internal.toList_eq_toList_iter, Iter.mem_toList_iff_isPlausibleIndirectOutput,
|
||||
Internal.isPlausibleIndirectOutput_iter_iff]
|
||||
|
||||
public theorem mem_toArray_iff_mem [LE α] [DecidableLE α] [LT α] [UpwardEnumerable α]
|
||||
[LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [LawfulUpwardEnumerableLT α]
|
||||
[Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {a : α} : a ∈ r.toArray ↔ a ∈ r := by
|
||||
[Rxc.IsAlwaysFinite α] {a : α} : a ∈ r.toArray ↔ a ∈ r := by
|
||||
rw [Internal.toArray_eq_toArray_iter, Iter.mem_toArray_iff_isPlausibleIndirectOutput,
|
||||
Internal.isPlausibleIndirectOutput_iter_iff]
|
||||
|
||||
public theorem pairwise_toList_upwardEnumerableLt [LE α] [DecidableLE α]
|
||||
[UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α]
|
||||
[Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
|
||||
[Rxc.IsAlwaysFinite α] :
|
||||
r.toList.Pairwise (fun a b => UpwardEnumerable.LT a b) := by
|
||||
rw [Internal.toList_eq_toList_iter]
|
||||
apply Rxc.Iterator.pairwise_toList_upwardEnumerableLt
|
||||
|
||||
public theorem pairwise_toList_ne [LE α] [DecidableLE α]
|
||||
[UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α]
|
||||
[Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
|
||||
[Rxc.IsAlwaysFinite α] :
|
||||
r.toList.Pairwise (fun a b => a ≠ b) :=
|
||||
List.Pairwise.imp (fun hlt => UpwardEnumerable.ne_of_lt hlt) pairwise_toList_upwardEnumerableLt
|
||||
|
||||
public theorem pairwise_toList_lt [LE α] [DecidableLE α] [LT α]
|
||||
[UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α]
|
||||
[LawfulUpwardEnumerableLT α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
|
||||
[LawfulUpwardEnumerableLT α] [Rxc.IsAlwaysFinite α] :
|
||||
r.toList.Pairwise (fun a b => a < b) :=
|
||||
List.Pairwise.imp
|
||||
(fun hlt => (LawfulUpwardEnumerableLT.lt_iff ..).mpr hlt) pairwise_toList_upwardEnumerableLt
|
||||
|
||||
public theorem pairwise_toList_le [LE α] [DecidableLE α] [LT α]
|
||||
[UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α]
|
||||
[Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
|
||||
[Rxc.IsAlwaysFinite α] :
|
||||
r.toList.Pairwise (fun a b => a ≤ b) :=
|
||||
pairwise_toList_upwardEnumerableLt
|
||||
|> List.Pairwise.imp UpwardEnumerable.le_of_lt
|
||||
|
|
@ -1466,8 +1459,7 @@ namespace Roo
|
|||
variable {r : Roo α}
|
||||
|
||||
public theorem toList_eq_match [LT α] [DecidableLT α] [UpwardEnumerable α]
|
||||
[LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α]
|
||||
[LawfulUpwardEnumerable α] :
|
||||
[LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] :
|
||||
r.toList = match UpwardEnumerable.succ? r.lower with
|
||||
| none => []
|
||||
| some next =>
|
||||
|
|
@ -1478,8 +1470,7 @@ public theorem toList_eq_match [LT α] [DecidableLT α] [UpwardEnumerable α]
|
|||
rw [Internal.toList_eq_toList_iter, Rxo.Iterator.toList_eq_match]; rfl
|
||||
|
||||
public theorem toArray_eq_match [LE α] [LT α] [DecidableLT α] [UpwardEnumerable α]
|
||||
[LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α]
|
||||
[LawfulUpwardEnumerable α] :
|
||||
[LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] :
|
||||
r.toArray = match UpwardEnumerable.succ? r.lower with
|
||||
| none => #[]
|
||||
| some next =>
|
||||
|
|
@ -1524,54 +1515,52 @@ public theorem toList_toArray [LT α] [DecidableLT α] [UpwardEnumerable α] [La
|
|||
simp [Internal.toList_eq_toList_iter, Internal.toArray_eq_toArray_iter]
|
||||
|
||||
public theorem toList_eq_nil_iff [LE α] [LT α] [DecidableLT α] [UpwardEnumerable α]
|
||||
[LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α]
|
||||
[LawfulUpwardEnumerable α] :
|
||||
[LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] :
|
||||
r.toList = [] ↔ ∀ a, UpwardEnumerable.succ? r.lower = some a → ¬ (a < r.upper) := by
|
||||
rw [Internal.toList_eq_toList_iter, Rxo.Iterator.toList_eq_match, Internal.iter]
|
||||
simp only
|
||||
split <;> rename_i heq <;> simp [heq]
|
||||
|
||||
public theorem toArray_eq_empty_iff [LE α] [LT α] [DecidableLT α] [UpwardEnumerable α]
|
||||
[LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α]
|
||||
[LawfulUpwardEnumerable α] :
|
||||
[LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] :
|
||||
r.toArray = #[] ↔ ∀ a, UpwardEnumerable.succ? r.lower = some a → ¬ (a < r.upper) := by
|
||||
simp [← toArray_toList, toList_eq_nil_iff]
|
||||
|
||||
public theorem mem_toList_iff_mem [LT α] [DecidableLT α] [UpwardEnumerable α]
|
||||
[LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α]
|
||||
[Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {a : α} : a ∈ r.toList ↔ a ∈ r := by
|
||||
[Rxo.IsAlwaysFinite α] {a : α} : a ∈ r.toList ↔ a ∈ r := by
|
||||
rw [Internal.toList_eq_toList_iter, Iter.mem_toList_iff_isPlausibleIndirectOutput,
|
||||
Internal.isPlausibleIndirectOutput_iter_iff]
|
||||
|
||||
public theorem mem_toArray_iff_mem [LT α] [DecidableLT α] [UpwardEnumerable α]
|
||||
[LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α]
|
||||
[Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {a : α} : a ∈ r.toArray ↔ a ∈ r := by
|
||||
[Rxo.IsAlwaysFinite α] {a : α} : a ∈ r.toArray ↔ a ∈ r := by
|
||||
rw [Internal.toArray_eq_toArray_iter, Iter.mem_toArray_iff_isPlausibleIndirectOutput,
|
||||
Internal.isPlausibleIndirectOutput_iter_iff]
|
||||
|
||||
public theorem pairwise_toList_upwardEnumerableLt [LT α] [DecidableLT α]
|
||||
[UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α]
|
||||
[Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
|
||||
[Rxo.IsAlwaysFinite α] :
|
||||
r.toList.Pairwise (fun a b => UpwardEnumerable.LT a b) := by
|
||||
rw [Internal.toList_eq_toList_iter]
|
||||
apply Rxo.Iterator.pairwise_toList_upwardEnumerableLt
|
||||
|
||||
public theorem pairwise_toList_ne [LT α] [DecidableLT α]
|
||||
[UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α]
|
||||
[Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
|
||||
[Rxo.IsAlwaysFinite α] :
|
||||
r.toList.Pairwise (fun a b => a ≠ b) :=
|
||||
List.Pairwise.imp (fun hlt => UpwardEnumerable.ne_of_lt hlt) pairwise_toList_upwardEnumerableLt
|
||||
|
||||
public theorem pairwise_toList_lt [LT α] [DecidableLT α]
|
||||
[UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α]
|
||||
[Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
|
||||
[Rxo.IsAlwaysFinite α] :
|
||||
r.toList.Pairwise (fun a b => a < b) :=
|
||||
List.Pairwise.imp
|
||||
(fun hlt => (LawfulUpwardEnumerableLT.lt_iff ..).mpr hlt) pairwise_toList_upwardEnumerableLt
|
||||
|
||||
public theorem pairwise_toList_le [LE α] [LT α] [DecidableLT α]
|
||||
[UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α]
|
||||
[LawfulUpwardEnumerableLE α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
|
||||
[LawfulUpwardEnumerableLE α] [Rxo.IsAlwaysFinite α] :
|
||||
r.toList.Pairwise (fun a b => a ≤ b) :=
|
||||
pairwise_toList_upwardEnumerableLt
|
||||
|> List.Pairwise.imp UpwardEnumerable.le_of_lt
|
||||
|
|
@ -1762,25 +1751,25 @@ public theorem toList_eq_match_rci [UpwardEnumerable α]
|
|||
split <;> simp
|
||||
|
||||
public theorem toList_eq_nil_iff [UpwardEnumerable α] [LawfulUpwardEnumerable α]
|
||||
[Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
|
||||
[Rxi.IsAlwaysFinite α] :
|
||||
r.toList = [] ↔ (UpwardEnumerable.succ? r.lower).isNone := by
|
||||
rw [Internal.toList_eq_toList_iter, Rxi.Iterator.toList_eq_match, Internal.iter]
|
||||
simp only
|
||||
split <;> rename_i heq <;> simp [heq]
|
||||
|
||||
public theorem toArray_eq_empty_iff [UpwardEnumerable α] [LawfulUpwardEnumerable α]
|
||||
[Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
|
||||
[Rxi.IsAlwaysFinite α] :
|
||||
r.toArray = #[] ↔ (UpwardEnumerable.succ? r.lower).isNone := by
|
||||
simp [← toArray_toList, toList_eq_nil_iff]
|
||||
|
||||
public theorem mem_toList_iff_mem [LT α] [UpwardEnumerable α]
|
||||
[LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α]
|
||||
[LawfulUpwardEnumerableLT α] {a : α} : a ∈ r.toList ↔ a ∈ r := by
|
||||
[LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerableLT α]
|
||||
{a : α} : a ∈ r.toList ↔ a ∈ r := by
|
||||
rw [Internal.toList_eq_toList_iter, Iter.mem_toList_iff_isPlausibleIndirectOutput,
|
||||
Internal.isPlausibleIndirectOutput_iter_iff]
|
||||
|
||||
public theorem mem_toArray_iff_mem [LT α] [UpwardEnumerable α]
|
||||
[LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α]
|
||||
[LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α]
|
||||
[LawfulUpwardEnumerableLT α] {a : α} : a ∈ r.toArray ↔ a ∈ r := by
|
||||
rw [Internal.toArray_eq_toArray_iter, Iter.mem_toArray_iff_isPlausibleIndirectOutput,
|
||||
Internal.isPlausibleIndirectOutput_iter_iff]
|
||||
|
|
@ -1977,7 +1966,7 @@ def toArray_eq_toArray_Rcc := @toArray_eq_toArray_rcc
|
|||
|
||||
public theorem toList_eq_if_roc [LE α] [DecidableLE α] [Least? α] [UpwardEnumerable α]
|
||||
[LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [LawfulUpwardEnumerableLeast? α]
|
||||
[Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
|
||||
[Rxc.IsAlwaysFinite α] :
|
||||
r.toList = let init : α := UpwardEnumerable.least (hn := ⟨r.upper⟩)
|
||||
if init ≤ r.upper then
|
||||
init :: (init<...=r.upper).toList
|
||||
|
|
@ -1990,7 +1979,7 @@ def toList_eq_if := @toList_eq_if_roc
|
|||
|
||||
public theorem toArray_eq_if_roc [LE α] [DecidableLE α] [Least? α] [UpwardEnumerable α]
|
||||
[LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [LawfulUpwardEnumerableLeast? α]
|
||||
[Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
|
||||
[Rxc.IsAlwaysFinite α] :
|
||||
r.toArray = let init : α := UpwardEnumerable.least (hn := ⟨r.upper⟩)
|
||||
if init ≤ r.upper then
|
||||
#[init] ++ (init<...=r.upper).toArray
|
||||
|
|
@ -2003,14 +1992,14 @@ def toArray_eq_if := @toArray_eq_if_roc
|
|||
|
||||
public theorem toList_ne_nil [LE α] [DecidableLE α] [Least? α] [UpwardEnumerable α]
|
||||
[LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α]
|
||||
[LawfulUpwardEnumerableLeast? α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
|
||||
[LawfulUpwardEnumerableLeast? α] [Rxc.IsAlwaysFinite α] :
|
||||
r.toList ≠ [] := by
|
||||
simp [toList_eq_toList_rcc, Rcc.toList_eq_nil_iff, UpwardEnumerable.le_iff,
|
||||
UpwardEnumerable.least_le]
|
||||
|
||||
public theorem toArray_ne_empty [LE α] [DecidableLE α] [Least? α] [UpwardEnumerable α]
|
||||
[LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α]
|
||||
[LawfulUpwardEnumerableLeast? α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
|
||||
[LawfulUpwardEnumerableLeast? α] [Rxc.IsAlwaysFinite α] :
|
||||
r.toArray ≠ #[] := by
|
||||
simp [toArray_eq_toArray_rcc, Rcc.toArray_eq_empty_iff, UpwardEnumerable.le_iff,
|
||||
UpwardEnumerable.least_le]
|
||||
|
|
@ -2026,29 +2015,29 @@ def mem_iff_mem_Rcc := @mem_iff_mem_rcc
|
|||
|
||||
public theorem mem_toList_iff_mem [LE α] [DecidableLE α] [Least? α] [UpwardEnumerable α]
|
||||
[LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [LawfulUpwardEnumerableLeast? α]
|
||||
[Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {a : α} : a ∈ r.toList ↔ a ∈ r := by
|
||||
[Rxc.IsAlwaysFinite α] {a : α} : a ∈ r.toList ↔ a ∈ r := by
|
||||
simp [toList_eq_toList_rcc, mem_iff_mem_rcc, Rcc.mem_toList_iff_mem]
|
||||
|
||||
public theorem mem_toArray_iff_mem [LE α] [DecidableLE α] [Least? α] [UpwardEnumerable α]
|
||||
[LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [LawfulUpwardEnumerableLeast? α]
|
||||
[Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {a : α} : a ∈ r.toArray ↔ a ∈ r := by
|
||||
[Rxc.IsAlwaysFinite α] {a : α} : a ∈ r.toArray ↔ a ∈ r := by
|
||||
simp [toArray_eq_toArray_rcc, mem_iff_mem_rcc, Rcc.mem_toArray_iff_mem]
|
||||
|
||||
public theorem pairwise_toList_upwardEnumerableLt [LE α] [DecidableLE α] [Least? α]
|
||||
[UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α]
|
||||
[LawfulUpwardEnumerableLeast? α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
|
||||
[LawfulUpwardEnumerableLeast? α] [Rxc.IsAlwaysFinite α] :
|
||||
r.toList.Pairwise (fun a b => UpwardEnumerable.LT a b) := by
|
||||
simp [toList_eq_toList_rcc, Rcc.pairwise_toList_upwardEnumerableLt]
|
||||
|
||||
public theorem pairwise_toList_ne [LE α] [DecidableLE α] [Least? α]
|
||||
[UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α]
|
||||
[LawfulUpwardEnumerableLeast? α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
|
||||
[LawfulUpwardEnumerableLeast? α] [Rxc.IsAlwaysFinite α] :
|
||||
r.toList.Pairwise (fun a b => a ≠ b) :=
|
||||
List.Pairwise.imp (fun hlt => UpwardEnumerable.ne_of_lt hlt) pairwise_toList_upwardEnumerableLt
|
||||
|
||||
public theorem pairwise_toList_lt [LE α] [DecidableLE α] [LT α] [Least? α]
|
||||
[UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α]
|
||||
[LawfulUpwardEnumerableLT α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α]
|
||||
[LawfulUpwardEnumerableLT α] [Rxc.IsAlwaysFinite α]
|
||||
[LawfulUpwardEnumerableLeast? α] :
|
||||
r.toList.Pairwise (fun a b => a < b) :=
|
||||
List.Pairwise.imp
|
||||
|
|
@ -2056,7 +2045,7 @@ public theorem pairwise_toList_lt [LE α] [DecidableLE α] [LT α] [Least? α]
|
|||
|
||||
public theorem pairwise_toList_le [LE α] [DecidableLE α] [LT α] [Least? α]
|
||||
[UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α]
|
||||
[LawfulUpwardEnumerableLeast? α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
|
||||
[LawfulUpwardEnumerableLeast? α] [Rxc.IsAlwaysFinite α] :
|
||||
r.toList.Pairwise (fun a b => a ≤ b) :=
|
||||
pairwise_toList_upwardEnumerableLt
|
||||
|> List.Pairwise.imp UpwardEnumerable.le_of_lt
|
||||
|
|
@ -2282,7 +2271,7 @@ def toArray_eq_toArray_Rco := @toArray_eq_toArray_rco
|
|||
|
||||
public theorem toList_eq_if_roo [LT α] [DecidableLT α] [Least? α] [UpwardEnumerable α]
|
||||
[LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] [LawfulUpwardEnumerableLeast? α]
|
||||
[Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
|
||||
[Rxo.IsAlwaysFinite α] :
|
||||
r.toList = let init : α := UpwardEnumerable.least (hn := ⟨r.upper⟩)
|
||||
if init < r.upper then
|
||||
init :: (init<...r.upper).toList
|
||||
|
|
@ -2296,7 +2285,7 @@ def toList_eq_if := @toList_eq_if_roo
|
|||
|
||||
public theorem toArray_eq_if_roo [LT α] [DecidableLT α] [Least? α] [UpwardEnumerable α]
|
||||
[LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] [LawfulUpwardEnumerableLeast? α]
|
||||
[Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
|
||||
[Rxo.IsAlwaysFinite α] :
|
||||
r.toArray = let init : α := UpwardEnumerable.least (hn := ⟨r.upper⟩)
|
||||
if init < r.upper then
|
||||
#[init] ++ (init<...r.upper).toArray
|
||||
|
|
@ -2310,13 +2299,13 @@ def toArray_eq_if := @toArray_eq_if_roo
|
|||
|
||||
public theorem toList_eq_nil_iff [LT α] [DecidableLT α] [Least? α] [UpwardEnumerable α]
|
||||
[LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α]
|
||||
[LawfulUpwardEnumerableLeast? α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
|
||||
[LawfulUpwardEnumerableLeast? α] [Rxo.IsAlwaysFinite α] :
|
||||
r.toList = [] ↔ ¬ UpwardEnumerable.least (hn := ⟨r.upper⟩) < r.upper := by
|
||||
simp [toList_eq_if_roo]
|
||||
|
||||
public theorem toArray_eq_nil_iff [LT α] [DecidableLT α] [Least? α] [UpwardEnumerable α]
|
||||
[LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α]
|
||||
[LawfulUpwardEnumerableLeast? α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
|
||||
[LawfulUpwardEnumerableLeast? α] [Rxo.IsAlwaysFinite α] :
|
||||
r.toArray = #[] ↔ ¬ UpwardEnumerable.least (hn := ⟨r.upper⟩) < r.upper := by
|
||||
simp [toArray_eq_if_roo]
|
||||
|
||||
|
|
@ -2331,7 +2320,7 @@ def mem_iff_mem_Rco := @mem_iff_mem_rco
|
|||
|
||||
public theorem mem_toList_iff_mem [LT α] [DecidableLT α] [Least? α] [UpwardEnumerable α]
|
||||
[LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] [LawfulUpwardEnumerableLeast? α]
|
||||
[Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {a : α} : a ∈ r.toList ↔ a ∈ r := by
|
||||
[Rxo.IsAlwaysFinite α] {a : α} : a ∈ r.toList ↔ a ∈ r := by
|
||||
simp only [toList_eq_if_roo, List.mem_ite_nil_right, List.mem_cons, Roo.mem_toList_iff_mem]
|
||||
simp only [Membership.mem]
|
||||
constructor
|
||||
|
|
@ -2348,12 +2337,12 @@ public theorem mem_toList_iff_mem [LT α] [DecidableLT α] [Least? α] [UpwardEn
|
|||
|
||||
public theorem mem_toArray_iff_mem [LT α] [DecidableLT α] [Least? α] [UpwardEnumerable α]
|
||||
[LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] [LawfulUpwardEnumerableLeast? α]
|
||||
[Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {a : α} : a ∈ r.toArray ↔ a ∈ r := by
|
||||
[Rxo.IsAlwaysFinite α] {a : α} : a ∈ r.toArray ↔ a ∈ r := by
|
||||
simp [← toArray_toList, mem_toList_iff_mem]
|
||||
|
||||
public theorem pairwise_toList_upwardEnumerableLt [LT α] [DecidableLT α] [Least? α]
|
||||
[UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α]
|
||||
[LawfulUpwardEnumerableLeast? α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
|
||||
[LawfulUpwardEnumerableLeast? α] [Rxo.IsAlwaysFinite α] :
|
||||
r.toList.Pairwise (fun a b => UpwardEnumerable.LT a b) := by
|
||||
simp only [toList_eq_if_roo]
|
||||
split
|
||||
|
|
@ -2365,13 +2354,13 @@ public theorem pairwise_toList_upwardEnumerableLt [LT α] [DecidableLT α] [Leas
|
|||
|
||||
public theorem pairwise_toList_ne [LT α] [DecidableLT α] [Least? α]
|
||||
[UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α]
|
||||
[LawfulUpwardEnumerableLeast? α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
|
||||
[LawfulUpwardEnumerableLeast? α] [Rxo.IsAlwaysFinite α] :
|
||||
r.toList.Pairwise (fun a b => a ≠ b) :=
|
||||
List.Pairwise.imp (fun hlt => UpwardEnumerable.ne_of_lt hlt) pairwise_toList_upwardEnumerableLt
|
||||
|
||||
public theorem pairwise_toList_lt [LT α] [DecidableLT α] [Least? α]
|
||||
[UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α]
|
||||
[LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α]
|
||||
[LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α]
|
||||
[LawfulUpwardEnumerableLeast? α] :
|
||||
r.toList.Pairwise (fun a b => a < b) :=
|
||||
List.Pairwise.imp
|
||||
|
|
@ -2379,8 +2368,7 @@ public theorem pairwise_toList_lt [LT α] [DecidableLT α] [Least? α]
|
|||
|
||||
public theorem pairwise_toList_le [LE α] [LT α] [DecidableLT α] [Least? α]
|
||||
[UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α]
|
||||
[LawfulUpwardEnumerableLE α] [LawfulUpwardEnumerableLeast? α] [Rxo.IsAlwaysFinite α]
|
||||
[LawfulUpwardEnumerable α] :
|
||||
[LawfulUpwardEnumerableLE α] [LawfulUpwardEnumerableLeast? α] [Rxo.IsAlwaysFinite α] :
|
||||
r.toList.Pairwise (fun a b => a ≤ b) :=
|
||||
pairwise_toList_upwardEnumerableLt
|
||||
|> List.Pairwise.imp UpwardEnumerable.le_of_lt
|
||||
|
|
@ -2585,7 +2573,7 @@ public theorem toArray_eq_match_rci [Least? α] [UpwardEnumerable α]
|
|||
def toArray_eq_match_toArray_Rci := @toArray_eq_match_rci
|
||||
|
||||
public theorem toList_eq_match_roi [Least? α] [UpwardEnumerable α]
|
||||
[LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
|
||||
[LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] :
|
||||
r.toList = match Least?.least? (α := α) with
|
||||
| none => []
|
||||
| some init => init :: (init<...*).toList := by
|
||||
|
|
@ -2597,7 +2585,7 @@ def toList_eq_match_toList_Roi := @toList_eq_match_roi
|
|||
|
||||
public theorem toArray_eq_match_roi [Least? α] [UpwardEnumerable α]
|
||||
[LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLeast? α]
|
||||
[Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
|
||||
[Rxi.IsAlwaysFinite α] :
|
||||
r.toArray = match Least?.least? (α := α) with
|
||||
| none => #[]
|
||||
| some init => #[init] ++ (init<...*).toArray := by
|
||||
|
|
@ -2609,7 +2597,7 @@ def toArray_eq_match_Roi := @toArray_eq_match_roi
|
|||
|
||||
public theorem toList_eq_nil_iff [LT α] [DecidableLT α] [Least? α] [UpwardEnumerable α]
|
||||
[LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α]
|
||||
[LawfulUpwardEnumerableLeast? α] [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
|
||||
[LawfulUpwardEnumerableLeast? α] [Rxi.IsAlwaysFinite α] :
|
||||
r.toList = [] ↔ ¬ Nonempty α := by
|
||||
simp only [toList_eq_match_roi]
|
||||
split
|
||||
|
|
@ -2619,7 +2607,7 @@ public theorem toList_eq_nil_iff [LT α] [DecidableLT α] [Least? α] [UpwardEnu
|
|||
|
||||
public theorem toArray_eq_empty_iff [LT α] [DecidableLT α] [Least? α] [UpwardEnumerable α]
|
||||
[LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α]
|
||||
[LawfulUpwardEnumerableLeast? α] [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
|
||||
[LawfulUpwardEnumerableLeast? α] [Rxi.IsAlwaysFinite α] :
|
||||
r.toArray = #[] ↔ ¬ Nonempty α := by
|
||||
simp [← toArray_toList, toList_eq_nil_iff]
|
||||
|
||||
|
|
@ -2634,7 +2622,7 @@ def mem_iff_mem_Rci := @mem_iff_mem_rci
|
|||
|
||||
public theorem mem_toList [Least? α] [UpwardEnumerable α]
|
||||
[LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLeast? α]
|
||||
[Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {a : α} : a ∈ r.toList := by
|
||||
[Rxi.IsAlwaysFinite α] {a : α} : a ∈ r.toList := by
|
||||
letI : LE α := ⟨UpwardEnumerable.LE⟩
|
||||
haveI : LawfulUpwardEnumerableLE α := ⟨fun _ _ => Iff.rfl⟩
|
||||
simp only [toList_eq_match_rci, UpwardEnumerable.least?_eq_some (hn := ⟨a⟩),
|
||||
|
|
@ -2643,12 +2631,12 @@ public theorem mem_toList [Least? α] [UpwardEnumerable α]
|
|||
|
||||
public theorem mem_toArray [Least? α] [UpwardEnumerable α]
|
||||
[LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLeast? α]
|
||||
[Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {a : α} : a ∈ r.toArray := by
|
||||
[Rxi.IsAlwaysFinite α] {a : α} : a ∈ r.toArray := by
|
||||
simp [← toArray_toList, mem_toList]
|
||||
|
||||
public theorem pairwise_toList_upwardEnumerableLt [Least? α]
|
||||
[UpwardEnumerable α] [LawfulUpwardEnumerable α]
|
||||
[LawfulUpwardEnumerableLeast? α] [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
|
||||
[LawfulUpwardEnumerableLeast? α] [Rxi.IsAlwaysFinite α] :
|
||||
r.toList.Pairwise (fun a b => UpwardEnumerable.LT a b) := by
|
||||
letI : LE α := ⟨UpwardEnumerable.LE⟩
|
||||
haveI : LawfulUpwardEnumerableLE α := ⟨fun _ _ => Iff.rfl⟩
|
||||
|
|
@ -2659,19 +2647,19 @@ public theorem pairwise_toList_upwardEnumerableLt [Least? α]
|
|||
|
||||
public theorem pairwise_toList_ne [Least? α]
|
||||
[UpwardEnumerable α] [LawfulUpwardEnumerable α]
|
||||
[LawfulUpwardEnumerableLeast? α] [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
|
||||
[LawfulUpwardEnumerableLeast? α] [Rxi.IsAlwaysFinite α] :
|
||||
r.toList.Pairwise (fun a b => a ≠ b) :=
|
||||
List.Pairwise.imp (fun hlt => UpwardEnumerable.ne_of_lt hlt) pairwise_toList_upwardEnumerableLt
|
||||
|
||||
public theorem pairwise_toList_lt [LT α] [Least? α] [UpwardEnumerable α] [LawfulUpwardEnumerable α]
|
||||
[LawfulUpwardEnumerableLT α] [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α]
|
||||
[LawfulUpwardEnumerableLT α] [Rxi.IsAlwaysFinite α]
|
||||
[LawfulUpwardEnumerableLeast? α] : r.toList.Pairwise (fun a b => a < b) :=
|
||||
List.Pairwise.imp
|
||||
(fun hlt => (LawfulUpwardEnumerableLT.lt_iff ..).mpr hlt) pairwise_toList_upwardEnumerableLt
|
||||
|
||||
public theorem pairwise_toList_le [LE α] [Least? α]
|
||||
[UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α]
|
||||
[LawfulUpwardEnumerableLeast? α] [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] :
|
||||
[LawfulUpwardEnumerableLeast? α] [Rxi.IsAlwaysFinite α] :
|
||||
r.toList.Pairwise (fun a b => a ≤ b) :=
|
||||
pairwise_toList_upwardEnumerableLt
|
||||
|> List.Pairwise.imp UpwardEnumerable.le_of_lt
|
||||
|
|
@ -2766,7 +2754,6 @@ private theorem Internal.iter_roc_eq_iter_rcc_of_isSome_succ?
|
|||
|
||||
public theorem toList_roc_eq_toList_rcc_of_isSome_succ? [LE α] [DecidableLE α] [UpwardEnumerable α]
|
||||
[LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α]
|
||||
[LawfulUpwardEnumerable α]
|
||||
{lo hi : α} (h : (UpwardEnumerable.succ? lo).isSome) :
|
||||
(lo<...=hi).toList =
|
||||
((UpwardEnumerable.succ? lo |>.get h)...=hi).toList := by
|
||||
|
|
@ -2786,7 +2773,7 @@ private theorem Internal.iter_roo_eq_iter_rco_of_isSome_succ?
|
|||
public theorem toList_roo_eq_toList_rco_of_isSome_succ?
|
||||
[LT α] [DecidableLT α] [UpwardEnumerable α]
|
||||
[LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α]
|
||||
[Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α]
|
||||
[Rxo.IsAlwaysFinite α]
|
||||
{lo hi : α} (h : (UpwardEnumerable.succ? lo).isSome) :
|
||||
(lo<...hi).toList =
|
||||
((UpwardEnumerable.succ? lo |>.get h)...hi).toList := by
|
||||
|
|
@ -2806,7 +2793,7 @@ private theorem Internal.iter_roi_eq_iter_rci_of_isSome_succ?
|
|||
public theorem toList_roi_eq_toList_rci_of_isSome_succ?
|
||||
[UpwardEnumerable α]
|
||||
[LawfulUpwardEnumerable α]
|
||||
[Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α]
|
||||
[Rxi.IsAlwaysFinite α]
|
||||
{lo : α} (h : (UpwardEnumerable.succ? lo).isSome) :
|
||||
(lo<...*).toList = ((UpwardEnumerable.succ? lo |>.get h)...*).toList := by
|
||||
simp [Rci.Internal.toList_eq_toList_iter, Roi.Internal.toList_eq_toList_iter,
|
||||
|
|
|
|||
|
|
@ -689,7 +689,7 @@ public instance [Ord α] {s : RicSlice α β} : ToIterator s Id ((a : α) × β
|
|||
|
||||
public theorem toList_ric {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] (t : Impl α β)
|
||||
(ordered : t.Ordered) (bound : α) : t[*...=bound].toList = t.toList.filter (fun e => (compare e.fst bound).isLE) := by
|
||||
simp only [Ric.Sliceable.mkSlice, Slice.toList_eq_toList_iter, Slice.iter,
|
||||
simp only [Ric.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter,
|
||||
Slice.Internal.iter_eq_toIteratorIter, ToIterator.iter, ToIterator.iterM_eq,
|
||||
Iter.toIter_toIterM]
|
||||
rw [RxcIterator.toList_rxcIter, RxcIterator.takeWhile_eq_filter]
|
||||
|
|
@ -717,7 +717,7 @@ public instance [Ord α] {s : Unit.RicSlice α} : ToIterator s Id α := by
|
|||
|
||||
public theorem toList_ric {α : Type u} [Ord α] [TransOrd α] (t : Impl α (fun _ => Unit))
|
||||
(ordered : t.Ordered) (bound : α) : (t : Impl α (fun _ => Unit))[*...=bound].toList = (Internal.Impl.keys t).filter (fun e => (compare e bound).isLE) := by
|
||||
simp only [Ric.Sliceable.mkSlice, Slice.toList_eq_toList_iter, Slice.iter,
|
||||
simp only [Ric.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter,
|
||||
Slice.Internal.iter_eq_toIteratorIter, ToIterator.iter, ToIterator.iterM_eq,
|
||||
Iter.toIter_toIterM]
|
||||
rw [Iter.toList_map]
|
||||
|
|
@ -749,7 +749,7 @@ public instance [Ord α] {s : RicSlice α β} : ToIterator s Id (α × β) := by
|
|||
|
||||
public theorem toList_ric {α : Type u} {β : Type v} [Ord α] [TransOrd α] (t : Impl α (fun _ => β))
|
||||
(ordered : t.Ordered) (bound : α) : t[*...=bound].toList = (Internal.Impl.Const.toList t).filter (fun e => (compare e.fst bound).isLE) := by
|
||||
simp only [Ric.Sliceable.mkSlice, Slice.toList_eq_toList_iter, Slice.iter,
|
||||
simp only [Ric.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter,
|
||||
Slice.Internal.iter_eq_toIteratorIter, ToIterator.iter, ToIterator.iterM_eq,
|
||||
Iter.toIter_toIterM]
|
||||
rw [Iter.toList_map]
|
||||
|
|
@ -780,7 +780,7 @@ public instance [Ord α] {s : RioSlice α β} : ToIterator s Id ((a : α) × β
|
|||
|
||||
public theorem toList_rio {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] (t : Impl α β)
|
||||
(ordered : t.Ordered) (bound : α) : t[*...bound].toList = t.toList.filter (fun e => (compare e.fst bound).isLT) := by
|
||||
simp only [Rio.Sliceable.mkSlice, Slice.toList_eq_toList_iter, Slice.iter,
|
||||
simp only [Rio.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter,
|
||||
Slice.Internal.iter_eq_toIteratorIter, ToIterator.iter, ToIterator.iterM_eq,
|
||||
Iter.toIter_toIterM]
|
||||
rw [RxoIterator.toList_rxoIter, RxoIterator.takeWhile_eq_filter]
|
||||
|
|
@ -808,7 +808,7 @@ public instance [Ord α] {s : Unit.RioSlice α} : ToIterator s Id α := by
|
|||
|
||||
public theorem toList_rio {α : Type u} [Ord α] [TransOrd α] (t : Impl α (fun _ => Unit))
|
||||
(ordered : t.Ordered) (bound : α) : (t : Impl α (fun _ => Unit))[*...<bound].toList = (Internal.Impl.keys t).filter (fun e => (compare e bound).isLT) := by
|
||||
simp only [Rio.Sliceable.mkSlice, Slice.toList_eq_toList_iter, Slice.iter,
|
||||
simp only [Rio.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter,
|
||||
Slice.Internal.iter_eq_toIteratorIter, ToIterator.iter, ToIterator.iterM_eq,
|
||||
Iter.toIter_toIterM]
|
||||
rw [Iter.toList_map]
|
||||
|
|
@ -840,7 +840,7 @@ public instance [Ord α] {s : RioSlice α β} : ToIterator s Id (α × β) := by
|
|||
|
||||
public theorem toList_rio {α : Type u} {β : Type v} [Ord α] [TransOrd α] (t : Impl α (fun _ => β))
|
||||
(ordered : t.Ordered) (bound : α) : t[*...<bound].toList = (Internal.Impl.Const.toList t).filter (fun e => (compare e.fst bound).isLT) := by
|
||||
simp only [Rio.Sliceable.mkSlice, Slice.toList_eq_toList_iter, Slice.iter,
|
||||
simp only [Rio.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter,
|
||||
Slice.Internal.iter_eq_toIteratorIter, ToIterator.iter, ToIterator.iterM_eq,
|
||||
Iter.toIter_toIterM]
|
||||
rw [Iter.toList_map]
|
||||
|
|
@ -904,7 +904,7 @@ public instance [Ord α] {s : RccSlice α β} : ToIterator s Id ((a : α) × β
|
|||
|
||||
public theorem toList_rcc {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] (t : Impl α β)
|
||||
(ordered : t.Ordered) (lowerBound upperBound : α) : t[lowerBound...=upperBound].toList = t.toList.filter (fun e => (compare e.fst lowerBound).isGE ∧ (compare e.fst upperBound).isLE) := by
|
||||
simp only [Rcc.Sliceable.mkSlice, Slice.toList_eq_toList_iter, Slice.iter,
|
||||
simp only [Rcc.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter,
|
||||
Slice.Internal.iter_eq_toIteratorIter, ToIterator.iter, ToIterator.iterM_eq,
|
||||
Iter.toIter_toIterM]
|
||||
rw [toList_rccIter]
|
||||
|
|
@ -929,7 +929,7 @@ public instance [Ord α] {s : Unit.RccSlice α} : ToIterator s Id α := by
|
|||
|
||||
public theorem toList_rcc {α : Type u} [Ord α] [TransOrd α] (t : Impl α (fun _ => Unit))
|
||||
(ordered : t.Ordered) (lowerBound upperBound: α) : (t : Impl α (fun _ => Unit))[lowerBound...=upperBound].toList = (Internal.Impl.keys t).filter (fun e => (compare e lowerBound).isGE ∧ (compare e upperBound).isLE) := by
|
||||
simp only [Rcc.Sliceable.mkSlice, Slice.toList_eq_toList_iter, Slice.iter,
|
||||
simp only [Rcc.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter,
|
||||
Slice.Internal.iter_eq_toIteratorIter, ToIterator.iter, ToIterator.iterM_eq,
|
||||
Iter.toIter_toIterM]
|
||||
rw [Iter.toList_map]
|
||||
|
|
@ -963,7 +963,7 @@ public instance [Ord α] {s : RccSlice α β} : ToIterator s Id (α × β) := by
|
|||
|
||||
public theorem toList_rcc {α : Type u} {β : Type v} [Ord α] [TransOrd α] (t : Impl α (fun _ => β))
|
||||
(ordered : t.Ordered) (lowerBound upperBound : α) : t[lowerBound...=upperBound].toList = (Internal.Impl.Const.toList t).filter (fun e => (compare e.fst lowerBound).isGE ∧ (compare e.fst upperBound).isLE) := by
|
||||
simp only [Rcc.Sliceable.mkSlice, Slice.toList_eq_toList_iter, Slice.iter,
|
||||
simp only [Rcc.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter,
|
||||
Slice.Internal.iter_eq_toIteratorIter, ToIterator.iter, ToIterator.iterM_eq,
|
||||
Iter.toIter_toIterM]
|
||||
rw [Iter.toList_map]
|
||||
|
|
@ -1031,7 +1031,7 @@ public instance [Ord α] {s : RcoSlice α β} : ToIterator s Id ((a : α) × β
|
|||
|
||||
public theorem toList_rco {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] (t : Impl α β)
|
||||
(ordered : t.Ordered) (lowerBound upperBound : α) : t[lowerBound...<upperBound].toList = t.toList.filter (fun e => (compare e.fst lowerBound).isGE ∧ (compare e.fst upperBound).isLT) := by
|
||||
simp only [Rco.Sliceable.mkSlice, Slice.toList_eq_toList_iter, Slice.iter,
|
||||
simp only [Rco.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter,
|
||||
Slice.Internal.iter_eq_toIteratorIter, ToIterator.iter, ToIterator.iterM_eq,
|
||||
Iter.toIter_toIterM]
|
||||
rw [toList_rcoIter]
|
||||
|
|
@ -1056,7 +1056,7 @@ public instance [Ord α] {s : Unit.RcoSlice α} : ToIterator s Id α := by
|
|||
|
||||
public theorem toList_rco {α : Type u} [Ord α] [TransOrd α] (t : Impl α (fun _ => Unit))
|
||||
(ordered : t.Ordered) (lowerBound upperBound: α) : (t : Impl α (fun _ => Unit))[lowerBound...<upperBound].toList = (Internal.Impl.keys t).filter (fun e => (compare e lowerBound).isGE ∧ (compare e upperBound).isLT) := by
|
||||
simp only [Rco.Sliceable.mkSlice, Slice.toList_eq_toList_iter, Slice.iter,
|
||||
simp only [Rco.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter,
|
||||
Slice.Internal.iter_eq_toIteratorIter, ToIterator.iter, ToIterator.iterM_eq,
|
||||
Iter.toIter_toIterM]
|
||||
rw [Iter.toList_map]
|
||||
|
|
@ -1090,7 +1090,7 @@ public instance [Ord α] {s : RcoSlice α β} : ToIterator s Id (α × β) := by
|
|||
|
||||
public theorem toList_rco {α : Type u} {β : Type v} [Ord α] [TransOrd α] (t : Impl α (fun _ => β))
|
||||
(ordered : t.Ordered) (lowerBound upperBound : α) : t[lowerBound...<upperBound].toList = (Internal.Impl.Const.toList t).filter (fun e => (compare e.fst lowerBound).isGE ∧ (compare e.fst upperBound).isLT) := by
|
||||
simp only [Rco.Sliceable.mkSlice, Slice.toList_eq_toList_iter, Slice.iter,
|
||||
simp only [Rco.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter,
|
||||
Slice.Internal.iter_eq_toIteratorIter, ToIterator.iter, ToIterator.iterM_eq,
|
||||
Iter.toIter_toIterM]
|
||||
rw [Iter.toList_map]
|
||||
|
|
@ -1157,7 +1157,7 @@ public instance [Ord α] {s : RooSlice α β} : ToIterator s Id ((a : α) × β
|
|||
|
||||
public theorem toList_roo {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] (t : Impl α β)
|
||||
(ordered : t.Ordered) (lowerBound upperBound : α) : t[lowerBound<...<upperBound].toList = t.toList.filter (fun e => (compare e.fst lowerBound).isGT ∧ (compare e.fst upperBound).isLT) := by
|
||||
simp only [Roo.Sliceable.mkSlice, Slice.toList_eq_toList_iter, Slice.iter,
|
||||
simp only [Roo.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter,
|
||||
Slice.Internal.iter_eq_toIteratorIter, ToIterator.iter, ToIterator.iterM_eq,
|
||||
Iter.toIter_toIterM]
|
||||
rw [toList_rooIter]
|
||||
|
|
@ -1182,7 +1182,7 @@ public instance [Ord α] {s : Unit.RooSlice α} : ToIterator s Id α := by
|
|||
|
||||
public theorem toList_roo {α : Type u} [Ord α] [TransOrd α] (t : Impl α (fun _ => Unit))
|
||||
(ordered : t.Ordered) (lowerBound upperBound: α) : (t : Impl α (fun _ => Unit))[lowerBound<...<upperBound].toList = (Internal.Impl.keys t).filter (fun e => (compare e lowerBound).isGT ∧ (compare e upperBound).isLT) := by
|
||||
simp only [Roo.Sliceable.mkSlice, Slice.toList_eq_toList_iter, Slice.iter,
|
||||
simp only [Roo.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter,
|
||||
Slice.Internal.iter_eq_toIteratorIter, ToIterator.iter, ToIterator.iterM_eq,
|
||||
Iter.toIter_toIterM]
|
||||
rw [Iter.toList_map]
|
||||
|
|
@ -1216,7 +1216,7 @@ public instance [Ord α] {s : RooSlice α β} : ToIterator s Id (α × β) := by
|
|||
|
||||
public theorem toList_roo {α : Type u} {β : Type v} [Ord α] [TransOrd α] (t : Impl α (fun _ => β))
|
||||
(ordered : t.Ordered) (lowerBound upperBound : α) : t[lowerBound<...<upperBound].toList = (Internal.Impl.Const.toList t).filter (fun e => (compare e.fst lowerBound).isGT ∧ (compare e.fst upperBound).isLT) := by
|
||||
simp only [Roo.Sliceable.mkSlice, Slice.toList_eq_toList_iter, Slice.iter,
|
||||
simp only [Roo.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter,
|
||||
Slice.Internal.iter_eq_toIteratorIter, ToIterator.iter, ToIterator.iterM_eq,
|
||||
Iter.toIter_toIterM]
|
||||
rw [Iter.toList_map]
|
||||
|
|
@ -1284,7 +1284,7 @@ public instance [Ord α] {s : RocSlice α β} : ToIterator s Id ((a : α) × β
|
|||
|
||||
public theorem toList_roc {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] (t : Impl α β)
|
||||
(ordered : t.Ordered) (lowerBound upperBound : α) : t[lowerBound<...=upperBound].toList = t.toList.filter (fun e => (compare e.fst lowerBound).isGT ∧ (compare e.fst upperBound).isLE) := by
|
||||
simp only [Roc.Sliceable.mkSlice, Slice.toList_eq_toList_iter, Slice.iter,
|
||||
simp only [Roc.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter,
|
||||
Slice.Internal.iter_eq_toIteratorIter, ToIterator.iter, ToIterator.iterM_eq,
|
||||
Iter.toIter_toIterM]
|
||||
rw [toList_rocIter]
|
||||
|
|
@ -1309,7 +1309,7 @@ public instance [Ord α] {s : Unit.RocSlice α} : ToIterator s Id α := by
|
|||
|
||||
public theorem toList_roc {α : Type u} [Ord α] [TransOrd α] (t : Impl α (fun _ => Unit))
|
||||
(ordered : t.Ordered) (lowerBound upperBound: α) : (t : Impl α (fun _ => Unit))[lowerBound<...=upperBound].toList = (Internal.Impl.keys t).filter (fun e => (compare e lowerBound).isGT ∧ (compare e upperBound).isLE) := by
|
||||
simp only [Roc.Sliceable.mkSlice, Slice.toList_eq_toList_iter, Slice.iter,
|
||||
simp only [Roc.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter,
|
||||
Slice.Internal.iter_eq_toIteratorIter, ToIterator.iter, ToIterator.iterM_eq,
|
||||
Iter.toIter_toIterM]
|
||||
rw [Iter.toList_map]
|
||||
|
|
@ -1343,7 +1343,7 @@ public instance [Ord α] {s : RocSlice α β} : ToIterator s Id (α × β) := by
|
|||
|
||||
public theorem toList_roc {α : Type u} {β : Type v} [Ord α] [TransOrd α] (t : Impl α (fun _ => β))
|
||||
(ordered : t.Ordered) (lowerBound upperBound : α) : t[lowerBound<...=upperBound].toList = (Internal.Impl.Const.toList t).filter (fun e => (compare e.fst lowerBound).isGT ∧ (compare e.fst upperBound).isLE) := by
|
||||
simp only [Roc.Sliceable.mkSlice, Slice.toList_eq_toList_iter, Slice.iter,
|
||||
simp only [Roc.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter,
|
||||
Slice.Internal.iter_eq_toIteratorIter, ToIterator.iter, ToIterator.iterM_eq,
|
||||
Iter.toIter_toIterM]
|
||||
rw [Iter.toList_map]
|
||||
|
|
@ -1396,7 +1396,7 @@ public instance [Ord α] {s : RciSlice α β} : ToIterator s Id ((a : α) × β
|
|||
|
||||
public theorem toList_rci {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] (t : Impl α β)
|
||||
(ordered : t.Ordered) (lowerBound : α) : t[lowerBound...*].toList = t.toList.filter (fun e => (compare e.fst lowerBound).isGE) := by
|
||||
simp only [Rci.Sliceable.mkSlice, Slice.toList_eq_toList_iter, Slice.iter,
|
||||
simp only [Rci.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter,
|
||||
Slice.Internal.iter_eq_toIteratorIter, ToIterator.iter, ToIterator.iterM_eq,
|
||||
Iter.toIter_toIterM]
|
||||
rw [toList_rciIter]
|
||||
|
|
@ -1421,7 +1421,7 @@ public instance [Ord α] {s : Unit.RciSlice α} : ToIterator s Id α := by
|
|||
|
||||
public theorem toList_rci {α : Type u} [Ord α] [TransOrd α] (t : Impl α (fun _ => Unit))
|
||||
(ordered : t.Ordered) (lowerBound : α) : (t : Impl α (fun _ => Unit))[lowerBound...*].toList = (Internal.Impl.keys t).filter (fun e => (compare e lowerBound).isGE) := by
|
||||
simp only [Rci.Sliceable.mkSlice, Slice.toList_eq_toList_iter, Slice.iter,
|
||||
simp only [Rci.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter,
|
||||
Slice.Internal.iter_eq_toIteratorIter, ToIterator.iter, ToIterator.iterM_eq,
|
||||
Iter.toIter_toIterM]
|
||||
rw [Iter.toList_map]
|
||||
|
|
@ -1458,7 +1458,7 @@ public instance [Ord α] {s : RciSlice α β} : ToIterator s Id (α × β) := by
|
|||
|
||||
public theorem toList_rci {α : Type u} {β : Type v} [Ord α] [TransOrd α] (t : Impl α (fun _ => β))
|
||||
(ordered : t.Ordered) (lowerBound : α) : t[lowerBound...*].toList = (Internal.Impl.Const.toList t).filter (fun e => (compare e.fst lowerBound).isGE) := by
|
||||
simp only [Rci.Sliceable.mkSlice, Slice.toList_eq_toList_iter, Slice.iter,
|
||||
simp only [Rci.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter,
|
||||
Slice.Internal.iter_eq_toIteratorIter, ToIterator.iter, ToIterator.iterM_eq,
|
||||
Iter.toIter_toIterM]
|
||||
rw [Iter.toList_map]
|
||||
|
|
@ -1512,7 +1512,7 @@ public instance [Ord α] {s : RoiSlice α β} : ToIterator s Id ((a : α) × β
|
|||
|
||||
public theorem toList_roi {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] (t : Impl α β)
|
||||
(ordered : t.Ordered) (lowerBound : α) : t[lowerBound<...*].toList = t.toList.filter (fun e => (compare e.fst lowerBound).isGT) := by
|
||||
simp only [Roi.Sliceable.mkSlice, Slice.toList_eq_toList_iter, Slice.iter,
|
||||
simp only [Roi.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter,
|
||||
Slice.Internal.iter_eq_toIteratorIter, ToIterator.iter, ToIterator.iterM_eq,
|
||||
Iter.toIter_toIterM]
|
||||
rw [toList_roiIter]
|
||||
|
|
@ -1537,7 +1537,7 @@ public instance [Ord α] {s : Unit.RoiSlice α} : ToIterator s Id α := by
|
|||
|
||||
public theorem toList_roi {α : Type u} [Ord α] [TransOrd α] (t : Impl α (fun _ => Unit))
|
||||
(ordered : t.Ordered) (lowerBound : α) : (t : Impl α (fun _ => Unit))[lowerBound<...*].toList = (Internal.Impl.keys t).filter (fun e => (compare e lowerBound).isGT) := by
|
||||
simp only [Roi.Sliceable.mkSlice, Slice.toList_eq_toList_iter, Slice.iter,
|
||||
simp only [Roi.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter,
|
||||
Slice.Internal.iter_eq_toIteratorIter, ToIterator.iter, ToIterator.iterM_eq,
|
||||
Iter.toIter_toIterM]
|
||||
rw [Iter.toList_map]
|
||||
|
|
@ -1574,7 +1574,7 @@ public instance [Ord α] {s : RoiSlice α β} : ToIterator s Id (α × β) := by
|
|||
|
||||
public theorem toList_roi {α : Type u} {β : Type v} [Ord α] [TransOrd α] (t : Impl α (fun _ => β))
|
||||
(ordered : t.Ordered) (lowerBound : α) : t[lowerBound<...*].toList = (Internal.Impl.Const.toList t).filter (fun e => (compare e.fst lowerBound).isGT) := by
|
||||
simp only [Roi.Sliceable.mkSlice, Slice.toList_eq_toList_iter, Slice.iter,
|
||||
simp only [Roi.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter,
|
||||
Slice.Internal.iter_eq_toIteratorIter, ToIterator.iter, ToIterator.iterM_eq,
|
||||
Iter.toIter_toIterM]
|
||||
rw [Iter.toList_map]
|
||||
|
|
@ -1621,7 +1621,7 @@ public instance {s : RiiSlice α β} : ToIterator s Id ((a : α) × β a) :=
|
|||
ToIterator.of (Zipper α β) (riiIterator s.1.treeMap)
|
||||
|
||||
public theorem toList_rii {α : Type u} {β : α → Type v} (t : Impl α β) : t[*...*].toList = t.toList := by
|
||||
simp only [Rii.Sliceable.mkSlice, Slice.toList_eq_toList_iter, Slice.iter,
|
||||
simp only [Rii.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter,
|
||||
Slice.Internal.iter_eq_toIteratorIter, ToIterator.iter, ToIterator.iterM_eq,
|
||||
Iter.toIter_toIterM]
|
||||
rw [toList_riiIter]
|
||||
|
|
@ -1645,7 +1645,7 @@ public instance {s : Unit.RiiSlice α} : ToIterator s Id α := by
|
|||
|
||||
public theorem toList_rii {α : Type u} (t : Impl α (fun _ => Unit)) :
|
||||
(t : Impl α fun _ => Unit)[*...*].toList = Internal.Impl.keys t := by
|
||||
simp only [Rii.Sliceable.mkSlice, Slice.toList_eq_toList_iter, Slice.iter,
|
||||
simp only [Rii.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter,
|
||||
Slice.Internal.iter_eq_toIteratorIter, ToIterator.iter, ToIterator.iterM_eq,
|
||||
Iter.toIter_toIterM]
|
||||
rw [Iter.toList_map]
|
||||
|
|
@ -1675,7 +1675,7 @@ public instance {s : Const.RiiSlice α β} : ToIterator s Id (α × β) := by
|
|||
|
||||
public theorem toList_rii {α : Type u} {β : Type v} (t : Impl α (fun _ => β)) :
|
||||
(t : Impl α fun _ => β)[*...*].toList = Internal.Impl.Const.toList t := by
|
||||
simp only [Rii.Sliceable.mkSlice, Slice.toList_eq_toList_iter, Slice.iter,
|
||||
simp only [Rii.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter,
|
||||
Slice.Internal.iter_eq_toIteratorIter, ToIterator.iter, ToIterator.iterM_eq,
|
||||
Iter.toIter_toIterM]
|
||||
rw [Iter.toList_map]
|
||||
|
|
|
|||
|
|
@ -15,51 +15,102 @@ namespace Std
|
|||
open Std.PRange Std.Iterators
|
||||
|
||||
@[simp]
|
||||
theorem Rcc.toList_iter [LE α] [DecidableLE α] [UpwardEnumerable α]
|
||||
[LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Rcc α} :
|
||||
r.iter.toList = r.toList := by
|
||||
rfl
|
||||
|
||||
@[deprecated Rcc.toList_iter (since := "2025-11-13")]
|
||||
theorem Rcc.toList_iter_eq_toList [LE α] [DecidableLE α] [UpwardEnumerable α]
|
||||
[LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Rcc α} :
|
||||
r.iter.toList = r.toList := by
|
||||
rfl
|
||||
|
||||
@[simp]
|
||||
theorem Rcc.toArray_iter [LE α] [DecidableLE α] [UpwardEnumerable α]
|
||||
[LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Rcc α} :
|
||||
r.iter.toArray = r.toArray := by
|
||||
rfl
|
||||
|
||||
@[deprecated Rcc.toArray_iter (since := "2025-11-13")]
|
||||
theorem Rcc.toArray_iter_eq_toArray [LE α] [DecidableLE α] [UpwardEnumerable α]
|
||||
[LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Rcc α} :
|
||||
r.iter.toArray = r.toArray := by
|
||||
rfl
|
||||
|
||||
@[simp]
|
||||
theorem Rcc.count_iter [LE α] [DecidableLE α] [UpwardEnumerable α]
|
||||
[LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α]
|
||||
[Rxc.HasSize α] [Rxc.LawfulHasSize α] {r : Rcc α} :
|
||||
r.iter.count = r.size := by
|
||||
rw [← size_toArray, ← toArray_iter, Iter.size_toArray_eq_count]
|
||||
|
||||
@[deprecated Rcc.count_iter (since := "2025-11-13")]
|
||||
theorem Rcc.count_iter_eq_size [LE α] [DecidableLE α] [UpwardEnumerable α]
|
||||
[LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α]
|
||||
[Rxc.HasSize α] [Rxc.LawfulHasSize α]
|
||||
{r : Rcc α} :
|
||||
r.iter.count = r.size := by
|
||||
rw [← size_toArray, ← toArray_iter_eq_toArray, Iter.size_toArray_eq_count]
|
||||
r.iter.count = r.size :=
|
||||
count_iter
|
||||
|
||||
@[simp]
|
||||
theorem Rco.toList_iter [LT α] [DecidableLT α] [UpwardEnumerable α]
|
||||
[LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Rco α} :
|
||||
r.iter.toList = r.toList := by
|
||||
rfl
|
||||
|
||||
@[deprecated Rco.toList_iter (since := "2025-11-13")]
|
||||
theorem Rco.toList_iter_eq_toList [LT α] [DecidableLT α] [UpwardEnumerable α]
|
||||
[LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Rco α} :
|
||||
r.iter.toList = r.toList := by
|
||||
rfl
|
||||
|
||||
@[simp]
|
||||
theorem Rco.toArray_iter [LT α] [DecidableLT α] [UpwardEnumerable α]
|
||||
[LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Rco α} :
|
||||
r.iter.toArray = r.toArray := by
|
||||
rfl
|
||||
|
||||
@[deprecated Rco.toArray_iter (since := "2025-11-13")]
|
||||
theorem Rco.toArray_iter_eq_toArray [LT α] [DecidableLT α] [UpwardEnumerable α]
|
||||
[LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Rco α} :
|
||||
r.iter.toArray = r.toArray := by
|
||||
rfl
|
||||
|
||||
@[simp]
|
||||
theorem Rco.count_iter [LT α] [DecidableLT α] [UpwardEnumerable α]
|
||||
[LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α]
|
||||
[Rxo.HasSize α] [Rxo.LawfulHasSize α]
|
||||
{r : Rco α} :
|
||||
r.iter.count = r.size := by
|
||||
rw [← size_toArray, ← toArray_iter, Iter.size_toArray_eq_count]
|
||||
|
||||
@[deprecated Rco.count_iter (since := "2025-11-13")]
|
||||
theorem Rco.count_iter_eq_size [LT α] [DecidableLT α] [UpwardEnumerable α]
|
||||
[LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α]
|
||||
[Rxo.HasSize α] [Rxo.LawfulHasSize α]
|
||||
{r : Rco α} :
|
||||
r.iter.count = r.size := by
|
||||
rw [← size_toArray, ← toArray_iter_eq_toArray, Iter.size_toArray_eq_count]
|
||||
rw [← size_toArray, ← toArray_iter, Iter.size_toArray_eq_count]
|
||||
|
||||
@[simp]
|
||||
theorem Rci.toList_iter [UpwardEnumerable α]
|
||||
[Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Rci α} :
|
||||
r.iter.toList = r.toList := by
|
||||
rfl
|
||||
|
||||
@[deprecated Rci.toList_iter (since := "2025-11-13")]
|
||||
theorem Rci.toList_iter_eq_toList [UpwardEnumerable α]
|
||||
[Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Rci α} :
|
||||
r.iter.toList = r.toList := by
|
||||
rfl
|
||||
|
||||
@[simp]
|
||||
theorem Rci.toArray_iter [UpwardEnumerable α]
|
||||
[Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Rci α} :
|
||||
r.iter.toArray = r.toArray := by
|
||||
rfl
|
||||
|
||||
@[simp]
|
||||
theorem Rci.toArray_iter_eq_toArray [UpwardEnumerable α]
|
||||
[Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Rci α} :
|
||||
|
|
@ -67,6 +118,14 @@ theorem Rci.toArray_iter_eq_toArray [UpwardEnumerable α]
|
|||
rfl
|
||||
|
||||
@[simp]
|
||||
theorem Rci.count_iter [UpwardEnumerable α]
|
||||
[Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α]
|
||||
[Rxi.HasSize α] [Rxi.LawfulHasSize α]
|
||||
{r : Rci α} :
|
||||
r.iter.count = r.size := by
|
||||
rw [← size_toArray, ← toArray_iter_eq_toArray, Iter.size_toArray_eq_count]
|
||||
|
||||
@[deprecated Rci.count_iter (since := "2025-11-13")]
|
||||
theorem Rci.count_iter_eq_size [UpwardEnumerable α]
|
||||
[Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α]
|
||||
[Rxi.HasSize α] [Rxi.LawfulHasSize α]
|
||||
|
|
@ -75,11 +134,23 @@ theorem Rci.count_iter_eq_size [UpwardEnumerable α]
|
|||
rw [← size_toArray, ← toArray_iter_eq_toArray, Iter.size_toArray_eq_count]
|
||||
|
||||
@[simp]
|
||||
theorem Roc.toList_iter [LE α] [DecidableLE α] [UpwardEnumerable α]
|
||||
[LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Roc α} :
|
||||
r.iter.toList = r.toList := by
|
||||
rfl
|
||||
|
||||
@[deprecated Roc.toList_iter (since := "2025-11-13")]
|
||||
theorem Roc.toList_iter_eq_toList [LE α] [DecidableLE α] [UpwardEnumerable α]
|
||||
[LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Roc α} :
|
||||
r.iter.toList = r.toList := by
|
||||
rfl
|
||||
|
||||
@[simp]
|
||||
theorem Roc.toArray_iter [LE α] [DecidableLE α] [UpwardEnumerable α]
|
||||
[LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Roc α} :
|
||||
r.iter.toArray = r.toArray := by
|
||||
rfl
|
||||
|
||||
@[simp]
|
||||
theorem Roc.toArray_iter_eq_toArray [LE α] [DecidableLE α] [UpwardEnumerable α]
|
||||
[LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Roc α} :
|
||||
|
|
@ -87,6 +158,14 @@ theorem Roc.toArray_iter_eq_toArray [LE α] [DecidableLE α] [UpwardEnumerable
|
|||
rfl
|
||||
|
||||
@[simp]
|
||||
theorem Roc.count_iter [LE α] [DecidableLE α] [UpwardEnumerable α]
|
||||
[LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α]
|
||||
[Rxc.HasSize α] [Rxc.LawfulHasSize α]
|
||||
{r : Roc α} :
|
||||
r.iter.count = r.size := by
|
||||
rw [← size_toArray, ← toArray_iter_eq_toArray, Iter.size_toArray_eq_count]
|
||||
|
||||
@[deprecated Roc.count_iter (since := "2025-11-13")]
|
||||
theorem Roc.count_iter_eq_size [LE α] [DecidableLE α] [UpwardEnumerable α]
|
||||
[LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α]
|
||||
[Rxc.HasSize α] [Rxc.LawfulHasSize α]
|
||||
|
|
@ -95,11 +174,23 @@ theorem Roc.count_iter_eq_size [LE α] [DecidableLE α] [UpwardEnumerable α]
|
|||
rw [← size_toArray, ← toArray_iter_eq_toArray, Iter.size_toArray_eq_count]
|
||||
|
||||
@[simp]
|
||||
theorem Roo.toList_iter [LT α] [DecidableLT α] [UpwardEnumerable α]
|
||||
[LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Roo α} :
|
||||
r.iter.toList = r.toList := by
|
||||
rfl
|
||||
|
||||
@[deprecated Roo.toList_iter (since := "2025-11-13")]
|
||||
theorem Roo.toList_iter_eq_toList [LT α] [DecidableLT α] [UpwardEnumerable α]
|
||||
[LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Roo α} :
|
||||
r.iter.toList = r.toList := by
|
||||
rfl
|
||||
|
||||
@[simp]
|
||||
theorem Roo.toArray_iter [LT α] [DecidableLT α] [UpwardEnumerable α]
|
||||
[LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Roo α} :
|
||||
r.iter.toArray = r.toArray := by
|
||||
rfl
|
||||
|
||||
@[simp]
|
||||
theorem Roo.toArray_iter_eq_toArray [LT α] [DecidableLT α] [UpwardEnumerable α]
|
||||
[LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Roo α} :
|
||||
|
|
@ -107,6 +198,14 @@ theorem Roo.toArray_iter_eq_toArray [LT α] [DecidableLT α] [UpwardEnumerable
|
|||
rfl
|
||||
|
||||
@[simp]
|
||||
theorem Roo.count_iter [LT α] [DecidableLT α] [UpwardEnumerable α]
|
||||
[LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α]
|
||||
[Rxo.HasSize α] [Rxo.LawfulHasSize α]
|
||||
{r : Roo α} :
|
||||
r.iter.count = r.size := by
|
||||
rw [← size_toArray, ← toArray_iter_eq_toArray, Iter.size_toArray_eq_count]
|
||||
|
||||
@[deprecated Roo.count_iter (since := "2025-11-13")]
|
||||
theorem Roo.count_iter_eq_size [LT α] [DecidableLT α] [UpwardEnumerable α]
|
||||
[LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α]
|
||||
[Rxo.HasSize α] [Rxo.LawfulHasSize α]
|
||||
|
|
@ -115,83 +214,163 @@ theorem Roo.count_iter_eq_size [LT α] [DecidableLT α] [UpwardEnumerable α]
|
|||
rw [← size_toArray, ← toArray_iter_eq_toArray, Iter.size_toArray_eq_count]
|
||||
|
||||
@[simp]
|
||||
theorem Roi.toList_iter [UpwardEnumerable α]
|
||||
[Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Roi α} :
|
||||
r.iter.toList = r.toList := by
|
||||
rfl
|
||||
|
||||
@[deprecated Roi.toList_iter (since := "2025-11-13")]
|
||||
theorem Roi.toList_iter_eq_toList [UpwardEnumerable α]
|
||||
[Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Roi α} :
|
||||
r.iter.toList = r.toList := by
|
||||
rfl
|
||||
|
||||
@[simp]
|
||||
theorem Roi.toArray_iter [UpwardEnumerable α]
|
||||
[Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Roi α} :
|
||||
r.iter.toArray = r.toArray := by
|
||||
rfl
|
||||
|
||||
@[deprecated Roi.toArray_iter (since := "2025-11-13")]
|
||||
theorem Roi.toArray_iter_eq_toArray [UpwardEnumerable α]
|
||||
[Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Roi α} :
|
||||
r.iter.toArray = r.toArray := by
|
||||
rfl
|
||||
|
||||
@[simp]
|
||||
theorem Roi.count_iter [UpwardEnumerable α]
|
||||
[Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α]
|
||||
[Rxi.HasSize α] [Rxi.LawfulHasSize α]
|
||||
{r : Roi α} :
|
||||
r.iter.count = r.size := by
|
||||
rw [← size_toArray, ← toArray_iter, Iter.size_toArray_eq_count]
|
||||
|
||||
@[deprecated Roi.count_iter (since := "2025-11-13")]
|
||||
theorem Roi.count_iter_eq_size [UpwardEnumerable α]
|
||||
[Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α]
|
||||
[Rxi.HasSize α] [Rxi.LawfulHasSize α]
|
||||
{r : Roi α} :
|
||||
r.iter.count = r.size := by
|
||||
rw [← size_toArray, ← toArray_iter_eq_toArray, Iter.size_toArray_eq_count]
|
||||
rw [← size_toArray, ← toArray_iter, Iter.size_toArray_eq_count]
|
||||
|
||||
@[simp]
|
||||
theorem Ric.toList_iter [Least? α] [LE α] [DecidableLE α] [UpwardEnumerable α]
|
||||
[LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Ric α} :
|
||||
r.iter.toList = r.toList := by
|
||||
rfl
|
||||
|
||||
@[deprecated Ric.toList_iter (since := "2025-11-13")]
|
||||
theorem Ric.toList_iter_eq_toList [Least? α] [LE α] [DecidableLE α] [UpwardEnumerable α]
|
||||
[LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Ric α} :
|
||||
r.iter.toList = r.toList := by
|
||||
rfl
|
||||
|
||||
@[simp]
|
||||
theorem Ric.toArray_iter [Least? α] [LE α] [DecidableLE α] [UpwardEnumerable α]
|
||||
[LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Ric α} :
|
||||
r.iter.toArray = r.toArray := by
|
||||
rfl
|
||||
|
||||
@[deprecated Ric.toArray_iter (since := "2025-11-13")]
|
||||
theorem Ric.toArray_iter_eq_toArray [Least? α] [LE α] [DecidableLE α] [UpwardEnumerable α]
|
||||
[LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Ric α} :
|
||||
r.iter.toArray = r.toArray := by
|
||||
rfl
|
||||
|
||||
@[simp]
|
||||
theorem Ric.count_iter [Least? α] [LE α] [DecidableLE α] [UpwardEnumerable α]
|
||||
[LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α]
|
||||
[Rxc.HasSize α] [Rxc.LawfulHasSize α]
|
||||
{r : Ric α} :
|
||||
r.iter.count = r.size := by
|
||||
rw [← size_toArray, ← toArray_iter, Iter.size_toArray_eq_count]
|
||||
|
||||
@[deprecated Ric.count_iter (since := "2025-11-13")]
|
||||
theorem Ric.count_iter_eq_size [Least? α] [LE α] [DecidableLE α] [UpwardEnumerable α]
|
||||
[LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α]
|
||||
[Rxc.HasSize α] [Rxc.LawfulHasSize α]
|
||||
{r : Ric α} :
|
||||
r.iter.count = r.size := by
|
||||
rw [← size_toArray, ← toArray_iter_eq_toArray, Iter.size_toArray_eq_count]
|
||||
rw [← size_toArray, ← toArray_iter, Iter.size_toArray_eq_count]
|
||||
|
||||
@[simp]
|
||||
theorem Rio.toList_iter [Least? α] [LT α] [DecidableLT α] [UpwardEnumerable α]
|
||||
[LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Rio α} :
|
||||
r.iter.toList = r.toList := by
|
||||
rfl
|
||||
|
||||
@[deprecated Rio.toList_iter (since := "2025-11-13")]
|
||||
theorem Rio.toList_iter_eq_toList [Least? α] [LT α] [DecidableLT α] [UpwardEnumerable α]
|
||||
[LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Rio α} :
|
||||
r.iter.toList = r.toList := by
|
||||
rfl
|
||||
|
||||
@[simp]
|
||||
theorem Rio.toArray_iter [Least? α] [LT α] [DecidableLT α] [UpwardEnumerable α]
|
||||
[LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Rio α} :
|
||||
r.iter.toArray = r.toArray := by
|
||||
rfl
|
||||
|
||||
@[deprecated Rio.toArray_iter (since := "2025-11-13")]
|
||||
theorem Rio.toArray_iter_eq_toArray [Least? α] [LT α] [DecidableLT α] [UpwardEnumerable α]
|
||||
[LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Rio α} :
|
||||
r.iter.toArray = r.toArray := by
|
||||
rfl
|
||||
|
||||
@[simp]
|
||||
theorem Rio.count_iter [Least? α] [LT α] [DecidableLT α] [UpwardEnumerable α]
|
||||
[LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α]
|
||||
[Rxo.HasSize α] [Rxo.LawfulHasSize α]
|
||||
{r : Rio α} :
|
||||
r.iter.count = r.size := by
|
||||
rw [← size_toArray, ← toArray_iter, Iter.size_toArray_eq_count]
|
||||
|
||||
@[deprecated Rio.count_iter (since := "2025-11-13")]
|
||||
theorem Rio.count_iter_eq_size [Least? α] [LT α] [DecidableLT α] [UpwardEnumerable α]
|
||||
[LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α]
|
||||
[Rxo.HasSize α] [Rxo.LawfulHasSize α]
|
||||
{r : Rio α} :
|
||||
r.iter.count = r.size := by
|
||||
rw [← size_toArray, ← toArray_iter_eq_toArray, Iter.size_toArray_eq_count]
|
||||
rw [← size_toArray, ← toArray_iter, Iter.size_toArray_eq_count]
|
||||
|
||||
@[simp]
|
||||
theorem Rii.toList_iter [Least? α] [UpwardEnumerable α]
|
||||
[Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Rii α} :
|
||||
r.iter.toList = r.toList := by
|
||||
rfl
|
||||
|
||||
@[deprecated Rii.toList_iter (since := "2025-11-13")]
|
||||
theorem Rii.toList_iter_eq_toList [Least? α] [UpwardEnumerable α]
|
||||
[Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Rii α} :
|
||||
r.iter.toList = r.toList := by
|
||||
rfl
|
||||
|
||||
@[simp]
|
||||
theorem Rii.toArray_iter [Least? α] [UpwardEnumerable α]
|
||||
[Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Rii α} :
|
||||
r.iter.toArray = r.toArray := by
|
||||
rfl
|
||||
|
||||
@[deprecated Rii.toArray_iter (since := "2025-11-13")]
|
||||
theorem Rii.toArray_iter_eq_toArray [Least? α] [UpwardEnumerable α]
|
||||
[Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Rii α} :
|
||||
r.iter.toArray = r.toArray := by
|
||||
rfl
|
||||
|
||||
@[simp]
|
||||
theorem Rii.count_iter [Least? α] [UpwardEnumerable α]
|
||||
[Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α]
|
||||
[Rxi.HasSize α] [Rxi.LawfulHasSize α]
|
||||
{r : Rii α} :
|
||||
r.iter.count = r.size := by
|
||||
rw [← size_toArray, ← toArray_iter, Iter.size_toArray_eq_count]
|
||||
|
||||
@[deprecated Rii.count_iter (since := "2025-11-13")]
|
||||
theorem Rii.count_iter_eq_size [Least? α] [UpwardEnumerable α]
|
||||
[Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α]
|
||||
[Rxi.HasSize α] [Rxi.LawfulHasSize α]
|
||||
{r : Rii α} :
|
||||
r.iter.count = r.size := by
|
||||
rw [← size_toArray, ← toArray_iter_eq_toArray, Iter.size_toArray_eq_count]
|
||||
rw [← size_toArray, ← toArray_iter, Iter.size_toArray_eq_count]
|
||||
|
||||
end Std
|
||||
|
|
|
|||
|
|
@ -43,21 +43,44 @@ theorem count_iter_eq_size [∀ s : Slice γ, ToIterator s Id β]
|
|||
s.iter.count = s.size :=
|
||||
size_eq_count_iter.symm
|
||||
|
||||
@[simp]
|
||||
theorem toArray_iter {s : Slice γ} [ToIterator s Id β]
|
||||
[Iterator (ToIterator.State s Id) Id β] [IteratorCollect (ToIterator.State s Id) Id Id]
|
||||
[Finite (ToIterator.State s Id) Id] :
|
||||
s.iter.toArray = s.toArray := by
|
||||
simp [Internal.iter_eq_iter, Internal.toArray_eq_toArray_iter]
|
||||
|
||||
@[deprecated toArray_iter (since := "2025-11-13")]
|
||||
theorem toArray_eq_toArray_iter {s : Slice γ} [ToIterator s Id β]
|
||||
[Iterator (ToIterator.State s Id) Id β] [IteratorCollect (ToIterator.State s Id) Id Id]
|
||||
[Finite (ToIterator.State s Id) Id] :
|
||||
s.toArray = s.iter.toArray := by
|
||||
simp [Internal.iter_eq_iter, Internal.toArray_eq_toArray_iter]
|
||||
simp
|
||||
|
||||
@[simp]
|
||||
theorem toList_iter {s : Slice γ} [ToIterator s Id β]
|
||||
[Iterator (ToIterator.State s Id) Id β] [IteratorCollect (ToIterator.State s Id) Id Id]
|
||||
[Finite (ToIterator.State s Id) Id] :
|
||||
s.iter.toList = s.toList := by
|
||||
simp [Internal.iter_eq_iter, Internal.toList_eq_toList_iter]
|
||||
|
||||
@[deprecated toList_iter (since := "2025-11-13")]
|
||||
theorem toList_eq_toList_iter {s : Slice γ} [ToIterator s Id β]
|
||||
[Iterator (ToIterator.State s Id) Id β] [IteratorCollect (ToIterator.State s Id) Id Id]
|
||||
[Finite (ToIterator.State s Id) Id] :
|
||||
s.toList = s.iter.toList := by
|
||||
simp [Internal.iter_eq_iter, Internal.toList_eq_toList_iter]
|
||||
simp
|
||||
|
||||
@[simp]
|
||||
theorem toListRev_iter {s : Slice γ} [ToIterator s Id β]
|
||||
[Iterator (ToIterator.State s Id) Id β] [Finite (ToIterator.State s Id) Id] :
|
||||
s.iter.toListRev = s.toListRev := by
|
||||
simp [Internal.iter_eq_iter, Internal.toListRev_eq_toListRev_iter]
|
||||
|
||||
@[deprecated toListRev_iter (since := "2025-11-13")]
|
||||
theorem toListRev_eq_toListRev_iter {s : Slice γ} [ToIterator s Id β]
|
||||
[Iterator (ToIterator.State s Id) Id β] [Finite (ToIterator.State s Id) Id] :
|
||||
s.toListRev = s.iter.toListRev := by
|
||||
simp [Internal.iter_eq_iter, Internal.toListRev_eq_toListRev_iter]
|
||||
simp
|
||||
|
||||
end Std.Slice
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue