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
- [Coq-Club] Grouping several canonical structures in one record - strange effect of Canonical Structure command, Soegtrop, Michael, 01/26/2015
- Re: [Coq-Club] Grouping several canonical structures in one record - strange effect of Canonical Structure command, Enrico Tassi, 01/28/2015
- RE: [Coq-Club] Grouping several canonical structures in one record - strange effect of Canonical Structure command, Soegtrop, Michael, 01/28/2015
- RE: [Coq-Club] Grouping several canonical structures in one record - strange effect of Canonical Structure command, Georges Gonthier, 01/28/2015
- RE: [Coq-Club] Grouping several canonical structures in one record - strange effect of Canonical Structure command, Soegtrop, Michael, 01/28/2015
- Re: [Coq-Club] Grouping several canonical structures in one record - strange effect of Canonical Structure command, Enrico Tassi, 01/28/2015
Archive powered by MHonArc 2.6.18.