Bracket notation in ext

Stream: general

[Michał Mrugała]

Hi, is there a way to add/remove lemmas from an ext call similarly to how we can do so with simp using bracket notation?

[Eric Wieser]

show_term ext then omit the one you don't want?

[Eric Wieser]

Or attribute [local -ext], or whatever the spelling is, just before the lemma.

[Michał Mrugała]

What if I'm in a scenario where I would want to have access to an ext lemma besides a specific ext call in the proof? The second solution wouldn't be great in that case. The first solution is basically what I'm asking for, but it would be nice if I could just get automation to do this for me instead of applying the ext lemmas myself.

[Eric Wieser]

Out of curiosity, which one do you want to avoid?

[Michał Mrugała]

I'm in a situation where I want Ideal.Quotient.algHom_ext to fire instead of AlgHom.ext

[Eric Wieser]

I think every situation is that situation?

[Eric Wieser]

docs#Ideal.Quotient.algHom_ext

[Eric Wieser]

So I think the solution in this case is add the attribute in mathlib

[Michał Mrugała]

Thanks, I think that makes sense. Still would be a nice feature for ext anyway if someone is bored at some point :slight_smile:

[Kevin Buzzard]

You have not yet done a good job of convincing anyone that the functionality is needed though!

[Michał Mrugała]

I don’t think it’s a necessary functionality, it just seems like a convenient thing to have. To be clear I don’t expect anyone to do this, I might try to work on this myself at some point!

[Bhavik Mehta]

It would also be nice to have ext? back

[Michał Mrugała]

Yeah this was a statement of the type: it would be nice to have X

[Kevin Buzzard]

It would be nice to have ext? back but I am confused about your claim that the thing that we currently have no use cases for would also be nice.

[Kevin Buzzard]

OTOH if you're looking for an excuse to learn some metaprogramming then maybe that's a reason in itself :-)

[Michał Mrugała]

The use case is that there are situations (or at least I seem to remember running into such situations) when one wants to violate the ext priority order in a single ext call, similarly to how sometimes we want to disable a single simp lemma.

[Michał Mrugała]

The example I ran into today is not a good example because it seems like the priority order is just wrong

[Yaël Dillies]

IMO it is simply more discoverable than attribute [local ext] foo in lemma ...

[Yaël Dillies]

Just like set_option push_neg.distrib in lemma ... is terrible for discoverability (in fact I use it so little because of that that I am not sure I got the option name right)

[Eric Wieser]

set_option isn't as bad, as it's at least allowed in term and tactic syntax