[Merged by Bors] - feat: positivity extension for ite#2273
[Merged by Bors] - feat: positivity extension for ite#2273YaelDillies wants to merge 4 commits intomasterfrom
positivity extension for ite#2273Conversation
Mathlib/Tactic/Positivity/Basic.lean
Outdated
| let .app (.app (.app f (p : Q(Prop))) (a : Q($α))) (b : Q($α)) ← withReducible (whnf e) | ||
| | throwError "not ite" |
There was a problem hiding this comment.
I think I messed up this pattern-matching, but I can't figure out how to fix it. @digama0, would you enlighten me?
There was a problem hiding this comment.
This needed an additional .app, to pick up the Decidable instance.
Mathlib/Tactic/Positivity/Basic.lean
Outdated
| let .app (.app (.app f (p : Q(Prop))) (a : Q($α))) (b : Q($α)) ← withReducible (whnf e) | ||
| | throwError "not ite" | ||
| let ra ← core zα pα a; let rb ← core zα pα b | ||
| let _a ← synthInstanceQ (q(Preorder $α) : Q(Type u)) |
There was a problem hiding this comment.
Synthesizing Preorder α that early means the extension is less general than its Lean 3 counterpart. Should I/can I move this line into each branch of the big ra, rb pattern-match, with an appropriate tweak to this instance I ask synthesis of?
There was a problem hiding this comment.
I went ahead and pushed the synthInstanceQ call into the branches that needed it.
|
bors merge |
Match leanprover-community/mathlib3#17650 Co-authored-by: David Renshaw <dwrenshaw@gmail.com>
|
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
positivity extension for itepositivity extension for ite
Match leanprover-community/mathlib3#17650 Co-authored-by: David Renshaw <dwrenshaw@gmail.com>
Match leanprover-community/mathlib3#17650 Co-authored-by: David Renshaw <dwrenshaw@gmail.com>
Match leanprover-community/mathlib3#17650