Ssreflect Users Discussion List

[Kazuhiko Sakaguchi <>]

Hello Jake,

This is my implementation of merge sort for lists in MathComp, proved
to be stable, and consumes only O(log n) stack space:
https://github.com/pi8027/efficient-finfun/blob/master/theories/misc/mergesort.v#L446

Best,
Kazuhiko

2019年2月6日(水) 6:41 Jake 
<>:
>
> Hi,
>
> I'm an undergraduate at Princeton working on a project in Coq that requires 
> a theory of stable sorts.
>
> Has anyone seen or done work on stable sorts in the past? The only thing I 
> found was Xavier Leroy's Mergesort proof, but I've found his definition 
> unwieldy in proving things about stable sorts.
>
> I'd like to make use of math-comp, especially the definition of 
> permutations, to formulate an elegant definition of what it means for sorts 
> to be stable, but I'm having trouble using the mathematical components 
> library and ssreflect. Is there anyone who could give me guidance on using 
> the permutations part of the library?
>
> One specific question I have about permutations is: how can I evaluate a 
> permutation in Coq? If I define the permutation (01) in S₃:
>
> Let n := 3.
>
> Program Definition zero : 'I_n := Ordinal (_ : 0 < n).
> Program Definition one  : 'I_n := Ordinal (_ : 1 < n).
> Program Definition two  : 'I_n := Ordinal (_ : 2 < n).
>
> Definition p := tperm zero one.
>
> I can prove things about the action of p:
>
> Goal p zero == one.
> Proof. by case: tpermP. Qed.
>
> Goal p one == zero.
> Proof. by case: tpermP. Qed.
>
> Goal p two == two.
> Proof. by case: tpermP. Qed.
>
> But I can't evaluate it directly like I would a normal Coq function:
>
> Eval compute in ((tperm zero one) zero).
> (*
>      = perm (can_inj (tperm_proof (Ordinal is_true_true) (Ordinal 
> is_true_true)))
>          (Ordinal is_true_true)
>      : ordinal_finType n
>  *)
>
> Thanks,
> Jake Waksbaum