The Coq mailing list

["D. Ben Knoble" <ben.knoble AT gmail.com>]

> This is where things start going wrong. There's a merge-sort provided in the
> standard theories, but it gets its type parameter as a module parameter. To 
> my
> understanding, there's no way to use it polymorphically to sort list (nat * 
> A)
> or anything similar. Is that right? Is there a mechanism I haven't thought 
> of?

Did you see the example in
https://coq.inria.fr/distrib/current/stdlib/Coq.Sorting.Mergesort.html
?

```
Module NatOrder <: TotalLeBool.
  Definition t := nat.
  Fixpoint leb x y :=
    match x, y with
    | 0, _ => true
    | _, 0 => false
    | S x', S y' => leb x' y'
    end.
  Infix "<=?" := leb (at level 70, no associativity).
  Theorem leb_total : forall a1 a2, a1 <=? a2 \/ a2 <=? a1.
End NatOrder.

Module Import NatSort := Sort NatOrder.

Example SimpleMergeExample := Eval compute in sort [5;3;6;1;8;6;0].
```

I'm sure it would be possible to do something like this (I did just now):

```
Require Import Equalities Orders Mergesort List.
Import ListNotations.

Theorem leb_total x y: Nat.leb x y = true \/ Nat.leb y x = true.
Proof.
  generalize dependent y.
  induction x; intros y; try easy; destruct y; simpl; auto.
Qed.

Module NatAOrder (A: Typ) <: TotalLeBool.
  Definition t: Type := nat * A.t.
  Definition leb (x y: t) := Nat.leb (fst x) (fst y).
  Infix "<=?" := leb (at level 70, no associativity).
  Theorem leb_total x y: x <=? y = true \/ y <=? x = true.
  Proof.
    destruct x; destruct y; simpl; apply leb_total.
  Qed.
End NatAOrder.

Module NatNatOrder := NatAOrder Nat.
Module NatNatSort := Sort NatNatOrder.

Eval compute in NatNatSort.sort [(2,10); (5,3); (1,7)].
```

We have to use a functor `NatAOrder`, and to instantiate it you need a
module `A` that defines a type `t`.

(Obviously it would be much simpler if `MergeSort` took its types more
like a section `Variable`; see _e.g._ Lists.List. I think the
`leb_order` could then be a section `Axiom` or similar.)