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 function 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 appearance 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) : monotone fun (x : γ) => g <$> f x

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 α)] {α β : 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 γ] [LawfulMonad m] (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) : monotone fun (x : γ) => o.getDM (y x)

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) : monotone fun (x : γ) => List.mapM (f x) xs

theorem Lean.Order.List.monotone_forM {m : Type u → Type v} [Monad m] [(α : Type u) → PartialOrder (m α)] [MonoBind m] {α : Type u} {γ : Type w} [PartialOrder γ] (f : γ → α → m PUnit) (xs : List α) (hmono : monotone f) : monotone fun (x : γ) => xs.forM (f x)

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_anyM {γ : 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.anyM (f x) xs

theorem Lean.Order.List.monotone_allM {γ : 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.allM (f x) 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) : monotone fun (x : γ) => forIn' as init (f x)

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) : monotone fun (x : γ) => forIn as init (f x)

theorem Lean.Order.Array.monotone_modifyM {m : Type u → Type v} [Monad m] [(α : Type u) → PartialOrder (m α)] [MonoBind m] {α : Type u} {γ : Type w} [PartialOrder γ] (a : Array α) (i : Nat) (f : γ → α → m α) (hmono : monotone f) : monotone fun (x : γ) => a.modifyM i (f x)

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) : monotone fun (x : γ) => forIn' as init (f x)

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) : monotone fun (x : γ) => forIn as init (f x)

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