Reordering ext lemmas

Stream: general

[Alex J. Best]

It seems the ext tactic is sensitive to the order in which lemmas are stated and/or tagged as ext (this is what I think is happening but frankly I'm a bit confused still).
In a PR me and @Johan Commelin are working on we reorder some a bunch of imports and correspondingly the proof at https://github.com/leanprover-community/mathlib/blob/master/src/algebraic_geometry/presheafed_space/has_colimits.lean#L253 breaks.
You can simulate this locally by adding the line attribute [ext] continuous_map.ext before that theorem, even though this is already an ext lemma, applying the ext attribute seems to cause this to fire first and leave the proof in a different state.

The specific question is what if anything should we do about this sort of behaviour when we observe it? If this was about simp-lemmas I'd look for more lemmas to add to make the simp-set confluent again, should something analogous be done here?
In this (or indeed any) specific example I can use ext? to replace the ext proof with some explicit apply statements, but I'd like to avoid that if possible.
@Scott Morrison I guess you know the design of this area the best?

[Eric Wieser]

What's the other ext lemma involved here that isn't docs#continuous_map.ext?

[Scott Morrison]

Yes, ext applies lemmas tagged @[ext] (or automatically generated by putting the @[ext] attribute on a structure in reverse order as they have been added to the environment.

[Scott Morrison]

(i.e. most recent has priority)

[Scott Morrison]

I'm not sure there is a general purpose solution to this sort of problem.

[Eric Wieser]

Which is usually a feature, since things like docs#linear_map.ext should be in the same file as linear_map, making them the lowest priority by default compared to something like docs#dfinsupp.lhom_ext

[Scott Morrison]

ext lemmas mean "you can prove this identity by working 'componentwise' in some sense", but there are situations where there are different valid interpretations of "in some sense".

[Scott Morrison]

Sometimes using ext1 is helpful. Other times I guess you'll have to resort to using apply.

[Scott Morrison]

The ext tactic itself can't be expected to be clever when you have defined multiple applicable ext lemmas.

[Kyle Miller]

It looks like it will apply a specific ext lemma for a given type if you've registered one with @[ext my_type] before trying general ext lemmas, if I understand docs#tactic.ext1_core correctly. It seems like there can be exactly one registered. (Just mentioning this because I hadn't seen this feature before.)

[Eric Wieser]

I think to usefully diagnose this we need to know which two ext lemmas are fighting for priority here, which one is "right", and why we think it is "right"

[Alex J. Best]

I shut my lean down for the night, but ext? should tell you the other one. I was wondering if giving ext lemmas priorities would help (currently it didn't do anything as far as I can tell)

[Alex J. Best]

As in I was wondering if we should add some knowledge of priorities to the ext tactic

[Eric Wieser]

They already can have priorities

[Alex J. Best]

Eric Wieser said:

They already can have priorities

How do they work?
Explicitly I want the following to apply a instead of b:
import tactic.ext

@[ext, priority 10000]
lemma a (f g : ℕ → ℕ) (h : f 1 = g 1) : f = g :=
sorry

@[ext]
lemma b (f g : ℕ → ℕ) (h : f 2 = g 2) : f = g :=
sorry

lemma c (f g : ℕ → ℕ) : f = g :=
begin
ext, -- want f 1 = g 1
end

[Gabriel Ebner]

What's the other ext lemma involved here that isn't docs#continuous_map.ext?

Did somebody already answer this question? The mathlib4 ext tactic uses term indexing for the extensionality lemmas, and I'd like to figure out if there's going to be a problem.

[Alex J. Best]

Nope I never answered sorry:
The ext as it currently stands does:

      apply category_theory.limits.colimit.hom_ext, intros j,
      apply continuous_map.ext, intros x,

if continuous_map.ext applies first then docs#category_theory.limits.colimit.hom_ext doesn't apply

[Gabriel Ebner]

This should be fine as long as the hom doesn't reducible reduce to continuous_map.

[Reid Barton]

It probably only instance reduces

[Floris van Doorn]

Kyle Miller said:

It looks like it will apply a specific ext lemma for a given type if you've registered one with @[ext my_type] before trying general ext lemmas, if I understand docs#tactic.ext1_core correctly. It seems like there can be exactly one registered. (Just mentioning this because I hadn't seen this feature before.)

It is true that for every type it has one "preferred" ext lemma that it tries first. However, this extattribute need not to have an explicit argument: it is the last ext lemma that proves an equality between objects of a specific type.

Currently, ext completely ignores priorities. I think I can fix that, but I'm not sure if that is worth doing in Lean 3.

[Eric Wieser]

There was a long discussion in a previous PR about adding priority attributes to some ext lemmas (in the end we didn't). Was it really a no-op the whole time?