feat(tactic/linear_combination): improve error messages and degenerat…

…e case (#12062)

This threads the expected type of the combination from the target throughout the tactic call.
If no hypotheses are given to combine, the behavior is effectively to just call the normalization tactic.

closes #11990





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

src/tactic/linear_combination.lean

@@ -141,6 +141,7 @@ Given that `l_sum1 = r_sum1`, `l_h1 = r_h1`, ..., `l_hn = r_hn`, and given
   `= r_sum1 + (c_1 * r_h1) + ... + (c_n * r_hn)`
 
 * Input:
+  * `expected_tp`: the type of the terms being compared in the target equality
   * an `option (tactic expr)` : `none`, if there is no sum to add to yet, or
       `some` containing the base summation equation
   * a `list name` : a list of names, referring to equalities in the local context
@@ -150,16 +151,21 @@ Given that `l_sum1 = r_sum1`, `l_h1 = r_h1`, ..., `l_hn = r_hn`, and given
 * Output: an `expr`, which proves that the weighted sum of the given
     equalities added to the base equation holds
 -/
-meta def make_sum_of_hyps_helper :
+meta def make_sum_of_hyps_helper (expected_tp : expr) :
   option (tactic expr) → list name → list pexpr → tactic expr
 | none [] []                                                             :=
-  do fail "There are no hypotheses to add"
+  to_expr ``(rfl : (0 : %%expected_tp) = 0)
 | (some tactic_hcombo) [] []                                             :=
   do tactic_hcombo
 | none (h_equality_nam :: 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,
+    `(@eq %%eqtp _ _) ← infer_type h_equality |
+      fail!"{h_equality_nam} 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" ++
+        " between terms of type {expected_tp}"),
     make_sum_of_hyps_helper
       (some (mul_equality_expr h_equality coeff))
       h_eqs_names
@@ -184,6 +190,7 @@ Given a list of names referencing equalities and a list of pexprs representing
   (where each equation is multiplied by the corresponding coefficient) holds.
 
 * Input:
+  * `expected_tp`: the type of the terms being compared in the target equality
   * `h_eqs_names` : a list of names, referring to equalities in the local
       context
   * `coeffs` : a list of coefficients to be multiplied with the corresponding
@@ -192,10 +199,9 @@ 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 (h_eqs_names : list name) (coeffs : list pexpr) :
+meta def make_sum_of_hyps (expected_tp : expr) (h_eqs_names : list name) (coeffs : list pexpr) :
   tactic expr :=
-make_sum_of_hyps_helper none h_eqs_names coeffs
-
+make_sum_of_hyps_helper expected_tp none h_eqs_names coeffs
 
 /-! ### Part 2: Simplifying -/
 
@@ -303,7 +309,8 @@ Note: The left and right sides of all the equalities should have the same
 meta def linear_combination (h_eqs_names : list name) (coeffs : list pexpr)
   (config : linear_combination_config := {}) : tactic unit :=
 do
-  hsum ← make_sum_of_hyps h_eqs_names coeffs,
+  `(@eq %%ext _ _) ← target | fail "linear_combination can only be used to prove equality goals",
+  hsum ← make_sum_of_hyps ext h_eqs_names coeffs,
   hsum_on_left ← move_to_left_side hsum,
   move_target_to_left_side,
   set_goal_to_hleft_eq_tleft hsum_on_left,

test/linear_combination.lean

@@ -165,6 +165,23 @@ begin
 end
 
 
+/-! ### Cases without any arguments provided -/
+
+-- the corner case is "just apply the normalization procedure"
+example {x y z w : ℤ} (h₁ : 3 * x = 4 + y) (h₂ : x + 2 * y = 1) : z + w = w + z :=
+by linear_combination
+
+-- this interacts as expected with options
+example {x y z w : ℤ} (h₁ : 3 * x = 4 + y) (h₂ : x + 2 * y = 1) : z + w = w + z :=
+begin
+  linear_combination {normalize := ff},
+  guard_target' z + w - (w + z) = 0 - 0,
+  simp [add_comm]
+end
+
+example {x y z w : ℤ} (h₁ : 3 * x = 4 + y) (h₂ : x + 2 * y = 1) : z + w = w + z :=
+by linear_combination {normalization_tactic := `[simp [add_comm]]}
+
 /-! ### Cases that should fail -/
 
 -- This should fail because there are no hypotheses given
@@ -215,3 +232,10 @@ begin
   success_if_fail {linear_combination (h1, (1 : ℕ))},
   exact h1
 end
+
+example (a b : ℤ) (x y : ℝ) (hab : a = b) (hxy : x = y) : 2*x = 2*y :=
+begin
+  success_if_fail_with_msg {linear_combination (hab, 2)}
+    "hab is an equality between terms of type ℤ, but is expected to be between terms of type ℝ",
+  linear_combination (hxy, 2)
+end