[Merged by Bors] - feat(Tactic.Bound): Add a bound tactic for inequalities by structure#10562
Conversation
|
This PR/issue depends on: |
|
I made two tiny PRs for the two general purpose lemmas, so those can be handled independently. I'll delete them from this one when done, but I don't think it blocks reviewing. |
Ruben-VandeVelde
left a comment
There was a problem hiding this comment.
Neat. A few comments below
jcommelin
left a comment
There was a problem hiding this comment.
A review of the module docstring.
|
Thank for all the comments! Will reply to them soon, but wanted to leave a separate thought here before I forget it. Currently one has to manually map each lemma to the appropriate rule type and priority, but I think this could be mostly automated:
Does that seem reasonable? I can make that refactoring if so, and it would make it way easier to register new bound lemmas. |
|
If this is your manual algorithm wrt applying the priorities to these lemmas, I think this would be most welcome! |
|
Priority selection is automatic now (see This will make it way easier to register lemmas downstream as well, as one doesn't have to think about priorities. |
Can it in fact not call |
|
It can call positivity as a closing tactic, and happy to add that if it seems reasonable, but this can do positivity goals that positivity cannot (in particular |
|
I argued before that Basically I'm trying to decide whether "Run |
|
But if we could extend to handle that kind of thing too, I’d be open to that alternative. My sense from the thread linked in the original post is that there isn’t interest in broadening positivity and gcongr, though. |
|
I just think it would be a shame to have three tools designed to solve basically the same problems. |
|
What’s the standard method of establishing consensus, given that this doesn’t seem to be general current view? (E.g., extending positivity further.) |
|
Talk to Zulip, open an outstandingly good PR, run performance tests... |
PR summary 6aff75ed71
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Tactic | 2144 | 2148 | +4 (+0.19%) |
Import changes for all files
| Files | Import difference |
|---|---|
| There are 2588 files with changed transitive imports: this is too many to display! |
Declarations diff
+ Bound.div_lt_one_of_pos_of_lt
+ Bound.le_self_pow_of_pos
+ Bound.one_lt_div_of_pos_of_lt
+ Bound.pow_le_pow_right_of_le_one_or_one_le
+ Nat.cast_pos_of_pos
+ Nat.one_le_cast_of_le
+ as
+ boundConfig
+ boundLinarith
+ boundNormNum
+ declPriority
+ ineqPriority
+ isZero
+ le_max_of_le_left_or_le_right
+ lt_max_of_lt_left_or_lt_right
+ min_le_of_left_le_or_right_le
+ min_lt_of_left_lt_or_right_lt
+ mul_lt_mul_left_of_pos_of_lt
+ mul_lt_mul_right_of_pos_of_lt
+ rpow_le_rpow_of_exponent_le_or_ge
+ scoreToConfig
+ test_unknown_identifier
+ typePriority
++ le_sqr_add
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.
Code courtesy of Kyle Miller, to fix metavariable bugs.
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
|
How do I kick the CI so that it runs again? This seems transient: |
|
@j-loreaux What's the next step? Should I still wait for the remaining two reviewers? |
|
Now that you've been delegated, you should feel free to merge! In any case, I'm happy with the current status! 🎉 |
|
I think things are okay. Kyle didn't revoke my delegation, so you could merge. But since I'm here: bors merge |
#10562) `bound` proves inequalities that follow "obviously by structure", assuming nonnegativity or positivity of subterms where necessary. It is built on top of Aesop. It has significant overlap with `positivity` and `gcongr`, but can also switch back and forth between those modes (such as when proving `0 < a * b - a * c` from `0 < a`, `c < b`). Zulip discussion: https://leanprover.zulipchat.com/#narrow/stream/239415-metaprogramming-.2F-tactics/topic/.60bound.60.20mixes.20.60gcongr.60.20and.20.60positivity.60/near/412120380
|
bors r- |
|
Canceled. |
|
Oops, I thought CI was successful? |
|
Sorry, I'd missed that the attribute test was broken by the namespace change. Fixed. |
|
@j-loreaux You up for one more merge try? I think I can't do it, since the delegation went away with the new commit. |
|
You should still have it delegated to you; adding commits doesn't remove that as far as I know. Maybe a bors r+ |
#10562) `bound` proves inequalities that follow "obviously by structure", assuming nonnegativity or positivity of subterms where necessary. It is built on top of Aesop. It has significant overlap with `positivity` and `gcongr`, but can also switch back and forth between those modes (such as when proving `0 < a * b - a * c` from `0 < a`, `c < b`). Zulip discussion: https://leanprover.zulipchat.com/#narrow/stream/239415-metaprogramming-.2F-tactics/topic/.60bound.60.20mixes.20.60gcongr.60.20and.20.60positivity.60/near/412120380
|
Pull request successfully merged into master. Build succeeded: |
bound tactic for inequalities by structurebound tactic for inequalities by structure
|
Woohoo, thank you! |
#10562) `bound` proves inequalities that follow "obviously by structure", assuming nonnegativity or positivity of subterms where necessary. It is built on top of Aesop. It has significant overlap with `positivity` and `gcongr`, but can also switch back and forth between those modes (such as when proving `0 < a * b - a * c` from `0 < a`, `c < b`). Zulip discussion: https://leanprover.zulipchat.com/#narrow/stream/239415-metaprogramming-.2F-tactics/topic/.60bound.60.20mixes.20.60gcongr.60.20and.20.60positivity.60/near/412120380
#10562) `bound` proves inequalities that follow "obviously by structure", assuming nonnegativity or positivity of subterms where necessary. It is built on top of Aesop. It has significant overlap with `positivity` and `gcongr`, but can also switch back and forth between those modes (such as when proving `0 < a * b - a * c` from `0 < a`, `c < b`). Zulip discussion: https://leanprover.zulipchat.com/#narrow/stream/239415-metaprogramming-.2F-tactics/topic/.60bound.60.20mixes.20.60gcongr.60.20and.20.60positivity.60/near/412120380
#10562) `bound` proves inequalities that follow "obviously by structure", assuming nonnegativity or positivity of subterms where necessary. It is built on top of Aesop. It has significant overlap with `positivity` and `gcongr`, but can also switch back and forth between those modes (such as when proving `0 < a * b - a * c` from `0 < a`, `c < b`). Zulip discussion: https://leanprover.zulipchat.com/#narrow/stream/239415-metaprogramming-.2F-tactics/topic/.60bound.60.20mixes.20.60gcongr.60.20and.20.60positivity.60/near/412120380
boundproves inequalities that follow "obviously by structure", assuming nonnegativity or positivity of subterms where necessary. It is built on top of Aesop. It has significant overlap withpositivityandgcongr, but can also switch back and forth between those modes (such as when proving0 < a * b - a * cfrom0 < a,c < b).Zulip discussion: https://leanprover.zulipchat.com/#narrow/stream/239415-metaprogramming-.2F-tactics/topic/.60bound.60.20mixes.20.60gcongr.60.20and.20.60positivity.60/near/412120380
Here's an initial implementation of the
boundtactic discussed on Zulip, upstreamed from https://github.com/girving/ray/blob/main/Ray/Tactic/Bound.lean. Happy to do whatever cleanup or further testing is deemed useful. Some notes:mul_inv_le_one_of_nonneg_of_leandReal.pi_nonnegshould probably be moved to their appropriate places, but I wanted to check first.le_self_pow_of_posis a wart due toboundnot knowing what to do withn ≠ 0goals. One option would be givebounda rule forNat.pos_iff_ne_zero, so thatn ≠ 0automatically turns into0 < n.Bound.leancurrently importsMathlib.Analysis.Analytic.Basicjust to addr_posas a forward rule. If this rule is reasonable it would of course be better to move that toMathlib.Analysis.Analytic.Basicto remove the heavy import.