push_neg extensibility

Stream: mathlib4

[Yaël Dillies]

I would like push_neg to simplify s ≠ ∅ to s.Nonempty when s : Finset α. push_neg already does this when s : Set α thanks to docs#Mathlib.Tactic.PushNeg.ne_empty_eq_nonempty. But this is a hardcoded lemma and we certainly don't want to import finsets in Tactic.PushNeg

[Yaël Dillies]

Does that mean we need a full redesign of push_neg?

[Jireh Loreaux]

I don't think a full redesign is necessary. You could add an attribute, and then mark theorems of a particular form (e.g., Ne) with it, and in the tactic you could apply these at the relevant point if they match.

[Yaël Dillies]

I think that would be a full redesign :sweat_smile: Look at the push_neg code.

[Kyle Miller]

I'm taking a look, and I'm not sure what I'm supposed to be seeing Yaël.

[Kyle Miller]

@Jireh Loreaux Yeah, there could be a @[push_neg] simp set that's used when invoking simp at Mathlib.Tactic.PushNeg.pushNegCore

[Jireh Loreaux]

Yaël, I looked at the code before I sent that message. I don't see anything that requires a full redesign.

[Jireh Loreaux]

I'll see if I can implement this real quick before I go teach.

[Kyle Miller]

Sometimes I wish it could be configurable whether push_neg pushes negations everywhere or just along the "spine". I tried doing this a couple years ago, but it'd take writing a new driver for it that doesn't use simp... It didn't seem worth it.

[Jireh Loreaux]

I don't know what you mean by "spine"

[Kyle Miller]

It currently pushes negations inside arguments and binder types too. The "spine" would be (1) the top level expression, (2) the conclusion of a forall or exists that is a spine expression, (3) the arguments to a conjunction or disjunction that is a spine expression.

[Jireh Loreaux]

What's an example where you would prefer this behavior?

[Kyle Miller]

I don't have any offhand, but I've wanted to be able to push the outermost negation inward before, and only the outermost negation, without simplifying anything else.

[Kyle Miller]

I think my motivation looking into it was during the SLMath Lean school a couple years ago, a student was surprised at how global push_neg was.

[Jireh Loreaux]

Hmmm... Is it not possible to just take docs#transformNegationStep and use it in simp with a singlePass downwards (like ↓simp)?

[Jireh Loreaux]

Also, is there some documentation on register_simp_attr? I would expect it to put some sort of docs#Lean.Meta.SimpTheoremsArray (or similar) into the environment, along with the attribute that actually adds the lemma, but I'm having trouble finding it.

[Kyle Miller]

Jireh Loreaux said:

Hmmm... Is it not possible to just take docs#transformNegationStep and use it in simp with a singlePass downwards (like ↓simp)?

I don't think so — simp will keep going into subexpressions even if transformNegationStep didn't do anything.

[Kyle Miller]

It looks like SimpExtension has a getTheorems function

[Kyle Miller]

(Found this by looking through docs#Lean.Elab.Tactic.elabSimpArgs)

[Jireh Loreaux]

So, I realized after you sent that message before that the thing I should have done was:

@loogle |- Lean.Meta.SimpTheorems

[loogle]

:search: Lean.Meta.addSimpTheoremEntry, Lean.Meta.SimpTheorems.addDeclToUnfoldCore, and 6 more

[Jireh Loreaux]

In any case, I'm having a bit of trouble because I think (using whatsnew in) that register_simp_attr creates a hygienic name for the docs#Lean.Meta.SimpExtension that it declares. I guess the point is that it is only meant to be used in the context of simp [my_fancy_simp_attr], and not intended for use with the internals of simp. Am I missing something? Or do I need to declare this attribute and register the simp extension manually (which would be :sad:).

[Jireh Loreaux]

I mean, it's not that hard to use registerSimpAttr directly, it just seems silly that register_simp_attr makes this hygienic for no apparent reason.

[Kyle Miller]

Yeah, it looks like you have to do it manually.

For why the extension is hygienic, I guess it's because it's not wanting to make a choice for what the simp extension's name should be. It seems like it could be reasonable to expose it.

I wonder if it would make sense to change push_neg to be a macro for simp only [push_neg], and move the main implementation into a simproc. It would be convenient being able to throw push_neg into any given simp

[Jireh Loreaux]

Well, the issue is that push_neg is also intended as a pedagogical tool. As such, it puts a large emphasis on preserving things like binder names. Would we be able to preserve that behavior if it were a simproc?

[Jireh Loreaux]

And also there is a flag for how ¬ (a ∧ b) should be handled.

[Kyle Miller]

Would we be able to preserve that behavior if it were a simproc?

Yes, definitely, and I would hope we would be able to preserve binder names even just for general usability.

[Kyle Miller]

I'm not sure if simprocs can access options. If they can, then that's solved, but if not, we could get it to work by conditionally inserting a simp lemma that overrides the normal push_neg set.

[Kyle Miller]

Maybe simprocs are how we can deal with commuting Finset.prod/Finset.prod and preserving the binder names... Though I suppose there's not a sophisticated enough interface to simprocs to be able to select which products to commute.

[Jireh Loreaux]

Aha, then I think a simproc for push_neg sounds like a nice idea.

[Kyle Miller]

The idea is that Mathlib.Tactic.PushNeg.transformNegation is already the simproc (it's got the correct signature and everything), and you just need to add it to the push_neg simp set