Ssreflect Users Discussion List

[Florent Hivert <>]

      Hi Georges,

> I'd be wary of using vernacular side effects to juggle between alternative
> structures. The alternative used in mathcomp is to define an alias for the
> carrier type to bear the alternative structure, for example R^c for the
> converse ring in ssralg, or baseFieldType L in fieldext for L as a field
> over F in a tower of extensions F : K : L.

I'm note sure what you mean by "alias" ? Considering your divisibility
example, is it just writing something like

Definition nat_div := nat.

Fact div_porder : PartOrder.axiom (fun m n : nat_div => m %| n).
Definition nat_divdMixin := PartOrder.Mixin div_porder.
Canonical nat_divType := Eval hnf in POrdType nat_div nat_divMixin.

Or is it something more tricky involving locking ?

> This way of proceeding lets you specify the structure with a regular type
> cast (or variable type declaration), which I think is more natural. Of
> course you have to be wary of the ambiguity of the displayed terms (which
> omit casts and structure arguments); also, there are performance issues with
> Coq unification in fieldext (probably tied to the complexity of the
> structure, so less likely to affect you).

Actually I realized that I already hit this problem:

Lemma dual_leqX m n : (@leqX_op (dual_pordType T) m n) = (@leqX_op T n m).

Those kind of lemmas are a nightmare to prove because it prints as

   (m <= n) = (n <= m)

with no clue for the actual order.

Thanks for the help,

Florent