The Coq mailing list

[Matthieu Sozeau <matthieu.sozeau AT inria.fr>]

Hi Randy,

On 10 sept. 2014, at 23:18, Randy Pollack 
<rpollack0 AT gmail.com>
 wrote:

> Hi Matthieu,
> 
> First: is there any document that explains eta in Coq?

I don’t think so, but it should be part of the reference manual. Anyway,
the idea is easily explained: Coq has eta-conversion only, not general
eta-reduction or expansion. It happens when comparing terms during conversion
and is inspired by typed equality presentations of the calculus of 
inductive constructions. Conversion implements the following rule 
(and its symmetric version).

Γ, x : T |- b = e x
--------------------
Γ |- λ x : T . b = e

It is assumed that the two terms being converted have a common super type. 
As cumulativity is equivariant on the domains of products, e must have 
type Π x : T’. U’ with T = T’, and the rule preserves this invariant.

The eta expansion you see is somewhat different...

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

This eta expansion is done by the coercion code which tries to 
coerce from [forall t : T, t -> t] to [forall t : Type (* Top.3 *), t -> t],
while already knowing that Top.3 < Top.1 (by the typing constraints
for the first argument of K) which prevents directly converting these types. 
So it builds:

[K : forall t : T, t -> t |- fun t : Type (* Top.3 *), K t : forall T : Type 
(* Top.3 *), T -> T

Which is well-typed and respects the constraints (using Top.3 <= Top.1). 
If by “clearly” safe you mean that it does not produce inconvertible terms, 
then no it isn’t as the type of K and forall T: Type(*Top.3*), T -> T don’t 
have a common supertype.

Best,
— Matthieu

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