The Coq mailing list

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

Dear Coq Users,

 

I try to put several canonical structures, e.g. equality, choice, countable and finite plus the required collateral, into a record, so that I can discharge all structure at once with a single ltac script. But somehow I cannot manage to make use of the structures defined in a record with a canonical structure command. See e.g. the below sample (modified from the manual). I don’t understand why the canonical projections involve the projection functions of the structure (like msCarrier) rather than the contents of the structure (like nat). Eval compute in nat_setoid results in the right thing.

 

Thanks & best regards,

 

Michael

 

P.S.: I am still at 8.4pl5, but I am working on switching to 8.5

 

(*********** Example Code ***********)

 

Require Import Relations.

Require Import EqNat.

 

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.

 

Print Canonical Projections.

 

(* Results in

msEqualIsEquiv <- sEqualIsEquiv ( nat_setoid )

msEqual <- sEqual ( nat_setoid )

msCarrier <- sCarrier ( nat_setoid )

*)