Skip to content

feat(Positivity): add support for positivity [h₁, h₂] syntax #30388

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 17 commits into
base: master
Choose a base branch
from
+22 −2
Open

feat(Positivity): add support for positivity [h₁, h₂] syntax #30388

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
17 commits
Select commit Hold shift + click to select a range
d0f4c1e
feat: add support for `positivity [h₁, h₂]` syntax
HugLycan Oct 9, 2025
79df7ee
Merge branch 'master' into feat/positivity-with-hyps
HugLycan Oct 9, 2025
7026c48
Merge branch 'leanprover-community:master' into feat/positivity-with-…
HugLycan Oct 10, 2025
0e2adb3
Merge branch 'leanprover-community:master' into feat/positivity-with-…
HugLycan Oct 10, 2025
a68f22c
add doc-strings to `positivity [_,,]`
HugLycan Oct 10, 2025
7c36ff8
Merge branch 'feat/positivity-with-hyps' of https://github.com/HugLyc…
HugLycan Oct 10, 2025
1c67d0f
Merge branch 'master' into feat/positivity-with-hyps
HugLycan Oct 10, 2025
eb0e068
Merge branch 'master' into feat/positivity-with-hyps
HugLycan Oct 10, 2025
12a540e
just make it nicer
HugLycan Oct 10, 2025
e30f668
Merge branch 'feat/positivity-with-hyps' of https://github.com/HugLyc…
HugLycan Oct 10, 2025
4a78394
Merge branch 'master' into feat/positivity-with-hyps
HugLycan Oct 10, 2025
b81ce6a
Update MathlibTest/positivity.lean
HugLycan Oct 10, 2025
c293b26
Update Core.lean
HugLycan Oct 11, 2025
71bf2ed
Update Mathlib/Tactic/Positivity/Core.lean
HugLycan Oct 15, 2025
3b8b131
Merge branch 'master' into feat/positivity-with-hyps
HugLycan Oct 15, 2025
30532c2
update `positivity []`
HugLycan Oct 16, 2025
1387869
Merge branch 'master' into feat/positivity-with-hyps
HugLycan Oct 16, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
16 changes: 14 additions & 2 deletions Mathlib/Tactic/Positivity/Core.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -491,18 +491,30 @@ according to the syntax of the expression `x`, if the atoms composing the expres
numeric lower bounds which can be proved positive/nonnegative/nonzero by `norm_num`. This tactic
either closes the goal or fails.
`positivity [t₁, …, tₙ]` first executes `have := t₁; …; have := tₙ` in the current goal,
then runs `positivity`. This is useful when `positivity` needs derived premises such as `0 < y`
for division/reciprocal, or `0 ≤ x` for real powers.
Examples:
```
example {a : ℤ} (ha : 3 < a) : 0 ≤ a ^ 3 + a := by positivity
example {a : ℤ} (ha : 1 < a) : 0 < |(3:ℤ) + a| := by positivity
example {b : ℤ} : 0 ≤ max (-3) (b ^ 2) := by positivity
example {a b c d : ℝ} (hab : 0 < a * b) (hb : 0 ≤ b) (hcd : c < d) :
0 < a ^ c + 1 / (d - c) := by
positivity [sub_pos_of_lt hcd, pos_of_mul_pos_left hab hb]
```
-/
elab (name := positivity) "positivity" : tactic => do
liftMetaTactic fun g => do Meta.Positivity.positivity g; pure []
syntax (name := positivity) "positivity" (" [" term,* "]")? : tactic

elab_rules : tactic
| `(tactic| positivity $[[]]?) => liftMetaTactic fun g => do Meta.Positivity.positivity g; pure []
Copy link
Collaborator

@thorimur thorimur Oct 16, 2025 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Sorry, my bad, I should have been less ambiguous: I only meant to test the behavior of positivity [] in the test file, not test for the case of [] in this syntax! :) (And I see you've added that test, so thanks!)

So, we are indeed okay with

Suggested change
| `(tactic| positivity $[[]]?) => liftMetaTactic fun g => do Meta.Positivity.positivity g; pure []
| `(tactic| positivity) => liftMetaTactic fun g => do Meta.Positivity.positivity g; pure []

The reason why this is okay after the earlier suggestion to use · ($[have := $h];*); positivity instead of · $[have := $h];*; positivity is indeed unintuitive; I'll explain it in a bit more depth here. :)

Writing · (); positivity directly in source, e.g. example : 0 ≤ 0 := by · (); positivity is indeed not parsed as we'd want it to be. This is due to how tactic sequences are parsed, and the parser avoids parsing an empty tactic sequence in this context.

But macro_rules take Syntax to Syntax (the result of parsing). We're defining the outcome of our macro rule using syntax quotations ( `()), which do their parsing at elaboration time, i.e. in this file, before the macro_rule is even registered and sent off to be used.

So the parsing of `(tactic| · ($[have := $h];*); positivity) into Syntax is already complete before the rule is recorded, and this syntax is sufficiently structured to know that a tactic sequence is what will end up inside (). When we apply this macro rule later, it will happily insert the tactic sequence $[have := $h];* inside the abstract syntax for ()—even if that sequence is empty.

Parsing into Syntax was what was preventing the source code version of · (); positivity from working, but we've gotten through that step by the time we apply a macro_rule. :)

(It's very verbose, but you could write

whatsnew in macro_rules
| `(tactic| positivity [$h,*]) => `(tactic| · ($[have := $h];*); positivity)

to see the definition it creates—not to read the individual parts, but just to see that the rule we've actually recorded is really a bunch of Syntax, not source code.)

Also, for some peace of mind that this is what's going on, you can write

elab_rules : tactic
| `(tactic| positivity $[[]%$tk]?) => do
  logInfo "got {tk}"
  liftMetaTactic fun g => do Meta.Positivity.positivity g; pure []

and see that even when matching [] in the elab_rules, we log got none (instead of got some []). The macro gets there first. :)

This is a bit of a crash course, so I've rushed through some things. Feel free to tag or DM me (Thomas Murrills) on Zulip if you have any more questions; as might be apparent, I really enjoy talking about metaprogramming, so I'd be happy to answer them. :)


macro_rules
| `(tactic| positivity [$h,*]) => `(tactic| · ($[have := $h];*); positivity)
end Positivity
Comment on lines +516 to 518
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Apologies, github ate this newline. :)

Suggested change
macro_rules
| `(tactic| positivity [$h,*]) => `(tactic| · ($[have := $h];*); positivity)
end Positivity
macro_rules
| `(tactic| positivity [$h,*]) => `(tactic| · ($[have := $h];*); positivity)
end Positivity


end Mathlib.Tactic
Expand Down
8 changes: 8 additions & 0 deletions MathlibTest/positivity.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -100,6 +100,9 @@ example {a b : ℤ} (h : 0 ≤ a + b) : 0 ≤ a + b := by positivity

example {a : ℤ} (hlt : 0 ≤ a) (hne : a ≠ 0) : 0 < a := by positivity

example {a b c d : ℤ} (ha : c < a) (hb : d < b) : 0 < (a - c) * (b - d) := by
positivity [sub_pos_of_lt ha, sub_pos_of_lt hb]

section

variable [Field α] [LinearOrder α] [IsStrictOrderedRing α]
Expand Down Expand Up @@ -334,6 +337,11 @@ example {a : ℝ≥0∞} : 0 < a ^ 0 := by positivity
example {a : ℝ≥0∞} {b : ℝ} (ha : 0 < a) (hat : a ≠ ⊤) : 0 < a ^ b := by positivity
example {a : ℝ} : 0 < a ^ 0 := by positivity

example {a : ℝ≥0∞} {b : ℝ} (ha : 0 < a) (hat : a ≠ ⊤) : 0 < a ^ b := by positivity []
example {a b c d : ℝ} (hab : 0 < a * b) (hb : 0 ≤ b) (hcd : c < d) :
0 < a ^ c + 1 / (d - c) := by
positivity [sub_pos_of_lt hcd, pos_of_mul_pos_left hab hb]

example {a : ℤ} (ha : 3 < a) : 0 ≤ a ^ 2 + a := by positivity
example {a : ℤ} (ha : 3 < a) : 0 ≤ a ^ 3 + a := by positivity
example {a : ℤ} (ha : 3 < a) : 0 < a ^ 2 + a := by positivity
Expand Down