The Coq mailing list

[Randy Pollack <rpollack0 AT gmail.com>]

Hi Matthieu,

First: is there any document that explains eta in Coq?

Now I will try again to explain what I don't understand.  I will do
this in LEGO, where we can write explicit universe numbers as well as
ambiguous Types.

We both agree that in my K example, there is no universe polymorphism
(as K is _declared_ rather than defined).

[T = Type(3)];      (* Fix a Type level *)
[J : {t:T} t -> t];    (* declare J *)
J ({t:Type(2)} t -> t) ([t:Type]J t);    (* typecheck *)

This is accepted, as in Coq, BUT, why is this last subterm a correct
eta expansion of J?  It seems to me that "Type" in ([t:Type]J t)
should not be a fresh Type (with an unconstrained Type level), but
should be "T".

J ({t:Type(2)} t -> t) ([t:T]J t);

LEGO rejects this.  Coq accepts this by doing another eta expansion,
creating a fresh Type instance.

Definition T := Type. (* Fix a level *)
Print T.
     T = Type (* Top.1 *)
          : Type (* (Top.1)+1 *)

Definition KK := K (forall t:Type, t -> t) (K:forall t:T, t -> t).
KK =
K (forall t : Type (* Top.3 *), t -> t)
  (fun t : Type (* Top.3 *) => (K:forall t0 : T, t0 -> t0) t)
     : forall t : Type (* Top.3 *), t -> t

With the only constraint Top.3 < Top.1.  Is it "clearly" safe for eta
expansion to create a fresh type instance?

Best
--Randy

On Wed, Sep 10, 2014 at 2:49 AM, Matthieu Sozeau
<matthieu.sozeau AT inria.fr>
 wrote:
> Hi Randy,
>
>   I think you’re just experiencing a bug in 8.4 that has been fixed already.
> Using pattern before rewrite, you can perform the selective rewrite.
>
> Lemma xxx:  KK = KK.
> unfold KK.
> pattern K at 2. rewrite K_eta.
>
> Best,
> — Matthieu
>
> On 10 sept. 2014, at 03:56, Randy Pollack 
> <rpollack AT inf.ed.ac.uk>
>  wrote:
>
>> Oops, I was still composing that email
>>
>> ---------- Forwarded message ----------
>> From: Randy Pollack 
>> <rpollack0 AT gmail.com>
>> Date: Tue, Sep 9, 2014 at 9:45 PM
>> Subject: Re: [Coq-Club] Universes
>> To: Coq-Club Club 
>> <coq-club AT inria.fr>
>>
>> Is there documentation of eta in Coq?
>>
>> Consider this:
>>
>> Definition T := Type. (* Fix a level *)
>> Parameter K : forall t:T, t -> t.
>>
>> Lemma K_eta: K = (fun t:T => K t).
>> change (K = K).  (* conversion contains eta *)
>> reflexivity.
>> Defined.
>>
>> BTW, tactic [compute] doesn't eta expand the LHS of this lemma, or
>> contract the RHS.
>>
>> Definition KK := K (forall t:Type, t -> t) K.
>>
>> is accepted with eta-expansion of the second K, as Jason and Matthieu 
>> point out.
>>
>> Lemma xxx:  KK = KK.
>> unfold KK.
>> rewrite K_eta at 2.   (* fails *)
>>
>> Toplevel input, characters 0-18:
>> Error: Illegal application (Type Error):
>> The term "K" of type "forall t : T, t -> t"
>> cannot be applied to the terms
>> "forall t : Type, t -> t" : "Type"
>> "fun t : T => K t" : "forall t : T, t -> t"
>> The 2nd term has type "forall t : T, t -> t" which should be coercible to
>> "forall t : Type, t -> t".
>>
>> Why does rewriting by K_eta cause this Type Error?
>>
>> Randy
>> --
>> On Sat, Sep 6, 2014 at 6:46 AM, Matthieu Sozeau
>> <matthieu.sozeau AT gmail.com>
>>  wrote:
>>> Indeed, eta allows to lower the second I/K’s levels in your definitions.
>>> What’s impossible however is to use K at a type larger or equal to it’s
>>> declared universe.
>>>
>>> Definition T := Type. (* Fix a level *)
>>> Parameter K : forall t:T, t -> t.
>>> Fail Check (K (forall t:T, t -> t) K).
>>>
>>> All the examples you gave do not use polymorphism, but typical ambiguity +
>>> eta-expansion only. In 8.4, only Inductves like:
>>>
>>> Inductive I (A : Type(* l *)) : A -> Type (* l *) := i : A -> I
>>>
>>> can be “polymorphic” on A, that is you can instantiate I at
>>> different incompatible levels, all lower than the initial global
>>> level l.
>>>
>>> Hope this helps,
>>> — Matthieu
>>>
>>> On 5 sept. 2014, at 23:17, Jason Gross 
>>> <jasongross9 AT gmail.com>
>>>  wrote:
>>>
>>>> There is no inconsistency here.  You are seeing the result of on-the-fly 
>>>> eta-expansion.  Note that [Definition KKs := K (forall t:Set, t -> t) 
>>>> K.] is also accepted, because the eta-expansion of [K] can be retyped as 
>>>> [forall t:Set, t -> t]. If you [Print KK], you'll notice that it uses 
>>>> [Type (* Top.2 *)], and the universe graph contains the constraint 
>>>> "Top.2 < Top.1".
>>>>
>>>> -Jason
>>>>
>>>>
>>>> On Fri, Sep 5, 2014 at 5:02 PM, Randy Pollack 
>>>> <rpollack AT inf.ed.ac.uk>
>>>>  wrote:
>>>> I'm using Coq 8.4pl4, which I think does not have Matthieu Sozeau's
>>>> new treatment of universes (is that true?).  Consider the examples:
>>>>
>>>>   Definition I := fun (t:Type) (x:t) => x.
>>>>   Definition II := I (forall t:Type, t -> t) I.
>>>>
>>>> This is accepted, as it should be (by universe polymorphism), as the 2
>>>> instances of "I" in Definition II can get different types.
>>>>
>>>> But consider
>>>>
>>>>   Set Printing Universes.
>>>>   Parameter K : forall t:Type, t -> t.
>>>>   Print K.
>>>>   *** [ K : forall t : Type (* Top.1 *), t -> t ]
>>>>   Print Universes
>>>>       (* no constraint on Top.1 shown *)
>>>>
>>>> So far, OK.  But...
>>>>
>>>>   Check (K (forall t:Type, t -> t) K).
>>>>
>>>> This is accepted, wrongly, as the 2 instances of "K" must have the same 
>>>> type.
>>>>
>>>>   Definition KK := K (forall t:Type, t -> t) K.
>>>>
>>>> This is accepted, and now we have an ill-typed term bound in the global 
>>>> context.
>>>>
>>>> --Randy
>
>