Zulip Chat Archive

Stream: general

Topic: unexpected funext / refl behaviour


view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Apr 11 2018 at 19:36):

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

view this post on Zulip Patrick Massot (Apr 11 2018 at 19:37):

(and hope Kevin stops trying to break everything)

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Apr 11 2018 at 19:40):

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

view this post on Zulip Kevin Buzzard (Apr 11 2018 at 19:41):

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

view this post on Zulip Kevin Buzzard (Apr 11 2018 at 19:42):

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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Apr 11 2018 at 19:43):

I was wondering if there was some implicit unification going on

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Apr 11 2018 at 19:44):

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

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Apr 11 2018 at 19:45):

Lean somehow fails to notice it's failing

view this post on Zulip 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.

view this post on Zulip 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 :-)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 16 2018 at 19:19):

That works fine.

view this post on Zulip Kevin Buzzard (Apr 16 2018 at 19:20):

But now let me change example to theorem strange:

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 16 2018 at 19:20):

The proof no longer typechecks if I name the theorem

view this post on Zulip Kevin Buzzard (Apr 16 2018 at 19:20):

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

view this post on Zulip Kevin Buzzard (Apr 16 2018 at 19:20):

That's not right, is it?

view this post on Zulip Kevin Buzzard (Apr 16 2018 at 19:22):

I think this has something to do with screwy universes

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip Kevin Buzzard (Apr 16 2018 at 19:30):

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

view this post on Zulip Kevin Buzzard (Apr 16 2018 at 19:37):

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

view this post on Zulip Kevin Buzzard (Apr 16 2018 at 20:48):

here's some possibly related weird behaviour:

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 16 2018 at 20:48):

the goal now is f = f

view this post on Zulip Kevin Buzzard (Apr 16 2018 at 20:48):

(at the point where the proof is not finished)

view this post on Zulip Kevin Buzzard (Apr 16 2018 at 20:48):

or with pp.all on

view this post on Zulip Kevin Buzzard (Apr 16 2018 at 20:49):

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

view this post on Zulip Kevin Buzzard (Apr 16 2018 at 20:49):

and the red squiggle is under end

view this post on Zulip Kevin Buzzard (Apr 16 2018 at 20:49):

because we wrote end before the proof was complete

view this post on Zulip Kevin Buzzard (Apr 16 2018 at 20:49):

However if we write admit to finish the proof

view this post on Zulip Kevin Buzzard (Apr 16 2018 at 20:49):

we get a new red squiggle

view this post on Zulip Kevin Buzzard (Apr 16 2018 at 20:50):

on the second funext :-)

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 16 2018 at 20:51):

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

view this post on Zulip Kevin Buzzard (Apr 16 2018 at 20:52):

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

view this post on Zulip 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