higher ext priority

Stream: mathlib4

[Johan Commelin]

-- Porting note: The priority should be higher than `LinearMap.ext`.
@[ext high]
theorem lhom_ext' ⦃φ ψ : (α →₀ M) →ₗ[R] N⦄ (h : ∀ a, φ.comp (lsingle a) = ψ.comp (lsingle a)) :

and

-- Porting note: we need high priority for this to fire first; not the case in ML3
attribute [local ext high] TensorProduct.ext

and

@[ext 1100] -- Porting note: increase priority so this applies before `LinearMap.ext`
theorem linearMap_qext ⦃f g : M ⧸ p →ₛₗ[τ₁₂] M₂⦄ (h : f.comp p.mkQ = g.comp p.mkQ) : f = g :=

This design seems to work as intended. Shall I change the 1100 to high, and remove the porting notes?

[Eric Wieser]

The notes here are I think because Lean 4 breaks ties in the opposite direction to Lean 3

[Eric Wieser]

And so we didn't need any priority markers before, because later declarations took priority over earlier ones in the case of a tie

[Johan Commelin]

Right. So remove the notes?

[Yaël Dillies]

Well, looks like the issue wasn't fixed?

[Johan Commelin]

Why? We have a new design. And now you tag these lemmas with high.

[Yaël Dillies]

How do you do if you have a series of three lemmas? Tag them ext, ext high, ext higher? What if you want to insert an extra one between the first and second? Tag it ext high and retag the latter two ext higher and ext higherer? I don't think that's sustainable

[Yaël Dillies]

The Lean 3 default was correct. The Lean 4 isn't. Why don't we just fix it?

[Ruben Van de Velde]

Is there an issue?

[Robert Maxton]

Yaël Dillies said:

How do you do if you have a series of three lemmas? Tag them ext, ext high, ext higher? What if you want to insert an extra one between the first and second? Tag it ext high and retag the latter two ext higher and ext higherer? I don't think that's sustainable

Tag them ext 1000, ext 1050, ext 1100? We have at least a thousand and probably more like MAXINT possible priorities going spare, so as long as we make our steps large enough to fit several extra new priorities between them, I don't think it'll be an issue.

[Kyle Miller]

Yaël Dillies said:

Why don't we just fix it?

"Just" is doing a lot of heavy lifting. What does "just" fixing it look like?

[Eric Wieser]

I think possibly I mispoke above, and the order changed from "declaration order" to "unspecified"

[Eric Wieser]

Does ext do discrtree matching on the type?

[Eric Wieser]

I think that would replace the need for (almost) any priorities

[Jireh Loreaux]

That would only work if it picks the thing that "matches best", not just something that matches at all. And it's not entirely clear what "matches best" means in all circumstances.

[Kyle Miller]

@Eric Wieser Yes, it uses a discrimination tree to match on the type.

[Eric Wieser]

Am I right in thinking that discrtrees prefer the most specific match first? So for instance, should match an ext lemma about linear maps from the tensor product before matching a lemma about linear maps over a free variable?

[Eric Wieser]

(and a related question: did ext in Lean 4 always do this? Maybe I'm remembering a much older and less useful version)

[Jireh Loreaux]

I'm not sure what "most specific" means, as I think there's only a partial order on discr tree keys (I don't mean an instance of PartialOrder). E.g., if I have keys foo a _, foo _ b and foo _ _, and I'm matching against foo a b, which one is "most specific"?

[Eric Wieser]

I think in practice the keys with these porting notes are SomeHom _ _ and SomeHom (F _) _

[Jireh Loreaux]

I understand, I'm just arguing that I don't know how ext could reliably choose the most specific match because that's not well-defined.

[Kyle Miller]

I think the order is lexicographic @Jireh Loreaux, with foo _ _ < foo _ b < foo a _. I don't know in what order discrimination trees return results though (whether it's least first or greatest first).

[Yaël Dillies]

Kyle Miller said:

Yaël Dillies said:

Why don't we just fix it?

"Just" is doing a lot of heavy lifting. What does "just" fixing it look like?

I am aware that I am being a bit :chili_pepper: but I really would like us not to remove those porting notes when improvements could be made

[Kim Morrison]

I think at some point porting notes like this need to either have a specific volunteer who will do the work, or be removed. As far as I am concerned it is by design the the order isn't specified here (because that then commits us to never changing the behaviour of discrimination trees), and there is a perfectly good mechanism to specify the order when needed.

[Jireh Loreaux]

Sorry, what's the perfectly good mechanism?

[Kim Morrison]

@[ext 1100]