Zulip Chat Archive

Stream: general

Topic: help with `unify`


Scott Morrison (Mar 25 2020 at 01:53):

I'm running into the following problem. I've built an expression
@equiv.arrow_congr.{1 1 1 ?l_1} α α ?m_2 ?m_3 ?m_4 ?m_5
which Lean tells me has type
equiv.{1 (imax 1 ?l_1)} (α → α) (?m_2 → ?m_3)
I want to unify this with another expression
?m_1
with type
equiv.{1 ?l_1} (α → α) ?m_2).

To me that looks good, and unification should succeed. But it doesn't. :-( Can anyone guess what is going on?

Alex J. Best (Mar 25 2020 at 01:56):

(deleted)

Scott Morrison (Mar 25 2020 at 01:57):

@Alex J. Best sorry, copy-paste error which I've just fixed.

Scott Morrison (Mar 25 2020 at 01:58):

Ah, I seem to have found the problem. With set_option pp.purify_metavars false, we instead see that the two types are:

equiv.{1 (imax 1 ?l__fresh.1092.218230)} (α → α) (?m__fresh.1092.218696 → ?m__fresh.1092.218697)

and

equiv.{1 ?l__fresh.1092.218230} (α → α) ?m__fresh.1092.218370

Scott Morrison (Mar 25 2020 at 02:00):

and we can see why unification fails: the two ?l_1s must be the same, so (imax 1 ?l_1) isn't unifying with ?l_1.

Scott Morrison (Mar 25 2020 at 02:00):

That's a bit weird, actually. Aren't they always equal, for any ?l_1?

Scott Morrison (Mar 25 2020 at 02:24):

I guess Lean can't see that ?l_1 = (imax 1 ?l_1). Can anyone who knows universe level unification confirm that this is a plausible explanation?

Scott Morrison (Mar 25 2020 at 02:25):

I guess my workaround is going to be to avoid Sort.

Chris Hughes (Mar 25 2020 at 04:13):

Page 2 of Mario's thesis has the universe unification rules. I can't find a way of deducing ?l_1 = (imax 1 ?l_1) from the rules given.

Mario Carneiro (Mar 25 2020 at 04:59):

Using the universe unification rules in my thesis, you can prove that and many other things, but crucially you have to use the split rule to case on whether ?l_1 is 0 or not, and lean doesn't have that rule, it has a fixed finite set of simplifications and that's it

Mario Carneiro (Mar 25 2020 at 05:00):

The way the proof goes is that imax 1 0 = 0 and imax 1 (suc u) = max 1 (suc u) = suc (max 0 u) = suc u, so imax 1 v = v

Mario Carneiro (Mar 25 2020 at 05:01):

this is the way trepplein does universe checking

Scott Morrison (Mar 25 2020 at 05:48):

This was a really confusing and hard to debug issue. :-( I understand the issue now, but it took me forever to work out that the problem I was having (solve_by_elim refusing to apply a lemma that worked fine by hand) had as its root cause a universe issue.

Mario Carneiro (Mar 25 2020 at 05:51):

What is the actual goal? I'm curious how this unification constraint can come up

Scott Morrison (Mar 25 2020 at 05:53):

Hmm... it will be a bit hard to re-extract, actually. I'll see if I can dig it out.


Last updated: Dec 20 2023 at 11:08 UTC