feat: add exponentiation option back to linear_combination (#7789)

[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]>

Mathlib/Tactic/LinearCombination.lean

@@ -106,28 +106,18 @@ partial def expandLinearCombo (stx : Syntax.Term) : TermElabM (Option Syntax.Ter
     some <$> e.toSyntax
   return result.map fun r => ⟨r.raw.setInfo (SourceInfo.fromRef stx true)⟩
 
-/-- A configuration object for `linear_combination`. -/
-structure Config where
-  /-- whether or not the normalization step should be used -/
-  normalize := true
-  /-- whether to make separate subgoals for both sides or just one for `lhs - rhs = 0` -/
-  twoGoals := false
-  /-- the tactic used for normalization when checking
-  if the weighted sum is equivalent to the goal (when `normalize` is `true`). -/
-  normTac : Syntax.Tactic := Unhygienic.run `(tactic| ring_nf)
-  deriving Inhabited
-
-/-- Function elaborating `LinearCombination.Config` -/
-declare_config_elab elabConfig Config
-
 theorem eq_trans₃ (p : (a:α) = b) (p₁ : a = a') (p₂ : b = b') : a' = b' := p₁ ▸ p₂ ▸ p
 
 theorem eq_of_add [AddGroup α] (p : (a:α) = b) (H : (a' - b') - (a - b) = 0) : a' = b' := by
   rw [← sub_eq_zero] at p ⊢; rwa [sub_eq_zero, p] at H
 
+theorem eq_of_add_pow [Ring α] [NoZeroDivisors α] (n : ℕ) (p : (a:α) = b)
+    (H : (a' - b')^n - (a - b) = 0) : a' = b' := by
+  rw [← sub_eq_zero] at p ⊢; apply pow_eq_zero (n := n); rwa [sub_eq_zero, p] at H
+
 /-- Implementation of `linear_combination` and `linear_combination2`. -/
 def elabLinearCombination
-    (norm? : Option Syntax.Tactic) (input : Option Syntax.Term)
+    (norm? : Option Syntax.Tactic) (exp? : Option Syntax.NumLit) (input : Option Syntax.Term)
     (twoGoals := false) : Tactic.TacticM Unit := Tactic.withMainContext do
   let p ← match input with
   | none => `(Eq.refl 0)
@@ -136,13 +126,18 @@ def elabLinearCombination
     | none => `(Eq.refl $e)
     | some p => pure p
   let norm := norm?.getD (Unhygienic.run `(tactic| ring1))
-  Tactic.evalTactic <|← withFreshMacroScope <| if twoGoals then
+  Tactic.evalTactic <| ← withFreshMacroScope <|
+  if twoGoals then
     `(tactic| (
       refine eq_trans₃ $p ?a ?b
       case' a => $norm:tactic
       case' b => $norm:tactic))
   else
-    `(tactic| (refine eq_of_add $p ?a; case' a => $norm:tactic))
+    match exp? with
+    | some n =>
+      if n.getNat = 1 then `(tactic| (refine eq_of_add $p ?a; case' a => $norm:tactic))
+      else `(tactic| (refine eq_of_add_pow $n $p ?a; case' a => $norm:tactic))
+    | _ => `(tactic| (refine eq_of_add $p ?a; case' a => $norm:tactic))
 
 /--
 The `(norm := $tac)` syntax says to use `tac` as a normalization postprocessor for
@@ -151,6 +146,12 @@ to get subgoals from `linear_combination` or with `skip` to disable normalizatio
 -/
 syntax normStx := atomic(" (" &"norm" " := ") withoutPosition(tactic) ")"
 
+/--
+The `(exp := n)` syntax for `linear_combination` says to take the goal to the `n`th power before
+subtracting the given combination of hypotheses.
+-/
+syntax expStx := atomic(" (" &"exp" " := ") withoutPosition(num) ")"
+
 /--
 `linear_combination` attempts to simplify the target by creating a linear combination
   of a list of equalities and subtracting it from the target.
@@ -175,6 +176,10 @@ Note: The left and right sides of all the equalities should have the same
   * To get a subgoal in the case that it is not immediately provable, use
     `ring_nf` as the normalization tactic.
   * To avoid normalization entirely, use `skip` as the normalization tactic.
+* `linear_combination (exp := n) e` will take the goal to the `n`th power before subtracting the
+  combination `e`. In other words, if the goal is `t1 = t2`, `linear_combination (exp := n) e`
+  will change the goal to `(t1 - t2)^n = 0` before proceeding as above.
+  This feature is not supported for `linear_combination2`.
 * `linear_combination2 e` is the same as `linear_combination e` but it produces two
   subgoals instead of one: rather than proving that `(a - b) - (a' - b') = 0` where
   `a' = b'` is the linear combination from `e` and `a = b` is the goal,
@@ -218,11 +223,13 @@ example (a b : ℚ) (h : ∀ p q : ℚ, p = q) : 3*a + qc = 3*b + 2*qc := by
   linear_combination 3 * h a b + hqc
 ```
 -/
-syntax (name := linearCombination) "linear_combination" (normStx)? (ppSpace colGt term)? : tactic
+syntax (name := linearCombination) "linear_combination"
+  (normStx)? (expStx)? (ppSpace colGt term)? : tactic
 elab_rules : tactic
-  | `(tactic| linear_combination $[(norm := $tac)]? $(e)?) => elabLinearCombination tac e
+  | `(tactic| linear_combination $[(norm := $tac)]? $[(exp := $n)]? $(e)?) =>
+    elabLinearCombination tac n e
 
 @[inherit_doc linearCombination]
 syntax "linear_combination2" (normStx)? (ppSpace colGt term)? : tactic
 elab_rules : tactic
-  | `(tactic| linear_combination2 $[(norm := $tac)]? $(e)?) => elabLinearCombination tac e true
+  | `(tactic| linear_combination2 $[(norm := $tac)]? $(e)?) => elabLinearCombination tac none e true

test/linear_combination.lean

@@ -197,6 +197,28 @@ example (a b : ℤ) (x y : ℝ) (hab : a = b) (hxy : x = y) : 2 * x = 2 * y := b
   fail_if_success linear_combination 2 * hab
   linear_combination 2 * hxy
 
+/-! ### Cases with exponent -/
+
+example (x y z : ℚ) (h : x = y) (h2 : x * y = 0) : x + y*z = 0 := by
+  linear_combination (exp := 2) (-y * z ^ 2 + x) * h + (z ^ 2 + 2 * z + 1) * h2
+
+example (x y z : ℚ) (h : x = y) (h2 : x * y = 0) : y*z = -x := by
+  linear_combination (norm := skip) (exp := 2) (-y * z ^ 2 + x) * h + (z ^ 2 + 2 * z + 1) * h2
+  ring
+
+example (K : Type)
+    [Field K]
+    [CharZero K]
+    {x y z : K}
+    (h₂ : y ^ 3 + x * (3 * z ^ 2) = 0)
+    (h₁ : x ^ 3 + z * (3 * y ^ 2) = 0)
+    (h₀ : y * (3 * x ^ 2) + z ^ 3 = 0)
+    (h : x ^ 3 * y + y ^ 3 * z + z ^ 3 * x = 0) :
+    x = 0 := by
+  linear_combination (exp := 6) 2 * y * z ^ 2 * h₂ / 7 + (x ^ 3  - y ^ 2 * z / 7) * h₁ -
+    x * y * z * h₀ + y * z * h / 7
+
+
 /-! ### Regression tests -/
 
 def g (a : ℤ) : ℤ := a ^ 2