[Merged by Bors] - feat: extensible `push` and `pull` tactics by JovanGerb · Pull Request #21965 · leanprover-community/mathlib4

JovanGerb · 2025-02-16T22:36:46Z

This PR defines the push and pull tactics, and makes push_neg a macro for push Not. The tactics are also available in conv mode.

For tagging, there is only the @[push] attribute, which adds the reverse rewrite for the pull tactic when relevant. In the future, we may also need a separate @[pull X] attribute for pulling X.

Thanks to this change, we will be able to make push_neg into a more powerful tactic by tagging more lemmas. It also means that about 60 files now don't need to import LinearOrder/PartialOrder. This will be especially useful when we get the @[to_dual] attribute.

This work originally started in #21769. There is now the follow up PR #29000 which adds push tags and tests for them.

The @[push] attribute is defined in Mathlib.Tactic.Push.Attr and the main implementation of push and pull is in Mathlib.Tactic.Push.

Some proofs need to be fixed because the new simp-based push_neg can see through more reducible definitions.

Zulip conversation: #mathlib4 > I made an extensible `push` tactic generalizing `push_neg`

closes #21841

github-actions · 2025-02-16T22:37:43Z

PR summary ea6c1124c8

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Tactic.Push	88	76	-12 (-13.64%)

Import changes for all files

Files	Import difference
There are 6451 files with changed transitive imports taking up over 278132 characters: this is too many to display!
You can run `scripts/import_trans_difference.sh all` locally to see the whole output.

Declarations diff

+ Head
+ Head.ofExpr?
+ Head.toString
+ PullTheorem
+ elabDischarger
+ elabHead
+ elabPushTree
+ instance : ToString Head := ⟨Head.toString⟩
+ isPullThm
+ log_abs
+ log_mul
+ nonempty_iff_empty_ne
+ not_exists
+ not_imp
+ not_le
+ not_not
+ pullCore
+ pullStep
+ pushCore
+ pushSimpConfig
+ pushStep
+ resolvePushId?
+-+ not_iff
- elabPushNegConv
- empty_ne_eq_nonempty
- ne_empty_eq_nonempty
- not_exists_eq
- not_ge_eq
- not_gt_eq
- not_implies_eq
- not_le_eq
- not_lt_eq
- not_ne_eq
- not_nonempty_eq
- not_not_eq
- not_or_eq
- pushNegCore
- transformNegationStep

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

JovanGerb · 2025-02-16T22:40:32Z

What should I do with the copyright docstring at the top of these files? I added myself as the main author, set the year to 2025, and left the names which were there in the original file.

grunweg · 2025-02-17T08:12:42Z

What should I do with the copyright docstring at the top of these files? I added myself as the main author, set the year to 2025, and left the names which were there in the original file.

Adding yourself as an author and leaving the original authors sounds good. Please leave the year as it was.

JovanGerb · 2025-02-18T02:46:17Z

!bench

leanprover-bot · 2025-02-18T03:17:16Z

Here are the benchmark results for commit 13affdb.
There were no significant changes against commit 6b9635f.

github-actions · 2025-02-18T03:17:49Z

File	Instructions	%
`build`	+28.471⬝10⁹	(+0.01%)
CI run

This PR renames the file `PushNeg.lean` to `Push.lean`, to help reviewing #21965. It also removes an import of PushNeg where it is already transitively imported

Mathlib/Tactic/Push.lean

Co-authored-by: grunweg <[email protected]>

JovanGerb · 2025-09-20T09:56:39Z

Thanks for the reviews!

For the Polynomial.coeff example, it should definitelly be possible to turn coeff (X ^ 2 + 3 * X) 1 into something like (if 1 = 2 then 1 else 0) + 3 * 1. The issue is that you will need to do some simplification afterwards, so I think you might be better off just using simp.

Mathlib/Data/Set/Basic.lean

adomani · 2025-09-21T11:17:08Z

I agree that simp could also achieve this, but I was more wondering whether pushCoeff could be a part of the compute_degree implementation, combined with some further norm_num/restricted simp call. Anyway, just an idea!

adomani · 2025-09-21T11:17:57Z

Ok, I think that this is probably the last extension that I will ask about push: would you mind adding tests for the #push ..., #pull ... and #push_discr_tree ... commands?

JovanGerb · 2025-09-22T15:31:21Z

I didn't put the command #push_discr_tree Not into the test file, because I think this will be annoying to update when tagging more push_neg lemmas. However, looking at the output made me realize that some @[push] tags that I added weren't supposed to be there, so I've removed them now.

JovanGerb · 2025-09-22T15:46:37Z

For a tactic that computes Polynomial.coeff, if you want to restrict your simp to a simp only, then you could indeed define a pushCoeff simproc to be an argument to the simp only. We can make a pushFoo simproc for any constant Foo where that is deemed useful, similar to pushNeg and pushFun.

adomani

I like the new tests, thanks! I also have a couple more that I just noticed...

I do not have a feeling for how much the #push_discr_tree test will cause issues. If it turns out to be quite fussy, there is always the option of commenting it out, while we think of an alternative.

Thank you for your patience through the various reviews!

bors d+

Mathlib/Data/Set/Basic.lean

Mathlib/Tactic/Push.lean

mathlib-bors · 2025-09-22T18:39:34Z

✌️ JovanGerb can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

JovanGerb · 2025-09-22T19:56:36Z

I forgot about the fact that I removed the pushNeg simproc, because the relevant lemmas tend to already be tagged with simp, so the simproc doesn't really add to what simp can already do. Do you think I should still add it?

For the pushFun simproc I have a test in the follow-up PR.

adomani · 2025-09-22T20:05:16Z

Ok, let's remove the pushNeg simproc, as adding it later is straightforward.

Thanks!

JovanGerb · 2025-09-22T22:39:36Z

bors r+

This PR defines the `push` and `pull` tactics, and makes `push_neg` a macro for `push Not`. The tactics are also available in `conv` mode. For tagging, there is only the `@[push]` attribute, which adds the reverse rewrite for the `pull` tactic when relevant. In the future, we may also need a separate `@[pull X]` attribute for pulling `X`. Thanks to this change, we will be able to make `push_neg` into a more powerful tactic by tagging more lemmas. It also means that about 60 files now don't need to import `LinearOrder`/`PartialOrder`. This will be especially useful when we get the `@[to_dual]` attribute. This work originally started in #21769. There is now the follow up PR #29000 which adds `push` tags and tests for them. The `@[push]` attribute is defined in `Mathlib.Tactic.Push.Attr` and the main implementation of `push` and `pull` is in `Mathlib.Tactic.Push`. Some proofs need to be fixed because the new simp-based `push_neg` can see through more reducible definitions. Zulip conversation: [#mathlib4 > I made an extensible `push` tactic generalizing `push_neg`](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/I.20made.20an.20extensible.20.60push.60.20tactic.20generalizing.20.60push_neg.60) closes #21841

mathlib-bors · 2025-09-22T22:42:47Z

Build failed:

CI Success

bryangingechen · 2025-09-23T03:06:48Z

I think this only failed due to a runner having a bad setup (which should be fixed now).
bors r+

This PR defines the `push` and `pull` tactics, and makes `push_neg` a macro for `push Not`. The tactics are also available in `conv` mode. For tagging, there is only the `@[push]` attribute, which adds the reverse rewrite for the `pull` tactic when relevant. In the future, we may also need a separate `@[pull X]` attribute for pulling `X`. Thanks to this change, we will be able to make `push_neg` into a more powerful tactic by tagging more lemmas. It also means that about 60 files now don't need to import `LinearOrder`/`PartialOrder`. This will be especially useful when we get the `@[to_dual]` attribute. This work originally started in #21769. There is now the follow up PR #29000 which adds `push` tags and tests for them. The `@[push]` attribute is defined in `Mathlib.Tactic.Push.Attr` and the main implementation of `push` and `pull` is in `Mathlib.Tactic.Push`. Some proofs need to be fixed because the new simp-based `push_neg` can see through more reducible definitions. Zulip conversation: [#mathlib4 > I made an extensible `push` tactic generalizing `push_neg`](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/I.20made.20an.20extensible.20.60push.60.20tactic.20generalizing.20.60push_neg.60) closes #21841

mathlib-bors · 2025-09-23T03:46:31Z

Pull request successfully merged into master.

Build succeeded:

CI Success

This PR defines the `push` and `pull` tactics, and makes `push_neg` a macro for `push Not`. The tactics are also available in `conv` mode. For tagging, there is only the `@[push]` attribute, which adds the reverse rewrite for the `pull` tactic when relevant. In the future, we may also need a separate `@[pull X]` attribute for pulling `X`. Thanks to this change, we will be able to make `push_neg` into a more powerful tactic by tagging more lemmas. It also means that about 60 files now don't need to import `LinearOrder`/`PartialOrder`. This will be especially useful when we get the `@[to_dual]` attribute. This work originally started in leanprover-community#21769. There is now the follow up PR leanprover-community#29000 which adds `push` tags and tests for them. The `@[push]` attribute is defined in `Mathlib.Tactic.Push.Attr` and the main implementation of `push` and `pull` is in `Mathlib.Tactic.Push`. Some proofs need to be fixed because the new simp-based `push_neg` can see through more reducible definitions. Zulip conversation: [#mathlib4 > I made an extensible &leanprover-community#96;push&leanprover-community#96; tactic generalizing &leanprover-community#96;push_neg&leanprover-community#96;](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/I.20made.20an.20extensible.20.60push.60.20tactic.20generalizing.20.60push_neg.60) closes leanprover-community#21841

JovanGerb added 3 commits February 16, 2025 21:28

feat: extensible push(_neg) tactic - part 1

127bd7c

ne_eq rewrite can be done with just the lemma.

087e853

feat: debug command #push_discr_tree

193e473

github-actions bot added the large-import Automatically added label for PRs with a significant increase in transitive imports label Feb 16, 2025

JovanGerb added the t-meta Tactics, attributes or user commands label Feb 16, 2025

JovanGerb added 2 commits February 18, 2025 02:44

fix

7ca6ef6

.

13affdb

leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 18, 2025

JovanGerb added 3 commits February 19, 2025 22:09

undo changes to help merge

23fb858

Merge remote-tracking branch 'origin' into push_tactic

b5bb0f9

redo change to import (after merge)

3f49992

github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 19, 2025

.

4a45e44

JovanGerb mentioned this pull request Feb 19, 2025

[Merged by Bors] - chore: rename PushNeg.lean to Push.lean #22108

Closed

.

c7b0f34

leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 20, 2025

JovanGerb added 2 commits February 20, 2025 12:07

Merge remote-tracking branch 'origin' into push_tactic

ec6adea

.

18d7166

github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 20, 2025

grunweg reviewed Feb 20, 2025

View reviewed changes

Mathlib/Tactic/Push.lean Outdated Show resolved Hide resolved

typo

9414b7e

Co-authored-by: grunweg <[email protected]>

grunweg mentioned this pull request Apr 5, 2025

feat: extensible push_neg tactic #21769

Closed

1 task

Merge branch 'master' into push_tactic

9e6deb9

.

c787fed

adomani reviewed Sep 21, 2025

View reviewed changes

Mathlib/Data/Set/Basic.lean Show resolved Hide resolved

JovanGerb added 2 commits September 22, 2025 17:27

remove wrong @[push] annotations

a97d0ff

use commands in test file

5daa58e

adomani reviewed Sep 22, 2025

View reviewed changes

Mathlib/Data/Set/Basic.lean Show resolved Hide resolved

Mathlib/Tactic/Push.lean Show resolved Hide resolved

ghost added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Sep 22, 2025

minor refactor

ebba7ac

Merge branch 'master' into push_tactic

f546121

ghost added the ready-to-merge This PR has been sent to bors. label Sep 23, 2025

mathlib-bors bot changed the title ~~feat: extensible push and pull tactics~~ [Merged by Bors] - feat: extensible push and pull tactics Sep 23, 2025

mathlib-bors bot closed this Sep 23, 2025

mathlib-bors bot deleted the push_tactic branch September 23, 2025 03:46

Conversation

JovanGerb commented Feb 16, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Feb 16, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary ea6c1124c8

Import changes for modified files

Declarations diff

Uh oh!

JovanGerb commented Feb 16, 2025

Uh oh!

grunweg commented Feb 17, 2025

Uh oh!

JovanGerb commented Feb 18, 2025

Uh oh!

leanprover-bot commented Feb 18, 2025

Uh oh!

github-actions bot commented Feb 18, 2025

Uh oh!

Uh oh!

JovanGerb commented Sep 20, 2025

Uh oh!

Uh oh!

adomani commented Sep 21, 2025

Uh oh!

adomani commented Sep 21, 2025

Uh oh!

JovanGerb commented Sep 22, 2025

Uh oh!

JovanGerb commented Sep 22, 2025

Uh oh!

adomani left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

mathlib-bors bot commented Sep 22, 2025

Uh oh!

JovanGerb commented Sep 22, 2025

Uh oh!

adomani commented Sep 22, 2025

Uh oh!

JovanGerb commented Sep 22, 2025

Uh oh!

mathlib-bors bot commented Sep 22, 2025

Uh oh!

bryangingechen commented Sep 23, 2025

Uh oh!

mathlib-bors bot commented Sep 23, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

10 participants

JovanGerb commented Feb 16, 2025 •

edited

Loading

github-actions bot commented Feb 16, 2025 •

edited

Loading