feat: add monad-polymorphic sorts

[eric-wieser]

These can be used to:

• replace the specialized timeM version (included in this PR)
• implement sorts that log as they sort
• specialize to FreeM or PFunctor.FreeM

The old copyright dates on these files are because they were written by directly copying the corresponding non-monadic code from mathlib / lean core.

As a general pattern, writing code monad generically, then specializing it, allows Lean's compiler to compile it efficiently in Id, but also allows it to be reasoned about for richer monads m. The alternative of starting with a rich monad like FreeM and transporting back to Id has two downsides:

• The algorithm itself must live inside CSLib, in order to have access to FreeM.
• The compiler must be able to fully optimize out FreeM.liftM / TimeM.ret to match performance characteristics.

If you have no intent of ever executing the code then these concerns don't matter all that much. For now, the main benefit to CSLib is that we can write the algorithms just once while exploring a zoo of computation models to evaluate them in.

As a bonus, this lets us reuse some proofs about List.mergeSort, reducing the length of some proofs.

[kim-em]

I think if you put @[expose] here you can avoid an import all in the later file. Not sure it's an improvement.

[eric-wieser]

Yeah, I wasn't sure about this either.

[kim-em]

Maybe

@[simp] theorem cons_mergeM_cons (x y : α) (xs ys : List α) (le : α → α → m Bool) :
    mergeM (x :: xs) (y :: ys) le = do
      if ← le x y then return x :: (← mergeM xs (y :: ys) le)
      else return y :: (← mergeM (x :: xs) ys le) := by
  simp [mergeM]

@[simp] theorem mergeSortM_nil (le : α → α → m Bool) : mergeSortM [] le = pure [] := by
  simp [mergeSortM]
@[simp] theorem mergeSortM_singleton (a : α) (le : α → α → m Bool) :
    mergeSortM [a] le = pure [a] := by
  simp [mergeSortM]

too?

[eric-wieser]

I thought the point of @[simp] def on pattern-matching defs was that we could skip writing these. Is that not the case?

[kim-em]

Indeed, as long as it is @[expose]'d. I think I (and the AIs!) write out all the simp lemmas out of habit. Somehow often enough you want to tweak the lemma that it still feels worthwhile to me to have them.

In particular mergeSortM (a :: b :: xs) le does warrant custom lemmas.

I'm happy either way here, no further comment. :-)

[kim-em]

Maybe

@[simp] theorem orderedInsertM_nil (a : α) : orderedInsertM r a [] = pure [a] := rfl
@[simp] theorem orderedInsertM_cons (a b : α) (l : List α) :
    orderedInsertM r a (b :: l) = do
      if ← r a b then return a :: b :: l else return b :: (← orderedInsertM r a l) := rfl
@[simp] theorem insertionSortM_nil : insertionSortM r [] = pure [] := rfl
@[simp] theorem insertionSortM_cons (b : α) (l : List α) :
    insertionSortM r (b :: l) = (do orderedInsertM r b (← insertionSortM r l)) := rfl

too?

[eric-wieser]

I think the second ones are already covered by simp on insertionSortM? Should I put simp on insertionSort too, for the same reason?

[kim-em]

As above.

[kim-em]

These could be proved in terms of a

variable {n} [Monad n]

theorem mergeM_hom (φ : {β : Type} → m β → n β)
    (hpure : ∀ {β} (b : β), φ (pure b) = pure b)
    (hbind : ∀ {β γ} (x : m β) (f : β → m γ), φ (x >>= f) = φ x >>= fun b => φ (f b))
    (xs ys : List α) (le : α → α → m Bool) :
    φ (mergeM xs ys le) = mergeM xs ys (fun x y => φ (le x y)) := by
  fun_induction mergeM xs ys le with
  | case1 | case2 => simp [hpure]
  | case3 x xs y ys ih1 ih2 =>
    simp only [mergeM, hbind]
    congr 1; funext b
    split <;> simp only [map_eq_pure_bind, hbind, hpure, ih1, ih2]

theorem mergeSortM_hom (φ : {β : Type} → m β → n β)
    (hpure : ∀ {β} (b : β), φ (pure b) = pure b)
    (hbind : ∀ {β γ} (x : m β) (f : β → m γ), φ (x >>= f) = φ x >>= fun b => φ (f b))
    (xs : List α) (le : α → α → m Bool) :
    φ (mergeSortM xs le) = mergeSortM xs (fun x y => φ (le x y)) := by
  fun_induction mergeSortM xs le with
  | case1 | case2 => simp [mergeSortM, hpure]
  | case3 a b xs le lr _ _ ih1 ih2 =>
    simp only [mergeSortM, hbind, ih1, ih2, mergeM_hom φ hpure hbind]
    rfl

and similarly for insertion sort. Not sure it is worth it.

[eric-wieser]

This is of course the motivation for #856. Once once lands, I'll add this result to the other.

[kim-em]

Looks good to me. Happy if this is merged, however Eric wants to handle the remaining @[simp] lemma questions.