ext debugging

Stream: mathlib4

[Patrick Massot]

Do we have any procedure to debug what the ext tactic is doing. I'm porting this line and the ext tactic simply isn't doing the same in mathlib4. I looked at what lemmas Lean 3 is calling here, and I can fix the Lean 4 proof by explicitly applying those lemmas. But it feels wrong. Both lemmas used by Lean 3 exist in mathlib4 and are tagged as ext.

[Gabriel Ebner]

Hmm you could try set_option trace.Meta.isDefEq true in ext1. This should tell you at least which lemmas ext is trying.

[Gabriel Ebner]

There has been a slight change in which lemmas ext tries. Just like simp (and everything really) ext now uses the discrimination tree indexing.

[Gabriel Ebner]

The old ext also resorted to trying all lemmas as a last resort, which is obviously a big performance problem that we wanted to avoid in Lean 4.

[Jireh Loreaux]

I would guess the issue is that some of the ext lemmas in Mathlib 4 now need their priority adjusted.

[Patrick Massot]

Indeed it applies ext lemmas in the "wrong" order, where wrong means not the one used by mathlib3 which succeeds here

[Gabriel Ebner]

In practice this means that the new ext will no longer see through defs. The fix is easy, you just need to add a new ext lemma for the defined type.

[Gabriel Ebner]

Yes the order is another thing. The Lean 3 ext tries the last declared lemma first. While the Lean 4 order is random unless you assign a priority.

[Patrick Massot]

Do we have any documentation about which priorities are sensible? I know (from reading the source code of ext) that default is 1000.

[Gabriel Ebner]

I would refer to https://github.com/leanprover-community/mathlib4/pull/2020/files and https://github.com/leanprover-community/mathlib4/pull/2979

[Patrick Massot]

Oh, I used 1001. I guess I'll switch to 1100.

[Jireh Loreaux]

Is there an upper bound on priorities?

[Floris van Doorn]

I believe high and low are also accepted as priorities, if you just want something that is higher or lower than the default.

[Jireh Loreaux]

I don't like using both quantitative and qualitative properties because the relationship between them is not clear (to me), and sometimes we need multiple levels.

[Eric Wieser]

Do you have an example of where we need more than two levels?

[Gabriel Ebner]

For ext we need at least four levels. But I agree that we should probably determine these levels automatically, like you've suggested before.

[Jireh Loreaux]

I certainly encountered a situation porting where I needed at least 3 levels, but I don't recall where.

[Eric Wieser]

I'm really struggling to think of a case where there are more than two in practice

[Eric Wieser]

In almost every case I know of the ext lemmas are for equality of

• SomeHom α β
• SomeHom (SomeType _) β

The only exception I know of is docs4#LinearMap.ext_ring, and that still feels like a special case of the second option

[Jeremy Tan]

One of the two problematic exts in !4#3441 required setting high priorities in two places. Is that still one level?

[Jeremy Tan]

(yes I have addressed your comments in that PR)

[Eric Wieser]

Yes that still counts as one level; the precise question here is "can you find a three ext lemmas that could all apply to the same situation"

[Jireh Loreaux]

docs#star_alg_hom.ext, docs#star_alg_hom.ext_adjoin, docs#star_alg_hom.ext_adjoin_singleton