ext doesn't fire when it should

Stream: mathlib4

[Jireh Loreaux]

in !4#1996 I had an issue (not my first) where ext didn't succeed where it did in Lean 3 and I had to manually apply the ext lemmas, see line 664. I don't understand why it didn't trigger, other than perhaps it failed with unification.

Notice that unification had an egregious failure just a few lines higher when I also had to manually apply ext lemmas. I have workarounds, but this is terrible. :sad:

[Kevin Buzzard]

Can you minimise and open an issue if nobody responds here? I've seen this too and I'm sure it will keep coming up. Probably just a bug in the tactic?

[Eric Wieser]

This came up in a previous thread; possibly about FreeMonoid?

[Xavier Roblot]

Eric Wieser said:

This came up in a previous thread; possibly about FreeMonoid?

Yes, I think I had a similar problem, see this Zulip conversation and the solution was indeed to replace each call to ext by the specific call to the ext lemma that was supposed to be used.

[Eric Wieser]

That's the one I was thinking of, thanks!

[Kevin Buzzard]

Right now the core lean people and the tactic people are all overwhelmed so I think we just have to keep creating issues to track the main problems and then work around them until the relevant people have time

[Gabriel Ebner]

the solution was indeed to replace each call to ext by the specific call to the ext lemma that was supposed to be used.

In that case, the solution was to add priorities to the ext lemmas (because in Lean 3 the order the lemmas appear in the file is the reverse of the order they're tried in, but this no longer works in Lean 4). Replacing ext by apply is of course only a workaround.

[Gabriel Ebner]

!4#2020 is how it should be done

[Jireh Loreaux]

Thanks! Do you understand why ext was able to unify, but manually doing apply or refine wasn't without help?

[Eric Wieser]

Could we restore the old behaviour by having the ext attribute:

• Call ext on the goal
• Ask which ext lemma was found
• Use a priority of p+1

[Gabriel Ebner]

That's an interesting idea (i.e., default the priority so that the lemma always fires), but it would be the only attribute that works that way. Alternatively we could also add an ext-linter.

[Jireh Loreaux]

That would only work if the other relevant ext lemmas are already imported though. I think a linter is a better approach.

[Eric Wieser]

In practice the weaker ext lemmas are always already imported; linear_map.ext always precedes tensor_product.hom_ext etc. We had this discussion in lean3 and concluded that adding manual priorities there did more harm than good.

[Eric Wieser]

Off the top of my head I can't think of a situation where there are more than two competing lemmas