The Coq mailing list

[Randy Pollack <rpollack0 AT gmail.com>]

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 by et-expansion of the second K, as Jason and Matthieu point out

Lemma xxx:  KK = KK.
unfold KK.
rewrite K_eta at 2.




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