help with `unify`

Stream: general

[Scott Morrison]

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]

(deleted)

[Scott Morrison]

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

[Scott Morrison]

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]

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]

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

[Scott Morrison]

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]

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

[Chris Hughes]

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]

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]

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]

this is the way trepplein does universe checking

[Scott Morrison]

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]

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

[Scott Morrison]

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