Ssreflect Users Discussion List

[Georges Gonthier <>]

  That was indeed just what I meant: a transparent definition, which lets you 
silently convert values from the carrier to its alias. If you don't need or 
want the silent conversion, then cloning the type (using a unary inductive) 
will give you more stability, though.
     Georges
(btw: this is now a private thread.)

-----Original Message-----
From: Florent Hivert 
[mailto:]
 
Sent: 09 May 2016 17:56
To: Georges Gonthier 
<>
Subject: Re: [ssreflect] Canonical Structure not so canonical

      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