simp lemma priority

Stream: general

[Violeta Hernández]

I have a very weird situation where I need two lemmas to be simp, even though one makes the other redundant. How do I set up the priorities so that simp_nf doesn't complain?

[Violeta Hernández]

Context: #14660

[Violeta Hernández]

I tried setting the priority of the obsoleted lemma to 100 to no avail. Is that the default? Did I set it improperly?

[Gabriel Ebner]

You need to go the other way around, give the subsumed lemma higher priority so that it is used preferentially (and thus no longer obsolete).

[Gabriel Ebner]

But I don't really see why we need forall_false_left. You mention the by_cases tactic in the PR, but it is in core (and doesn't use the simplifier). Why does it depend on simp lemmas in mathlib?

[Violeta Hernández]

I have no idea

[Violeta Hernández]

All I know is, once I delete those theorems, the by_cases tactic starts giving very weird error messages about how it's not able to solve goals that look like those of the deleted theorems

[Violeta Hernández]

Maybe it does call simp internally?

[Violeta Hernández]

And unfortunately, I can't move forall_iff and empty_iff to this file, because is_empty is defined after logic/basic

[Violeta Hernández]

I'm surprised this isn't defined in core

[Violeta Hernández]

image.png I deleted forall_false_left and this happens

[Violeta Hernández]

I'm in logic/basic, not in core

[Violeta Hernández]

Note that it isn't the lemma that fails, but the tactic itself

[Violeta Hernández]

Who might know about something like this? @Mario Carneiro or @Eric Wieser maybe?

[Eric Wieser]

I'm confused, I thought docs#tactic.by_cases does nothing more than apply decidable.em. Does it do something else?

[Eric Wieser]

Oh, I just clicked the screenshot; that's the simp failing not the by_cases

[Eric Wieser]

; makes a mess of the info view

[Violeta Hernández]

Oh, you're right :face_palm:

[Violeta Hernández]

Thanks everyone, I didn't know that ; screwed over the error highlighting