Skip to Content.
Sympa Menu

coq-club - RE: [Coq-Club] Grouping several canonical structures in one record - strange effect of Canonical Structure command

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

RE: [Coq-Club] Grouping several canonical structures in one record - strange effect of Canonical Structure command


Chronological Thread 
  • From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
  • To: "coq-club AT inria.fr" <coq-club AT inria.fr>
  • Subject: RE: [Coq-Club] Grouping several canonical structures in one record - strange effect of Canonical Structure command
  • Date: Wed, 28 Jan 2015 10:26:28 +0000
  • Accept-language: de-DE, en-US

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



Archive powered by MHonArc 2.6.18.

Top of Page