[Merged by Bors] - feat(tactic/linear_combination): allow linear_combination with { exponent := n }
#15428
Conversation
robertylewis
added
awaiting-review
src/tactic/linear_combination.lean
Outdated
| @@ -415,10 +435,16 @@ by linear_combination 3 * h a b + hqc | |||
| meta def _root_.tactic.interactive.linear_combination | |||
| (input : parse (as_linear_combo ff [] <$> texpr)?) | |||
| (_ : parse (tk "with")?) | |||
| (exponent : parse (prod.mk <$> ident <*> small_nat)?) | |||
There was a problem hiding this comment.
This results in the slightly unhelpful help text,
linear_combination expr? with? (id n)? linear_combo.linear_combination_config?
I think either:
exponentshould appear in this help text- we should make
exponenta field oflinear_combination_config
There was a problem hiding this comment.
I'd lean towards the second; linear_combination _ with { exponent := 2 } is much easier to extend later, doesn't involve any surprising new syntax, and has default values built in.
There was a problem hiding this comment.
I'd lean towards the second;
linear_combination _ with { exponent := 2 }is much easier to extend later, doesn't involve any surprising new syntax, and has default values built in.
I'm not opposed, but there's another linear_combination feature under discussion that wouldn't fit this pattern. We're scheming up syntax for a "contraposed" version, something like linear_combination 3*⊢ with target zero_ne_one that would work on disequality goals and a single disequality hypothesis/proof term. I don't think we can take an arbitrary proof of an arbitrary proposition in the config structure with convenient syntax and a default value.
So that would leave us at linear_combination _ with target zero_ne_one {exponent := 2} which is a little funny.
There was a problem hiding this comment.
What would your proposed spelling me for both options simultaneously?
There was a problem hiding this comment.
At a glance, "linear_combination _ with target x" feels a bit like simpa _ using x
There was a problem hiding this comment.
@eric-wieser I've taken your suggestion and reimplemented this as a field of the config object!
|
Sorry for the delay in updating this. I think it's ready for another review. |
YaelDillies
changed the title
linear_combination with exponent nlinear_combination with { exponent := n }
|
I took the freedom to apply Eric's last suggestions. I assume this will be quite easy to port to mathlib4. maintainer merge |
|
🚀 Pull request has been placed on the maintainer queue by YaelDillies. |
|
Implementing the exponent as a config option with a default value is a nice idea, I should remember that! bors r+ |
github-actions
bot
added
ready-to-merge
…onent := n }` (#15428) #15425 will solve problems where the goal is not a linear combination of hypotheses, but a *power* of the goal is. This PR provides a more natural certificate for these proofs. Writing `linear_combination ... with { exponent := 2 }` will square the goal before subtracting the linear combination. In principle this could be useful even outside of `polyrith`. Co-authored-by: Rob Lewis <[email protected]> Co-authored-by: Yaël Dillies <[email protected]>
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
linear_combination with { exponent := n }linear_combination with { exponent := n }
[mathlib3#15428](leanprover-community/mathlib3#15428) added an exponent option to `linear_combination`. The idea is that `linear_combination (exp := 2) ...` will take a linear combination of hypotheses adding up to the *square* of the goal. This is only mildly useful on its own, but it's a very useful certificate syntax for [mathlib3#15425](leanprover-community/mathlib3#15425). Co-authored-by: Rob Lewis <[email protected]>
#15425 will solve problems where the goal is not a linear combination of hypotheses, but a power of the goal is. This PR provides a more natural certificate for these proofs. Writing
linear_combination ... with { exponent := 2 }will square the goal before subtracting the linear combination. In principle this could be useful even outside ofpolyrith.