Add the distributive law to MyNat and create a `distrib` tactic.

In this post, we will explore how to cleverly leverage the distributive law to transform equivalent polynomial expressions into a form that can be fully proven using ac_rfl. While Mathlib comes equipped with the ring tactic—which automatically proves identities in commutative rings—you can think of this exercise as building a mini version of it from scratch. We are continuing to use "Introduction to the Lean Language from Scratch: Hands-on Formal Mathematics Library Development" as our learning material.

Applying the Distributive Law with rw

First, let's consider how to expand expressions into a sum-of-products form. If you pass the distributive law to the rw tactic, it applies it only once and stops.

example (m n : MyNat) : m * (n + 1) + 2 * (m + n) = m * n + 3 * m + 2 * n := by
  rw [MyNat.mul_add]

  -- remain 2 * (m + n)
  guard_target =ₛ m * n + m * 1 + 2 * (m + n) = m * n + 3 * m + 2 * n

  sorry

By passing the distributive law to rw twice, we can carry out the transformation further into the sum-of-products form.

example (m n : MyNat) : m * (n + 1) + 2 * (m + n) = m * n + 3 * m + 2 * n := by
  rw [MyNat.mul_add, MyNat.mul_add]

  -- remain 2 * (m + n)
  guard_target =ₛ m * n + m * 1 + (2 * m + 2 * n) = m * n + 3 * m + 2 * n

  sorry

Expanding All at Once with simp

Using simp allows Lean to batch-transform all applicable locations at once, saving us from writing out the distributive law repeatedly.

example (m n : MyNat) : m * (n + 1) + 2 * (m + n) = m * n + 3 * m + 2 * n := by
  simp only [MyNat.mul_add]

  -- remain 2 * (m + n)
  guard_target =ₛ m * n + m * 1 + (2 * m + 2 * n) = m * n + 3 * m + 2 * n

  sorry

Consequently, by specifying simp only [MyNat.mul_add, MyNat.add_mul], we can utilize both the left and right distributive laws to expand everything completely into a sum of polynomials.

example (m n : MyNat) : m * (n + 1) + (2 + m) * m = m * n + 3 * m + m * m := by
  simp only [MyNat.mul_add, MyNat.add_mul]

  guard_target =ₛ m * n + m * 1 + (2 * m + m * m) = m * n + 3 * m + m * m

  sorry

Building a distrib Tactic

Let's bundle this polynomial expansion workflow into a custom tactic called distrib, which acts as a lightweight alternative to ring. Using the macro command, we can name a combination of existing tactics and define it as a new one.

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

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

  guard_target =ₛ m * n + m * 1 + (2 * m + m * m) = m * n + 3 * m + m * m

  sorry

With just this basic version of distrib, we cannot fully close the proof for the example above. Additional transformations are required. We need to break down numbers like 2 and 3 into expressions like 1 + 1 + 1 so that we can apply mul_one and one_mul, and finally close the proof using ac_rfl.

example (m n : MyNat) : m * (n + 1) + (2 + m) * m = m * n + 3 * m + m * m := by
  rw [show 3 = 1 + 2 from rfl]
  rw [show 2 = 1 + 1 from rfl] -- m * (n + 1) + (1 + 1 + m) * m = m * n + (1 + (1 + 1)) * m + m * m
  simp only [MyNat.mul_add, MyNat.add_mul] -- m * n + m * 1 + (1 * m + 1 * m + m * m)
  simp only [MyNat.mul_one, MyNat.one_mul] -- m * n + m + (m + m + m * m)
  ac_rfl

By wrapping these tactics using focus, we can handle the entire proof with just the distrib macro.

macro "distrib" : tactic => `(tactic| focus
  rw [show 3 = 1 + 2 from rfl]
  rw [show 2 = 1 + 1 from rfl]
  simp only [MyNat.mul_add, MyNat.add_mul]
  simp only [MyNat.mul_zero, MyNat.zero_mul, MyNat.mul_one, MyNat.one_mul]
  ac_rfl
)

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

Handling Numbers Greater Than 3

As it stands, our tactic cannot prove propositions containing numbers greater than 3. To solve this, we will build another macro called expand_num. First, we prove the theorem unfoldNatList to establish that x + 2 = x + 1 + 1, and use OfNat.ofNat to enable converting Nat into MyNat. While the textbook includes simp only [Nat.reduceAdd] inside expand_num, the proof goes through without it, so I have omitted it here.

theorem unfoldNatList (x : Nat)
  : (OfNat.ofNat (x + 2) : MyNat) = (OfNat.ofNat (x + 1) : MyNat) + 1 := rfl

macro "expand_num" : tactic => `(tactic| focus
  simp only [unfoldNatList]
  dsimp only [OfNat.ofNat]
  simp only [
    show MyNat.ofNat 1 = 1 from rfl,
    show MyNat.ofNat 0 = 0 from rfl
  ]
)

example (n : MyNat) : 3 * n = 2 * n + 1 * n := by
  expand_num

  guard_target =ₛ (1 + 1 + 1) * n = (1 + 1) * n + 1 * n

  simp only [MyNat.add_mul]

By integrating expand_num into distrib, we can now successfully prove propositions that involve values greater than 3.

macro "distrib" : tactic => `(tactic| focus
  expand_num
  simp only [MyNat.mul_add, MyNat.add_mul]
  simp only [MyNat.mul_zero, MyNat.zero_mul, MyNat.mul_one, MyNat.one_mul]
  ac_rfl
)

example (m n : MyNat) : (m + 4) * n + n = m * n + 5 * n := by
  distrib

Avoiding "No Progress" Errors with try

In its current state, distrib will throw an error if simp fails to make any transformations.

example (m n : MyNat) : m * n + n * n = (m + n) * n := by
  -- distrib `simp` made no progress
  sorry

To prevent this, we append try so that the tactic simply ignores instances where no progress is made.

macro "expand_num" : tactic => `(tactic| focus
  try simp only [unfoldNatList]
  try dsimp only [OfNat.ofNat]
  try simp only [
    show MyNat.ofNat 1 = 1 from rfl,
    show MyNat.ofNat 0 = 0 from rfl
  ]
)

macro "distrib" : tactic => `(tactic| focus
  expand_num
  try simp only [MyNat.mul_add, MyNat.add_mul,
                 MyNat.mul_zero, MyNat.zero_mul,
                 MyNat.mul_one, MyNat.one_mul]
  try ac_rfl
)

example (m n : MyNat) : m * n + n * n = (m + n) * n := by
  distrib