Zulip Chat Archive

Stream: general

Topic: simp lemma priority


Violeta Hernández (Jun 10 2022 at 07:34):

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 (Jun 10 2022 at 07:34):

Context: #14660

Violeta Hernández (Jun 10 2022 at 07:35):

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 (Jun 10 2022 at 10:18):

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 (Jun 10 2022 at 10:19):

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 (Jun 10 2022 at 16:39):

I have no idea

Violeta Hernández (Jun 10 2022 at 16:39):

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 (Jun 10 2022 at 16:39):

Maybe it does call simp internally?

Violeta Hernández (Jun 10 2022 at 16:41):

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 (Jun 10 2022 at 16:41):

I'm surprised this isn't defined in core

Violeta Hernández (Jun 10 2022 at 16:42):

image.png I deleted forall_false_left and this happens

Violeta Hernández (Jun 10 2022 at 16:42):

I'm in logic/basic, not in core

Violeta Hernández (Jun 10 2022 at 16:43):

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

Violeta Hernández (Jun 10 2022 at 16:43):

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

Eric Wieser (Jun 10 2022 at 16:44):

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

Eric Wieser (Jun 10 2022 at 16:45):

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

Eric Wieser (Jun 10 2022 at 16:45):

; makes a mess of the info view

Violeta Hernández (Jun 10 2022 at 16:46):

Oh, you're right :face_palm:

Violeta Hernández (Jun 10 2022 at 16:49):

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


Last updated: Aug 03 2023 at 10:10 UTC