This file contains monotonicity lemmas for higher-order monadic operations (e.g. mapM) in the
standard library. This allows recursive definitions using partial_fixpoint to use nested
recursion.
Ideally, every higher-order monadic funciton in the standard library has a lemma here. At the time of writing, this file covers functions from
- Init/Data/Option/Basic.lean
- Init/Data/List/Control.lean
- Init/Data/Array/Basic.lean
in the order of their apperance there. No automation to check the exhaustiveness exists yet.
The lemma statements are written manually, but follow a predictable scheme, and could be automated.
Likewise, the proofs are written very naively. Most of them could be handled by a tactic like
monotonicity (extended to make use of local hypotheses).
theorem
Lean.Order.Functor.monotone_map
{m : Type u → Type v}
[Monad m]
[(α : Type u) → PartialOrder (m α)]
[MonoBind m]
{α β : Type u}
{γ : Type w}
[PartialOrder γ]
[LawfulMonad m]
(f : γ → m α)
(g : α → β)
(hmono : monotone f)
:
theorem
Lean.Order.Seq.monotone_seq
{m : Type u → Type v}
[Monad m]
[(α : Type u) → PartialOrder (m α)]
[MonoBind m]
{α β : Type u}
{γ : Type w}
[PartialOrder γ]
[LawfulMonad m]
(f : γ → m α)
(g : γ → m (α → β))
(hmono₁ : monotone g)
(hmono₂ : monotone f)
:
monotone fun (x : γ) => g x <*> f x
theorem
Lean.Order.SeqLeft.monotone_seqLeft
{m : Type u → Type v}
[Monad m]
[(α : Type u) → PartialOrder (m α)]
[MonoBind m]
{α β : Type u}
{γ : Type w}
[PartialOrder γ]
[LawfulMonad m]
(f : γ → m α)
(g : γ → m β)
(hmono₁ : monotone g)
(hmono₂ : monotone f)
:
monotone fun (x : γ) => g x <* f x
theorem
Lean.Order.SeqRight.monotone_seqRight
{m : Type u → Type v}
[Monad m]
[(α : Type u) → PartialOrder (m α)]
[MonoBind m]
{α β : Type u}
{γ : Type w}
[PartialOrder γ]
[LawfulMonad m]
(f : γ → m α)
(g : γ → m β)
(hmono₁ : monotone g)
(hmono₂ : monotone f)
:
monotone fun (x : γ) => g x *> f x
theorem
Lean.Order.Option.monotone_bindM
{m : Type u → Type v}
[Monad m]
[(α : Type u) → PartialOrder (m α)]
[MonoBind m]
{α β : Type u}
{γ : Type w}
[PartialOrder γ]
(f : γ → α → m (Option β))
(xs : Option α)
(hmono : monotone f)
:
monotone fun (x : γ) => Option.bindM (f x) xs
theorem
Lean.Order.Option.monotone_mapM
{m : Type u → Type v}
[Monad m]
[(α : Type u) → PartialOrder (m α)]
[MonoBind m]
{α β : Type u}
{γ : Type w}
[PartialOrder γ]
(f : γ → α → m β)
(xs : Option α)
(hmono : monotone f)
:
monotone fun (x : γ) => Option.mapM (f x) xs
theorem
Lean.Order.Option.monotone_elimM
{m : Type u → Type v}
[Monad m]
[(α : Type u) → PartialOrder (m α)]
[MonoBind m]
{α β : Type u}
{γ : Type w}
[PartialOrder γ]
(a : γ → m (Option α))
(n : γ → m β)
(s : γ → α → m β)
(hmono₁ : monotone a)
(hmono₂ : monotone n)
(hmono₃ : monotone s)
:
monotone fun (x : γ) => Option.elimM (a x) (n x) (s x)
theorem
Lean.Order.Option.monotone_getDM
{m : Type u → Type v}
[Monad m]
[(α : Type u) → PartialOrder (m α)]
{α : Type u}
{γ : Type w}
[PartialOrder γ]
(o : Option α)
(y : γ → m α)
(hmono : monotone y)
:
theorem
Lean.Order.List.monotone_mapM
{m : Type u → Type v}
[Monad m]
[(α : Type u) → PartialOrder (m α)]
[MonoBind m]
{α β : Type u}
{γ : Type w}
[PartialOrder γ]
(f : γ → α → m β)
(xs : List α)
(hmono : monotone f)
:
theorem
Lean.Order.List.monotone_filterAuxM
{γ : Type w}
[PartialOrder γ]
{m : Type → Type v}
[Monad m]
[(α : Type) → PartialOrder (m α)]
[MonoBind m]
{α : Type}
(f : γ → α → m Bool)
(xs acc : List α)
(hmono : monotone f)
:
monotone fun (x : γ) => List.filterAuxM (f x) xs acc
theorem
Lean.Order.List.monotone_filterM
{γ : Type w}
[PartialOrder γ]
{m : Type → Type v}
[Monad m]
[(α : Type) → PartialOrder (m α)]
[MonoBind m]
{α : Type}
(f : γ → α → m Bool)
(xs : List α)
(hmono : monotone f)
:
monotone fun (x : γ) => List.filterM (f x) xs
theorem
Lean.Order.List.monotone_filterRevM
{γ : Type w}
[PartialOrder γ]
{m : Type → Type v}
[Monad m]
[(α : Type) → PartialOrder (m α)]
[MonoBind m]
{α : Type}
(f : γ → α → m Bool)
(xs : List α)
(hmono : monotone f)
:
monotone fun (x : γ) => List.filterRevM (f x) xs
theorem
Lean.Order.List.monotone_foldlM
{m : Type u → Type v}
[Monad m]
[(α : Type u) → PartialOrder (m α)]
[MonoBind m]
{α β : Type u}
{γ : Type w}
[PartialOrder γ]
(f : γ → β → α → m β)
(init : β)
(xs : List α)
(hmono : monotone f)
:
monotone fun (x : γ) => List.foldlM (f x) init xs
theorem
Lean.Order.List.monotone_foldrM
{m : Type u → Type v}
[Monad m]
[(α : Type u) → PartialOrder (m α)]
[MonoBind m]
{α β : Type u}
{γ : Type w}
[PartialOrder γ]
(f : γ → α → β → m β)
(init : β)
(xs : List α)
(hmono : monotone f)
:
monotone fun (x : γ) => List.foldrM (f x) init xs
theorem
Lean.Order.List.monotone_findM?
{γ : Type w}
[PartialOrder γ]
{m : Type → Type v}
[Monad m]
[(α : Type) → PartialOrder (m α)]
[MonoBind m]
{α : Type}
(f : γ → α → m Bool)
(xs : List α)
(hmono : monotone f)
:
monotone fun (x : γ) => List.findM? (f x) xs
theorem
Lean.Order.List.monotone_findSomeM?
{m : Type u → Type v}
[Monad m]
[(α : Type u) → PartialOrder (m α)]
[MonoBind m]
{α β : Type u}
{γ : Type w}
[PartialOrder γ]
(f : γ → α → m (Option β))
(xs : List α)
(hmono : monotone f)
:
monotone fun (x : γ) => List.findSomeM? (f x) xs
theorem
Lean.Order.List.monotone_forIn'_loop
{m : Type u → Type v}
[Monad m]
[(α : Type u) → PartialOrder (m α)]
[MonoBind m]
{β : Type u}
{γ : Type w}
[PartialOrder γ]
{α : Type uu}
(as : List α)
(f : γ → (a : α) → a ∈ as → β → m (ForInStep β))
(as' : List α)
(b : β)
(p : ∃ (bs : List α), bs ++ as' = as)
(hmono : monotone f)
:
monotone fun (x : γ) => List.forIn'.loop as (f x) as' b p
theorem
Lean.Order.List.monotone_forIn'
{m : Type u → Type v}
[Monad m]
[(α : Type u) → PartialOrder (m α)]
[MonoBind m]
{β : Type u}
{γ : Type w}
[PartialOrder γ]
{α : Type uu}
(as : List α)
(init : β)
(f : γ → (a : α) → a ∈ as → β → m (ForInStep β))
(hmono : monotone f)
:
theorem
Lean.Order.List.monotone_forIn
{m : Type u → Type v}
[Monad m]
[(α : Type u) → PartialOrder (m α)]
[MonoBind m]
{β : Type u}
{γ : Type w}
[PartialOrder γ]
{α : Type uu}
(as : List α)
(init : β)
(f : γ → α → β → m (ForInStep β))
(hmono : monotone f)
:
theorem
Lean.Order.Array.monotone_forIn'_loop
{m : Type u → Type v}
[Monad m]
[(α : Type u) → PartialOrder (m α)]
[MonoBind m]
{β : Type u}
{γ : Type w}
[PartialOrder γ]
{α : Type uu}
(as : Array α)
(f : γ → (a : α) → a ∈ as → β → m (ForInStep β))
(i : Nat)
(h : i ≤ as.size)
(b : β)
(hmono : monotone f)
:
monotone fun (x : γ) => Array.forIn'.loop as (f x) i h b
theorem
Lean.Order.Array.monotone_forIn'
{m : Type u → Type v}
[Monad m]
[(α : Type u) → PartialOrder (m α)]
[MonoBind m]
{β : Type u}
{γ : Type w}
[PartialOrder γ]
{α : Type uu}
(as : Array α)
(init : β)
(f : γ → (a : α) → a ∈ as → β → m (ForInStep β))
(hmono : monotone f)
:
theorem
Lean.Order.Array.monotone_forIn
{m : Type u → Type v}
[Monad m]
[(α : Type u) → PartialOrder (m α)]
[MonoBind m]
{β : Type u}
{γ : Type w}
[PartialOrder γ]
{α : Type uu}
(as : Array α)
(init : β)
(f : γ → α → β → m (ForInStep β))
(hmono : monotone f)
:
theorem
Lean.Order.Array.monotone_foldlM_loop
{m : Type u → Type v}
[Monad m]
[(α : Type u) → PartialOrder (m α)]
[MonoBind m]
{α β : Type u}
{γ : Type w}
[PartialOrder γ]
(f : γ → β → α → m β)
(xs : Array α)
(stop : Nat)
(h : stop ≤ xs.size)
(i j : Nat)
(b : β)
(hmono : monotone f)
:
monotone fun (x : γ) => Array.foldlM.loop (f x) xs stop h i j b
theorem
Lean.Order.Array.monotone_foldlM
{m : Type u → Type v}
[Monad m]
[(α : Type u) → PartialOrder (m α)]
[MonoBind m]
{α β : Type u}
{γ : Type w}
[PartialOrder γ]
(f : γ → β → α → m β)
(init : β)
(xs : Array α)
(start stop : Nat)
(hmono : monotone f)
:
monotone fun (x : γ) => Array.foldlM (f x) init xs start stop
theorem
Lean.Order.Array.monotone_foldrM_fold
{m : Type u → Type v}
[Monad m]
[(α : Type u) → PartialOrder (m α)]
[MonoBind m]
{α β : Type u}
{γ : Type w}
[PartialOrder γ]
(f : γ → α → β → m β)
(xs : Array α)
(stop i : Nat)
(h : i ≤ xs.size)
(b : β)
(hmono : monotone f)
:
monotone fun (x : γ) => Array.foldrM.fold (f x) xs stop i h b
theorem
Lean.Order.Array.monotone_foldrM
{m : Type u → Type v}
[Monad m]
[(α : Type u) → PartialOrder (m α)]
[MonoBind m]
{α β : Type u}
{γ : Type w}
[PartialOrder γ]
(f : γ → α → β → m β)
(init : β)
(xs : Array α)
(start stop : Nat)
(hmono : monotone f)
:
monotone fun (x : γ) => Array.foldrM (f x) init xs start stop
theorem
Lean.Order.Array.monotone_mapM
{m : Type u → Type v}
[Monad m]
[(α : Type u) → PartialOrder (m α)]
[MonoBind m]
{α β : Type u}
{γ : Type w}
[PartialOrder γ]
(xs : Array α)
(f : γ → α → m β)
(hmono : monotone f)
:
monotone fun (x : γ) => Array.mapM (f x) xs
theorem
Lean.Order.Array.monotone_mapFinIdxM
{m : Type u → Type v}
[Monad m]
[(α : Type u) → PartialOrder (m α)]
[MonoBind m]
{α β : Type u}
{γ : Type w}
[PartialOrder γ]
(xs : Array α)
(f : γ → (i : Nat) → α → i < xs.size → m β)
(hmono : monotone f)
:
monotone fun (x : γ) => xs.mapFinIdxM (f x)
theorem
Lean.Order.Array.monotone_findSomeM?
{m : Type u → Type v}
[Monad m]
[(α : Type u) → PartialOrder (m α)]
[MonoBind m]
{α β : Type u}
{γ : Type w}
[PartialOrder γ]
(f : γ → α → m (Option β))
(xs : Array α)
(hmono : monotone f)
:
monotone fun (x : γ) => Array.findSomeM? (f x) xs
theorem
Lean.Order.Array.monotone_findM?
{γ : Type w}
[PartialOrder γ]
{m : Type → Type}
[Monad m]
[(α : Type) → PartialOrder (m α)]
[MonoBind m]
{α : Type}
(f : γ → α → m Bool)
(xs : Array α)
(hmono : monotone f)
:
monotone fun (x : γ) => Array.findM? (f x) xs
theorem
Lean.Order.Array.monotone_findIdxM?
{γ : Type w}
[PartialOrder γ]
{m : Type → Type v}
[Monad m]
[(α : Type) → PartialOrder (m α)]
[MonoBind m]
{α : Type u}
(f : γ → α → m Bool)
(xs : Array α)
(hmono : monotone f)
:
monotone fun (x : γ) => Array.findIdxM? (f x) xs
theorem
Lean.Order.Array.monotone_anyM_loop
{γ : Type w}
[PartialOrder γ]
{m : Type → Type v}
[Monad m]
[(α : Type) → PartialOrder (m α)]
[MonoBind m]
{α : Type u}
(f : γ → α → m Bool)
(xs : Array α)
(stop : Nat)
(h : stop ≤ xs.size)
(j : Nat)
(hmono : monotone f)
:
monotone fun (x : γ) => Array.anyM.loop (f x) xs stop h j
theorem
Lean.Order.Array.monotone_anyM
{γ : Type w}
[PartialOrder γ]
{m : Type → Type v}
[Monad m]
[(α : Type) → PartialOrder (m α)]
[MonoBind m]
{α : Type u}
(f : γ → α → m Bool)
(xs : Array α)
(start stop : Nat)
(hmono : monotone f)
:
monotone fun (x : γ) => Array.anyM (f x) xs start stop
theorem
Lean.Order.Array.monotone_allM
{γ : Type w}
[PartialOrder γ]
{m : Type → Type v}
[Monad m]
[(α : Type) → PartialOrder (m α)]
[MonoBind m]
{α : Type u}
(f : γ → α → m Bool)
(xs : Array α)
(start stop : Nat)
(hmono : monotone f)
:
monotone fun (x : γ) => Array.allM (f x) xs start stop
theorem
Lean.Order.Array.monotone_findSomeRevM?
{m : Type u → Type v}
[Monad m]
[(α : Type u) → PartialOrder (m α)]
[MonoBind m]
{α β : Type u}
{γ : Type w}
[PartialOrder γ]
(f : γ → α → m (Option β))
(xs : Array α)
(hmono : monotone f)
:
monotone fun (x : γ) => Array.findSomeRevM? (f x) xs
theorem
Lean.Order.Array.monotone_findRevM?
{γ : Type w}
[PartialOrder γ]
{m : Type → Type v}
[Monad m]
[(α : Type) → PartialOrder (m α)]
[MonoBind m]
{α : Type}
(f : γ → α → m Bool)
(xs : Array α)
(hmono : monotone f)
:
monotone fun (x : γ) => Array.findRevM? (f x) xs
theorem
Lean.Order.Array.monotone_array_forM
{m : Type u → Type v}
[Monad m]
[(α : Type u) → PartialOrder (m α)]
[MonoBind m]
{α : Type u}
{γ : Type w}
[PartialOrder γ]
(f : γ → α → m PUnit)
(xs : Array α)
(start stop : Nat)
(hmono : monotone f)
:
monotone fun (x : γ) => Array.forM (f x) xs start stop
theorem
Lean.Order.Array.monotone_array_forRevM
{m : Type u → Type v}
[Monad m]
[(α : Type u) → PartialOrder (m α)]
[MonoBind m]
{α : Type u}
{γ : Type w}
[PartialOrder γ]
(f : γ → α → m PUnit)
(xs : Array α)
(start stop : Nat)
(hmono : monotone f)
:
monotone fun (x : γ) => Array.forRevM (f x) xs start stop
theorem
Lean.Order.Array.monotone_flatMapM
{m : Type u → Type v}
[Monad m]
[(α : Type u) → PartialOrder (m α)]
[MonoBind m]
{α β : Type u}
{γ : Type w}
[PartialOrder γ]
(f : γ → α → m (Array β))
(xs : Array α)
(hmono : monotone f)
:
monotone fun (x : γ) => Array.flatMapM (f x) xs
theorem
Lean.Order.Array.monotone_array_filterMapM
{m : Type u → Type v}
[Monad m]
[(α : Type u) → PartialOrder (m α)]
[MonoBind m]
{α β : Type u}
{γ : Type w}
[PartialOrder γ]
(f : γ → α → m (Option β))
(xs : Array α)
(hmono : monotone f)
:
monotone fun (x : γ) => Array.filterMapM (f x) xs