[Merged by Bors] - refactor(Tactic/Positivity): use stricter Qq matching #10196
Conversation
The previous code often discarded the safety features of Qq by casting quoted terms to `Expr` and back. This is far from an exhaustive replacement.
leanprover-community-mathlib4-bot
added
the
blocked-by-other-PR
leanprover-community-mathlib4-bot
removed
the
blocked-by-other-PR
|
!bench |
|
Here are the benchmark results for commit 4162ad4. |
eric-wieser
added
awaiting-review
leanprover-community-mathlib4-bot
added
the
merge-conflict
|
Sorry, the conflicts are from me moving the extensions around. |
leanprover-community-mathlib4-bot
added
blocked-by-other-PR
leanprover-community-mathlib4-bot
removed
the
merge-conflict
| | .nonnegative _pa => | ||
| pure .none | ||
| | .none => | ||
| pure .none |
There was a problem hiding this comment.
| | .nonnegative _pa => | |
| pure .none | |
| | .none => | |
| pure .none | |
| | _ => pure .none |
There was a problem hiding this comment.
I'd prefer to keep this change focused on the match changes and nothing more (these lines vanish from the diff once you ignore whitespace).
|
Let's get this done. (and thanks for always being a step ahead, I was just wondering what happened to that universe match issue) maintainer merge |
|
maintainer merge |
|
🚀 Pull request has been placed on the maintainer queue by eric-wieser. |
leanprover-community-mathlib4-bot
added
the
merge-conflict
leanprover-community-mathlib4-bot
added
blocked-by-other-PR
| @@ -350,29 +350,29 @@ open Lean Meta Qq | |||
|
|
|||
| /-- Extension for the `positivity` tactic: exponentiation by a real number is positive (namely 1) | |||
| when the exponent is zero. The other cases are done in `evalRpow`. -/ | |||
| @[positivity (_ : ℝ) ^ (0 : ℝ), Pow.pow (_ : ℝ) (0 : ℝ), Real.rpow (_ : ℝ) (0 : ℝ)] | |||
There was a problem hiding this comment.
The changes to this line are why I marked a dependency on #10344
| def evalNNRealSqrt : PositivityExt where eval {u α} _zα _pα e := do | ||
| match u, α, e with | ||
| | 0, ~q(NNReal), ~q(NNReal.sqrt $a) => | ||
| let ra ← core q(inferInstance) q(inferInstance) a |
There was a problem hiding this comment.
| let ra ← core q(inferInstance) q(inferInstance) a | |
| let ra ← core q(inferInstance) q(inferInstance) a |
| let ra ← core zα' pα' a | ||
| match ra with | ||
| | .positive pa => | ||
| assertInstancesCommute |
There was a problem hiding this comment.
Sometimes you write assertInstancesCommute before the match, sometimes after. Is there a reason for this (that you can document somewhere easily found)?
There was a problem hiding this comment.
All that matters is the position of the assertInstancesCommute/assumeInstancesCommute wrt the inferInstances. In fact, all that matters is that there's no inferInstance not followed by assertInstancesCommute/assumeInstancesCommute before a q() quotation. This is something that's automatically checked by the Qq quotations as you write the code.
The only slight difference is that assertInstancesCommute actually checks that the instance diamonds are defeq, while assumeInstancesCommute simply assumes they are (hence has epsilon performance cost). Hence running assertInstancesCommute before a match that could potentially result in no strictness being found is slightly wasteful.
|
✌️ eric-wieser can now approve this pull request. To approve and merge a pull request, simply reply with |
leanprover-community-mathlib4-bot
added
delegated
and removed
awaiting-review
leanprover-community-mathlib4-bot
removed
the
blocked-by-other-PR
|
This PR/issue depends on: |
|
bors merge |
The previous code often discarded the safety features of Qq by casting quoted terms to `Expr` and back. This is far from an exhaustive replacement. This makes use of a bug fix in Lean 4.6.0rc1 that allows us to write things like ```lean match u, α, e with | 0, ~q(ℤ), ~q(@int.floor $α' $i $j $a) => ``` Previously these `match`es did not generalize `u` correctly. To make Qq happy, we introduce a few more `assertInstancesCommute` that were not previously here. Without them, there is a higher risk that `positivity` produces an ill-typed proof in weird situations. Like every `assertInstancesCommute`, this comes at a small performance cost that could be eliminated by using the unsafe `assumeInstancesCommute` instead. Another very small performance hit here is from the (possibly unnecessary) defeq check of the types before checking defeq of the values. On the other hand, this might actually increase performance when the match fails due to a type mismatch. There is probably some boilerplate that can be extracted from the repetition here; but I am declaring that out of scope for this PR: the goal is to establish a canonical spelling for this sort of matching, so that future extensions copy-pasted from these extensions inherit the spelling automatically.
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
The previous code often discarded the safety features of Qq by casting quoted terms to `Expr` and back. This is far from an exhaustive replacement. This makes use of a bug fix in Lean 4.6.0rc1 that allows us to write things like ```lean match u, α, e with | 0, ~q(ℤ), ~q(@int.floor $α' $i $j $a) => ``` Previously these `match`es did not generalize `u` correctly. To make Qq happy, we introduce a few more `assertInstancesCommute` that were not previously here. Without them, there is a higher risk that `positivity` produces an ill-typed proof in weird situations. Like every `assertInstancesCommute`, this comes at a small performance cost that could be eliminated by using the unsafe `assumeInstancesCommute` instead. Another very small performance hit here is from the (possibly unnecessary) defeq check of the types before checking defeq of the values. On the other hand, this might actually increase performance when the match fails due to a type mismatch. There is probably some boilerplate that can be extracted from the repetition here; but I am declaring that out of scope for this PR: the goal is to establish a canonical spelling for this sort of matching, so that future extensions copy-pasted from these extensions inherit the spelling automatically.
The previous code often discarded the safety features of Qq by casting quoted terms to
Exprand back. This is far from an exhaustive replacement.This makes use of a bug fix in Lean 4.6.0rc1 that allows us to write things like
Previously these
matches did not generalizeucorrectly.To make Qq happy, we introduce a few more
assertInstancesCommutethat were not previously here.Without them, there is a higher risk that
positivityproduces an ill-typed proof in weird situations.Like every
assertInstancesCommute, this comes at a small performance cost that could be eliminated by using the unsafeassumeInstancesCommuteinstead.Another very small performance hit here is from the (possibly unnecessary) defeq check of the types before checking defeq of the values. On the other hand, this might actually increase performance when the match fails due to a type mismatch.
There is probably some boilerplate that can be extracted from the repetition here; but I am declaring that out of scope for this PR: the goal is to establish a canonical spelling for this sort of matching, so that future extensions copy-pasted from these extensions inherit the spelling automatically.
q()notation #10227