The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Enrico,

what I want to achieve is to define several canonical structures (e.g. 
ssreflect equality, choice, countable, finite) in one record, so that I can 
discharge all of them with a single tactic script. This is just an exercise 
to make things a bit more convenient. I have a tactic script which does this 
for the types I am interested in, but I am not able to extract the structures 
from the record in a way which is suitable for Canonical Structure.

Naively I thought that 

Canonical Structure nat_setoid := Build_Setoid nat eq_nat eq_nat_equiv.

and

Canonical Structure nat_setoid := msSetoid multistruct_nat.

have the same effect, because the right hand side of both evaluates to the 
same term. The second one just accesses a setoid structure which is defines 
inside of the record in the same way as in the first line. But the first one 
works (defines a setoid structure for nat) while the second doesn't work.

Best regards,

Michael

-----Original Message-----
From: 
coq-club-request AT inria.fr
 
[mailto:coq-club-request AT inria.fr]
 On Behalf Of Enrico Tassi
Sent: Wednesday, January 28, 2015 10:38 AM
To: 
coq-club AT inria.fr
Subject: Re: [Coq-Club] Grouping several canonical structures in one record - 
strange effect of Canonical Structure command

On Mon, Jan 26, 2015 at 03:27:07PM +0000, Soegtrop, Michael wrote:
> Structure Setoid : Type :=
> {
>   sCarrier      :> Set;
>   sEqual        : relation sCarrier;
>   sEqualIsEquiv : equivalence sCarrier sEqual }.
> 
> Record MultiStruct : Type :=
> {
> msCarrier      : Set;
>   msEqual        : relation msCarrier;
>   msEqualIsEquiv : equivalence msCarrier msEqual;
>   msSetoid       := Build_Setoid msCarrier msEqual msEqualIsEquiv
> }.
> 
> Axiom eq_nat_equiv : equivalence nat eq_nat.
> Definition multistruct_nat := Build_MultiStruct nat eq_nat eq_nat_equiv.
> 
> Canonical Structure nat_setoid := msSetoid multistruct_nat.
> 
> msCarrier <- sCarrier ( nat_setoid )

This print is misleading because it only prints the head constant of the 
value on the left.  The hint you are adding is:

  ?Y   ===   multi_struct_nat
  ?X   ===   nat_setoid
 -----------------------------------
  sCarrier ?X   ===   msCarrier ?Y

To test it:

Fail Check (refl_equal _ : sCarrier _ = nat).
Check (refl_equal _ : sCarrier _ = msCarrier _).

Also "Print msSetoid" tells you why this is the case:

 msSetoid = fun m : MultiStruct =>
   Build_Setoid (msCarrier m) (msEqual m) (msEqualIsEquiv m)

This way you see eactly the values of the fields of the record instance you 
are declaring as canonical.  Its sCarrier component is (msCarrier m) for the 
m you passed to it, here multi_struct_nat.

Not sure what you are trying to achieve, but the hint you declare does not 
make much sense to me.

Hope it helps,
--
Enrico Tassi