The Coq mailing list

[Laurent Thery <laurent.thery AT inria.fr>]

On 09/21/2011 08:06 PM, Chad E Brown wrote:

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?

You can use Georges Gonthier's trick of using phantom types to introduce extra projections so to trigger
the canonical structures unification.

Applied to your example, this gives

Record PType : Type := mk_PType {
 Pcarrier :> Type;
 Ppoint : Pcarrier
}.

Canonical Structure Prop_ : PType := mk_PType Prop True.

(* The phantom  types *)
Inductive phant (p : Type) := Phant.

(* u and v are there to create the unification problem (Phant (Pcarrier ?)) = Prop *)
Definition Par (A B:PType) (u : phant A) (v : phant B) := mk_PType (A -> B) (fun _ => (Ppoint B)).

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

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

--
Laurent