## Stream: general

### Topic: unexpected funext / refl behaviour

#### Kevin Buzzard (Apr 11 2018 at 19:31):

set_option pp.universes true -- might help
example : -- phenomenon won't occur if you replace this with theorem T!
(λ (X : Sort*) (f : X → X) , f) = (λ (X : Sort*) (f : X → X), f) :=
begin
funext, -- only pulls off X, possibly because of universe issues
-- two failed attempts to pull off f now:
-- funext, -- does nothing
-- apply funext, -- fails to unify
refine funext _, -- Type of X now Sort (imax ? ?) and a type mismatch error reported **but goal changes anyway**
intro f,
-- goal now f = f
-- refl, -- doesn't work! Fails to unify.
exact rfl, -- does work
end


#### Kevin Buzzard (Apr 11 2018 at 19:32):

I am pleased to have confused tactic mode so much that refl won't work but exact rfl will.

#### Kevin Buzzard (Apr 11 2018 at 19:32):

I am not sure if my goal is true, as the sorts may or may not be in different universes initially. However the funext tactic seems to buy it, although after pulling off the X it gets confused and won't pull off the f.

#### Kevin Buzzard (Apr 11 2018 at 19:33):

apply f won't do it but I seem to be able to explicitly do it with refine funext _ although now Lean is in a funny state -- the refine tactic does appear to do something, but reports an error anyway.

#### Kevin Buzzard (Apr 11 2018 at 19:34):

replacing example with theorem T makes all the problems go away, which is to me very surprising behaviour.

#### Patrick Massot (Apr 11 2018 at 19:36):

This Lean 3 is all broken. Let's have Lean 4.

#### Patrick Massot (Apr 11 2018 at 19:37):

(and hope Kevin stops trying to break everything)

#### Chris Hughes (Apr 11 2018 at 19:38):

Isn't it just because your X's are in different universes. And then if you put them in the same universe, it fails because the funext tactic gets rid of both lambdas.

#### Kevin Buzzard (Apr 11 2018 at 19:40):

I agree that if you put them in the same universe, all is well.

#### Kevin Buzzard (Apr 11 2018 at 19:41):

But if you leave them in different universes, Lean ends up in a weird state.

#### Kevin Buzzard (Apr 11 2018 at 19:42):

After the intro f, you have a goal f = f which refl won't close

#### Kevin Buzzard (Apr 11 2018 at 19:43):

but exact rfl will. However we are now passed a red squiggly line and I am not too sure how seriously to take Lean.

#### Chris Hughes (Apr 11 2018 at 19:43):

I'm beginning to see the problem. Is it something to do with, it let's you do funext the first time, so if you can prove their equal, it will deduce the universes are the same. So your proposition is a bit like an heq?

#### Kevin Buzzard (Apr 11 2018 at 19:43):

I was wondering if there was some implicit unification going on

#### Kevin Buzzard (Apr 11 2018 at 19:44):

Also it was very strange to see a line in tactic mode fail and yet see the goal change.

#### Patrick Massot (Apr 11 2018 at 19:44):

Looks a bit in the same spirit as your most recent issue on Lean github

#### Chris Hughes (Apr 11 2018 at 19:45):

And it automatically lifts the functions to a different universe to be able to state that they're equal.

#### Patrick Massot (Apr 11 2018 at 19:45):

Lean somehow fails to notice it's failing

#### Chris Hughes (Apr 11 2018 at 19:46):

Haven't ever done anything that really tests the universe system so I don't really know.

#### Kevin Buzzard (Apr 11 2018 at 19:48):

I just started playing with it recently. I'm just trying to get the hang of it :-)

#### Kevin Buzzard (Apr 16 2018 at 19:19):

I know there's something strange going on here but I've not explained it very well. How about this

#### Kevin Buzzard (Apr 16 2018 at 19:19):

example :
(λ (X : Sort*) (f : X → X) , f) = (λ (X : Sort*) (f : X → X), f) :=
begin
funext, -- it's not very effective
refine @funext (X → X) _ _ _ _, -- back on track
intro f,
refl,
end


That works fine.

#### Kevin Buzzard (Apr 16 2018 at 19:20):

But now let me change example to theorem strange:

#### Kevin Buzzard (Apr 16 2018 at 19:20):

theorem strange :
(λ (X : Sort*) (f : X → X) , f) = (λ (X : Sort*) (f : X → X), f) :=
begin
funext, -- it's super effective!
refine @funext (X → X) _ _ _ _, -- invalid type ascription
intro f,
refl,
end


#### Kevin Buzzard (Apr 16 2018 at 19:20):

The proof no longer typechecks if I name the theorem

#### Kevin Buzzard (Apr 16 2018 at 19:20):

because the behaviour of funext changes now the theorem has a name

#### Kevin Buzzard (Apr 16 2018 at 19:20):

That's not right, is it?

#### Kevin Buzzard (Apr 16 2018 at 19:22):

I think this has something to do with screwy universes

#### Johannes Hölzl (Apr 16 2018 at 19:26):

Yes, it could be related to the fact that example (compared to theorem) does allow meta (universe) variables in its statement. So the type is not fully elaborated, it gets fully elaborated together with the value like def. So maybe funext has a problem with instantiating them.

#### Kevin Buzzard (Apr 16 2018 at 19:30):

Oh yes! If I set pp.universes true then I see that in the theorem the goal has (X : Sort u_1)

#### Kevin Buzzard (Apr 16 2018 at 19:30):

but in the example it has (X : Sort ?l_1)

#### Kevin Buzzard (Apr 16 2018 at 19:37):

I see, so definition strange fixes the problem :-)

#### Kevin Buzzard (Apr 16 2018 at 20:48):

here's some possibly related weird behaviour:

#### Kevin Buzzard (Apr 16 2018 at 20:48):

example :
(λ (X : Sort*) (f : X → X) , f) = (λ (X : Sort*) (f : X → X), f) :=
begin
funext,
refine funext _,
intro f,
-- this proof isn't finished yet
end


#### Kevin Buzzard (Apr 16 2018 at 20:48):

the goal now is f = f

#### Kevin Buzzard (Apr 16 2018 at 20:48):

(at the point where the proof is not finished)

#### Kevin Buzzard (Apr 16 2018 at 20:48):

or with pp.all on

#### Kevin Buzzard (Apr 16 2018 at 20:49):

⊢ @eq.{?l_2} (X → X) f f

#### Kevin Buzzard (Apr 16 2018 at 20:49):

and the red squiggle is under end

#### Kevin Buzzard (Apr 16 2018 at 20:49):

because we wrote end before the proof was complete

#### Kevin Buzzard (Apr 16 2018 at 20:49):

However if we write admit to finish the proof

#### Kevin Buzzard (Apr 16 2018 at 20:49):

we get a new red squiggle

#### Kevin Buzzard (Apr 16 2018 at 20:50):

on the second funext :-)

#### Kevin Buzzard (Apr 16 2018 at 20:50):

Maybe the universe unification or whatever only takes place after the admit, and then Lean decides something was wrong all along

#### Kevin Buzzard (Apr 16 2018 at 20:51):

I guess this is the price I pay for the silly Sort* choices I made earlier

#### Kevin Buzzard (Apr 16 2018 at 20:52):

changing example to theorem T gives me the red squiggle on the second funext immediately

#### Chris Hughes (Apr 16 2018 at 21:39):

I think it might be because the proof could give a clue about universes, but not if the proof is admit.

Last updated: May 15 2021 at 23:13 UTC