Ssreflect Users Discussion List

[Georges Gonthier <>]

 Dear Florent,

 You are in trouble because your definition of dual aliases a pordType rather 
than a type.
You want to have
   Definition dual T : Type := T.
  Variable T : pordType.
  (* Theory for the dual T type *)

What happens in the code below is that you define structures for 
PartOrder.sort (dual T), which will never be used because type inference 
would only look them up to resolve unification problems of the form
    PartOrder.sort ?this =?= PartOrder.sort  ?that
For which it will always try to unify ?this ?=? ?that instead...

You won't have that issue if you define dual as a Record, but it's still best 
to make the T parameter a Type rather than a pordType, so that you can write 
dual nat rather than dual nat_pordType. This will prevent you from making 
dual_val a Coercion, which would only be useful in the development of the 
generic theory, though.

 Finally, in the specific case of dual you might want "(x : dual T) <= y" to 
simplify to "y <= x", to limit some of the confusion you experienced; this 
can be done by flagging an extra argument to pordType with the ! annotation 
in an Arguments command... although you will have to declare that argument 
all over the generic order theory.

-----Original Message-----
From: Florent Hivert 
[mailto:]
 
Sent: 09 May 2016 19:03
To: Georges Gonthier 
<>
Cc: 

Subject: Re: [ssreflect] Canonical Structure not so canonical

      Dear Georges,

On Mon, May 09, 2016 at 05:05:45PM +0000, Georges Gonthier wrote:
> That was indeed just what I meant: a transparent definition, which 
> lets you silently convert values from the carrier to its alias.

I'm having trouble with this approach. The following works:

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

Then, as expected:

   Eval compute in ((3 : nat_div) <= (5 : nat_div)). (* = false *)
   Eval compute in (3 <= 5).  (* = true *)

However, if I write:

   Variable T : pordType.
   Definition dual := T.
   Definition dual_comp := (fun x y : dual => (y : T) <= (x : T)).
   Fact geqX_order : PartOrder.axiom dual_comp.
   [...]
   Definition dual_pordMixin := PartOrder.Mixin geqX_order.
   Canonical dual_pordType := Eval hnf in POrdType dual dual_pordMixin.

Then I can write prove:

   Lemma dual_leqX m n : (@leqX_op dual_pordType m n) = (@leqX_op T n m).
   Proof using . by rewrite leqXE /=. Qed.

However, the cast trick doesn't work:

   Lemma dual_leqX_cast (m n : T) : ((m : dual) <= (n : dual)) = (n <= m).
   Proof using . rewrite /dual !leqXE /=. Qed.

   T : pordType
   i, j : dual
   ============================
    PartOrder.r (PartOrder.mixin (PartOrder.class T)) m n =
    PartOrder.r (PartOrder.mixin (PartOrder.class T)) n m

Note that "m <= n" is a notation for "leqX_op m n". Do you have any idea what 
can go wrong ? I don't see any difference.

> If you don't need or want the silent conversion, then cloning the type 
> (using a unary inductive) will give you more stability, though.

You mean something such as the following ?

    Record dual (T : pordType) := Dual { dual_val :> T }.

Cheers,

Florent