feat(tactic/linear_combination): allow `linear_combination with { exp…

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

src/tactic/linear_combination.lean

@@ -73,6 +73,7 @@ checking if the weighted sum is equivalent to the goal (when `normalize` is `tt`
 meta structure linear_combination_config : Type :=
 (normalize : bool := tt)
 (normalization_tactic : tactic unit := `[ring_nf SOP])
+(exponent : ℕ := 1)
 
 
 /-! ### Part 1: Multiplying Equations by Constants and Adding Them Together -/
@@ -266,6 +267,17 @@ This tactic only should be used when the target's type is an equality whose
 meta def set_goal_to_hleft_sub_tleft (hsum_on_left : expr) : tactic unit :=
 do to_expr ``(eq_zero_of_sub_eq_zero %%hsum_on_left) >>= apply, skip
 
+/--
+If an exponent `n` is provided, changes the goal from `t = 0` to `t^n = 0`.
+* Input:
+  * `exponent : ℕ`, the power to raise the goal by. If `1`, this tactic is a no-op.
+
+* Output: N/A
+-/
+meta def raise_goal_to_power : ℕ → tactic unit
+| 1 := skip
+| n := refine ``(@pow_eq_zero _ _ _ _ %%`(n) _)
+
 /--
 This tactic attempts to prove the goal by normalizing the target if the
 `normalize` field of the given configuration is true.
@@ -314,6 +326,7 @@ do
   hsum ← make_sum_of_hyps ext h_eqs coeffs,
   hsum_on_left ← move_to_left_side hsum,
   move_target_to_left_side,
+  raise_goal_to_power config.exponent,
   set_goal_to_hleft_sub_tleft hsum_on_left,
   normalize_if_desired config
 
@@ -354,6 +367,9 @@ setup_tactic_parser
   configuration is set to false, then the tactic will simply set the user up to
   prove their target using the linear combination instead of normalizing the subtraction.
 
+Users may provide an optional `with { exponent := n }`. This will raise the goal to the power `n`
+  before subtracting the linear combination.
+
 Note: The left and right sides of all the equalities should have the same
   type, and the coefficients should also have this type.  There must be
   instances of `has_mul` and `add_group` for this type.
@@ -406,6 +422,9 @@ begin
   norm_cast
 end
 
+example (x y z : ℚ) (h : x = y) (h2 : x * y = 0) : x + y*z = 0 :=
+by linear_combination (-y * z ^ 2 + x) * h + (z ^ 2 + 2 * z + 1) * h2 with { exponent := 2 }
+
 constants (qc : ℚ) (hqc : qc = 2*qc)
 
 example (a b : ℚ) (h : ∀ p q : ℚ, p = q) : 3*a + qc = 3*b + 2*qc :=

test/linear_combination.lean

@@ -199,6 +199,31 @@ end
 example {x y z w : ℤ} (h₁ : 3 * x = 4 + y) (h₂ : x + 2 * y = 1) : z + w = w + z :=
 by linear_combination with {normalization_tactic := `[simp [add_comm]]}
 
+/-! ### Cases with exponent -/
+
+example (x y z : ℚ) (h : x = y) (h2 : x * y = 0) : x + y*z = 0 :=
+by linear_combination (-y * z ^ 2 + x) * h + (z ^ 2 + 2 * z + 1) * h2 with {exponent := 2}
+
+example (x y z : ℚ) (h : x = y) (h2 : x * y = 0) : y*z = -x :=
+begin
+  linear_combination (-y * z ^ 2 + x) * h + (z ^ 2 + 2 * z + 1) * h2
+    with {exponent := 2, normalize := ff},
+  ring
+end
+
+example (K : Type)
+  [field K]
+  [char_zero 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 2 * y * z ^ 2 * h₂ / 7 + (x ^ 3  - y ^ 2 * z / 7) * h₁ -
+  x * y * z * h₀ + y * z * h / 7 with {exponent := 6}
+
+
 /-! ### Cases where the goal is not closed -/
 
 example (x y : ℚ) (h1 : x + y = 3) (h2 : 3*x = 7) :