The Coq mailing list

[Chad E Brown <cebrown2323 AT yahoo.com>]

Thanks. I misunderstood how Canonical Structures are used.

I'm trying to work with pointed types (nonempty types with a 'default' element).

It's easy to preserve being pointed under function types. My current way of working with

pointed types in Coq is as follows:

Record PType : Type := mk_PType {

 Pcarrier :> Type;

 Ppoint : Pcarrier

}.

Definition Prop_ : PType := mk_PType Prop True.

Definition Par (A B:PType) := mk_PType (A -> B) (fun _ => (Ppoint B)).

Notation "A --> B" := (Par A B) (at level 70, right associativity).

Check (fun p:PType -> Prop => p ((Prop_ --> Prop_) --> Prop_)).

I'm OK with this solution, but I'd rather write "Prop" instead of "Prop_" and "->" instead of "-->".

Can anyone suggest an alternative?

- Chad

---

From: Laurent Th�ry <Laurent.Thery AT inria.fr>
To: Chad E Brown <cebrown2323 AT yahoo.com>
Cc: "coq-club AT inria.fr" <coq-club AT inria.fr>
Sent: Wednesday, September 21, 2011 6:05 PM
Subject: Re: [Coq-Club] Canonical Structures

On 09/21/2011 05:31 PM, Chad E Brown wrote:

I'm having trouble getting an easy canonical structure to work as I expect. The final Check below doesn't work.

Could someone please let me know what I'm doing wrong, or point me to an appropriate link.

Structure PType : Type := mk_PType {

 Pcarrier :> Type;

 Ppoint : Pcarrier

}.

Canonical Structure Prop_ : PType := mk_PType Prop True.

Check (fun p:PType -> Prop => p Prop).

- Thanks, Chad

The inference of canonical structure only works for projections. You can see this with the command

Print Canonical Projections.

that gives:

True <- Ppoint ( Prop_ )
Prop <- Pcarrier ( Prop_ )


This means that during the unification process, if it has True and expects and Ppoint ?,
it will be able to guess that ? is Prop_.
Only the projections (Ppoint and Pcarrier) trigger this inference.
In your example, you just ask to  unify  Prop to PType which just fails
--
Laurent