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. :-)

[eric-wieser]

I've added your suggestions.

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

I assume you are not asking for these? I think probably stating anything interesting requires using wp on the comparator, which I intend to declare out of scope for this PR.

[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.

[eric-wieser]

Let's put these in #856, which will allow me to test the grind annotations.

[kim-em]

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