Documentation

Cslib.Algorithms.Lean.Sort.Merge

A Monadic version of the builtin List.mergeSort #

This can be instantiated with Id to recover the original, or with TimeM or FreeM for algorithmic analysis.

source
@[irreducible]
def List.mergeM {m : Type → Type u_1} [Monad m] {α : Type} (xs ys : List α) (le : α → α → m Bool) :
m (List α)

A monadic version of List.merge

Equations
Instances For
    source
    @[simp]
    theorem List.nil_mergeM {m : Type → Type u_1} [Monad m] {α : Type} (ys : List α) (le : α → α → m Bool) :
    [].mergeM ys le = pure ys
    source
    @[simp]
    theorem List.mergeM_right {m : Type → Type u_1} [Monad m] {α : Type} (xs : List α) (le : α → α → m Bool) :
    xs.mergeM [] le = pure xs
    source
    @[simp]
    theorem List.cons_mergeM_cons {m : Type → Type u_1} [Monad m] {α : Type} (x y : α) (xs ys : List α) (le : α → α → m Bool) :
    (x :: xs).mergeM (y :: ys) le = do let __do_lift ← le x y if __do_lift = true then do let __do_lift ← xs.mergeM (y :: ys) le pure (x :: __do_lift) else do let __do_lift ← (x :: xs).mergeM ys le pure (y :: __do_lift)
    source
    @[simp]
    theorem List.mergeM_pure {m : Type → Type u_1} [Monad m] {α : Type} [LawfulMonad m] (xs ys : List α) (le : α → α → Bool) :
    (xs.mergeM ys fun (x y : α) => pure (le x y)) = pure (xs.merge ys le)
    source
    @[simp]
    theorem List.idRun_mergeM {α : Type} (xs ys : List α) (le : α → α → Id Bool) :
    (xs.mergeM ys le).run = xs.merge ys fun (x y : α) => (le x y).run
    source
    theorem Cslib.IsMonadHom.map_listMergeM {m : Type → Type u_1} {n : Type → Type u_2} [Monad m] [Monad n] {α : Type} {f : {β : Type} → m β → n β} (hf : IsMonadHom m n fun {α : Type} => f) (xs ys : List α) (le : α → α → m Bool) :
    f (xs.mergeM ys le) = xs.mergeM ys fun (x y : α) => f (le x y)
    source
    @[irreducible]
    def List.mergeSortM {m : Type → Type u_1} [Monad m] {α : Type} (xs : List α) (le : α → α → m Bool) :
    m (List α)

    A monadic version of List.mergeSortM

    Equations
    Instances For
      source
      @[simp]
      theorem List.mergeSortM_nil {m : Type → Type u_1} [Monad m] {α : Type} (le : α → α → m Bool) :
      [].mergeSortM le = pure []
      source
      @[simp]
      theorem List.mergeSortM_singleton {m : Type → Type u_1} [Monad m] {α : Type} (a : α) (le : α → α → m Bool) :
      [a].mergeSortM le = pure [a]
      source
      @[simp]
      theorem List.mergeSortM_pure {m : Type → Type u_1} [Monad m] {α : Type} [LawfulMonad m] (xs : List α) (le : α → α → Bool) :
      (xs.mergeSortM fun (x y : α) => pure (le x y)) = pure (xs.mergeSort le)
      source
      @[simp]
      theorem List.idRun_mergeSortM {α : Type} (xs : List α) (le : α → α → Id Bool) :
      (xs.mergeSortM le).run = xs.mergeSort fun (x y : α) => (le x y).run
      source
      theorem Cslib.IsMonadHom.map_listMergeSortM {m : Type → Type u_1} {n : Type → Type u_2} [Monad m] [Monad n] {α : Type} {f : {β : Type} → m β → n β} (hf : IsMonadHom m n fun {α : Type} => f) (xs : List α) (le : α → α → m Bool) :
      f (xs.mergeSortM le) = xs.mergeSortM fun (x y : α) => f (le x y)