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: Georges Gonthier <gonthier AT microsoft.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:36:17 +0000
  • Accept-language: en-GB, en-US
  • Authentication-results: spf=pass (sender IP is 206.191.248.244) smtp.mailfrom=gonthier AT microsoft.com; inria.fr; dkim=none (message not signed) header.d=none;inria.fr; dmarc=pass action=none header.from=microsoft.com;

I think I understand what you are trying to achieve, and why it doesn't
work.
Canonical declarations work by giving hints to the unification engine: the
declaration
Canonical Structure nat_setoid := {|sCarrier = nat; sEqual = eq_nat;
sEqualsEquiv = eq_nat_equiv|}.
adds (amongst others) the rule nat <- sCarrier (nat_setoid), which the lets
it solve unification problems of the form
sCarrier ?33 =~= nat
with ?33 := nat_setoid. To form this rule Coq need to peek inside the
definition of nat_setoid, find an explicit record construction, pull out the
expressions for the fields with named projectors (here, sCarrier) that are
either constant or the application of a constant (plus a handful of special
cases).
Each such field yields a rule that matches problems of the form projector _
... _ =~= constant _ ... _. The matching is SYNTACTIC, so Coq never tries to
evaluate the field value, since this would nearly always destroy head
constants. However, Coq will try to reduce the Canonical structure in order
to expose an explicit record constructor, but using HEAD call-by-name
reduction ONLY.
In your case this means that the sCarrier field vaulue msCarrier
multi_struct_nat is never reduced to nat, hence Coq does not register the
hint you intended. The solution is to write msCarrier more carefully, and
ensure that you only construct the fields you intend. You can do this here by
using match rather than projectors to get at the MultiStruct fields:
Definition msCarrier m := let 'Build_MultiStruct T e EQ_e := m in
Build_Setoid T e EQ_e.
This way, head evaluation has to reduce the let in order to expose
Build_Setoid. You can use type inference and unification to extract fields;
this is somewhat more flexible in dealing with intricate dependent types and
multiple inheritance. The idiom for doing that is described at the end of the
new chapter on canonical structures in the 8.5beta manual.
Cheers,
Georges

-----Original Message-----
From:
coq-club-request AT inria.fr

[mailto:coq-club-request AT inria.fr]
On Behalf Of Enrico Tassi
Sent: 28 January 2015 09:38
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