A Monadic version of Mathlib's List.insertionSort

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

def List.orderedInsertM {α : Type} {m : Type → Type u_1} [Monad m] (r : α → α → m Bool) (a : α) : List α → m (List α)

A monadic version of List.orderedInsert.

Equations

• List.orderedInsertM r a [] = pure [a]
• List.orderedInsertM r a (b :: l) = do let __do_lift ← r a b if __do_lift = true then pure (a :: b :: l) else do let __do_lift ← List.orderedInsertM r a l pure (b :: __do_lift)

@[simp]

theorem List.orderedInsertM_nil {α : Type} {m : Type → Type u_1} [Monad m] (r : α → α → m Bool) (a : α) : orderedInsertM r a [] = pure [a]

@[simp]

theorem List.orderedInsertM_cons {α : Type} {m : Type → Type u_1} [Monad m] (r : α → α → m Bool) (a b : α) (l : List α) : orderedInsertM r a (b :: l) = do let __do_lift ← r a b if __do_lift = true then pure (a :: b :: l) else do let __do_lift ← orderedInsertM r a l pure (b :: __do_lift)

@[simp]

theorem List.orderedInsertM_pure {α : Type} {m : Type → Type u_1} [Monad m] [LawfulMonad m] (r : α → α → Bool) (a : α) (xs : List α) : orderedInsertM (fun (x y : α) => pure (r x y)) a xs = pure (orderedInsert (fun (x1 x2 : α) => r x1 x2 = true) a xs)

@[simp]

theorem List.idRun_orderedInsertM {α : Type} (r : α → α → Id Bool) (a : α) (xs : List α) : (orderedInsertM r a xs).run = orderedInsert (fun (x y : α) => (r x y).run = true) a xs

theorem Cslib.IsMonadHom.map_orderedInsertM {α : Type} {m : Type → Type u_1} {n : Type → Type u_2} [Monad m] [Monad n] {f : {β : Type} → m β → n β} (hf : IsMonadHom m n fun {α : Type} => f) (r : α → α → m Bool) (a : α) (xs : List α) : f (List.orderedInsertM r a xs) = List.orderedInsertM (fun (x y : α) => f (r x y)) a xs

def List.insertionSortM {α : Type} {m : Type → Type u_1} [Monad m] (r : α → α → m Bool) : List α → m (List α)

A monadic version of List.insertionSort.

Equations

• List.insertionSortM r [] = pure []
• List.insertionSortM r (b :: l) = do let __do_lift ← List.insertionSortM r l List.orderedInsertM r b __do_lift

@[simp]

theorem List.insertionSortM_nil {α : Type} {m : Type → Type u_1} [Monad m] (r : α → α → m Bool) : insertionSortM r [] = pure []

@[simp]

theorem List.insertionSortM_cons {α : Type} {m : Type → Type u_1} [Monad m] (r : α → α → m Bool) (b : α) (l : List α) : insertionSortM r (b :: l) = do let __do_lift ← insertionSortM r l orderedInsertM r b __do_lift

@[simp]

theorem List.insertionSortM_pure {α : Type} {m : Type → Type u_1} [Monad m] [LawfulMonad m] (xs : List α) (r : α → α → Bool) : insertionSortM (fun (x y : α) => pure (r x y)) xs = pure (insertionSort (fun (x1 x2 : α) => r x1 x2 = true) xs)

@[simp]

theorem List.idRun_insertionSortM {α : Type} (xs : List α) (r : α → α → Id Bool) : (insertionSortM r xs).run = insertionSort (fun (x y : α) => (r x y).run = true) xs

theorem Cslib.IsMonadHom.map_listInsertionSortM {α : Type} {m : Type → Type u_1} {n : Type → Type u_2} [Monad m] [Monad n] {f : {β : Type} → m β → n β} (hf : IsMonadHom m n fun {α : Type} => f) (r : α → α → m Bool) (xs : List α) : f (List.insertionSortM r xs) = List.insertionSortM (fun (x y : α) => f (r x y)) xs