The Coq mailing list

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

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