Tactic for simplification in division with many variables?

Stream: new members

[Tyler Josephson ⚛️]

One of my students needed this theorem to solve a bigger problem, and we found the last step of the calc block particularly cumbersome, mainly due to the order of operations and the challenge of moving terms around. How to do this in fewer lines?

import Mathlib.Tactic

theorem helper {a b c d e : ℝ}
(hb : b ≠ 0) (h1 : a ^ 2 * b = c * d * b / e * 2) : a ^ 2 = c * d / e * 2
:= by
  calc
    a ^ 2 = a ^ 2 * b / b := by rw[mul_div_cancel]; apply hb
    _ = (c * d * b / e * 2) / b := by rw[h1]
    _ = c * d / e * 2 := by ring; rw[mul_comm c, mul_assoc (d * c), mul_comm b, ← mul_assoc, mul_assoc (d * c * e⁻¹), mul_inv_cancel]; ring; apply hb

Is there a tactic that can automatically cancel equal terms in the numerator and denominator, no matter where in the numerator and denominator may appear, provided the term being canceled is nonzero?

[Heather Macbeth]

Quick solution, not using your scaffolding:

theorem helper {a b c d e : ℝ} (hb : b ≠ 0) (h1 : a ^ 2 * b = c * d * b / e * 2) :
    a ^ 2 = c * d / e * 2 := by
  apply mul_left_cancel₀ hb
  linear_combination h1

[Heather Macbeth]

Minimizing the last of your steps, it seems that field_simp is not doing what one would hope there:

import Mathlib.Tactic

example {a b c d e : ℝ} (hb: b ≠ 0) :
    c * d * b / e * 2 / b = c * d / e * 2 := by
  field_simp

leaves the goal

⊢ c * d * b * 2 / (e * b) = c * d * 2 / e

where you'd hope that it would use hb to leave

⊢ c * d * 2 / e = c * d * 2 / e

instead. This might be a bug in field_simp. Or it might be just an expected consequence of the somewhat simplistic implementation of field_simp (literally, it's a wrapper around simp ...), fixable by giving a more principled implementation.

[Tyler Josephson ⚛️]

We'd love a more powerful field_simp - is anyone with know-how interested in this? In our science derivations, we often have to juggle expressions like these.

[Martin Dvořák]

My students also complain about insufficient automation when working with fractions. I guess these tactics aren't easy to develop. I don't know about anyone working on better field_simp now.

[Alex J. Best]

We could add some field_simp lemmas like so

import Mathlib.Tactic

variable {K : Type*} [Field K]
@[field_simps]
theorem div_mul_eq_iff {a b c d : K} (hb : b ≠ 0) : a / (b * d) = c ↔ a / d = c * b := by
  by_cases hd : d = 0; simp [hd, hb]; tauto
  have : b * d ≠ 0 := by simp [hb, hd]
  field_simp [mul_assoc]

@[field_simps]
theorem div_mul_eq_iff' {a b c d : K} (hd : d ≠ 0) : a / (b * d) = c ↔ a / b = c * d := by
  by_cases hb : b = 0; simp [hd, hb]; tauto
  have : b * d ≠ 0 := by simp [hb, hd]
  field_simp
  ring_nf

example {a b c d e : ℝ} (hb: b ≠ 0) :
    c * d * b / e * 2 / b = c * d / e * 2 := by
  field_simp

[Alex J. Best]

There will of course be many (too many!) variations, but perhaps these ones are common enough to be useful.