feat: extensible `push_neg` tactic by JovanGerb · Pull Request #21769 · leanprover-community/mathlib4

JovanGerb · 2025-02-12T03:41:15Z

This was started by point (3) of https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Possible.20improvements.20to.20Lean.2FMathlib/near/499085779

To be able to use push_neg more generally, this PR reimplements the tactic so that it is extensible. So, users can tag lemmas to be used by push_neg.

This PR tags lemmas concerning empty/nonempty, subsingleton/nontrivial, and finite/infinite to be used in push_neg.

Additionally, the tactic is extended to be able to push any constant that you want to push, and push_neg is now a macro for push Not. So far, I've tried to add lemmas for pushing Real.log. I could imagine it could also be used for Real.exp, pow, mul, smul, or even Set.mem. (the Set.mem lemmas are mostly tagged with @[simp] already, but push_mem could be more readable than simp or dsimp). Or a combination of pushing Not and Set.compl could be useful.

The implementation is with the simp infrastructure, but instead of using post lemmas, like in simp, push uses pre lemmas, so we rewrite each expression before its subterms are rewritten. This is a more efficient way to "push" constants recursively. Most lemmas are added via the @[push] attribute, but a few cases require some special handling, so they are implemented "by hand" in a simproc that is tried after the push lemmas.

For example the simproc simplifies ¬∀ n, p ⇨ ∃ n, ¬p, but, this is overridden by the push lemma that rewrites ¬(p → q) ⇨ p ∧ ¬q (which doesn't apply at every forall)

depends on: [Merged by Bors] - feat: extensible push and pull tactics #21965

github-actions · 2025-02-12T03:42:16Z

PR summary a7bfbd40d3

Import changes exceeding 2%

%	File
+3.48%	`Mathlib.Algebra.Group.Pi.Basic`
+5.56%	`Mathlib.Logic.IsEmpty`
+2.70%	`Mathlib.Logic.Nontrivial.Defs`
+2.22%	`Mathlib.Order.Defs.LinearOrder`

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Tactic.PushNeg	62	0	-62 (-100.00%)
Mathlib.Tactic.Contrapose	63	45	-18 (-28.57%)
Mathlib.Tactic.ByContra	64	46	-18 (-28.12%)
Mathlib.Logic.IsEmpty	72	76	+4 (+5.56%)
Mathlib.Algebra.Group.Pi.Basic	115	119	+4 (+3.48%)
Mathlib.Tactic.Common	241	239	-2 (-0.83%)

Import changes for all files

Files	Import difference
There are 5500 files with changed transitive imports taking up over 232079 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.isHeadOf
+ Nat.not_nonneg_iff_eq_zero
+ PushSimpConfig
+ elabHead
+ elabPush
+ elabPushConv
+ mem_compl
+ nonempty_iff_empty_ne'
+ not_finite
+ not_imp
+ not_not
+ not_one_lt_iff_eq_one
+ not_zero_lt_iff
+ pushCore
+ pushStep
++ nonempty_iff_empty_ne
+-+ not_iff
- elabPushNegConv
- empty_ne_eq_nonempty
- ne_empty_eq_nonempty
- 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).

grunweg · 2025-02-12T08:53:46Z

Thanks a lot for starting this discussion! I for one believe a push_neg attribute would be rather nice (but I don't know how hard this would make it to write this tactic).

Mathlib/Tactic/Push.lean

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

mathlib4-dependent-issues-bot · 2025-09-23T04:29:10Z

This PR/issue depends on:

~~[Merged by Bors] - feat: extensible push and pull tactics #21965~~
By Dependent Issues (🤖). Happy coding!

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

feat: let push_neg replace ¬Finite with Infinite

1f2c20c

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

JovanGerb added 5 commits February 12, 2025 04:11

fixes

10ff78e

fix

e219fb4

fix

c1b535d

fixes

5cd85a9

fix & clean up some proofs

613fb41

JovanGerb added 10 commits February 12, 2025 23:46

feat: extensible push tactic generalizing push_neg

a914490

move location of files

cf513e4

allow for backwards lemmas

cf24af5

add the push tag to various lemmas

836671e

add a discharger option

9e015aa

test for conv mode

7e1d6f6

rename to Lemmas.lean

d9ea2a9

now use the improved tactic

05864c1

fix

e128f2b

fix

e5992e3

JovanGerb changed the title ~~feat: let push_neg replace ¬Finite with Infinite~~ feat: extenisble push_neg tactic Feb 13, 2025

JovanGerb added 8 commits February 13, 2025 06:31

restore assert_not_exists

8039176

define attribute before tactic, to reduce import size

c4fe9e8

add docstrings

ffb7970

delete Lemmas.lean

1d7e441

add comment about loop

f6ed5ae

shake update

cb24e95

remove unneeded import

7b8de76

move content from Basic.lean to Push.lean

b0e1f42

adomani reviewed Feb 13, 2025

View reviewed changes

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

doc

a1c8071

JovanGerb added 18 commits February 15, 2025 18:18

tag lemmas about mem_insert and mem_singleton

53c45ef

more tests

c4dc45c

better syntax for notational constants, and push_neg for Filter

1b69d95

push_neg for ¬0 < a -> a = 0

f414831

.

9c51ef5

some fixes

6359b0a

add not_nonneg_iff_eq_zero for Nat

38776f9

Merge remote-tracking branch 'upstream' into push_neg-Finite

7fbf46e

.

3356ee3

fixes

4b8cd19

tag Finset.not_mem_compl

1c1531e

fix

510fe91

fix elaborator

37dcb9a

fix

78b8652

fix

637dfa9

fix

7bb1352

add not_zero_lt_iff

5254bd3

update noshake

a7bfbd4

JovanGerb mentioned this pull request Feb 16, 2025

[Merged by Bors] - feat: extensible push and pull tactics #21965

Closed

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 17, 2025

mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Apr 5, 2025

mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Sep 23, 2025

JovanGerb closed this Sep 23, 2025

YaelDillies deleted the push_neg-Finite branch October 13, 2025 07:55

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: extensible `push_neg` tactic#21769

feat: extensible `push_neg` tactic#21769
JovanGerb wants to merge 55 commits intomasterfrom
push_neg-Finite

JovanGerb commented Feb 12, 2025 •

edited by grunweg

Loading

Uh oh!

github-actions bot commented Feb 12, 2025 •

edited

Loading

Import changes for modified files

Declarations diff

Uh oh!

grunweg commented Feb 12, 2025

Uh oh!

Uh oh!

mathlib4-dependent-issues-bot commented Sep 23, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

Conversation

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

Uh oh!

Uh oh!

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

Uh oh!

PR summary a7bfbd40d3

Import changes for modified files

Declarations diff

Uh oh!

grunweg commented Feb 12, 2025

Uh oh!

Uh oh!

mathlib4-dependent-issues-bot commented Sep 23, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

JovanGerb commented Feb 12, 2025 •

edited by grunweg

Loading

github-actions bot commented Feb 12, 2025 •

edited

Loading