I made an extensible `push` tactic generalizing `push_neg`

Stream: mathlib4

[Jovan Gerbscheid]

I started out trying to make push_neg be aware of Finite and Infinite, but figured out that the tactic should be made extensible with a tag. I have now implemented this tactic here: #21769.

As requested by @Yaël Dillies, this, among others, tags the lemma docs#Finset.nonempty_iff_ne_empty.

Given this tactic, it is really easy to extend it to work with any constant, not just Not. So I have generalized it, so that when you write push C, then it will rewrite any expression that has head constant C, using the lemmas tagged with push.

The implementation is to use simp rewriting, and use a simproc for a few rewrites that can't be implemented with just a lemma (i.e. preserving variable names, folding ¬(a = b) into a ≠ b, and choosing which lemma to use at ¬(a ∧ b)). Unlike in simp, the rewrites are done before the subterms are rewritten. This is a more efficient approach when using push lemmas.

Many proofs can be simplified with this new tactic.

[Yaël Dillies]

Thousands of lemmas could be tagged with push! If it's not too hard, can we also a version that pulls the constant as far out as possible? cf push_cast vs norm_cast

[Jovan Gerbscheid]

As a follow up, I think is would be nice to see more tactics making use of push_neg in the way that contrapose! and by_contra! do. When refactoring proofs, I kept running into the pattern of by_cases h : p followed by a push_neg at h in the second branch. Other candidates for a ! version could be wlog, absurd and split_ifs.

[Jovan Gerbscheid]

This would also allow one to write by_cases h: ¬p, in order to swap the order of the two cases, without adding too many ¬ to the goals

[Ruben Van de Velde]

You can also do

by_cases h : p
case neg =>
case pos =>

[Jovan Gerbscheid]

Since this tactic requires special handling of ≠, I thought it was also going to be necessary for ∉, but it turns out that ∉ is just notation, and isn't its own constant. Wouldn't it be more convenient if the same held for ≠? Then you could rewrite the underlying equality without having to first unfold the Ne.

[Yaël Dillies]

Maybe, but then you wouldn't get anything to dot notate on. docs#Ne.symm, the most important lemma to have dot notation for, doesn't have an analogue with ∉

[Jovan Gerbscheid]

Makes sense (docs#Ne.symm)

[Jovan Gerbscheid]

I've also added an option for a discharger in the tactic, because lemmas about log_mul and log_sqrt have side goals. I haven't tested this yet, but it may be handy to define push_log as push (disch := positivity) Real.log.

[Johan Commelin]

@Patrick Massot mentioned that push_neg takes extra care to preserve variable names. Which is something that other tactics sometimes mess up. How does push fare in this regard?

[Eric Wieser]

(support for) preserving variable names in binders is coming in the next Lean release, right?

[Jovan Gerbscheid]

The lemmas about exists and forall aren't tagged by @[push], but instead are rewritten in the simproc (using the same implementation as was originally there), So variable names are preserved.

[Jovan Gerbscheid]

But if one were to add other push lemmas with binders, it wouldn't preserve the variable names (at least until the next release)

[Jovan Gerbscheid]

Hmm, I could also add a push_lambda version of the tactic that can push things like fun x => a x + b x into (fun x => a x) + (fun x => b x), if that is useful. And a push_forall for things like ∀ a, p → q a into p → ∀ a, q a. (These need special casing because forall and lambda aren't constants)

[Johan Commelin]

They need special casing in the implementation of the tactic. But it could still be push lambda from the user perspective, right?

[Tomas Skrivan]

First of all, this is great! I have a bunch of simp attributes push_neg, push_smul, push_exp, .. and it was on my todo list to implement tactic like this. So thanks for doing this!

---

An idea for possible extension:

I also have attributes pull_neg, pull_smul, pull_exp, ... to do the reverse. Also for a theorem f_linear : IsLinearMap 𝕜 f I can call command #generate_linear_map_simps f_linear that automatically generates simp theorems for f x + f y = f (x + y) or - f x = f (- x) which can be used left to right by simp [push_add, push_neg] or right to left simp [pull_add,pull_neg]. The main point of doing this is that the equality f (- x) = - f x is not a valid simp theorem as it has variable head. The command #generate_linear_map_simps f_linear allows you to quickly instantiate this theorems for concrete f.

So simp [pull_neg,pull_add] is effectively push for all linear maps.

---

Jovan Gerbscheid said:

Unlike in simp, the rewrites are done before the subterms are rewritten. This is a more efficient approach when using push lemmas.

Is this true? Isn't this what pre/post simp ↑/simp ↓ is for? i.e. if you mark your theorems with @[simp ↓] the theorem is applied before subterms are visited.

[Jovan Gerbscheid]

Yes, but nobody seems to actually use pre lemmas in simp

[Tomas Skrivan]

You can also call simp as simp [↓thm, ↓attr, ↓siproc] to specifically say apply theorem/simp attribute/simproc as pre, so you do not have to mark theorems themselves.

Sometimes I wonder how much speed up could be gained in mathlib by being more careful about pre/post for simp theorem. In my applications when transforming programs using simp this can make a big difference.

[Eric Wieser]

Tomas Skrivan said:

The main point of doing this is that the equality f (- x) = - f x is not a valid simp theorem as it has variable head.

I don't follow, for map_neg the head is DFunLike.coe, for your example f is a constant name, right?

[Tomas Skrivan]

I'm not talking about LinearMap but about IsLinearMap i.e. you have a predicate on f : X -> Y.

[Tomas Skrivan]

Maybe this is non issue for mathlib as it mainly works with bundled linear maps but in SciLean I mostly work with unbundled maps.

[Eric Wieser]

I think your #generate_linear_map_simps was confusing me, which surely only works for one particular f?

[Kyle Miller]

Jovan Gerbscheid said:

Yes, but nobody seems to actually use pre lemmas in simp

I'm not understanding this "yes but". People might not be using the feature, but it's definitely there and has been there for a long time; saying "unlike in simp" is not correct. I think the issue is that people haven't had much guidance on pre-simp lemmas.

By the way, I once looked into trying to make push_neg operate only on the "spine" of an expression by default. At least pedagogically, it's odd to me that it pushes negations everywhere, even deep within subexpressions. Is this something we would want to look into? Or are we all happy with the push-everything-pushable semantics?

[Tomas Skrivan]

Eric Wieser said:

I think your #generate_linear_map_simps was confusing me, which surely only works for one particular f?

Sorry I didn't explain that well. Yes you have to call #generate_linear_map_simps for every concrete f.

[Damiano Testa]

Kyle Miller said:

By the way, I once looked into trying to make push_neg operate only on the "spine" of an expression by default. At least pedagogically, it's odd to me that it pushes negations everywhere, even deep within subexpressions. Is this something we would want to look into? Or are we all happy with the push-everything-pushable semantics?

I personally have not had the need for this feature. However, if it were implemented, it could follow the congr i syntax, like push_neg 7? Or did want more granular control as a gcongr/congrm pattern match?

[Kyle Miller]

Ah, no, it wouldn't be for the depth, I don't think that would be particularly useful. Imagine that there's a negation in the hypothesis of an implication. Should push_neg affect that hypothesis too? In a workshop, some students found that behavior to be surprising.

It's similar to ring vs ring_nf. The latter does ring normalization everywhere, but the former just applies to the target equality itself.

[Damiano Testa]

Oh, I see, I had not understood the use-case that you mention. I agree that it could be confusing, but I also do not think that I came across the issue.

[Jovan Gerbscheid]

Before looking into it, I expected that push_neg would only push the negation that started at the root of the expression. I think it is like this mostly because it is more tricky to implement, because you would have to keep track of which Not was "pushed" by the tactic, and which was there to begin with.

[Kyle Miller]

Yeah, that's what I ran into in my investigations. It's too convenient using simp.

By the way, something I've wanted to see is for push_neg to be a simple wrapper around simp itself. There should be a user-accessible simproc so that people can write simp [↓pushNeg] or at least a simp set so they can write simp [pushNeg], where the simp set contains the simproc. This would be convenient because then other simp lemmas can be interleaved. It's much more composable than a separate tactic.

[Kyle Miller]

That's not to say that there shouldn't be a push_neg, just that a pushNeg simproc would give flexibility when it's wanted.

[Bolton Bailey]

Thanks for making this! This implements one of the tactics on my wishlist - hopefully you don't mind but I've linked your PR to that issue.

[Jovan Gerbscheid]

@Kyle Miller, great idea, I've added the pushNeg simproc_decl now, which can be used with simp [↓pushNeg].

[Patrick Massot]

Again the main motivation for not using simp was keeping bound variable names.

[Kyle Miller]

@Patrick Massot You mean the motivation for not implementing it as a simp set of simp lemmas, right? With a simproc, bound variable names is not an issue.

[Patrick Massot]

Yes

[Patrick Massot]

I don’t know anything about simproc

[Kyle Miller]

Maybe you're thinking of the Lean 3 implementation of push_neg @Patrick Massot.

When it got ported to Lean 4, Alice Laroche made use of the simp machinery to do the transformation. (With the consequence that the Lean 4 version does push_neg in places that the Lean 3 never did.)

This function has the signature of a simproc. In that last message, Jovan made the simproc be usable in a simp argument list.

[Patrick Massot]

Does it mean the Lean 4 version does not preserve variable names?

[Patrick Massot]

That would be a very bad surprise that will hit me hard in a couple of weeks.

[Kyle Miller]

No, that's the point, simp preserves variable names. It's simp lemmas that don't (yet) preserve variables names, because simp lemmas are applied using unification, and unification doesn't copy binder names.

[Kyle Miller]

A simproc is an arbitrary transformation that can hook into the simp machinery. It can preserve variable names if it wants to (and the pushNeg simproc does)

[Patrick Massot]

I’m asking about the current version of push_neg

[Kyle Miller]

The current version of push_neg, which is implemented using simp since 2022, preserves binder names, as far as I know.

[Patrick Massot]

Ok, great

[Kyle Miller]

(I was telling you about the current version of push_neg for what it's worth.)

[Yury G. Kudryashov]

It would be really nice to have an extensible push_neg in Mathlib! E.g., I often wanted it to support Filter.Eventually/Filter.Frequently.

[Jovan Gerbscheid]

Thanks for the suggestion! In the PR, I have now tagged a bunch of lemmas with push:

push_neg

• Filter.Eventually/Filter.Frequently
• (Set.)Finite/Infinite
• (Set./Finset.)Nonempty/_ = ∅/Empty

• ¬n > 0 -> n = 0 instead of n ≤ 0 when possible (e.g. in Nat) (and similar for 1, ⊤, ⊥)
  This is because n = 0 is generally nicer than n ≤ 0. For the reverse opposite statement, I think it's not clear which form is nicer to use: 0 < n or n ≠ 0.

• x ∉ sᶜ -> x ∈ s

push

I've tagged relevant lemmas for a couple of constants:

• Real.log, which can be used as push (disch := positivity) Real.log
• Set membership: for example push _ ∈ _ rewrites x ∈ {a : p a}ᶜ -> ¬ p x
• Set complement
• -, ⁻¹and ^.
• And, Or, Exists, Forall
• fun, for pushing through + * etc. (Note that these lemmas can't make use of the discrimination tree properly, unless we switch to my RefinedDiscrTree)

[Jovan Gerbscheid]

It is a bit cumbersome to write out names like HPow.hPow, So I extended the notation so that you can provide a pattern, and the tactic will look at the head constant of the pattern. For example, push ∀ _, _, push fun _ ↦ _, push _ ∈ _, push _ ^ _. And push_neg is equivalent to either push Not or push ¬_

[Jovan Gerbscheid]

The PR is getting really big, so should I split it into the following 3 parts?

• add the new implementation of the tactic, without tagging new lemmas
• add tags for many push_neg lemmas
• add tags for many push lemmas

[Jovan Gerbscheid]

Here is the first part as a PR on its own: #21965

[Johan Commelin]

Jovan Gerbscheid said:

It is a bit cumbersome to write out names like HPow.hPow, So I extended the notation so that you can provide a pattern, and the tactic will look at the head constant of the pattern. For example, push ∀ _, _, push fun _ ↦ _, push _ ∈ _, push _ ^ _. And push_neg is equivalent to either push Not or push ¬_

This sounds useful! Do you need the underscores? Or could it be made to work with push ∀ etc...?

[Jovan Gerbscheid]

I could special case some notations like forall, but I don't know how to make that work with all notations.

[Patrick Massot]

I think consistency would be nicer. This syntax is used in other places.

[Kyle Miller]

I'd say let's not try to get token parsing to work — it seems like a nightmare to me, if you were to try to make it use the general term syntax!

[Kyle Miller]

Here's an option though, to let people define tokens one-by-one from outside of push itself:

import Lean

open Lean

declare_syntax_cat push_token
syntax ident : push_token

syntax "push" (ppSpace push_token)? : tactic

open Elab.Command in
elab "declare_push_token " s:str " => " id:ident : command => do
  let n ← liftTermElabM <| Elab.realizeGlobalConstNoOverloadWithInfo id
  let id' : Ident := mkIdentFrom id n (canonical := true)
  let pushNegSyntaxName := mkIdent <| Name.mkSimple s!"pushNegToken_{s}"
  Elab.Command.elabCommand <| ← `(
    syntax (name := $pushNegSyntaxName) $s:str : push_token
    open Lean in
    @[macro $pushNegSyntaxName]
    aux_def $pushNegSyntaxName : Macro := fun stx => `(push_token| $id':ident)
  )

declare_push_token "¬" => Not

[Kyle Miller]

Then it would be the responsibility of the push tactic to do macro expansion of its push_token until it gets an ident.

[Kyle Miller]

Just putting this idea out there. @Patrick Massot's point about consistency with other syntaxes makes sense too. Writing push _ ∈ _ is clear, and push ∈ doesn't look like anything else in Lean.

[Kyle Miller]

Though perhaps push [∈] isn't too out of place, if there are delimiters to contain the seemingly-invalid syntax.

[Jovan Gerbscheid]

Should I also make a PR that changes the name of the PushNeg file to Push, so that the diff in the other PR becomes more useable?

[Michael Rothgang]

Sure, why not? Would be easy to review!

[Jovan Gerbscheid]

#22108

[Jovan Gerbscheid]

I tried to use the binderNameHint gadget to remove the need for special handling of forall and exists in push_neg. However, I found it didn't work for the forall (@Joachim Breitner).
MWE:

import Mathlib

theorem not_forall_eq {α} {s : α → Prop} :
  (¬ ∀ x, s x) ↔ (∃ x, binderNameHint x s (¬ s x)) := not_forall

example : ¬ ∀ n : Nat, n = 0 := by
  rw [not_forall_eq] -- preserves binder name
example : ¬ ∀ n : Nat, n = 0 := by
  simp [not_forall_eq] -- changes binder name to `x`

I think this is a matter of the order of the arguments to isDefEq.

import Qq

open Qq Lean Meta

run_meta do
  let a := q(∀ x : Nat, x = 0)
  let b ← mkFreshExprMVarQ q(Nat → Prop)
  let c := q(∀ y : Nat, $b y)
  withoutModifyingMCtx do
    _ ← isDefEq c a
    logInfo b -- fun y => y = 0
  withoutModifyingMCtx do
    _ ← isDefEq a c
    logInfo b -- fun x => x = 0

[Joachim Breitner]

Yes, indeed, forall is too special in Lean. With exits you can rewrite Exists s and preserve the lambda in s, but with forall, in ∃ x, s x the s is not a manifest lambda from the original goal, so while pattern matching the rewrite lean will eta-expand or something something like that to produce it, and that's where we get the fun x =>:

theorem not_forall_eq {α} {s : α → Prop} :
  (¬ ∀ x, s x) ↔ (∃ x, binderNameHint x s (¬ s x)) := Classical.not_forall

example : ¬ ∀ n : Nat, n = 0 := by
  rw [not_forall_eq] -- preserves binder name


set_option trace.Meta.Tactic.simp true

/--
error: unsolved goals
⊢ ∃ x, ¬x = 0
---
info: [Meta.Tactic.simp.unify] eq_self:1000, failed to unify
      ?a = ?a
    with
      n = 0
[Meta.Tactic.simp.rewrite] not_forall_eq:1000:
      ¬∀ (n : Nat), n = 0
    ==>
      ∃ x, binderNameHint x (fun x => x = 0) ¬x = 0
[Meta.Tactic.simp.unify] eq_self:1000, failed to unify ?a = ?a with x = 0
-/
#guard_msgs in
example : ¬ ∀ n : Nat, n = 0 := by
  simp only [not_forall_eq] -- changes binder name to `x`

Not sure if there is a good way to fix that.