feat(tactic/linear_combination): allow arbitrary proof terms (#13979)

This extends `linear_combination` to allow arbitrary proof terms of equalities instead of just local hypotheses. 

```lean
constants (qc : ℚ) (hqc : qc = 2*qc)

example (a b : ℚ) (h : ∀ p q : ℚ, p = q) : 3*a + qc = 3*b + 2*qc :=
by linear_combination (h a b, 3) (hqc)
```

This changes the syntax of `linear_combination` in the case where no coefficient is provided and it defaults to 1. A space-separated list of pexprs won't parse, since there's an ambiguity in `h1 h2` between an application or two arguments. So this case now requres parentheses around the argument:
`linear_combination (h1, 3) (h2)`

Does anyone object to this syntax change?



Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>

archive/imo/imo2008_q4.lean

@@ -97,7 +97,7 @@ begin
   -- f(ab) = 1/ab → a^4 = 1 → a = 1 → f(a) = 1/a → false
   { have hb_ne_0 : b ≠ 0 := ne_of_gt hb,
     field_simp [hab₂] at H₂,
-    have H₃ : 2 * b ^ 4 * (a ^ 4 - 1) = 0 := by linear_combination H₂,
+    have H₃ : 2 * b ^ 4 * (a ^ 4 - 1) = 0 := by linear_combination (H₂),
     have h2b4_ne_0 : 2 * (b ^ 4) ≠ 0 := mul_ne_zero two_ne_zero (pow_ne_zero 4 hb_ne_0),
     have ha₁ : a ^ 4 = 1, { simpa [sub_eq_zero, h2b4_ne_0] using H₃ },
     obtain ha₂ := abs_eq_one_of_pow_eq_one a 4 (show 4 ≠ 0, by norm_num) ha₁,

src/algebra/quadratic_discriminant.lean

@@ -82,7 +82,7 @@ begin
   field_simp,
   apply or_congr,
   { split; intro h'; linear_combination (h', -1) },
-  { split; intro h'; linear_combination h' },
+  { split; intro h'; linear_combination (h') },
 end
 
 /-- A quadratic has roots if its discriminant has square roots -/

src/number_theory/fermat4.lean

@@ -40,8 +40,7 @@ begin
     split, { exact right_ne_zero_of_mul f42.1 },
     split, { exact right_ne_zero_of_mul f42.2.1 },
     apply (mul_right_inj' (pow_ne_zero 4 hk0)).mp,
-    have H : (k * a) ^ 4 + (k * b) ^ 4 = (k ^ 2 * c) ^ 2 := f42.2.2,
-    linear_combination H }
+    linear_combination (f42.2.2) }
 end
 
 lemma ne_zero {a b c : ℤ} (h : fermat_42 a b c) : c ≠ 0 :=
@@ -167,8 +166,7 @@ begin
   -- first the formula:
   have ht : pythagorean_triple (a ^ 2) (b ^ 2) c,
   { delta pythagorean_triple,
-    have H := h.1.2.2,
-    linear_combination H },
+    linear_combination (h.1.2.2) },
   -- coprime requirement:
   have h2 : int.gcd (a ^ 2) (b ^ 2) = 1 :=
     int.gcd_eq_one_iff_coprime.mpr (coprime_of_minimal h).pow,
@@ -181,7 +179,7 @@ begin
   -- formula:
   have htt : pythagorean_triple a n m,
   { delta pythagorean_triple,
-    linear_combination ht1 },
+    linear_combination (ht1) },
   -- a and n are coprime, because a ^ 2 = m ^ 2 - n ^ 2 and m and n are coprime.
   have h3 : int.gcd a n = 1,
   { apply int.gcd_eq_one_iff_coprime.mpr,

src/tactic/linear_combination.lean

@@ -152,27 +152,27 @@ Given that `l_sum1 = r_sum1`, `l_h1 = r_h1`, ..., `l_hn = r_hn`, and given
     equalities added to the base equation holds
 -/
 meta def make_sum_of_hyps_helper (expected_tp : expr) :
-  option (tactic expr) → list name → list pexpr → tactic expr
+  option (tactic expr) → list expr → list pexpr → tactic expr
 | none [] []                                                             :=
   to_expr ``(rfl : (0 : %%expected_tp) = 0)
 | (some tactic_hcombo) [] []                                             :=
   do tactic_hcombo
-| none (h_equality_nam :: h_eqs_names) (coeff :: coeffs)                 :=
+| none (h_equality :: h_eqs_names) (coeff :: coeffs)                 :=
  do
     -- This is the first equality, and we do not have anything to add to it
-    h_equality ← get_local h_equality_nam,
+    -- h_equality ← get_local h_equality_nam,
     `(@eq %%eqtp _ _) ← infer_type h_equality |
-      fail!"{h_equality_nam} is expected to be a proof of an equality",
+      fail!"{h_equality} is expected to be a proof of an equality",
     is_def_eq eqtp expected_tp <|>
-      fail!("{h_equality_nam} is an equality between terms of type {eqtp}, but is expected to be" ++
+      fail!("{h_equality} is an equality between terms of type {eqtp}, but is expected to be" ++
         " between terms of type {expected_tp}"),
     make_sum_of_hyps_helper
       (some (mul_equality_expr h_equality coeff))
       h_eqs_names
       coeffs
-| (some tactic_hcombo) (h_equality_nam :: h_eqs_names) (coeff :: coeffs) :=
+| (some tactic_hcombo) (h_equality :: h_eqs_names) (coeff :: coeffs) :=
   do
-    h_equality ← get_local h_equality_nam,
+    -- h_equality ← get_local h_equality_nam,
     hcombo ← tactic_hcombo,
     -- We want to add this weighted equality to the current equality in
     --   the hypothesis
@@ -199,7 +199,7 @@ Given a list of names referencing equalities and a list of pexprs representing
 * Output: an `expr`, which proves that the weighted sum of the equalities
     holds
 -/
-meta def make_sum_of_hyps (expected_tp : expr) (h_eqs_names : list name) (coeffs : list pexpr) :
+meta def make_sum_of_hyps (expected_tp : expr) (h_eqs_names : list expr) (coeffs : list pexpr) :
   tactic expr :=
 make_sum_of_hyps_helper expected_tp none h_eqs_names coeffs
 
@@ -306,11 +306,12 @@ Note: The left and right sides of all the equalities should have the same
 
 * Output: N/A
 -/
-meta def linear_combination (h_eqs_names : list name) (coeffs : list pexpr)
+meta def linear_combination (h_eqs_names : list pexpr) (coeffs : list pexpr)
   (config : linear_combination_config := {}) : tactic unit :=
 do
   `(@eq %%ext _ _) ← target | fail "linear_combination can only be used to prove equality goals",
-  hsum ← make_sum_of_hyps ext h_eqs_names coeffs,
+  h_eqs ← h_eqs_names.mmap to_expr,
+  hsum ← make_sum_of_hyps ext h_eqs coeffs,
   hsum_on_left ← move_to_left_side hsum,
   move_target_to_left_side,
   set_goal_to_hleft_eq_tleft hsum_on_left,
@@ -330,9 +331,12 @@ was given a `pexpr ` of ``(1) along with the identifier.
 
 * Output: a `lean.parser (name × pexpr)`
 -/
-meta def parse_name_pexpr_pair : lean.parser (name × pexpr) :=
-(tk "(" *> prod.mk <$> ident <*> (tk "," *> parser.pexpr 0 <* tk ")")) <|>
-((λ id, (id, ``(1))) <$> ident)
+meta def parse_name_pexpr_pair : lean.parser (pexpr × pexpr) :=
+with_desc "(pexpr, pexpr) <|> (pexpr)" $ do
+  tk "(",
+  pe ← parser.pexpr 0,
+  (tk ")" >> return (pe, ``(1))) <|>
+  (do tk ",", cf ← parser.pexpr 0, tk ")", return (pe, cf))
 
 /--
 `linear_combination` attempts to prove the target by creating and applying a
@@ -365,7 +369,7 @@ by linear_combination (h1, 1) (h2, -2)
 
 example (x y : ℤ) (h1 : x*y + 2*x = 1) (h2 : x = y) :
   x*y = -2*y + 1 :=
-by linear_combination h1 (h2, -2)
+by linear_combination (h1) (h2, -2)
 
 example (x y z : ℝ) (ha : x + 2*y - z = 4) (hb : 2*x + y + z = -2)
     (hc : x + 2*y + z = 2) :

test/linear_combination.lean

@@ -10,7 +10,7 @@ by linear_combination (h1, 1)
 
 example (x y : ℤ) (h1 : 3*x + 2*y = 10):
   3*x + 2*y = 10 :=
-by linear_combination h1
+by linear_combination (h1)
 
 example (x y : ℤ) (h1 : x + 2 = -3) (h2 : y = 10) :
   2*x + 4 = -6 :=
@@ -22,7 +22,7 @@ by linear_combination (h1, 1) (h2, -2)
 
 example (x y : ℤ) (h1 : x*y + 2*x = 1) (h2 : x = y) :
   x*y = -2*y + 1 :=
-by linear_combination (h2, -2) h1
+by linear_combination (h2, -2) (h1)
 
 example (x y : ℤ) (h1 : x + 2 = -3) (h2 : y = 10) :
   2*x + 4 - y = -16 :=
@@ -93,7 +93,7 @@ by linear_combination (h1, 2) (h2, 1) (h3, -2)
 example (w x y z : ℝ) (h1 : x + 2.1*y + 2*z = 2) (h2 : x + 8*z + 5*w = -6.5)
     (h3 : x + y + 5*z + 5*w = 3) :
   x + 2.2*y + 2*z - 5*w = -8.5 :=
-by linear_combination (h1, 2) h2 (h3, -2)
+by linear_combination (h1, 2) (h2) (h3, -2)
 
 example (a b c d : ℚ) (h1 : a = 4) (h2 : 3 = b) (h3 : c*3 = d) (h4 : -d = a) :
   2*a - 3 + 9*c + 3*d = 8 - b + 3*d - 3*a :=
@@ -104,6 +104,13 @@ example (a b c d : ℚ) (h1 : a = 4) (h2 : 3 = b) (h3 : c*3 = d) (h4 : -d = a) :
 by linear_combination (h2, 2) (h3, -1) (h1, 3) (h4, -3)
 
 
+/-! ### Cases with non-hypothesis inputs -/
+
+constants (qc : ℚ) (hqc : qc = 2*qc)
+
+example (a b : ℚ) (h : ∀ p q : ℚ, p = q) : 3*a + qc = 3*b + 2*qc :=
+by linear_combination (h a b, 3) (hqc)
+
 /-! ### Cases with arbitrary coefficients -/
 
 example (a b : ℤ) (h : a = b) :