feat(tactic/linear_combination): add parser for h / a (#15284)

As reported during LFTCM 2022.

src/tactic/linear_combination.lean

@@ -337,6 +337,7 @@ meta def as_linear_combo : bool → list pexpr → pexpr → list (pexpr × pexp
   | ``has_add.add, [e1, e2] := as_linear_combo neg ms e1 ++ as_linear_combo neg ms e2
   | ``has_sub.sub, [e1, e2] := as_linear_combo neg ms e1 ++ as_linear_combo (bnot neg) ms e2
   | ``has_mul.mul, [e1, e2] := as_linear_combo neg (e1::ms) e2
+  | ``has_div.div, [e1, e2] := as_linear_combo neg (``((%%e2)⁻¹)::ms) e1
   | ``has_neg.neg, [e1] := as_linear_combo (bnot neg) ms e1
   | _, _ := let m := mk_mul ms in [(e, if neg then ``(-%%m) else m)]
   end

src/tactic/polyrith.lean

@@ -389,6 +389,15 @@ do
   some j ← pure (json.parse s) | fail!"Invalid json: {s}",
   pure j
 
+/--
+Adds parentheses around additions and subtractions, for printing at
+precedence 65.
+-/
+meta def add_parens : expr → tactic format
+| e@`(_ + _) := pformat!"({e})"
+| e@`(_ - _) := pformat!"({e})"
+| e := pformat!"{e}"
+
 /--
 Given a pair of `expr`s, where one represents the hypothesis/proof term,
 and the other representes the coefficient attached to it, this tactic
@@ -402,12 +411,10 @@ because it may appear as a negation (if this is the first component)
 or a subtraction.
 -/
 meta def component_to_lc_format : expr × expr → tactic (bool × format)
-| (ex, `(-@has_one.one _ _)) := prod.mk tt <$> pformat!"{ex}"
 | (ex, `(@has_one.one _ _))  := prod.mk ff <$> pformat!"{ex}"
+| (ex, `(@has_one.one _ _ / %%cf))  := do f ← add_parens cf, prod.mk ff <$> pformat!"{ex} / {f}"
 | (ex, `(-%%cf)) := do (neg, fmt) ← component_to_lc_format (ex, cf), return (!neg, fmt)
-| (ex, cf@`(_ + _)) := prod.mk ff <$> pformat!"({cf}) * {ex}"
-| (ex, cf@`(_ - _)) := prod.mk ff <$> pformat!"({cf}) * {ex}"
-| (ex, cf) := prod.mk ff <$> pformat!"{cf} * {ex}"
+| (ex, cf) := do f ← add_parens cf, prod.mk ff <$> pformat!"{f} * {ex}"
 
 private meta def intersperse_ops_aux : list (bool × format) → format
 | [] := ""

test/linear_combination.lean

@@ -61,7 +61,7 @@ by linear_combination 2*h1 - 3*h2
 
 example (a b : ℝ) (ha : 2*a = 4) (hab : 2*b = a - b) :
   b = 2 / 3 :=
-by linear_combination 1/6 * ha + 1/3 * hab
+by linear_combination ha/6 + hab/3
 
 
 /-! ### Cases with more than 2 equations -/

test/polyrith.lean

@@ -181,7 +181,7 @@ by test_polyrith "{\"data\":[\"(poly.add (poly.mul (poly.const 1/1) (poly.var 0)
 
 example (a b : ℝ) (ha : 2*a = 4) (hab : 2*b = a - b) (hignore : 3 = a + b) :
   b = 2 / 3 :=
-by test_polyrith only [ha, hab] "{\"data\":[\"(poly.const 1/6)\",\"(poly.const 1/3)\"],\"success\":true}" ["ff", "real", "2", "[((2 * var1) - 4), ((2 * var0) - (var1 - var0))]", "(var0 - 2/3)"]  "linear_combination 1 / 6 * ha + 1 / 3 * hab"
+by test_polyrith only [ha, hab] "{\"data\":[\"(poly.const 1/6)\",\"(poly.const 1/3)\"],\"success\":true}" ["ff", "real", "2", "[((2 * var1) - 4), ((2 * var0) - (var1 - var0))]", "(var0 - 2/3)"]  "linear_combination ha / 6 + hab / 3"
 
 constant term : ∀ a b : ℚ, a + b = 0
 
@@ -236,13 +236,13 @@ end
 /-! ## Degenerate cases -/
 
 example {K : Type*} [field K] [char_zero K] {s : K} (hs : 3 * s + 1 = 4) : s = 1 :=
-by test_polyrith "{\"data\":[\"(poly.const 1/3)\"],\"success\":true}" ["ff", "K", "1", "[(((3 * var0) + 1) - 4)]", "(var0 - 1)"]  "linear_combination 1 / 3 * hs"
+by test_polyrith "{\"data\":[\"(poly.const 1/3)\"],\"success\":true}" ["ff", "K", "1", "[(((3 * var0) + 1) - 4)]", "(var0 - 1)"]  "linear_combination hs / 3"
 
 example {x : ℤ} (h1 : x + 4 = 2) : x = -2 :=
 by test_polyrith "{\"data\":[\"(poly.const 1/1)\"],\"success\":true}" ["ff", "int", "1", "[((var0 + 4) - 2)]", "(var0 - (-1 * 2))"]  "linear_combination h1"
 
 example {w : ℚ} (h1 : 3 * w + 1 = 4) : w = 1 :=
-by test_polyrith "{\"data\":[\"(poly.const 1/3)\"],\"success\":true}" ["ff", "rat", "1", "[(((3 * var0) + 1) - 4)]", "(var0 - 1)"]  "linear_combination 1 / 3 * h1"
+by test_polyrith "{\"data\":[\"(poly.const 1/3)\"],\"success\":true}" ["ff", "rat", "1", "[(((3 * var0) + 1) - 4)]", "(var0 - 1)"]  "linear_combination h1 / 3"
 
 example {x : ℤ} (h1 : 2 * x + 3 = x) : x = -3 :=
 by test_polyrith "{\"data\":[\"(poly.const 1/1)\"],\"success\":true}" ["ff", "int", "1", "[(((2 * var0) + 3) - var0)]", "(var0 - (-1 * 3))"]  "linear_combination h1"