The Coq mailing list

[Assia Mahboubi <Assia.Mahboubi AT inria.fr>]

Dear Chad,

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

> My current way of working with
> pointed types in Coq is as follows:
> 
> Record PType : Type := mk_PType {
>  Pcarrier :> Type;
>  Ppoint : Pcarrier
> }.

Then the PType record type packages a carrier (accessed through the Pcarrier
constructor) and a point (accesses through the Ppoint projection). Let me 
remove
the coercion for sake of clarity, you are not really using it so far.

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

And I define a canonical structure for Prop the way you did:

Canonical Structure Prop_ : PType := mk_PType Prop True.

As Laurent explained, from now on, the unification algorithm of Coq finds a
canonical solution to the previously unsolvable unification problem (I write
'==' for 'should be unified with')

Pcarrier ? == Prop

by choosing

? == Prop_

Hence Prop is canonically the carrier of a PType, the Prop_ PType.

This corresponds to the:

Prop <- Pcarrier ( Prop_ )

line of the answer of the:

Print Canonical Projections.

command if it is executed after the canonical declaration.

> It's easy to preserve being pointed under function types.

Indeed, given (A B : PType), the type (Pcarrier A) -> (Pcarrier B) is non 
empty
for it contains at least the point (fun _ => Ppoint B). Let's turn this remark
into a canonical construction:

Canonical Structure Par (A : PType)(B : PType) :=
   mk_PType (Pcarrier A -> Pcarrier B) (fun _ => (Ppoint B)).

Now any arrow type between the respective carriers of two arbitrary PTypes can
be canonically seen as the carrier of a PType, built as above. Otherwise said,
when facing a problem of the form:

(Pcarrier ?1) -> (Pcarrier ?2) == Pcarrier ?3

the unification algorithm looks one step further and tries to solve this 
problem
with ?3 == Par ?1 ?2

This corresponds to the:

_ -> _ <- Pcarrier ( Par )

line of the answer of the:

Print Canonical Projections.

command if it is executed after this new canonical declaration.

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

For instance, if we declare:

Variable f : forall P : PType, Pcarrier P -> Prop.
Variable x : Prop -> Prop.

Then the command:

Check (f _ x).

answers:
 f (Par Prop_ Prop_) x : Prop

and your wish is actually granted :).

The trick proposed by Laurent solves a different issue, which is to infer the
PType structure canonically associated to an arrow carrier even when no
unification problem can actually trigger it. This was actually the case in 
your
initial Check query, as it was not featuring any projection of the PType 
record
type.

We can add to the above canonical declarations the helper proposed by Laurent:

Inductive phant (p : Type) := Phant.
Definition Par_of (A B:PType) (u : phant A) (v : phant B) := mk_PType (A -> B)
(fun _ => (Ppoint B)).
Notation "A --> B" := (Par_of _ _ (Phant B) (Phant A)) (at level 70, right
associativity).

This will be required if you encounter situations where this kind of inference
is needed in you goals.
Note that Par_of does need to be a canonical declaration since it is present 
as
such under the --> notation.


A couple of elementary examples of the use canonical structures are described 
in
chapter 5 of "An introduction to small scale reflection in Coq":

http://jfr.cib.unibo.it/article/view/1979

A more complete description of how to program best with this inference 
mechanism
to be read in the ICFP'11 paper of Georges Gonthier, Beta Ziliani, Aleks
Nanevski and Derek Dreyer "How to make ad hoc proof automation less ad hoc", 
see
Beta's page:

http://www.mpi-sws.org/~beta/lessadhoc/

Hope this helps.

assia


> 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_)).
> 

> 
> 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