The Coq mailing list

[AUGER <Cedric.Auger AT lri.fr>]

Le Wed, 28 Apr 2010 16:18:17 +0200, Loic Pottier
<loic.pottier AT sophia.inria.fr>
 a écrit:

> Hi,
> I have the following problem with universes and type classes (?):
>
> Class Qs(E :Type)(F:Type)(P:E ->Prop)(A:F):= {qsprop: Prop}.
> Notation "'for_all' x 'in' A , P " :=
>    (@qsprop _ _ (fun x => P) A _) (right associativity, at level 200, x  
> ident).
>
> Instance qsprop1(E:Type)(P:E ->Prop):Qs E _ P E:= {qsprop := forall x:E,  
> P x}.
>
> Definition empty{E:Type} := fun x:E => False.

> Goal for_all E in Type, for_all x in E, not (empty x).
> intro E.
> intro x.
> intro.
> apply H.
> Qed.
> Error: Universe inconsistency.
>
> but with (@empty E x), it works!
>
> Loïc

Strange specification...

I rather have defined:
Definition empty(E:Type) := E -> False.

and then tried to show: for_all E in Type, for_all x in E, not (empty E)
or for_all E in Type, E -> not (empty E).

That said, I have not your problem on the coqide|trunk12911:

Error:
Unable to satisfy the following constraints:
EVARS:
   ?91==[ |- Qs ?85 Type (fun E : ?85 => for_all x in E, ~ empty x) Type]
   ?90==[E |- Qs ?87 ?88 (fun x : ?87 => ~ empty x) E]
   ?89==[E x |- Type]
   ?88==[E |- Type]
   ?87==[E |- Type]
   ?85==[ |- Type]

occurs at "Goal" level and (@empty E x) makes it work.

Your Notation is quite complex:


Class Qs(E :Type)(F:Type)(P:E ->Prop)(A:F):= {qsprop: Prop}.
Notation "'for_all' x 'in' A , P " :=
    (@qsprop _1 _2 (fun x => P) A _3) (right associativity, at level 200, x
ident).

"for_all x in A, P"
means that:
x is of type _1 (and not necessarily A) (but is a binder under a lambda)
A is of type _2
P is of type Prop
and we have an implicit argument _3 of type Qs _1 _2 (fun _ : _1 => P) A

when you write this, you give A, so we know _2, but you cannot give x,
nor _3, so you cannot infer _1.

By defining Instance qsprop1,
You make qsprop1 a default for _3,
so now by default, A is unified with _1, so now

you force the fact that x is of type A in a very complicate way...

Does
"
Variable T2: Type.
Variable A: T2.
Variable P: Prop.

Check (for_all x in A, P).
"
work well?
(It doesn't work in my trunk)

Did you meant to make some variant of JMeq?

Record is not good for dependant types AFAIK;
for instance, "eq" has a single constructor,
but I don't know how to convert it into a Record,
due to the fact that the constructor of a Record cannot be type casted
(or rather, I don't know if it is possible).


Rewriting it a little like in the kernel would then give:


Inductive Qs(E :Type)(P:E ->Prop): forall F, F -> Type :=
Build_Qs : forall (qsprop:Prop), Qs E P Type E.

(* redefinition of projection *)
Definition qsprop {E P F f} (qs: Qs E P F f) :=
let (q) := qs in q.

(* unsuccessful tentative of instanciation *)
Section canon.
Variable E: Type.
Variable P: E -> Prop.
Definition qsprop1 :Qs E P _ E:=
   @Build_Qs E P (forall x:E, P x).
(* Canonical Structure doesn't work here :( *)
End canon.

(* so we have to give explicitely our instance,
instead of letting it infered *)
Notation "'for_all' x 'in' A , P " :=
    (@qsprop _ (fun x => P) _ A (qsprop1 _ _))
   (right associativity, at level 200, x ident).

(* what follows has no more problem! *)

Definition empty{E:Type} := fun x:E => False.

Goal for_all E in Type, for_all x in E, not (empty x).
intro E.
intro x.
intro.
apply H.
Qed.






--
Cédric AUGER

Univ Paris-Sud, Laboratoire LRI, UMR 8623, F-91405, Orsay