Lemmas about ranges #
This file provides lemmas about Std.PRange.
theorem
Std.PRange.RangeIterator.toList_eq_match
{α : Type u}
{su : BoundShape}
[UpwardEnumerable α]
[SupportsUpperBound su α]
[HasFiniteRanges su α]
[LawfulUpwardEnumerable α]
{it : Iter α}
:
it.toList = match it.internalState.next with
| none => []
| some a =>
if SupportsUpperBound.IsSatisfied it.internalState.upperBound a then
a :: { internalState := { next := succ? a, upperBound := it.internalState.upperBound } }.toList
else []
theorem
Std.PRange.RangeIterator.toArray_eq_match
{α : Type u}
{su : BoundShape}
[UpwardEnumerable α]
[SupportsUpperBound su α]
[HasFiniteRanges su α]
[LawfulUpwardEnumerable α]
{it : Iter α}
:
it.toArray = match it.internalState.next with
| none => #[]
| some a =>
if SupportsUpperBound.IsSatisfied it.internalState.upperBound a then
#[a] ++ { internalState := { next := succ? a, upperBound := it.internalState.upperBound } }.toArray
else #[]
@[simp]
theorem
Std.PRange.toList_toArray
{α : Type u}
{sl su : BoundShape}
[UpwardEnumerable α]
[BoundedUpwardEnumerable sl α]
[SupportsUpperBound su α]
[HasFiniteRanges su α]
[LawfulUpwardEnumerable α]
{r : PRange { lower := sl, upper := su } α}
:
@[simp]
theorem
Std.PRange.toArray_toList
{α : Type u}
{sl su : BoundShape}
[UpwardEnumerable α]
[BoundedUpwardEnumerable sl α]
[SupportsUpperBound su α]
[HasFiniteRanges su α]
[LawfulUpwardEnumerable α]
{r : PRange { lower := sl, upper := su } α}
:
theorem
Std.PRange.toList_eq_match
{α : Type u}
{sl su : BoundShape}
[UpwardEnumerable α]
[BoundedUpwardEnumerable sl α]
[SupportsUpperBound su α]
[HasFiniteRanges su α]
[LawfulUpwardEnumerable α]
{r : PRange { lower := sl, upper := su } α}
:
theorem
Std.PRange.toArray_eq_match
{α : Type u}
{sl su : BoundShape}
[UpwardEnumerable α]
[BoundedUpwardEnumerable sl α]
[SupportsUpperBound su α]
[HasFiniteRanges su α]
[LawfulUpwardEnumerable α]
{r : PRange { lower := sl, upper := su } α}
:
theorem
Std.PRange.toList_Rox_eq_toList_Rcx_of_isSome_succ?
{α : Type u}
{su : BoundShape}
[UpwardEnumerable α]
[SupportsUpperBound su α]
[HasFiniteRanges su α]
[LawfulUpwardEnumerable α]
{lo : Bound BoundShape.open α}
{hi : Bound { lower := BoundShape.open, upper := su }.upper α}
(h : (succ? lo).isSome = true)
:
@[deprecated Std.PRange.toList_Rox_eq_toList_Rcx_of_isSome_succ? (since := "2025-08-22")]
theorem
Std.PRange.toList_open_eq_toList_closed_of_isSome_succ?
{α : Type u}
{su : BoundShape}
[UpwardEnumerable α]
[SupportsUpperBound su α]
[HasFiniteRanges su α]
[LawfulUpwardEnumerable α]
{lo : Bound BoundShape.open α}
{hi : Bound { lower := BoundShape.open, upper := su }.upper α}
(h : (succ? lo).isSome = true)
:
theorem
Std.PRange.toArray_Rox_eq_toList_Rcx_of_isSome_succ?
{α : Type u}
{su : BoundShape}
[UpwardEnumerable α]
[SupportsUpperBound su α]
[HasFiniteRanges su α]
[LawfulUpwardEnumerable α]
{lo : Bound BoundShape.open α}
{hi : Bound { lower := BoundShape.open, upper := su }.upper α}
(h : (succ? lo).isSome = true)
:
theorem
Std.PRange.toList_eq_nil_iff
{α : Type u}
{sl su : BoundShape}
[UpwardEnumerable α]
[SupportsUpperBound su α]
[HasFiniteRanges su α]
[BoundedUpwardEnumerable sl α]
[LawfulUpwardEnumerable α]
{r : PRange { lower := sl, upper := su } α}
:
theorem
Std.PRange.toArray_eq_empty_iff
{α : Type u}
{sl su : BoundShape}
[UpwardEnumerable α]
[SupportsUpperBound su α]
[HasFiniteRanges su α]
[BoundedUpwardEnumerable sl α]
[LawfulUpwardEnumerable α]
{r : PRange { lower := sl, upper := su } α}
:
theorem
Std.PRange.mem_toList_iff_mem
{α : Type u}
{sl su : BoundShape}
[UpwardEnumerable α]
[SupportsUpperBound su α]
[SupportsLowerBound sl α]
[HasFiniteRanges su α]
[BoundedUpwardEnumerable sl α]
[LawfulUpwardEnumerable α]
[LawfulUpwardEnumerableLowerBound sl α]
[LawfulUpwardEnumerableUpperBound su α]
{r : PRange { lower := sl, upper := su } α}
{a : α}
:
theorem
Std.PRange.mem_toArray_iff_mem
{α : Type u}
{sl su : BoundShape}
[UpwardEnumerable α]
[SupportsUpperBound su α]
[SupportsLowerBound sl α]
[HasFiniteRanges su α]
[BoundedUpwardEnumerable sl α]
[LawfulUpwardEnumerable α]
[LawfulUpwardEnumerableLowerBound sl α]
[LawfulUpwardEnumerableUpperBound su α]
{r : PRange { lower := sl, upper := su } α}
{a : α}
:
theorem
Std.PRange.BoundedUpwardEnumerable.init?_succ?_closed
{α : Type u}
[UpwardEnumerable α]
[LawfulUpwardEnumerable α]
{lower lower' : Bound BoundShape.closed α}
(h : succ? lower = some lower')
:
@[deprecated Std.PRange.BoundedUpwardEnumerable.init?_succ?_closed (since := "2025-08-22")]
theorem
Std.PRange.BoundedUpwardEnumerable.Closed.init?_succ
{α : Type u}
[UpwardEnumerable α]
[LawfulUpwardEnumerable α]
{lower lower' : Bound BoundShape.closed α}
(h : succ? lower = some lower')
:
theorem
Std.PRange.pairwise_toList_upwardEnumerableLt
{α : Type u}
{sl su : BoundShape}
[UpwardEnumerable α]
[SupportsUpperBound su α]
[SupportsLowerBound sl α]
[HasFiniteRanges su α]
[BoundedUpwardEnumerable sl α]
[LawfulUpwardEnumerable α]
[LawfulUpwardEnumerableLowerBound sl α]
[LawfulUpwardEnumerableUpperBound su α]
{r : PRange { lower := sl, upper := su } α}
:
List.Pairwise (fun (a b : α) => UpwardEnumerable.LT a b) r.toList
theorem
Std.PRange.pairwise_toList_ne
{α : Type u}
{sl su : BoundShape}
[UpwardEnumerable α]
[SupportsUpperBound su α]
[SupportsLowerBound sl α]
[HasFiniteRanges su α]
[BoundedUpwardEnumerable sl α]
[LawfulUpwardEnumerable α]
[LawfulUpwardEnumerableLowerBound sl α]
[LawfulUpwardEnumerableUpperBound su α]
{r : PRange { lower := sl, upper := su } α}
:
List.Pairwise (fun (a b : α) => a ≠ b) r.toList
theorem
Std.PRange.pairwise_toList_lt
{α : Type u}
{sl su : BoundShape}
[LT α]
[UpwardEnumerable α]
[SupportsUpperBound su α]
[SupportsLowerBound sl α]
[HasFiniteRanges su α]
[BoundedUpwardEnumerable sl α]
[LawfulUpwardEnumerable α]
[LawfulUpwardEnumerableLT α]
[LawfulUpwardEnumerableLowerBound sl α]
[LawfulUpwardEnumerableUpperBound su α]
{r : PRange { lower := sl, upper := su } α}
:
List.Pairwise (fun (a b : α) => a < b) r.toList
theorem
Std.PRange.pairwise_toList_le
{α : Type u}
{sl su : BoundShape}
[LE α]
[UpwardEnumerable α]
[SupportsUpperBound su α]
[SupportsLowerBound sl α]
[HasFiniteRanges su α]
[BoundedUpwardEnumerable sl α]
[LawfulUpwardEnumerable α]
[LawfulUpwardEnumerableLE α]
[LawfulUpwardEnumerableLowerBound sl α]
[LawfulUpwardEnumerableUpperBound su α]
{r : PRange { lower := sl, upper := su } α}
:
List.Pairwise (fun (a b : α) => a ≤ b) r.toList
theorem
Std.PRange.mem_Rco_succ_succ_iff
{α : Type u}
[UpwardEnumerable α]
[LinearlyUpwardEnumerable α]
[InfinitelyUpwardEnumerable α]
[SupportsUpperBound BoundShape.open α]
[SupportsLowerBound BoundShape.closed α]
[LawfulUpwardEnumerableLowerBound BoundShape.closed α]
[HasFiniteRanges BoundShape.open α]
[LawfulUpwardEnumerable α]
[LawfulOpenUpperBound α]
{lower : Bound BoundShape.closed α}
{upper : Bound BoundShape.open α}
{a : α}
:
@[deprecated Std.PRange.mem_Rco_succ_succ_iff (since := "2025-08-22")]
theorem
Std.PRange.ClosedOpen.mem_succ_iff
{α : Type u}
[UpwardEnumerable α]
[LinearlyUpwardEnumerable α]
[InfinitelyUpwardEnumerable α]
[SupportsUpperBound BoundShape.open α]
[SupportsLowerBound BoundShape.closed α]
[LawfulUpwardEnumerableLowerBound BoundShape.closed α]
[HasFiniteRanges BoundShape.open α]
[LawfulUpwardEnumerable α]
[LawfulOpenUpperBound α]
{lower : Bound BoundShape.closed α}
{upper : Bound BoundShape.open α}
{a : α}
:
theorem
Std.PRange.toList_Rco_succ_succ_eq_map
{α : Type u}
[UpwardEnumerable α]
[SupportsLowerBound BoundShape.closed α]
[LinearlyUpwardEnumerable α]
[InfinitelyUpwardEnumerable α]
[SupportsUpperBound BoundShape.open α]
[HasFiniteRanges BoundShape.open α]
[LawfulUpwardEnumerable α]
[LawfulOpenUpperBound α]
[LawfulUpwardEnumerableLowerBound BoundShape.closed α]
[LawfulUpwardEnumerableUpperBound BoundShape.open α]
{lower : Bound BoundShape.closed α}
{upper : Bound BoundShape.open α}
:
@[deprecated Std.PRange.toList_Rco_succ_succ_eq_map (since := "2025-08-22")]
theorem
Std.PRange.ClosedOpen.toList_succ_succ_eq_map
{α : Type u}
[UpwardEnumerable α]
[SupportsLowerBound BoundShape.closed α]
[LinearlyUpwardEnumerable α]
[InfinitelyUpwardEnumerable α]
[SupportsUpperBound BoundShape.open α]
[HasFiniteRanges BoundShape.open α]
[LawfulUpwardEnumerable α]
[LawfulOpenUpperBound α]
[LawfulUpwardEnumerableLowerBound BoundShape.closed α]
[LawfulUpwardEnumerableUpperBound BoundShape.open α]
{lower : Bound BoundShape.closed α}
{upper : Bound BoundShape.open α}
:
theorem
Std.PRange.toArray_Rco_succ_succ_eq_map
{α : Type u}
[UpwardEnumerable α]
[SupportsLowerBound BoundShape.closed α]
[LinearlyUpwardEnumerable α]
[InfinitelyUpwardEnumerable α]
[SupportsUpperBound BoundShape.open α]
[HasFiniteRanges BoundShape.open α]
[LawfulUpwardEnumerable α]
[LawfulOpenUpperBound α]
[LawfulUpwardEnumerableLowerBound BoundShape.closed α]
[LawfulUpwardEnumerableUpperBound BoundShape.open α]
{lower : Bound BoundShape.closed α}
{upper : Bound BoundShape.open α}
:
theorem
Std.PRange.forIn'_eq_forIn'_toList
{α : Type u}
{su sl : BoundShape}
[UpwardEnumerable α]
[SupportsUpperBound su α]
[SupportsLowerBound sl α]
[HasFiniteRanges su α]
[BoundedUpwardEnumerable sl α]
[LawfulUpwardEnumerable α]
[LawfulUpwardEnumerableLowerBound sl α]
[LawfulUpwardEnumerableUpperBound su α]
{r : PRange { lower := sl, upper := su } α}
{γ : Type u}
{init : γ}
{m : Type u → Type w}
[Monad m]
[LawfulMonad m]
{f : (a : α) → a ∈ r → γ → m (ForInStep γ)}
:
theorem
Std.PRange.forIn'_eq_forIn'_toArray
{α : Type u}
{su sl : BoundShape}
[UpwardEnumerable α]
[SupportsUpperBound su α]
[SupportsLowerBound sl α]
[HasFiniteRanges su α]
[BoundedUpwardEnumerable sl α]
[LawfulUpwardEnumerable α]
[LawfulUpwardEnumerableLowerBound sl α]
[LawfulUpwardEnumerableUpperBound su α]
{r : PRange { lower := sl, upper := su } α}
{γ : Type u}
{init : γ}
{m : Type u → Type w}
[Monad m]
[LawfulMonad m]
{f : (a : α) → a ∈ r → γ → m (ForInStep γ)}
:
theorem
Std.PRange.forIn'_toList_eq_forIn'
{α : Type u}
{su sl : BoundShape}
[UpwardEnumerable α]
[SupportsUpperBound su α]
[SupportsLowerBound sl α]
[HasFiniteRanges su α]
[BoundedUpwardEnumerable sl α]
[LawfulUpwardEnumerable α]
[LawfulUpwardEnumerableLowerBound sl α]
[LawfulUpwardEnumerableUpperBound su α]
{r : PRange { lower := sl, upper := su } α}
{γ : Type u}
{init : γ}
{m : Type u → Type w}
[Monad m]
[LawfulMonad m]
{f : (a : α) → a ∈ r.toList → γ → m (ForInStep γ)}
:
theorem
Std.PRange.forIn'_toArray_eq_forIn'
{α : Type u}
{su sl : BoundShape}
[UpwardEnumerable α]
[SupportsUpperBound su α]
[SupportsLowerBound sl α]
[HasFiniteRanges su α]
[BoundedUpwardEnumerable sl α]
[LawfulUpwardEnumerable α]
[LawfulUpwardEnumerableLowerBound sl α]
[LawfulUpwardEnumerableUpperBound su α]
{r : PRange { lower := sl, upper := su } α}
{γ : Type u}
{init : γ}
{m : Type u → Type w}
[Monad m]
[LawfulMonad m]
{f : (a : α) → a ∈ r.toArray → γ → m (ForInStep γ)}
:
theorem
Std.PRange.mem_of_mem_open
{α : Type u}
{su sl : BoundShape}
[UpwardEnumerable α]
[SupportsUpperBound su α]
[SupportsLowerBound sl α]
[HasFiniteRanges su α]
[BoundedUpwardEnumerable sl α]
[LawfulUpwardEnumerable α]
[LawfulUpwardEnumerableLowerBound sl α]
[LawfulUpwardEnumerableUpperBound su α]
[SupportsLowerBound BoundShape.open α]
[LawfulUpwardEnumerableLowerBound BoundShape.open α]
{r : PRange { lower := sl, upper := su } α}
{a b : α}
(hrb : SupportsLowerBound.IsSatisfied r.lower b)
(hmem : a ∈ { lower := b, upper := r.upper })
:
theorem
Std.PRange.SupportsLowerBound.isSatisfied_init?
{α : Type u}
{sl : BoundShape}
[UpwardEnumerable α]
[SupportsLowerBound sl α]
[BoundedUpwardEnumerable sl α]
[LawfulUpwardEnumerable α]
[LawfulUpwardEnumerableLowerBound sl α]
{bound : Bound sl α}
{a : α}
(h : init? bound = some a)
:
IsSatisfied bound a
theorem
Std.PRange.forIn'_eq_match
{α : Type u}
{sl su : BoundShape}
[UpwardEnumerable α]
[SupportsUpperBound su α]
[SupportsLowerBound sl α]
[HasFiniteRanges su α]
[BoundedUpwardEnumerable sl α]
[LawfulUpwardEnumerable α]
[LawfulUpwardEnumerableLowerBound sl α]
[LawfulUpwardEnumerableUpperBound su α]
[SupportsLowerBound BoundShape.open α]
[LawfulUpwardEnumerableLowerBound BoundShape.open α]
{r : PRange { lower := sl, upper := su } α}
{γ : Type u}
{init : γ}
{m : Type u → Type w}
[Monad m]
[LawfulMonad m]
{f : (a : α) → a ∈ r → γ → m (ForInStep γ)}
:
forIn' r init f = match hi : init? r.lower with
| none => pure init
| some a =>
if hu : SupportsUpperBound.IsSatisfied r.upper a then do
let __do_lift ← f a ⋯ init
match __do_lift with
| ForInStep.yield c =>
forIn' { lower := a, upper := r.upper } c
fun (a_1 : α) (ha : a_1 ∈ { lower := a, upper := r.upper }) (acc : γ) => f a_1 ⋯ acc
| ForInStep.done c => pure c
else pure init
instance
Std.PRange.instLawfulIteratorSizeRangeIteratorOfLawfulRangeSize
{α : Type u}
{su : BoundShape}
[UpwardEnumerable α]
[SupportsUpperBound su α]
[RangeSize su α]
[LawfulUpwardEnumerable α]
[HasFiniteRanges su α]
[LawfulRangeSize su α]
:
theorem
Std.PRange.length_toList
{α : Type u}
{sl su : BoundShape}
[UpwardEnumerable α]
[SupportsUpperBound su α]
[RangeSize su α]
[LawfulUpwardEnumerable α]
[BoundedUpwardEnumerable sl α]
[HasFiniteRanges su α]
[LawfulRangeSize su α]
{r : PRange { lower := sl, upper := su } α}
:
theorem
Std.PRange.size_toArray
{α : Type u}
{sl su : BoundShape}
[UpwardEnumerable α]
[SupportsUpperBound su α]
[RangeSize su α]
[LawfulUpwardEnumerable α]
[BoundedUpwardEnumerable sl α]
[HasFiniteRanges su α]
[LawfulRangeSize su α]
{r : PRange { lower := sl, upper := su } α}
:
theorem
Std.PRange.isEmpty_iff_forall_not_mem
{α : Type u}
{sl su : BoundShape}
[UpwardEnumerable α]
[LawfulUpwardEnumerable α]
[BoundedUpwardEnumerable sl α]
[SupportsLowerBound sl α]
[SupportsUpperBound su α]
[LawfulUpwardEnumerableLowerBound sl α]
[LawfulUpwardEnumerableUpperBound su α]
{r : PRange { lower := sl, upper := su } α}
:
theorem
Std.PRange.Std.PRange.getElem?_toList_Rcx_eq
{α : Type u}
{su : BoundShape}
[LE α]
[UpwardEnumerable α]
[LawfulUpwardEnumerable α]
[SupportsUpperBound su α]
[LawfulUpwardEnumerableUpperBound su α]
[LawfulUpwardEnumerableLE α]
[HasFiniteRanges su α]
{r : PRange { lower := BoundShape.closed, upper := su } α}
{i : Nat}
:
theorem
Std.PRange.Std.PRange.getElem?_toArray_Rcx_eq
{α : Type u}
{su : BoundShape}
[LE α]
[UpwardEnumerable α]
[LawfulUpwardEnumerable α]
[SupportsUpperBound su α]
[LawfulUpwardEnumerableUpperBound su α]
[LawfulUpwardEnumerableLE α]
[HasFiniteRanges su α]
{r : PRange { lower := BoundShape.closed, upper := su } α}
{i : Nat}
:
theorem
Std.PRange.Std.PRange.isSome_succMany?_of_lt_length_toList_Rcx
{α : Type u}
{su : BoundShape}
[LE α]
[UpwardEnumerable α]
[LawfulUpwardEnumerable α]
[SupportsUpperBound su α]
[LawfulUpwardEnumerableUpperBound su α]
[LawfulUpwardEnumerableLE α]
[HasFiniteRanges su α]
{r : PRange { lower := BoundShape.closed, upper := su } α}
{i : Nat}
(h : i < r.toList.length)
:
theorem
Std.PRange.Std.PRange.isSome_succMany?_of_lt_size_toArray_Rcx
{α : Type u}
{su : BoundShape}
[LE α]
[UpwardEnumerable α]
[LawfulUpwardEnumerable α]
[SupportsUpperBound su α]
[LawfulUpwardEnumerableUpperBound su α]
[LawfulUpwardEnumerableLE α]
[HasFiniteRanges su α]
{r : PRange { lower := BoundShape.closed, upper := su } α}
{i : Nat}
(h : i < r.toArray.size)
:
theorem
Std.PRange.Std.PRange.getElem_toList_Rcx_eq
{α : Type u}
{su : BoundShape}
[LE α]
[UpwardEnumerable α]
[LawfulUpwardEnumerable α]
[SupportsUpperBound su α]
[LawfulUpwardEnumerableUpperBound su α]
[LawfulUpwardEnumerableLE α]
[HasFiniteRanges su α]
{r : PRange { lower := BoundShape.closed, upper := su } α}
{i : Nat}
{h : i < r.toList.length}
:
theorem
Std.PRange.Std.PRange.getElem_toArray_Rcx_eq
{α : Type u}
{su : BoundShape}
[LE α]
[UpwardEnumerable α]
[LawfulUpwardEnumerable α]
[SupportsUpperBound su α]
[LawfulUpwardEnumerableUpperBound su α]
[LawfulUpwardEnumerableLE α]
[HasFiniteRanges su α]
{r : PRange { lower := BoundShape.closed, upper := su } α}
{i : Nat}
{h : i < r.toArray.size}
:
theorem
Std.PRange.Std.PRange.eq_succMany?_of_toList_Rcx_eq_append_cons
{α : Type u}
{su : BoundShape}
[LE α]
[UpwardEnumerable α]
[LawfulUpwardEnumerable α]
[LawfulUpwardEnumerableLE α]
[SupportsUpperBound su α]
[HasFiniteRanges su α]
[LawfulUpwardEnumerableUpperBound su α]
{r : PRange { lower := BoundShape.closed, upper := su } α}
{pref suff : List α}
{cur : α}
(h : r.toList = pref ++ cur :: suff)
:
theorem
Std.PRange.Std.PRange.eq_succMany?_of_toArray_Rcx_eq_append_append
{α : Type u}
{su : BoundShape}
[LE α]
[UpwardEnumerable α]
[LawfulUpwardEnumerable α]
[LawfulUpwardEnumerableLE α]
[SupportsUpperBound su α]
[HasFiniteRanges su α]
[LawfulUpwardEnumerableUpperBound su α]
{r : PRange { lower := BoundShape.closed, upper := su } α}
{pref suff : Array α}
{cur : α}
(h : r.toArray = pref ++ #[cur] ++ suff)
: