Zulip Chat Archive

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

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

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