uniform way to unfold numerical literal

Stream: Is there code for X?

[Asei Inoue]

macro "distrib" : tactic => `(tactic| with_reducible
  simp only [Nat.add_mul, Nat.mul_add]
  ac_rfl
)

-- adhoc way
macro_rules
  | `(tactic| distrib) => `(tactic| rw [show 2 = 1 + 1 from rfl]; distrib)

macro_rules
  | `(tactic| distrib) => `(tactic| rw [show 3 = 2 + 1 from rfl]; distrib)


section TestCase

example (a b c d : Nat) : (a + b) * (c + d) = a * c + a * d + b * c + b * d := by
  distrib

example (l m n :Nat) : (l + m) * (l + n) = l * l + l * (m + n) + m * n := by
  distrib

example (m n : Nat) : (m + n) * (m + n) = m * m + 2 * m * n + n * n := by
  distrib

example (m n : Nat) : (m + 2 * n) * (m + n) = m * m + 3 * m * n + 2 * n * n := by
  distrib

end TestCase

[Asei Inoue]

I would like to create my own tactic of proof using the exchange and combination laws of addition and the distribution laws of multiplication of natural numbers.

simp only [Nat.add_mul, Nat.mul_add] does quite a lot of work, but I got stuck at the point where I had to rewrite constants like 2 and 3 as 1 + 1 and 1 + 1 + 1.

The above code solves this ad hoc by adding rw [show 3 = 2 + 1 from rfl] etc., but is there a more uniform solution?

[Asei Inoue]

Using Mathlib, the following can be proved. However, I am looking for an easier way that does not use Mathlib.

import Mathlib.Tactic

example (m n : Nat) : (m + 2 * n) * (m + n) = m * m + 3 * m * n + 2 * n * n := by
  zify
  ring

[Ruben Van de Velde]

omega?

[Kim Morrison]

No, omega knows nothing about multiplication of variables.

[Daniel Weber]

example (m n : Nat) : (m + 2 * n) * (m + n) = m * m + 3 * m * n + 2 * n * n := by
  simp only [Nat.mul_add, Nat.add_mul, Nat.mul_assoc, Nat.mul_comm m n]
  omega

works

[Ruben Van de Velde]

Yeah, but omega should be able to handle the ad-hoc 3 = 2 + 1 goals mentioned above

[Daniel Weber]

macro "distrib" : tactic => `(tactic| with_reducible
  simp only [Nat.add_mul, Nat.mul_add, Nat.succ_mul, Nat.mul_succ]
  ac_rfl
)

also works, although it will be inefficient with larger numbers