feat: any/all predicates for iterators (#10686)
This PR introduces `any`, `anyM`, `all` and `allM` for pure and monadic iterators. It also provides lemmas about them.
This commit is contained in:
Paul Reichert
GitHub
parent
3931a72573
commit
a73ebe8a77
9 changed files with 1372 additions and 4 deletions
|
|
@ -252,6 +252,7 @@ instance : LawfulMonad Id := by
|
|||
@[simp] theorem run_map (x : Id α) (f : α → β) : (f <$> x).run = f x.run := rfl
|
||||
@[simp] theorem run_bind (x : Id α) (f : α → Id β) : (x >>= f).run = (f x.run).run := rfl
|
||||
@[simp] theorem run_pure (a : α) : (pure a : Id α).run = a := rfl
|
||||
@[simp] theorem pure_run (a : Id α) : pure a.run = a := rfl
|
||||
@[simp] theorem run_seqRight (x y : Id α) : (x *> y).run = y.run := rfl
|
||||
@[simp] theorem run_seqLeft (x y : Id α) : (x <* y).run = x.run := rfl
|
||||
@[simp] theorem run_seq (f : Id (α → β)) (x : Id α) : (f <*> x).run = f.run x.run := rfl
|
||||
|
|
|
|||
|
|
@ -463,7 +463,7 @@ For each value emitted by the base iterator `it`, this combinator calls `f`.
|
|||
@[inline, expose]
|
||||
def IterM.mapM {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Iterator α m β]
|
||||
[Monad n] [MonadLiftT m n] (f : β → n γ) (it : IterM (α := α) m β) :=
|
||||
(it.filterMapWithPostcondition (fun b => some <$> PostconditionT.lift (f b)) : IterM n γ)
|
||||
(it.mapWithPostcondition (fun b => PostconditionT.lift (f b)) : IterM n γ)
|
||||
|
||||
/--
|
||||
If `it` is an iterator, then `it.filterM f` is another iterator that applies a monadic
|
||||
|
|
|
|||
|
|
@ -139,6 +139,70 @@ def Iter.Partial.fold {α : Type w} {β : Type w} {γ : Type x} [Iterator α Id
|
|||
(init : γ) (it : Iter.Partial (α := α) β) : γ :=
|
||||
ForIn.forIn (m := Id) it init (fun x acc => ForInStep.yield (f acc x))
|
||||
|
||||
set_option doc.verso true in
|
||||
/--
|
||||
Returns {lean}`true` if the monadic predicate {name}`p` returns {lean}`true` for
|
||||
any element emitted by the iterator {name}`it`.
|
||||
|
||||
{lit}`O(|xs|)`. Short-circuits upon encountering the first match. The elements in {name}`it` are
|
||||
examined in order of iteration.
|
||||
-/
|
||||
@[specialize]
|
||||
def Iter.anyM {α β : Type w} {m : Type → Type w'} [Monad m]
|
||||
[Iterator α Id β] [IteratorLoop α Id m] [Finite α Id]
|
||||
(p : β → m Bool) (it : Iter (α := α) β) : m Bool :=
|
||||
ForIn.forIn it false (fun x _ => do
|
||||
if ← p x then
|
||||
return .done true
|
||||
else
|
||||
return .yield false)
|
||||
|
||||
set_option doc.verso true in
|
||||
/--
|
||||
Returns {lean}`true` if the pure predicate {name}`p` returns {lean}`true` for
|
||||
any element emitted by the iterator {name}`it`.
|
||||
|
||||
{lit}`O(|xs|)`. Short-circuits upon encountering the first match. The elements in {name}`it` are
|
||||
examined in order of iteration.
|
||||
-/
|
||||
@[inline]
|
||||
def Iter.any {α β : Type w}
|
||||
[Iterator α Id β] [IteratorLoop α Id Id] [Finite α Id]
|
||||
(p : β → Bool) (it : Iter (α := α) β) : Bool :=
|
||||
(it.anyM (fun x => pure (f := Id) (p x))).run
|
||||
|
||||
set_option doc.verso true in
|
||||
/--
|
||||
Returns {lean}`true` if the monadic predicate {name}`p` returns {lean}`true` for
|
||||
all elements emitted by the iterator {name}`it`.
|
||||
|
||||
{lit}`O(|xs|)`. Short-circuits upon encountering the first mismatch. The elements in {name}`it` are
|
||||
examined in order of iteration.
|
||||
-/
|
||||
@[specialize]
|
||||
def Iter.allM {α β : Type w} {m : Type → Type w'} [Monad m]
|
||||
[Iterator α Id β] [IteratorLoop α Id m] [Finite α Id]
|
||||
(p : β → m Bool) (it : Iter (α := α) β) : m Bool :=
|
||||
ForIn.forIn it true (fun x _ => do
|
||||
if ← p x then
|
||||
return .yield true
|
||||
else
|
||||
return .done false)
|
||||
|
||||
set_option doc.verso true in
|
||||
/--
|
||||
Returns {lean}`true` if the pure predicate {name}`p` returns {lean}`true` for
|
||||
all elements emitted by the iterator {name}`it`.
|
||||
|
||||
{lit}`O(|xs|)`. Short-circuits upon encountering the first mismatch. The elements in {name}`it` are
|
||||
examined in order of iteration.
|
||||
-/
|
||||
@[inline]
|
||||
def Iter.all {α β : Type w}
|
||||
[Iterator α Id β] [IteratorLoop α Id Id] [Finite α Id]
|
||||
(p : β → Bool) (it : Iter (α := α) β) : Bool :=
|
||||
(it.allM (fun x => pure (f := Id) (p x))).run
|
||||
|
||||
@[always_inline, inline, expose, inherit_doc IterM.size]
|
||||
def Iter.size {α : Type w} {β : Type w} [Iterator α Id β] [IteratorSize α Id]
|
||||
(it : Iter (α := α) β) : Nat :=
|
||||
|
|
|
|||
|
|
@ -416,6 +416,169 @@ def IterM.Partial.drain {α : Type w} {m : Type w → Type w'} [Monad m] {β : T
|
|||
m PUnit :=
|
||||
it.fold (γ := PUnit) (fun _ _ => .unit) .unit
|
||||
|
||||
set_option doc.verso true in
|
||||
/--
|
||||
Returns {lean}`ULift.up true` if the monadic predicate {name}`p` returns {lean}`ULift.up true` for
|
||||
any element emitted by the iterator {name}`it`.
|
||||
|
||||
{lit}`O(|xs|)`. Short-circuits upon encountering the first match. The elements in {name}`it` are
|
||||
examined in order of iteration.
|
||||
|
||||
This function requires a {name}`Finite` instance proving that the iterator will finish after a
|
||||
finite number of steps. If the iterator is not finite or such an instance is not available,
|
||||
consider using {lit}`it.allowNontermination.anyM` instead of {lean}`it.anyM`. However, it is not
|
||||
possible to formally verify the behavior of the partial variant.
|
||||
-/
|
||||
@[specialize]
|
||||
def IterM.anyM {α β : Type w} {m : Type w → Type w'} [Monad m]
|
||||
[Iterator α m β] [IteratorLoop α m m] [Finite α m]
|
||||
(p : β → m (ULift Bool)) (it : IterM (α := α) m β) : m (ULift Bool) :=
|
||||
ForIn.forIn it (ULift.up false) (fun x _ => do
|
||||
if (← p x).down then
|
||||
return .done (.up true)
|
||||
else
|
||||
return .yield (.up false))
|
||||
|
||||
set_option doc.verso true in
|
||||
/--
|
||||
Returns {lean}`ULift.up true` if the monadic predicate {name}`p` returns {lean}`ULift.up true` for
|
||||
any element emitted by the iterator {name}`it`.
|
||||
|
||||
{lit}`O(|xs|)`. Short-circuits upon encountering the first match. The elements in {name}`it` are
|
||||
examined in order of iteration.
|
||||
|
||||
This is a partial, potentially nonterminating, function. It is not possible to formally verify
|
||||
its behavior. If the iterator has a {name}`Finite` instance, consider using {name}`IterM.anyM`
|
||||
instead.
|
||||
-/
|
||||
@[specialize]
|
||||
def IterM.Partial.anyM {α β : Type w} {m : Type w → Type w'} [Monad m]
|
||||
[Iterator α m β] [IteratorLoopPartial α m m]
|
||||
(p : β → m (ULift Bool)) (it : IterM.Partial (α := α) m β) : m (ULift Bool) :=
|
||||
ForIn.forIn it (ULift.up false) (fun x _ => do
|
||||
if (← p x).down then
|
||||
return .done (.up true)
|
||||
else
|
||||
return .yield (.up false))
|
||||
|
||||
set_option doc.verso true in
|
||||
/--
|
||||
Returns {lean}`ULift.up true` if the pure predicate {name}`p` returns {lean}`true` for
|
||||
any element emitted by the iterator {name}`it`.
|
||||
|
||||
{lit}`O(|xs|)`. Short-circuits upon encountering the first match. The elements in {name}`it` are
|
||||
examined in order of iteration.
|
||||
|
||||
This function requires a {name}`Finite` instance proving that the iterator will finish after a
|
||||
finite number of steps. If the iterator is not finite or such an instance is not available,
|
||||
consider using {lit}`it.allowNontermination.any` instead of {lean}`it.any`. However, it is not
|
||||
possible to formally verify the behavior of the partial variant.
|
||||
-/
|
||||
@[inline]
|
||||
def IterM.any {α β : Type w} {m : Type w → Type w'} [Monad m]
|
||||
[Iterator α m β] [IteratorLoop α m m] [Finite α m]
|
||||
(p : β → Bool) (it : IterM (α := α) m β) : m (ULift Bool) := do
|
||||
it.anyM (fun x => pure (.up (p x)))
|
||||
|
||||
set_option doc.verso true in
|
||||
/--
|
||||
Returns {lean}`ULift.up true` if the pure predicate {name}`p` returns {lean}`true` for
|
||||
any element emitted by the iterator {name}`it`.
|
||||
|
||||
{lit}`O(|xs|)`. Short-circuits upon encountering the first match. The elements in {name}`it` are
|
||||
examined in order of iteration.
|
||||
|
||||
This is a partial, potentially nonterminating, function. It is not possible to formally verify
|
||||
its behavior. If the iterator has a {name}`Finite` instance, consider using {name}`IterM.any`
|
||||
instead.
|
||||
-/
|
||||
@[inline]
|
||||
def IterM.Partial.any {α β : Type w} {m : Type w → Type w'} [Monad m]
|
||||
[Iterator α m β] [IteratorLoopPartial α m m]
|
||||
(p : β → Bool) (it : IterM.Partial (α := α) m β) : m (ULift Bool) := do
|
||||
it.anyM (fun x => pure (.up (p x)))
|
||||
|
||||
set_option doc.verso true in
|
||||
/--
|
||||
Returns {lean}`ULift.up true` if the monadic predicate {name}`p` returns {lean}`ULift.up true` for
|
||||
all elements emitted by the iterator {name}`it`.
|
||||
|
||||
{lit}`O(|xs|)`. Short-circuits upon encountering the first mismatch. The elements in {name}`it` are
|
||||
examined in order of iteration.
|
||||
|
||||
This function requires a {name}`Finite` instance proving that the iterator will finish after a
|
||||
finite number of steps. If the iterator is not finite or such an instance is not available,
|
||||
consider using {lit}`it.allowNontermination.allM` instead of {lean}`it.allM`. However, it is not
|
||||
possible to formally verify the behavior of the partial variant.
|
||||
-/
|
||||
@[specialize]
|
||||
def IterM.allM {α β : Type w} {m : Type w → Type w'} [Monad m]
|
||||
[Iterator α m β] [IteratorLoop α m m] [Finite α m]
|
||||
(p : β → m (ULift Bool)) (it : IterM (α := α) m β) : m (ULift Bool) := do
|
||||
ForIn.forIn it (ULift.up true) (fun x _ => do
|
||||
if (← p x).down then
|
||||
return .yield (.up true)
|
||||
else
|
||||
return .done (.up false))
|
||||
set_option doc.verso true in
|
||||
/--
|
||||
Returns {lean}`ULift.up true` if the monadic predicate {name}`p` returns {lean}`ULift.up true` for
|
||||
all elements emitted by the iterator {name}`it`.
|
||||
|
||||
{lit}`O(|xs|)`. Short-circuits upon encountering the first mismatch. The elements in {name}`it` are
|
||||
examined in order of iteration.
|
||||
|
||||
This is a partial, potentially nonterminating, function. It is not possible to formally verify
|
||||
its behavior. If the iterator has a {name}`Finite` instance, consider using {name}`IterM.allM`
|
||||
instead.
|
||||
-/
|
||||
@[specialize]
|
||||
def IterM.Partial.allM {α β : Type w} {m : Type w → Type w'} [Monad m]
|
||||
[Iterator α m β] [IteratorLoopPartial α m m]
|
||||
(p : β → m (ULift Bool)) (it : IterM.Partial (α := α) m β) : m (ULift Bool) := do
|
||||
ForIn.forIn it (ULift.up true) (fun x _ => do
|
||||
if (← p x).down then
|
||||
return .yield (.up true)
|
||||
else
|
||||
return .done (.up false))
|
||||
|
||||
set_option doc.verso true in
|
||||
/--
|
||||
Returns {lean}`ULift.up true` if the pure predicate {name}`p` returns {lean}`true` for
|
||||
all elements emitted by the iterator {name}`it`.
|
||||
|
||||
{lit}`O(|xs|)`. Short-circuits upon encountering the first mismatch. The elements in {name}`it` are
|
||||
examined in order of iteration.
|
||||
|
||||
This function requires a {name}`Finite` instance proving that the iterator will finish after a
|
||||
finite number of steps. If the iterator is not finite or such an instance is not available,
|
||||
consider using {lit}`it.allowNontermination.all` instead of {lean}`it.all`. However, it is not
|
||||
possible to formally verify the behavior of the partial variant.
|
||||
-/
|
||||
@[inline]
|
||||
def IterM.all {α β : Type w} {m : Type w → Type w'} [Monad m]
|
||||
[Iterator α m β] [IteratorLoop α m m] [Finite α m]
|
||||
(p : β → Bool) (it : IterM (α := α) m β) : m (ULift Bool) := do
|
||||
it.allM (fun x => pure (.up (p x)))
|
||||
|
||||
set_option doc.verso true in
|
||||
/--
|
||||
Returns {lean}`ULift.up true` if the pure predicate {name}`p` returns {lean}`true` for
|
||||
all elements emitted by the iterator {name}`it`.
|
||||
|
||||
{lit}`O(|xs|)`. Short-circuits upon encountering the first mismatch. The elements in {name}`it` are
|
||||
examined in order of iteration.
|
||||
|
||||
This is a partial, potentially nonterminating, function. It is not possible to formally verify
|
||||
its behavior. If the iterator has a {name}`Finite` instance, consider using {name}`IterM.all`
|
||||
instead.
|
||||
-/
|
||||
@[inline]
|
||||
def IterM.Partial.all {α β : Type w} {m : Type w → Type w'} [Monad m]
|
||||
[Iterator α m β] [IteratorLoopPartial α m m]
|
||||
(p : β → Bool) (it : IterM.Partial (α := α) m β) : m (ULift Bool) := do
|
||||
it.allM (fun x => pure (.up (p x)))
|
||||
|
||||
section Size
|
||||
|
||||
/--
|
||||
|
|
|
|||
|
|
@ -179,7 +179,7 @@ theorem Iter.step_filterM {f : β → n (ULift Bool)}
|
|||
| .done h => rfl
|
||||
|
||||
theorem Iter.step_mapM {f : β → n γ}
|
||||
[Monad n] [LawfulMonad n] [MonadLiftT m n] :
|
||||
[Monad n] [LawfulMonad n] :
|
||||
(it.mapM f).step = (do
|
||||
match it.step with
|
||||
| .yield it' out h => do
|
||||
|
|
@ -195,7 +195,6 @@ theorem Iter.step_mapM {f : β → n γ}
|
|||
match step with
|
||||
| .yield it' out h =>
|
||||
simp only [bind_pure_comp]
|
||||
simp only [Functor.map]
|
||||
rfl
|
||||
| .skip it' h => rfl
|
||||
| .done h => rfl
|
||||
|
|
@ -222,6 +221,24 @@ theorem Iter.step_filterMap {f : β → Option γ} :
|
|||
· simp
|
||||
· simp
|
||||
|
||||
/--
|
||||
a weaker version of `step_filterMap` that does not use dependent `match`
|
||||
-/
|
||||
theorem Iter.val_step_filterMap {f : β → Option γ} :
|
||||
(it.filterMap f).step.val = match it.step.val with
|
||||
| .yield it' out =>
|
||||
match f out with
|
||||
| none => .skip (it'.filterMap f)
|
||||
| some out' => .yield (it'.filterMap f) out'
|
||||
| .skip it' => .skip (it'.filterMap f)
|
||||
| .done => .done := by
|
||||
simp [step_filterMap]
|
||||
cases it.step using PlausibleIterStep.casesOn
|
||||
· simp only
|
||||
split <;> simp_all
|
||||
· simp
|
||||
· simp
|
||||
|
||||
theorem Iter.step_map {f : β → γ} :
|
||||
(it.map f).step = match it.step with
|
||||
| .yield it' out h =>
|
||||
|
|
@ -253,6 +270,25 @@ def Iter.step_filter {f : β → Bool} :
|
|||
· simp
|
||||
· simp
|
||||
|
||||
def Iter.val_step_filter {f : β → Bool} :
|
||||
(it.filter f).step.val = match it.step.val with
|
||||
| .yield it' out =>
|
||||
if f out = true then
|
||||
.yield (it'.filter f) out
|
||||
else
|
||||
.skip (it'.filter f)
|
||||
| .skip it' =>
|
||||
.skip (it'.filter f)
|
||||
| .done =>
|
||||
.done := by
|
||||
simp only [filter_eq_toIter_filter_toIterM, step, toIterM_toIter, IterM.step_filter, Id.run_bind]
|
||||
generalize it.toIterM.step.run = step
|
||||
cases step using PlausibleIterStep.casesOn
|
||||
· simp only
|
||||
split <;> simp [*]
|
||||
· simp
|
||||
· simp
|
||||
|
||||
@[simp]
|
||||
theorem Iter.toList_filterMap
|
||||
[IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] [Finite α Id]
|
||||
|
|
@ -431,4 +467,317 @@ theorem Iter.fold_map {α β γ : Type w} {δ : Type x}
|
|||
|
||||
end Fold
|
||||
|
||||
theorem Iter.anyM_filterMapM {α β β' : Type w} {m : Type w → Type w'}
|
||||
[Iterator α Id β] [Finite α Id] [Monad m] [LawfulMonad m]
|
||||
{it : Iter (α := α) β} {f : β → m (Option β')} {p : β' → m (ULift Bool)} :
|
||||
(it.filterMapM f).anyM p = (it.mapM (pure (f := m))).anyM (fun x => do
|
||||
match ← f x with
|
||||
| some fx => p fx
|
||||
| none => return .up false) := by
|
||||
simp only [filterMapM_eq_toIter_filterMapM_toIterM, IterM.anyM_filterMapM]
|
||||
rfl
|
||||
|
||||
-- There is hope to generalize the following theorem as soon there is a `Shrink` type.
|
||||
/--
|
||||
This lemma expresses `Iter.anyM` in terms of `IterM.anyM`.
|
||||
It requires all involved types to live in `Type 0`.
|
||||
-/
|
||||
theorem Iter.anyM_eq_anyM_mapM_pure {α β : Type} {m : Type → Type w'} [Iterator α Id β]
|
||||
[Finite α Id] [Monad m] [LawfulMonad m] [IteratorLoop α Id m] [LawfulIteratorLoop α Id m]
|
||||
{it : Iter (α := α) β} {p : β → m Bool} :
|
||||
it.anyM p = ULift.down <$> (it.mapM (α := α) (pure (f := m))).anyM (fun x => ULift.up <$> p x) := by
|
||||
rw [anyM_eq_forIn, IterM.anyM_eq_forIn, map_eq_pure_bind]
|
||||
induction it using Iter.inductSteps with | step it ihy ihs =>
|
||||
rw [forIn_eq_match_step, IterM.forIn_eq_match_step, bind_assoc, step_mapM]
|
||||
cases it.step using PlausibleIterStep.casesOn
|
||||
· simp only [bind_assoc, liftM_pure, pure_bind, map_eq_pure_bind]
|
||||
apply bind_congr; intro px
|
||||
split
|
||||
· simp
|
||||
· simp [ihy ‹_›]
|
||||
· simp [ihs ‹_›]
|
||||
· simp
|
||||
|
||||
theorem Iter.anyM_mapM {α β β' : Type w} {m : Type w → Type w'}
|
||||
[Iterator α Id β] [Finite α Id] [Monad m] [LawfulMonad m]
|
||||
{it : Iter (α := α) β} {f : β → m β'} {p : β' → m (ULift Bool)} :
|
||||
(it.mapM f).anyM p = (it.mapM (pure (f := m))).anyM (fun x => do p (← f x)) := by
|
||||
rw [mapM_eq_toIter_mapM_toIterM, IterM.anyM_mapM, mapM_eq_toIter_mapM_toIterM]
|
||||
|
||||
theorem Iter.anyM_filterM {α β : Type w} {m : Type w → Type w'}
|
||||
[Iterator α Id β] [Finite α Id] [Monad m] [LawfulMonad m]
|
||||
{it : Iter (α := α) β} {f : β → m (ULift Bool)} {p : β → m (ULift Bool)} :
|
||||
(it.filterM f).anyM p = (it.mapM (pure (f := m))).anyM (fun x => do
|
||||
if (← f x).down then
|
||||
p x
|
||||
else
|
||||
return .up false) := by
|
||||
rw [filterM_eq_toIter_filterM_toIterM, IterM.anyM_filterM, mapM_eq_toIter_mapM_toIterM]
|
||||
|
||||
theorem Iter.anyM_filterMap {α β β' : Type w} {m : Type → Type w'}
|
||||
[Iterator α Id β] [Finite α Id] [Monad m] [IteratorLoop α Id m]
|
||||
[LawfulMonad m] [LawfulIteratorLoop α Id m]
|
||||
{it : Iter (α := α) β} {f : β → Option β'} {p : β' → m Bool} :
|
||||
(it.filterMap f).anyM p = it.anyM (fun x => do
|
||||
match f x with
|
||||
| some fx => p fx
|
||||
| none => return false) := by
|
||||
induction it using Iter.inductSteps with | step it ihy ihs
|
||||
rw [anyM_eq_match_step, anyM_eq_match_step, val_step_filterMap]
|
||||
cases it.step using PlausibleIterStep.casesOn
|
||||
· rename_i out _
|
||||
simp only
|
||||
cases f out
|
||||
· simp [ihy ‹_›]
|
||||
· apply bind_congr; intro px
|
||||
split <;> simp [ihy ‹_›]
|
||||
· simp [ihs ‹_›]
|
||||
· simp
|
||||
|
||||
theorem Iter.anyM_map {α β β' : Type w} {m : Type → Type w'}
|
||||
[Iterator α Id β] [Finite α Id] [Monad m] [IteratorLoop α Id m]
|
||||
[LawfulMonad m] [LawfulIteratorLoop α Id m]
|
||||
{it : Iter (α := α) β} {f : β → β'} {p : β' → m Bool} :
|
||||
(it.map f).anyM p = it.anyM (fun x => p (f x)) := by
|
||||
induction it using Iter.inductSteps with | step it ihy ihs
|
||||
rw [anyM_eq_match_step, anyM_eq_match_step, step_map]
|
||||
cases it.step using PlausibleIterStep.casesOn
|
||||
· simp [ihy ‹_›]
|
||||
· simp [ihs ‹_›]
|
||||
· simp
|
||||
|
||||
theorem Iter.anyM_filter {α β : Type w} {m : Type → Type w'}
|
||||
[Iterator α Id β] [Finite α Id] [Monad m][IteratorLoop α Id m]
|
||||
[LawfulMonad m] [LawfulIteratorLoop α Id m]
|
||||
{it : Iter (α := α) β} {f : β → Bool} {p : β → m Bool} :
|
||||
(it.filter f).anyM p = it.anyM (fun x => do
|
||||
if f x then
|
||||
p x
|
||||
else
|
||||
return false) := by
|
||||
induction it using Iter.inductSteps with | step it ihy ihs
|
||||
rw [anyM_eq_match_step, anyM_eq_match_step, val_step_filter]
|
||||
cases it.step using PlausibleIterStep.casesOn
|
||||
· rename_i out _
|
||||
simp only
|
||||
cases f out <;> simp [ihy ‹_›]
|
||||
· simp [ihs ‹_›]
|
||||
· simp
|
||||
|
||||
theorem Iter.any_filterMapM {α β β' : Type w} {m : Type w → Type w'}
|
||||
[Iterator α Id β] [Finite α Id] [Monad m] [IteratorLoop α Id m]
|
||||
[LawfulMonad m] [LawfulIteratorLoop α Id m]
|
||||
{it : Iter (α := α) β} {f : β → m (Option β')} {p : β' → Bool} :
|
||||
(it.filterMapM f).any p = (it.mapM (pure (f := m))).anyM (fun x => do
|
||||
match ← f x with
|
||||
| some fx => return .up (p fx)
|
||||
| none => return .up false) := by
|
||||
simp [IterM.any_eq_anyM, anyM_filterMapM]
|
||||
|
||||
theorem Iter.any_mapM {α β β' : Type w} {m : Type w → Type w'}
|
||||
[Iterator α Id β] [Finite α Id] [Monad m] [IteratorLoop α Id m]
|
||||
[LawfulMonad m] [LawfulIteratorLoop α Id m]
|
||||
{it : Iter (α := α) β} {f : β → m β'} {p : β' → Bool} :
|
||||
(it.mapM f).any p = (it.mapM pure).anyM (fun x => (.up <| p ·) <$> (f x)) := by
|
||||
simp [IterM.any_eq_anyM, anyM_mapM]
|
||||
|
||||
theorem Iter.any_filterM {α β : Type w} {m : Type w → Type w'}
|
||||
[Iterator α Id β] [Finite α Id] [Monad m] [IteratorLoop α Id m]
|
||||
[LawfulMonad m] [LawfulIteratorLoop α Id m]
|
||||
{it : Iter (α := α) β} {f : β → m (ULift Bool)} {p : β → Bool} :
|
||||
(it.filterM f).any p = (it.mapM (pure (f := m))).anyM (fun x => do
|
||||
if (← f x).down then
|
||||
return .up (p x)
|
||||
else
|
||||
return .up false) := by
|
||||
simp [IterM.any_eq_anyM, anyM_filterM]
|
||||
|
||||
theorem Iter.any_filterMap {α β β' : Type w}
|
||||
[Iterator α Id β] [Finite α Id][IteratorLoop α Id Id]
|
||||
[LawfulIteratorLoop α Id Id]
|
||||
{it : Iter (α := α) β} {f : β → Option β'} {p : β' → Bool} :
|
||||
(it.filterMap f).any p = it.any (fun x =>
|
||||
match f x with
|
||||
| some fx => (p fx)
|
||||
| none => false) := by
|
||||
induction it using Iter.inductSteps with | step it ihy ihs
|
||||
rw [any_eq_match_step, any_eq_match_step, val_step_filterMap]
|
||||
cases it.step using PlausibleIterStep.casesOn
|
||||
· rename_i out _
|
||||
simp only
|
||||
cases f out
|
||||
· simp [*, ihy ‹_›]
|
||||
· simp only
|
||||
split <;> simp [ihy ‹_›]
|
||||
· simp [ihs ‹_›]
|
||||
· simp
|
||||
|
||||
theorem Iter.any_map {α β β' : Type w}
|
||||
[Iterator α Id β] [Finite α Id] [IteratorLoop α Id Id]
|
||||
[LawfulIteratorLoop α Id Id]
|
||||
{it : Iter (α := α) β} {f : β → β'} {p : β' → Bool} :
|
||||
(it.map f).any p = it.any (fun x => p (f x)) := by
|
||||
induction it using Iter.inductSteps with | step it ihy ihs
|
||||
rw [any_eq_match_step, any_eq_match_step, step_map]
|
||||
cases it.step using PlausibleIterStep.casesOn
|
||||
· simp [ihy ‹_›]
|
||||
· simp [ihs ‹_›]
|
||||
· simp
|
||||
|
||||
theorem Iter.allM_filterMapM {α β β' : Type w} {m : Type w → Type w'}
|
||||
[Iterator α Id β] [Finite α Id] [Monad m] [LawfulMonad m]
|
||||
{it : Iter (α := α) β} {f : β → m (Option β')} {p : β' → m (ULift Bool)} :
|
||||
(it.filterMapM f).allM p = (it.mapM (pure (f := m))).allM (fun x => do
|
||||
match ← f x with
|
||||
| some fx => p fx
|
||||
| none => return .up true) := by
|
||||
simp only [filterMapM_eq_toIter_filterMapM_toIterM, IterM.allM_filterMapM]
|
||||
rfl
|
||||
|
||||
/--
|
||||
This lemma expresses `Iter.allM` in terms of `IterM.allM`.
|
||||
It requires all involved types to live in `Type 0`.
|
||||
-/
|
||||
theorem Iter.allM_eq_allM_mapM_pure {α β : Type} {m : Type → Type w'} [Iterator α Id β]
|
||||
[Finite α Id] [Monad m] [LawfulMonad m] [IteratorLoop α Id m] [LawfulIteratorLoop α Id m]
|
||||
{it : Iter (α := α) β} {p : β → m Bool} :
|
||||
it.allM p = ULift.down <$> (it.mapM (α := α) (pure (f := m))).allM (fun x => ULift.up <$> p x) := by
|
||||
rw [allM_eq_forIn, IterM.allM_eq_forIn, map_eq_pure_bind]
|
||||
induction it using Iter.inductSteps with | step it ihy ihs =>
|
||||
rw [forIn_eq_match_step, IterM.forIn_eq_match_step, bind_assoc, step_mapM]
|
||||
cases it.step using PlausibleIterStep.casesOn
|
||||
· simp only [bind_assoc, liftM_pure, pure_bind, map_eq_pure_bind]
|
||||
apply bind_congr; intro px
|
||||
split
|
||||
· simp [ihy ‹_›]
|
||||
· simp
|
||||
· simp [ihs ‹_›]
|
||||
· simp
|
||||
|
||||
theorem Iter.allM_mapM {α β β' : Type w} {m : Type w → Type w'}
|
||||
[Iterator α Id β] [Finite α Id] [Monad m] [LawfulMonad m]
|
||||
{it : Iter (α := α) β} {f : β → m β'} {p : β' → m (ULift Bool)} :
|
||||
(it.mapM f).allM p = (it.mapM (pure (f := m))).allM (fun x => do p (← f x)) := by
|
||||
rw [mapM_eq_toIter_mapM_toIterM, IterM.allM_mapM, mapM_eq_toIter_mapM_toIterM]
|
||||
|
||||
theorem Iter.allM_filterM {α β : Type w} {m : Type w → Type w'}
|
||||
[Iterator α Id β] [Finite α Id] [Monad m] [LawfulMonad m]
|
||||
{it : Iter (α := α) β} {f : β → m (ULift Bool)} {p : β → m (ULift Bool)} :
|
||||
(it.filterM f).allM p = (it.mapM (pure (f := m))).allM (fun x => do
|
||||
if (← f x).down then
|
||||
p x
|
||||
else
|
||||
return .up true) := by
|
||||
rw [filterM_eq_toIter_filterM_toIterM, IterM.allM_filterM, mapM_eq_toIter_mapM_toIterM]
|
||||
|
||||
theorem Iter.allM_filterMap {α β β' : Type w} {m : Type → Type w'}
|
||||
[Iterator α Id β] [Finite α Id] [Monad m] [IteratorLoop α Id m]
|
||||
[LawfulMonad m] [LawfulIteratorLoop α Id m]
|
||||
{it : Iter (α := α) β} {f : β → Option β'} {p : β' → m Bool} :
|
||||
(it.filterMap f).allM p = it.allM (fun x => do
|
||||
match f x with
|
||||
| some fx => p fx
|
||||
| none => return true) := by
|
||||
induction it using Iter.inductSteps with | step it ihy ihs
|
||||
rw [allM_eq_match_step, allM_eq_match_step, val_step_filterMap]
|
||||
cases it.step using PlausibleIterStep.casesOn
|
||||
· rename_i out _
|
||||
simp only
|
||||
cases f out
|
||||
· simp [ihy ‹_›]
|
||||
· apply bind_congr; intro px
|
||||
split <;> simp [ihy ‹_›]
|
||||
· simp [ihs ‹_›]
|
||||
· simp
|
||||
|
||||
theorem Iter.allM_map {α β β' : Type w} {m : Type → Type w'}
|
||||
[Iterator α Id β] [Finite α Id] [Monad m] [IteratorLoop α Id m]
|
||||
[LawfulMonad m] [LawfulIteratorLoop α Id m]
|
||||
{it : Iter (α := α) β} {f : β → β'} {p : β' → m Bool} :
|
||||
(it.map f).allM p = it.allM (fun x => p (f x)) := by
|
||||
induction it using Iter.inductSteps with | step it ihy ihs
|
||||
rw [allM_eq_match_step, allM_eq_match_step, step_map]
|
||||
cases it.step using PlausibleIterStep.casesOn
|
||||
· simp [ihy ‹_›]
|
||||
· simp [ihs ‹_›]
|
||||
· simp
|
||||
|
||||
theorem Iter.allM_filter {α β : Type w} {m : Type → Type w'}
|
||||
[Iterator α Id β] [Finite α Id] [Monad m][IteratorLoop α Id m]
|
||||
[LawfulMonad m] [LawfulIteratorLoop α Id m]
|
||||
{it : Iter (α := α) β} {f : β → Bool} {p : β → m Bool} :
|
||||
(it.filter f).allM p = it.allM (fun x => do
|
||||
if f x then
|
||||
p x
|
||||
else
|
||||
return true) := by
|
||||
induction it using Iter.inductSteps with | step it ihy ihs
|
||||
rw [allM_eq_match_step, allM_eq_match_step, val_step_filter]
|
||||
cases it.step using PlausibleIterStep.casesOn
|
||||
· rename_i out _
|
||||
simp only
|
||||
cases f out <;> simp [ihy ‹_›]
|
||||
· simp [ihs ‹_›]
|
||||
· simp
|
||||
|
||||
theorem Iter.all_filterMapM {α β β' : Type w} {m : Type w → Type w'}
|
||||
[Iterator α Id β] [Finite α Id] [Monad m] [IteratorLoop α Id m]
|
||||
[LawfulMonad m] [LawfulIteratorLoop α Id m]
|
||||
{it : Iter (α := α) β} {f : β → m (Option β')} {p : β' → Bool} :
|
||||
(it.filterMapM f).all p = (it.mapM (pure (f := m))).allM (fun x => do
|
||||
match ← f x with
|
||||
| some fx => return .up (p fx)
|
||||
| none => return .up true) := by
|
||||
simp [IterM.all_eq_allM, allM_filterMapM]
|
||||
|
||||
theorem Iter.all_mapM {α β β' : Type w} {m : Type w → Type w'}
|
||||
[Iterator α Id β] [Finite α Id] [Monad m] [IteratorLoop α Id m]
|
||||
[LawfulMonad m] [LawfulIteratorLoop α Id m]
|
||||
{it : Iter (α := α) β} {f : β → m β'} {p : β' → Bool} :
|
||||
(it.mapM f).all p = (it.mapM pure).allM (fun x => (.up <| p ·) <$> (f x)) := by
|
||||
simp [IterM.all_eq_allM, allM_mapM]
|
||||
|
||||
theorem Iter.all_filterM {α β : Type w} {m : Type w → Type w'}
|
||||
[Iterator α Id β] [Finite α Id] [Monad m] [IteratorLoop α Id m]
|
||||
[LawfulMonad m] [LawfulIteratorLoop α Id m]
|
||||
{it : Iter (α := α) β} {f : β → m (ULift Bool)} {p : β → Bool} :
|
||||
(it.filterM f).all p = (it.mapM (pure (f := m))).allM (fun x => do
|
||||
if (← f x).down then
|
||||
return .up (p x)
|
||||
else
|
||||
return .up true) := by
|
||||
simp [IterM.all_eq_allM, allM_filterM]
|
||||
|
||||
theorem Iter.all_filterMap {α β β' : Type w}
|
||||
[Iterator α Id β] [Finite α Id][IteratorLoop α Id Id]
|
||||
[LawfulIteratorLoop α Id Id]
|
||||
{it : Iter (α := α) β} {f : β → Option β'} {p : β' → Bool} :
|
||||
(it.filterMap f).all p = it.all (fun x =>
|
||||
match f x with
|
||||
| some fx => (p fx)
|
||||
| none => true) := by
|
||||
induction it using Iter.inductSteps with | step it ihy ihs
|
||||
rw [all_eq_match_step, all_eq_match_step, val_step_filterMap]
|
||||
cases it.step using PlausibleIterStep.casesOn
|
||||
· rename_i out _
|
||||
simp only
|
||||
cases f out
|
||||
· simp [*, ihy ‹_›]
|
||||
· simp only
|
||||
split <;> simp [ihy ‹_›]
|
||||
· simp [ihs ‹_›]
|
||||
· simp
|
||||
|
||||
theorem Iter.all_map {α β β' : Type w}
|
||||
[Iterator α Id β] [Finite α Id] [IteratorLoop α Id Id]
|
||||
[LawfulIteratorLoop α Id Id]
|
||||
{it : Iter (α := α) β} {f : β → β'} {p : β' → Bool} :
|
||||
(it.map f).all p = it.all (fun x => p (f x)) := by
|
||||
induction it using Iter.inductSteps with | step it ihy ihs
|
||||
rw [all_eq_match_step, all_eq_match_step, step_map]
|
||||
cases it.step using PlausibleIterStep.casesOn
|
||||
· simp [ihy ‹_›]
|
||||
· simp [ihs ‹_›]
|
||||
· simp
|
||||
|
||||
end Std.Iterators
|
||||
|
|
|
|||
|
|
@ -160,7 +160,7 @@ theorem IterM.step_mapM {γ : Type w} {f : β → n γ}
|
|||
match step with
|
||||
| .yield it' out h =>
|
||||
simp only [bind_pure_comp]
|
||||
simp only [PostconditionT.lift, Functor.map]
|
||||
simp only [PostconditionT.lift]
|
||||
simp only [PostconditionT.operation_map, Functor.map_map, PlausibleIterStep.skip,
|
||||
PlausibleIterStep.yield, bind_map_left, bind_pure_comp]
|
||||
rfl
|
||||
|
|
@ -539,4 +539,356 @@ theorem IterM.fold_map {α β γ δ : Type w} {m : Type w → Type w'}
|
|||
|
||||
end Fold
|
||||
|
||||
section AnyAll
|
||||
|
||||
theorem IterM.anyM_filterMapM {α β β' : Type w} {m : Type w → Type w'} {n : Type w → Type w''}
|
||||
[Iterator α m β] [Finite α m] [Monad m] [Monad n] [MonadLiftT m n]
|
||||
[LawfulMonad m] [LawfulMonad n]
|
||||
{it : IterM (α := α) m β} {f : β → n (Option β')} {p : β' → n (ULift Bool)} :
|
||||
(it.filterMapM f).anyM p = (it.mapM (pure (f := n))).anyM (fun x => do
|
||||
match ← f x with
|
||||
| some fx => p fx
|
||||
| none => return .up false) := by
|
||||
induction it using IterM.inductSteps with | step it ihy ihs
|
||||
rw [anyM_eq_match_step, anyM_eq_match_step, step_filterMapM, step_mapM, bind_assoc, bind_assoc]
|
||||
apply bind_congr; intro step
|
||||
split
|
||||
· simp only [bind_assoc, pure_bind]
|
||||
apply bind_congr; intro fx
|
||||
split
|
||||
· simp [ihy ‹_›]
|
||||
· simp only [PlausibleIterStep.yield, pure_bind]
|
||||
apply bind_congr; intro px
|
||||
split <;> simp [ihy ‹_›]
|
||||
· simp only [PlausibleIterStep.skip, pure_bind, bind_assoc]
|
||||
simp [ihs ‹_›]
|
||||
· simp
|
||||
|
||||
theorem IterM.anyM_mapM {α β β' : Type w} {m : Type w → Type w'} {n : Type w → Type w''}
|
||||
[Iterator α m β] [Finite α m] [Monad m] [Monad n] [MonadLiftT m n]
|
||||
[LawfulMonad m] [LawfulMonad n]
|
||||
{it : IterM (α := α) m β} {f : β → n β'} {p : β' → n (ULift Bool)} :
|
||||
(it.mapM f).anyM p = (it.mapM (pure (f := n))).anyM (fun x => do p (← f x)) := by
|
||||
induction it using IterM.inductSteps with | step it ihy ihs
|
||||
rw [anyM_eq_match_step, anyM_eq_match_step, step_mapM, step_mapM, bind_assoc, bind_assoc]
|
||||
apply bind_congr; intro step
|
||||
split
|
||||
· simp only [bind_assoc, pure_bind]
|
||||
apply bind_congr; intro fx
|
||||
simp [ihy ‹_›]
|
||||
· simp only [PlausibleIterStep.skip, pure_bind, bind_assoc]
|
||||
simp [ihs ‹_›]
|
||||
· simp
|
||||
|
||||
theorem IterM.anyM_filterM {α β : Type w} {m : Type w → Type w'} {n : Type w → Type w''}
|
||||
[Iterator α m β] [Finite α m] [Monad m] [Monad n] [MonadLiftT m n]
|
||||
[LawfulMonad m] [LawfulMonad n]
|
||||
{it : IterM (α := α) m β} {f : β → n (ULift Bool)} {p : β → n (ULift Bool)} :
|
||||
(it.filterM f).anyM p = (it.mapM (pure (f := n))).anyM (fun x => do
|
||||
if (← f x).down then
|
||||
p x
|
||||
else
|
||||
return .up false) := by
|
||||
induction it using IterM.inductSteps with | step it ihy ihs
|
||||
rw [anyM_eq_match_step, anyM_eq_match_step, step_mapM, step_filterM, bind_assoc, bind_assoc]
|
||||
apply bind_congr; intro step
|
||||
split
|
||||
· simp only [bind_assoc, pure_bind]
|
||||
apply bind_congr; intro fx
|
||||
split <;> simp [ihy ‹_›]
|
||||
· simp only [PlausibleIterStep.skip, pure_bind, bind_assoc]
|
||||
simp [ihs ‹_›]
|
||||
· simp
|
||||
|
||||
theorem IterM.anyM_filterMap {α β β' : Type w} {m : Type w → Type w'}
|
||||
[Iterator α m β] [Finite α m] [Monad m] [IteratorLoop α m m]
|
||||
[LawfulMonad m] [LawfulIteratorLoop α m m]
|
||||
{it : IterM (α := α) m β} {f : β → Option β'} {p : β' → m (ULift Bool)} :
|
||||
(it.filterMap f).anyM p = it.anyM (fun x => do
|
||||
match f x with
|
||||
| some fx => p fx
|
||||
| none => return .up false) := by
|
||||
induction it using IterM.inductSteps with | step it ihy ihs
|
||||
rw [anyM_eq_match_step, anyM_eq_match_step, step_filterMap, bind_assoc]
|
||||
apply bind_congr; intro step
|
||||
split
|
||||
· split
|
||||
· simp [*, ihy ‹_›]
|
||||
· simp only [*, PlausibleIterStep.yield, pure_bind]
|
||||
apply bind_congr; intro px
|
||||
split <;> simp [ihy ‹_›]
|
||||
· simp [PlausibleIterStep.skip, pure_bind, ihs ‹_›]
|
||||
· simp
|
||||
|
||||
theorem IterM.anyM_map {α β β' : Type w} {m : Type w → Type w'}
|
||||
[Iterator α m β] [Finite α m] [Monad m] [IteratorLoop α m m]
|
||||
[LawfulMonad m] [LawfulIteratorLoop α m m]
|
||||
{it : IterM (α := α) m β} {f : β → β'} {p : β' → m (ULift Bool)} :
|
||||
(it.map f).anyM p = it.anyM (fun x => p (f x)) := by
|
||||
induction it using IterM.inductSteps with | step it ihy ihs
|
||||
rw [anyM_eq_match_step, anyM_eq_match_step, step_map, bind_assoc]
|
||||
apply bind_congr; intro step
|
||||
split
|
||||
· simp only [pure_bind]
|
||||
apply bind_congr; intro fx
|
||||
simp [ihy ‹_›]
|
||||
· simp [PlausibleIterStep.skip, pure_bind, ihs ‹_›]
|
||||
· simp
|
||||
|
||||
theorem IterM.anyM_filter {α β : Type w} {m : Type w → Type w'}
|
||||
[Iterator α m β] [Finite α m] [Monad m][IteratorLoop α m m]
|
||||
[LawfulMonad m] [LawfulIteratorLoop α m m]
|
||||
{it : IterM (α := α) m β} {f : β → Bool} {p : β → m (ULift Bool)} :
|
||||
(it.filter f).anyM p = it.anyM (fun x => do
|
||||
if f x then
|
||||
p x
|
||||
else
|
||||
return .up false) := by
|
||||
induction it using IterM.inductSteps with | step it ihy ihs
|
||||
rw [anyM_eq_match_step, anyM_eq_match_step, step_filter, bind_assoc]
|
||||
apply bind_congr; intro step
|
||||
split
|
||||
· simp only
|
||||
split <;> simp [ihy ‹_›]
|
||||
· simp only [PlausibleIterStep.skip, pure_bind]
|
||||
simp [ihs ‹_›]
|
||||
· simp
|
||||
|
||||
theorem IterM.any_filterMapM {α β β' : Type w} {m : Type w → Type w'} {n : Type w → Type w''}
|
||||
[Iterator α m β] [Finite α m] [Monad m] [Monad n] [MonadLiftT m n] [IteratorLoop α m m]
|
||||
[LawfulMonad m] [LawfulMonad n] [LawfulMonadLiftT m n] [LawfulIteratorLoop α m m]
|
||||
{it : IterM (α := α) m β} {f : β → n (Option β')} {p : β' → Bool} :
|
||||
(it.filterMapM f).any p = (it.mapM (pure (f := n))).anyM (fun x => do
|
||||
match ← f x with
|
||||
| some fx => return .up (p fx)
|
||||
| none => return .up false) := by
|
||||
simp [any_eq_anyM, anyM_filterMapM]
|
||||
|
||||
theorem IterM.any_mapM {α β β' : Type w} {m : Type w → Type w'} {n : Type w → Type w''}
|
||||
[Iterator α m β] [Finite α m] [Monad m] [Monad n] [MonadLiftT m n] [IteratorLoop α m m]
|
||||
[LawfulMonad m] [LawfulMonad n] [LawfulMonadLiftT m n] [LawfulIteratorLoop α m m]
|
||||
{it : IterM (α := α) m β} {f : β → n β'} {p : β' → Bool} :
|
||||
(it.mapM f).any p = (it.mapM (pure (f := n))).anyM (fun x => (.up <| p ·) <$> (f x)) := by
|
||||
simp [any_eq_anyM, anyM_mapM]
|
||||
|
||||
theorem IterM.any_filterM {α β : Type w} {m : Type w → Type w'} {n : Type w → Type w''}
|
||||
[Iterator α m β] [Finite α m] [Monad m] [Monad n] [MonadLiftT m n] [IteratorLoop α m m]
|
||||
[LawfulMonad m] [LawfulMonad n] [LawfulMonadLiftT m n] [LawfulIteratorLoop α m m]
|
||||
{it : IterM (α := α) m β} {f : β → n (ULift Bool)} {p : β → Bool} :
|
||||
(it.filterM f).any p = (it.mapM (pure (f := n))).anyM (fun x => do
|
||||
if (← f x).down then
|
||||
return .up (p x)
|
||||
else
|
||||
return .up false) := by
|
||||
simp [any_eq_anyM, anyM_filterM]
|
||||
|
||||
theorem IterM.any_filterMap {α β β' : Type w} {m : Type w → Type w'}
|
||||
[Iterator α m β] [Finite α m] [Monad m] [IteratorLoop α m m]
|
||||
[LawfulMonad m] [LawfulIteratorLoop α m m]
|
||||
{it : IterM (α := α) m β} {f : β → Option β'} {p : β' → Bool} :
|
||||
(it.filterMap f).any p = it.any (fun x =>
|
||||
match f x with
|
||||
| some fx => (p fx)
|
||||
| none => false) := by
|
||||
induction it using IterM.inductSteps with | step it ihy ihs
|
||||
rw [any_eq_match_step, any_eq_match_step, step_filterMap, bind_assoc]
|
||||
apply bind_congr; intro step
|
||||
split
|
||||
· split
|
||||
· simp [*, ihy ‹_›]
|
||||
· simp only [*, PlausibleIterStep.yield, pure_bind]
|
||||
split <;> simp [ihy ‹_›]
|
||||
· simp [PlausibleIterStep.skip, pure_bind, ihs ‹_›]
|
||||
· simp
|
||||
|
||||
theorem IterM.any_map {α β β' : Type w} {m : Type w → Type w'}
|
||||
[Iterator α m β] [Finite α m] [Monad m] [IteratorLoop α m m]
|
||||
[LawfulMonad m] [LawfulIteratorLoop α m m]
|
||||
{it : IterM (α := α) m β} {f : β → β'} {p : β' → Bool} :
|
||||
(it.map f).any p = it.any (fun x => p (f x)) := by
|
||||
induction it using IterM.inductSteps with | step it ihy ihs
|
||||
rw [any_eq_match_step, any_eq_match_step, step_map, bind_assoc]
|
||||
apply bind_congr; intro step
|
||||
split
|
||||
· simp only [pure_bind]
|
||||
simp [ihy ‹_›]
|
||||
· simp [PlausibleIterStep.skip, pure_bind, ihs ‹_›]
|
||||
· simp
|
||||
|
||||
theorem IterM.allM_filterMapM {α β β' : Type w} {m : Type w → Type w'} {n : Type w → Type w''}
|
||||
[Iterator α m β] [Finite α m] [Monad m] [Monad n] [MonadLiftT m n]
|
||||
[LawfulMonad m] [LawfulMonad n] [LawfulMonadLiftT m n]
|
||||
{it : IterM (α := α) m β} {f : β → n (Option β')} {p : β' → n (ULift Bool)} :
|
||||
(it.filterMapM f).allM p = (it.mapM (pure (f := n))).allM (fun x => do
|
||||
match ← f x with
|
||||
| some fx => p fx
|
||||
| none => return .up true) := by
|
||||
induction it using IterM.inductSteps with | step it ihy ihs
|
||||
rw [allM_eq_match_step, allM_eq_match_step, step_filterMapM, step_mapM, bind_assoc, bind_assoc]
|
||||
apply bind_congr; intro step
|
||||
split
|
||||
· simp only [bind_assoc, pure_bind]
|
||||
apply bind_congr; intro fx
|
||||
split
|
||||
· simp [ihy ‹_›]
|
||||
· simp only [PlausibleIterStep.yield, pure_bind]
|
||||
apply bind_congr; intro px
|
||||
split <;> simp [ihy ‹_›]
|
||||
· simp only [PlausibleIterStep.skip, pure_bind, bind_assoc]
|
||||
simp [ihs ‹_›]
|
||||
· simp
|
||||
|
||||
theorem IterM.allM_mapM {α β β' : Type w} {m : Type w → Type w'} {n : Type w → Type w''}
|
||||
[Iterator α m β] [Finite α m] [Monad m] [Monad n] [MonadLiftT m n]
|
||||
[LawfulMonad m] [LawfulMonad n] [LawfulMonadLiftT m n]
|
||||
{it : IterM (α := α) m β} {f : β → n β'} {p : β' → n (ULift Bool)} :
|
||||
(it.mapM f).allM p = (it.mapM (pure (f := n))).allM (fun x => do p (← f x)) := by
|
||||
induction it using IterM.inductSteps with | step it ihy ihs
|
||||
rw [allM_eq_match_step, allM_eq_match_step, step_mapM, step_mapM, bind_assoc, bind_assoc]
|
||||
apply bind_congr; intro step
|
||||
split
|
||||
· simp only [bind_assoc, pure_bind]
|
||||
apply bind_congr; intro fx
|
||||
simp [ihy ‹_›]
|
||||
· simp only [PlausibleIterStep.skip, pure_bind, bind_assoc]
|
||||
simp [ihs ‹_›]
|
||||
· simp
|
||||
|
||||
theorem IterM.allM_filterM {α β : Type w} {m : Type w → Type w'} {n : Type w → Type w''}
|
||||
[Iterator α m β] [Finite α m] [Monad m] [Monad n] [MonadLiftT m n]
|
||||
[LawfulMonad m] [LawfulMonad n] [LawfulMonadLiftT m n]
|
||||
{it : IterM (α := α) m β} {f : β → n (ULift Bool)} {p : β → n (ULift Bool)} :
|
||||
(it.filterM f).allM p = (it.mapM (pure (f := n))).allM (fun x => do
|
||||
if (← f x).down then
|
||||
p x
|
||||
else
|
||||
return .up true) := by
|
||||
induction it using IterM.inductSteps with | step it ihy ihs
|
||||
rw [allM_eq_match_step, allM_eq_match_step, step_mapM, step_filterM, bind_assoc, bind_assoc]
|
||||
apply bind_congr; intro step
|
||||
split
|
||||
· simp only [bind_assoc, pure_bind]
|
||||
apply bind_congr; intro fx
|
||||
split <;> simp [ihy ‹_›]
|
||||
· simp only [PlausibleIterStep.skip, pure_bind, bind_assoc]
|
||||
simp [ihs ‹_›]
|
||||
· simp
|
||||
|
||||
theorem IterM.allM_filterMap {α β β' : Type w} {m : Type w → Type w'}
|
||||
[Iterator α m β] [Finite α m] [Monad m] [IteratorLoop α m m]
|
||||
[LawfulMonad m] [LawfulIteratorLoop α m m]
|
||||
{it : IterM (α := α) m β} {f : β → Option β'} {p : β' → m (ULift Bool)} :
|
||||
(it.filterMap f).allM p = it.allM (fun x => do
|
||||
match f x with
|
||||
| some fx => p fx
|
||||
| none => return .up true) := by
|
||||
induction it using IterM.inductSteps with | step it ihy ihs
|
||||
rw [allM_eq_match_step, allM_eq_match_step, step_filterMap, bind_assoc]
|
||||
apply bind_congr; intro step
|
||||
split
|
||||
· split
|
||||
· simp [*, ihy ‹_›]
|
||||
· simp only [*, PlausibleIterStep.yield, pure_bind]
|
||||
apply bind_congr; intro px
|
||||
split <;> simp [ihy ‹_›]
|
||||
· simp [PlausibleIterStep.skip, pure_bind, ihs ‹_›]
|
||||
· simp
|
||||
|
||||
theorem IterM.allM_map {α β β' : Type w} {m : Type w → Type w'}
|
||||
[Iterator α m β] [Finite α m] [Monad m] [IteratorLoop α m m]
|
||||
[LawfulMonad m] [LawfulIteratorLoop α m m]
|
||||
{it : IterM (α := α) m β} {f : β → β'} {p : β' → m (ULift Bool)} :
|
||||
(it.map f).allM p = it.allM (fun x => p (f x)) := by
|
||||
induction it using IterM.inductSteps with | step it ihy ihs
|
||||
rw [allM_eq_match_step, allM_eq_match_step, step_map, bind_assoc]
|
||||
apply bind_congr; intro step
|
||||
split
|
||||
· simp only [pure_bind]
|
||||
apply bind_congr; intro fx
|
||||
simp [ihy ‹_›]
|
||||
· simp [PlausibleIterStep.skip, pure_bind, ihs ‹_›]
|
||||
· simp
|
||||
|
||||
theorem IterM.allM_filter {α β : Type w} {m : Type w → Type w'}
|
||||
[Iterator α m β] [Finite α m] [Monad m][IteratorLoop α m m]
|
||||
[LawfulMonad m] [LawfulIteratorLoop α m m]
|
||||
{it : IterM (α := α) m β} {f : β → Bool} {p : β → m (ULift Bool)} :
|
||||
(it.filter f).allM p = it.allM (fun x => do
|
||||
if f x then
|
||||
p x
|
||||
else
|
||||
return .up true) := by
|
||||
induction it using IterM.inductSteps with | step it ihy ihs
|
||||
rw [allM_eq_match_step, allM_eq_match_step, step_filter, bind_assoc]
|
||||
apply bind_congr; intro step
|
||||
split
|
||||
· simp only
|
||||
split <;> simp [ihy ‹_›]
|
||||
· simp only [PlausibleIterStep.skip, pure_bind]
|
||||
simp [ihs ‹_›]
|
||||
· simp
|
||||
|
||||
theorem IterM.all_filterMapM {α β β' : Type w} {m : Type w → Type w'} {n : Type w → Type w''}
|
||||
[Iterator α m β] [Finite α m] [Monad m] [Monad n] [MonadLiftT m n] [IteratorLoop α m m]
|
||||
[LawfulMonad m] [LawfulMonad n] [LawfulMonadLiftT m n] [LawfulIteratorLoop α m m]
|
||||
{it : IterM (α := α) m β} {f : β → n (Option β')} {p : β' → Bool} :
|
||||
(it.filterMapM f).all p = (it.mapM (pure (f := n))).allM (fun x => do
|
||||
match ← f x with
|
||||
| some fx => return .up (p fx)
|
||||
| none => return .up true) := by
|
||||
simp [all_eq_allM, allM_filterMapM]
|
||||
|
||||
theorem IterM.all_mapM {α β β' : Type w} {m : Type w → Type w'} {n : Type w → Type w''}
|
||||
[Iterator α m β] [Finite α m] [Monad m] [Monad n] [MonadLiftT m n] [IteratorLoop α m m]
|
||||
[LawfulMonad m] [LawfulMonad n] [LawfulMonadLiftT m n] [LawfulIteratorLoop α m m]
|
||||
{it : IterM (α := α) m β} {f : β → n β'} {p : β' → Bool} :
|
||||
(it.mapM f).all p = (it.mapM (pure (f := n))).allM (fun x => (.up <| p ·) <$> (f x)) := by
|
||||
simp [all_eq_allM, allM_mapM]
|
||||
|
||||
theorem IterM.all_filterM {α β : Type w} {m : Type w → Type w'} {n : Type w → Type w''}
|
||||
[Iterator α m β] [Finite α m] [Monad m] [Monad n] [MonadLiftT m n] [IteratorLoop α m m]
|
||||
[LawfulMonad m] [LawfulMonad n] [LawfulMonadLiftT m n] [LawfulIteratorLoop α m m]
|
||||
{it : IterM (α := α) m β} {f : β → n (ULift Bool)} {p : β → Bool} :
|
||||
(it.filterM f).all p = (it.mapM (pure (f := n))).allM (fun x => do
|
||||
if (← f x).down then
|
||||
return .up (p x)
|
||||
else
|
||||
return .up true) := by
|
||||
simp [all_eq_allM, allM_filterM]
|
||||
|
||||
theorem IterM.all_filterMap {α β β' : Type w} {m : Type w → Type w'}
|
||||
[Iterator α m β] [Finite α m] [Monad m] [IteratorLoop α m m]
|
||||
[LawfulMonad m] [LawfulIteratorLoop α m m]
|
||||
{it : IterM (α := α) m β} {f : β → Option β'} {p : β' → Bool} :
|
||||
(it.filterMap f).all p = it.all (fun x =>
|
||||
match f x with
|
||||
| some fx => (p fx)
|
||||
| none => true) := by
|
||||
induction it using IterM.inductSteps with | step it ihy ihs
|
||||
rw [all_eq_match_step, all_eq_match_step, step_filterMap, bind_assoc]
|
||||
apply bind_congr; intro step
|
||||
split
|
||||
· split
|
||||
· simp [*, ihy ‹_›]
|
||||
· simp only [*, PlausibleIterStep.yield, pure_bind]
|
||||
split <;> simp [ihy ‹_›]
|
||||
· simp [PlausibleIterStep.skip, pure_bind, ihs ‹_›]
|
||||
· simp
|
||||
|
||||
theorem IterM.all_map {α β β' : Type w} {m : Type w → Type w'}
|
||||
[Iterator α m β] [Finite α m] [Monad m] [IteratorLoop α m m]
|
||||
[LawfulMonad m] [LawfulIteratorLoop α m m]
|
||||
{it : IterM (α := α) m β} {f : β → β'} {p : β' → Bool} :
|
||||
(it.map f).all p = it.all (fun x => p (f x)) := by
|
||||
induction it using IterM.inductSteps with | step it ihy ihs
|
||||
rw [all_eq_match_step, all_eq_match_step, step_map, bind_assoc]
|
||||
apply bind_congr; intro step
|
||||
split
|
||||
· simp only [pure_bind]
|
||||
simp [ihy ‹_›]
|
||||
· simp [PlausibleIterStep.skip, pure_bind, ihs ‹_›]
|
||||
· simp
|
||||
|
||||
end AnyAll
|
||||
|
||||
end Std.Iterators
|
||||
|
|
|
|||
|
|
@ -497,4 +497,236 @@ theorem Iter.length_toListRev_eq_size {α β : Type w} [Iterator α Id β] [Fini
|
|||
it.toListRev.length = it.size := by
|
||||
rw [toListRev_eq, List.length_reverse, length_toList_eq_size]
|
||||
|
||||
theorem Iter.anyM_eq_forIn {α β : Type w} {m : Type → Type w'} [Iterator α Id β]
|
||||
[Finite α Id] [Monad m] [LawfulMonad m] [IteratorLoop α Id m] [LawfulIteratorLoop α Id m]
|
||||
{it : Iter (α := α) β} {p : β → m Bool} :
|
||||
it.anyM p = (ForIn.forIn it false (fun x _ => do
|
||||
if ← p x then
|
||||
return .done true
|
||||
else
|
||||
return .yield false)) := by
|
||||
rfl
|
||||
|
||||
theorem Iter.anyM_eq_match_step {α β : Type w} {m : Type → Type w'} [Iterator α Id β]
|
||||
[Finite α Id] [Monad m] [LawfulMonad m] [IteratorLoop α Id m] [LawfulIteratorLoop α Id m]
|
||||
{it : Iter (α := α) β} {p : β → m Bool} :
|
||||
it.anyM p = (do
|
||||
match it.step.val with
|
||||
| .yield it' x =>
|
||||
if (← p x) then
|
||||
return true
|
||||
else
|
||||
it'.anyM p
|
||||
| .skip it' => it'.anyM p
|
||||
| .done => return false) := by
|
||||
rw [anyM_eq_forIn, forIn_eq_match_step]
|
||||
simp only [bind_assoc]
|
||||
cases it.step using PlausibleIterStep.casesOn
|
||||
· apply bind_congr; intro px
|
||||
split
|
||||
· simp
|
||||
· simp [anyM_eq_forIn]
|
||||
· simp [anyM_eq_forIn]
|
||||
· simp
|
||||
|
||||
theorem Iter.anyM_toList {α β : Type w} {m : Type → Type w'} [Iterator α Id β]
|
||||
[Finite α Id] [Monad m] [LawfulMonad m] [IteratorLoop α Id m] [LawfulIteratorLoop α Id m]
|
||||
[IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id]
|
||||
{it : Iter (α := α) β} {p : β → m Bool} :
|
||||
it.toList.anyM p = it.anyM p := by
|
||||
induction it using Iter.inductSteps with | step it ihy ihs =>
|
||||
rw [it.toList_eq_match_step, anyM_eq_match_step]
|
||||
cases it.step using PlausibleIterStep.casesOn
|
||||
· simp only [List.anyM_cons, ihy ‹_›]
|
||||
· simp only [ihs ‹_›]
|
||||
· simp only [List.anyM_nil]
|
||||
|
||||
theorem Iter.anyM_toArray {α β : Type w} {m : Type → Type w'} [Iterator α Id β]
|
||||
[Finite α Id] [Monad m] [LawfulMonad m] [IteratorLoop α Id m] [LawfulIteratorLoop α Id m]
|
||||
[IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id]
|
||||
{it : Iter (α := α) β} {p : β → m Bool} :
|
||||
it.toArray.anyM p = it.anyM p := by
|
||||
simp only [← Iter.toArray_toList, List.anyM_toArray, anyM_toList]
|
||||
|
||||
theorem Iter.any_eq_anyM {α β : Type w} [Iterator α Id β]
|
||||
[Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
|
||||
{it : Iter (α := α) β} {p : β → Bool} :
|
||||
it.any p = (it.anyM (fun x => pure (f := Id) (p x))).run := by
|
||||
rfl
|
||||
|
||||
theorem Iter.anyM_pure {α β : Type w} [Iterator α Id β]
|
||||
[Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
|
||||
{it : Iter (α := α) β} {p : β → Bool} :
|
||||
it.anyM (fun x => pure (f := Id) (p x)) = pure (it.any (fun x => p x)) := by
|
||||
simp [any_eq_anyM]
|
||||
|
||||
theorem Iter.any_eq_match_step {α β : Type w} [Iterator α Id β]
|
||||
[Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
|
||||
{it : Iter (α := α) β} {p : β → Bool} :
|
||||
it.any p = (match it.step.val with
|
||||
| .yield it' x =>
|
||||
if p x then
|
||||
true
|
||||
else
|
||||
it'.any p
|
||||
| .skip it' => it'.any p
|
||||
| .done => false) := by
|
||||
rw [any_eq_anyM, anyM_eq_match_step]
|
||||
split
|
||||
· simp only [pure_bind, Bool.if_true_left, Bool.decide_eq_true, any_eq_anyM]
|
||||
split <;> simp [*]
|
||||
· simp [any_eq_anyM]
|
||||
· simp
|
||||
|
||||
theorem Iter.any_eq_forIn {α β : Type w} [Iterator α Id β]
|
||||
[Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
|
||||
{it : Iter (α := α) β} {p : β → Bool} :
|
||||
it.any p = (ForIn.forIn (m := Id) it false (fun x _ => do
|
||||
if p x then
|
||||
return .done true
|
||||
else
|
||||
return .yield false)).run := by
|
||||
simp [any_eq_anyM, anyM_eq_forIn]
|
||||
|
||||
theorem Iter.any_toList {α β : Type w} [Iterator α Id β]
|
||||
[Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
|
||||
[IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id]
|
||||
{it : Iter (α := α) β} {p : β → Bool} :
|
||||
it.toList.any p = it.any p := by
|
||||
induction it using Iter.inductSteps with | step it ihy ihs =>
|
||||
rw [it.toList_eq_match_step, any_eq_match_step]
|
||||
cases it.step using PlausibleIterStep.casesOn
|
||||
· simp only [List.any_cons, ihy ‹_›]
|
||||
split <;> simp [*]
|
||||
· simp only [ihs ‹_›]
|
||||
· simp only [List.any_nil]
|
||||
|
||||
theorem Iter.any_toArray {α β : Type w} [Iterator α Id β]
|
||||
[Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
|
||||
[IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id]
|
||||
{it : Iter (α := α) β} {p : β → Bool} :
|
||||
it.toArray.any p = it.any p := by
|
||||
simp only [← Iter.toArray_toList, List.any_toArray, any_toList]
|
||||
|
||||
theorem Iter.allM_eq_forIn {α β : Type w} {m : Type → Type w'} [Iterator α Id β]
|
||||
[Finite α Id] [Monad m] [LawfulMonad m] [IteratorLoop α Id m] [LawfulIteratorLoop α Id m]
|
||||
{it : Iter (α := α) β} {p : β → m Bool} :
|
||||
it.allM p = (ForIn.forIn it true (fun x _ => do
|
||||
if ← p x then
|
||||
return .yield true
|
||||
else
|
||||
return .done false)) := by
|
||||
rfl
|
||||
|
||||
theorem Iter.allM_eq_match_step {α β : Type w} {m : Type → Type w'} [Iterator α Id β]
|
||||
[Finite α Id] [Monad m] [LawfulMonad m] [IteratorLoop α Id m] [LawfulIteratorLoop α Id m]
|
||||
{it : Iter (α := α) β} {p : β → m Bool} :
|
||||
it.allM p = (do
|
||||
match it.step.val with
|
||||
| .yield it' x =>
|
||||
if (← p x) then
|
||||
it'.allM p
|
||||
else
|
||||
return false
|
||||
| .skip it' => it'.allM p
|
||||
| .done => return true) := by
|
||||
rw [allM_eq_forIn, forIn_eq_match_step]
|
||||
simp only [bind_assoc]
|
||||
cases it.step using PlausibleIterStep.casesOn
|
||||
· apply bind_congr; intro px
|
||||
split
|
||||
· simp [allM_eq_forIn]
|
||||
· simp
|
||||
· simp [allM_eq_forIn]
|
||||
· simp
|
||||
|
||||
theorem Iter.all_eq_allM {α β : Type w} [Iterator α Id β]
|
||||
[Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
|
||||
{it : Iter (α := α) β} {p : β → Bool} :
|
||||
it.all p = (it.allM (fun x => pure (f := Id) (p x))).run := by
|
||||
rfl
|
||||
|
||||
theorem Iter.allM_pure {α β : Type w} [Iterator α Id β]
|
||||
[Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
|
||||
{it : Iter (α := α) β} {p : β → Bool} :
|
||||
it.allM (fun x => pure (f := Id) (p x)) = pure (it.all (fun x => p x)) := by
|
||||
simp [all_eq_allM]
|
||||
|
||||
theorem Iter.all_eq_match_step {α β : Type w} [Iterator α Id β]
|
||||
[Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
|
||||
{it : Iter (α := α) β} {p : β → Bool} :
|
||||
it.all p = (match it.step.val with
|
||||
| .yield it' x =>
|
||||
if p x then
|
||||
it'.all p
|
||||
else
|
||||
false
|
||||
| .skip it' => it'.all p
|
||||
| .done => true) := by
|
||||
rw [all_eq_allM, allM_eq_match_step]
|
||||
split
|
||||
· simp only [pure_bind, all_eq_allM, Bool.if_false_right, Bool.decide_eq_true]
|
||||
split <;> simp [*]
|
||||
· simp [all_eq_allM]
|
||||
· simp
|
||||
|
||||
theorem Iter.all_eq_forIn {α β : Type w} [Iterator α Id β]
|
||||
[Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
|
||||
{it : Iter (α := α) β} {p : β → Bool} :
|
||||
it.all p = (ForIn.forIn (m := Id) it true (fun x _ => do
|
||||
if p x then
|
||||
return .yield true
|
||||
else
|
||||
return .done false)).run := by
|
||||
simp [all_eq_allM, allM_eq_forIn]
|
||||
|
||||
theorem Iter.all_toList {α β : Type w} [Iterator α Id β]
|
||||
[Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
|
||||
[IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id]
|
||||
{it : Iter (α := α) β} {p : β → Bool} :
|
||||
it.toList.all p = it.all p := by
|
||||
induction it using Iter.inductSteps with | step it ihy ihs =>
|
||||
rw [it.toList_eq_match_step, all_eq_match_step]
|
||||
cases it.step using PlausibleIterStep.casesOn
|
||||
· simp only [List.all_cons, ihy ‹_›]
|
||||
split <;> simp [*]
|
||||
· simp only [ihs ‹_›]
|
||||
· simp only [List.all_nil]
|
||||
|
||||
theorem Iter.all_toArray {α β : Type w} [Iterator α Id β]
|
||||
[Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
|
||||
[IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id]
|
||||
{it : Iter (α := α) β} {p : β → Bool} :
|
||||
it.toArray.all p = it.all p := by
|
||||
simp only [← Iter.toArray_toList, List.all_toArray, all_toList]
|
||||
|
||||
theorem Iter.allM_eq_not_anyM_not {α β : Type w} {m : Type → Type w'} [Iterator α Id β]
|
||||
[Finite α Id] [Monad m] [LawfulMonad m] [IteratorLoop α Id m] [LawfulIteratorLoop α Id m]
|
||||
{it : Iter (α := α) β} {p : β → m Bool} :
|
||||
it.allM p = (! ·) <$> it.anyM ((! ·) <$> p ·) := by
|
||||
induction it using Iter.inductSteps with | step it ihy ihs =>
|
||||
rw [allM_eq_match_step, anyM_eq_match_step, map_eq_pure_bind]
|
||||
cases it.step using PlausibleIterStep.casesOn
|
||||
· simp only [map_eq_pure_bind, bind_assoc, pure_bind]
|
||||
apply bind_congr; intro px
|
||||
split
|
||||
· simp [*, ihy ‹_›]
|
||||
· simp [*]
|
||||
· simp [ihs ‹_›]
|
||||
· simp
|
||||
|
||||
theorem Iter.all_eq_not_any_not {α β : Type w} [Iterator α Id β]
|
||||
[Finite α Id] [Monad m] [LawfulMonad m] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
|
||||
{it : Iter (α := α) β} {p : β → Bool} :
|
||||
it.all p = ! it.any (! p ·) := by
|
||||
induction it using Iter.inductSteps with | step it ihy ihs =>
|
||||
rw [all_eq_match_step, any_eq_match_step]
|
||||
cases it.step using PlausibleIterStep.casesOn
|
||||
· simp only
|
||||
split
|
||||
· simp [*, ihy ‹_›]
|
||||
· simp [*]
|
||||
· simp [ihs ‹_›]
|
||||
· simp
|
||||
|
||||
end Std.Iterators
|
||||
|
|
|
|||
|
|
@ -334,4 +334,183 @@ theorem IterM.drain_eq_map_toArray {α β : Type w} {m : Type w → Type w'} [It
|
|||
it.drain = (fun _ => .unit) <$> it.toList := by
|
||||
simp [IterM.drain_eq_map_toList]
|
||||
|
||||
theorem IterM.anyM_eq_forIn {α β : Type w} {m : Type w → Type w'} [Iterator α m β]
|
||||
[Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m]
|
||||
{it : IterM (α := α) m β} {p : β → m (ULift Bool)} :
|
||||
it.anyM p = (ForIn.forIn it (.up false) (fun x _ => do
|
||||
if (← p x).down then
|
||||
return .done (.up true)
|
||||
else
|
||||
return .yield (.up false))) := by
|
||||
rfl
|
||||
|
||||
theorem IterM.anyM_eq_match_step {α β : Type w} {m : Type w → Type w'} [Iterator α m β]
|
||||
[Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m]
|
||||
{it : IterM (α := α) m β} {p : β → m (ULift Bool)} :
|
||||
it.anyM p = (do
|
||||
match (← it.step).val with
|
||||
| .yield it' x =>
|
||||
if (← p x).down then
|
||||
return .up true
|
||||
else
|
||||
it'.anyM p
|
||||
| .skip it' => it'.anyM p
|
||||
| .done => return .up false) := by
|
||||
rw [anyM_eq_forIn, forIn_eq_match_step]
|
||||
simp only [monadLift_self, bind_assoc]
|
||||
apply bind_congr; intro step
|
||||
split
|
||||
· apply bind_congr; intro px
|
||||
split
|
||||
· simp
|
||||
· simp [anyM_eq_forIn]
|
||||
· simp [anyM_eq_forIn]
|
||||
· simp
|
||||
|
||||
theorem IterM.any_eq_anyM {α β : Type w} {m : Type w → Type w'} [Iterator α m β]
|
||||
[Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m]
|
||||
{it : IterM (α := α) m β} {p : β → Bool} :
|
||||
it.any p = it.anyM (fun x => pure (.up (p x))) := by
|
||||
rfl
|
||||
|
||||
theorem IterM.anyM_pure {α β : Type w} {m : Type w → Type w'} [Iterator α m β]
|
||||
[Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m]
|
||||
{it : IterM (α := α) m β} {p : β → ULift Bool} :
|
||||
it.anyM (fun x => pure (p x)) = it.any (fun x => (p x).down) := by
|
||||
simp [any_eq_anyM]
|
||||
|
||||
theorem IterM.any_eq_match_step {α β : Type w} {m : Type w → Type w'} [Iterator α m β]
|
||||
[Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m]
|
||||
{it : IterM (α := α) m β} {p : β → Bool} :
|
||||
it.any p = (do
|
||||
match (← it.step).val with
|
||||
| .yield it' x =>
|
||||
if p x then
|
||||
return .up true
|
||||
else
|
||||
it'.any p
|
||||
| .skip it' => it'.any p
|
||||
| .done => return .up false) := by
|
||||
rw [any_eq_anyM, anyM_eq_match_step]
|
||||
apply bind_congr; intro step
|
||||
split
|
||||
· simp [any_eq_anyM]
|
||||
· simp [any_eq_anyM]
|
||||
· simp
|
||||
|
||||
theorem IterM.any_eq_forIn {α β : Type w} {m : Type w → Type w'} [Iterator α m β]
|
||||
[Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m]
|
||||
{it : IterM (α := α) m β} {p : β → Bool} :
|
||||
it.any p = (ForIn.forIn it (.up false) (fun x _ => do
|
||||
if p x then
|
||||
return .done (.up true)
|
||||
else
|
||||
return .yield (.up false))) := by
|
||||
simp [any_eq_anyM, anyM_eq_forIn]
|
||||
|
||||
theorem IterM.allM_eq_forIn {α β : Type w} {m : Type w → Type w'} [Iterator α m β]
|
||||
[Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m]
|
||||
{it : IterM (α := α) m β} {p : β → m (ULift Bool)} :
|
||||
it.allM p = (ForIn.forIn it (.up true) (fun x _ => do
|
||||
if (← p x).down then
|
||||
return .yield (.up true)
|
||||
else
|
||||
return .done (.up false))) := by
|
||||
rfl
|
||||
|
||||
theorem IterM.allM_eq_match_step {α β : Type w} {m : Type w → Type w'} [Iterator α m β]
|
||||
[Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m]
|
||||
{it : IterM (α := α) m β} {p : β → m (ULift Bool)} :
|
||||
it.allM p = (do
|
||||
match (← it.step).val with
|
||||
| .yield it' x =>
|
||||
if (← p x).down then
|
||||
it'.allM p
|
||||
else
|
||||
return .up false
|
||||
| .skip it' => it'.allM p
|
||||
| .done => return .up true) := by
|
||||
rw [allM_eq_forIn, forIn_eq_match_step]
|
||||
simp only [monadLift_self, bind_assoc]
|
||||
apply bind_congr; intro step
|
||||
split
|
||||
· apply bind_congr; intro px
|
||||
split
|
||||
· simp [allM_eq_forIn]
|
||||
· simp
|
||||
· simp [allM_eq_forIn]
|
||||
· simp
|
||||
|
||||
theorem IterM.all_eq_allM {α β : Type w} {m : Type w → Type w'} [Iterator α m β]
|
||||
[Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m]
|
||||
{it : IterM (α := α) m β} {p : β → Bool} :
|
||||
it.all p = it.allM (fun x => pure (.up (p x))) := by
|
||||
rfl
|
||||
|
||||
theorem IterM.allM_pure {α β : Type w} {m : Type w → Type w'} [Iterator α m β]
|
||||
[Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m]
|
||||
{it : IterM (α := α) m β} {p : β → ULift Bool} :
|
||||
it.allM (fun x => pure (p x)) = it.all (fun x => (p x).down) := by
|
||||
simp [all_eq_allM]
|
||||
|
||||
theorem IterM.all_eq_match_step {α β : Type w} {m : Type w → Type w'} [Iterator α m β]
|
||||
[Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m]
|
||||
{it : IterM (α := α) m β} {p : β → Bool} :
|
||||
it.all p = (do
|
||||
match (← it.step).val with
|
||||
| .yield it' x =>
|
||||
if p x then
|
||||
it'.all p
|
||||
else
|
||||
return .up false
|
||||
| .skip it' => it'.all p
|
||||
| .done => return .up true) := by
|
||||
rw [all_eq_allM, allM_eq_match_step]
|
||||
apply bind_congr; intro step
|
||||
split
|
||||
· simp [all_eq_allM]
|
||||
· simp [all_eq_allM]
|
||||
· simp
|
||||
|
||||
theorem IterM.all_eq_forIn {α β : Type w} {m : Type w → Type w'} [Iterator α m β]
|
||||
[Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m]
|
||||
{it : IterM (α := α) m β} {p : β → Bool} :
|
||||
it.all p = (ForIn.forIn it (.up true) (fun x _ => do
|
||||
if p x then
|
||||
return .yield (.up true)
|
||||
else
|
||||
return .done (.up false))) := by
|
||||
simp [all_eq_allM, allM_eq_forIn]
|
||||
|
||||
theorem IterM.allM_eq_not_anyM_not {α β : Type w} {m : Type w → Type w'} [Iterator α m β]
|
||||
[Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m]
|
||||
{it : IterM (α := α) m β} {p : β → m (ULift Bool)} :
|
||||
it.allM p = (fun x => .up !x.down) <$> it.anyM ((fun x => .up !x.down) <$> p ·) := by
|
||||
induction it using IterM.inductSteps with | step it ihy ihs =>
|
||||
rw [allM_eq_match_step, anyM_eq_match_step, map_eq_pure_bind, bind_assoc]
|
||||
apply bind_congr; intro step
|
||||
cases step using PlausibleIterStep.casesOn
|
||||
· simp only [map_eq_pure_bind, bind_assoc, pure_bind]
|
||||
apply bind_congr; intro px
|
||||
split
|
||||
· simp [*, ihy ‹_›]
|
||||
· simp [*]
|
||||
· simp [ihs ‹_›]
|
||||
· simp
|
||||
|
||||
theorem IterM.all_eq_not_any_not {α β : Type w} {m : Type w → Type w'} [Iterator α m β]
|
||||
[Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m]
|
||||
{it : IterM (α := α) m β} {p : β → Bool} :
|
||||
it.all p = (fun x => .up !x.down) <$> it.any (! p ·) := by
|
||||
induction it using IterM.inductSteps with | step it ihy ihs =>
|
||||
rw [all_eq_match_step, any_eq_match_step, map_eq_pure_bind, bind_assoc]
|
||||
apply bind_congr; intro step
|
||||
cases step using PlausibleIterStep.casesOn
|
||||
· simp only
|
||||
split
|
||||
· simp [*, ihy ‹_›]
|
||||
· simp [*]
|
||||
· simp [ihs ‹_›]
|
||||
· simp
|
||||
|
||||
end Std.Iterators
|
||||
|
|
|
|||
|
|
@ -481,10 +481,38 @@ theorem allM_eq_not_anyM_not [Monad m] [LawfulMonad m] {p : α → m Bool} {as :
|
|||
simp only [anyM, ih, pure_bind]
|
||||
split <;> simp_all
|
||||
|
||||
@[simp] theorem anyM_nil [Monad m] {p : α → m Bool} :
|
||||
([] : List α).anyM p = pure false :=
|
||||
(rfl)
|
||||
|
||||
@[simp] theorem anyM_cons [Monad m] {p : α → m Bool} {x : α} {xs : List α} :
|
||||
(x :: xs).anyM p = (do
|
||||
if (← p x) then
|
||||
return true
|
||||
else
|
||||
xs.anyM p) := by
|
||||
rw [anyM]
|
||||
apply bind_congr; intro px
|
||||
split <;> simp
|
||||
|
||||
@[simp] theorem allM_pure [Monad m] [LawfulMonad m] {p : α → Bool} {as : List α} :
|
||||
as.allM (m := m) (pure <| p ·) = pure (as.all p) := by
|
||||
simp [allM_eq_not_anyM_not, all_eq_not_any_not]
|
||||
|
||||
@[simp] theorem allM_nil [Monad m] {p : α → m Bool} :
|
||||
([] : List α).allM p = pure true :=
|
||||
(rfl)
|
||||
|
||||
@[simp] theorem allM_cons [Monad m] {p : α → m Bool} {x : α} {xs : List α} :
|
||||
(x :: xs).allM p = (do
|
||||
if (← p x) then
|
||||
xs.allM p
|
||||
else
|
||||
return false) := by
|
||||
rw [allM]
|
||||
apply bind_congr; intro px
|
||||
split <;> simp
|
||||
|
||||
/-! ### Recognizing higher order functions using a function that only depends on the value. -/
|
||||
|
||||
/--
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue