Ssreflect Users Discussion List

[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