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 := UpwardEnumerable.succ? a, upperBound := it.internalState.upperBound } }.toList
else []
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.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 : (UpwardEnumerable.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.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.BoundedUpwardEnumerable.Closed.init?_succ
{α : Type u}
[UpwardEnumerable α]
[LawfulUpwardEnumerable α]
{lower lower' : Bound BoundShape.closed α}
(h : UpwardEnumerable.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.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.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 α}
:
{ lower := UpwardEnumerable.succ lower, upper := UpwardEnumerable.succ upper }.toList = List.map UpwardEnumerable.succ { lower := lower, upper := upper }.toList
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'_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.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 : BoundedUpwardEnumerable.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 : BoundedUpwardEnumerable.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.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 } α}
: