The Coq mailing list

[Georges Gonthier <gonthier AT microsoft.com>]

  The system is indeed justified in complaining. Canonical structures let Coq 
infer records from projection equations arising from type-checking.
As the Print Canonical Projection diagnosis indicates, your CS declaration 
tells Coq that it can resolve the equation
   uu1.pr21 ?hP == A -> B
by setting hP := isapropimpl_hprop X Y
   provided X and Y are respectively solutions of
  uu1.pr21 X == A and uu1.pr21 Y = B
(I'm guessing that you've declared uu1.pr21 a Coercion so it isn't usually 
printed, but I'll put it explicitly for the sake of clarity).

Now your redefined /\ operator expects arguments of type hProp, but uu1.pr21 
A -> uu1.pr21 B has type Type, and isapropimpl_hprop says nothing about 
solving the equation hProp == Type (fortunately!).
  In short, CS resolve structures based on types. To resolve a structure on 
the basis of a value, the value must be lifted to the type level, using for 
example the phantom type pattern (see (2) below).
(1) The very first file of the ssreflect library supplies boilerplate for 
this: it lets you write
   Definition iff (A B : hProp) := [the hProp of A -> B] /\  [the hProp of B 
-> A].
with the  /\ operator defined as it is now.
 (2) You could also redefine the /\ notation so that it stands for
   hprop_and_for (Phant A) (Phant B)
where hprop_and_for (A B : hProp) of phant (uu1.pr21 A) & phant (uu1.pr21 B) 
:= hprop_and A B.
(in which hprop_and is your old /\)
(3) Even more simply, you could bind a notation scope to hProp, and overload 
the -> operator in that scope to mean isapropimpl_hprop (you've probably 
already done this for /\).
   In practice all three techniques are useful, and the ssreflect library 
uses each of them where appropriate.

I hope this will help,
  Georges

-----Original Message-----
From: Vladimir Voevodsky 
[mailto:vladimir AT ias.edu]
 
Sent: 22 May 2011 19:20
To: Coq-Club Club
Subject: [Coq-Club] canonical structures

I have some trouble with canonical structures. In one file I have:

Definition isapropimpl_hprop ( X Y : hProp ) : hProp := hProppair ( X -> Y ) 
( isapropimpl X Y (uu1.pr22 _ _ Y) ) .
Canonical Structure isapropimpl_hprop.


which is accepted.

In another one which imports the first I have:


Definition iff (A B: hProp) :=  ( A -> B ) /\ ( B -> A ) .

where /\ has been re-defined for hProp.  

The system complains:

Toplevel input, characters 64-70:
Error: In environment
A : hProp
B : hProp
The term "A -> B" has type "Type" while it is expected to have type "hProp".


When I check things by Print Canonical Projections it shows me :

_ -> _ <- uu1.pr21 ( isapropimpl_hprop ) 

What's wrong here?

Vladimir.