Defining Multiplication for MyInt in Lean 4: Registering CommRing and the ring Tactic

In the previous article, we defined addition for MyInt and registered it as an additive commutative group (AddCommGroup), which let us use the abel tactic. This time we define multiplication for MyInt and register it as a commutative ring (CommRing), which lets us use the ring tactic. This series follows ゼロから始めるLean言語入門 手を動かして学ぶ形式数学ライブラリ開発.

Registering MyNat as a CommSemiring

To use the ring tactic in proofs about multiplication, we first need to register the natural number type MyNat as both an additive commutative monoid (AddCommMonoid) and a commutative semiring (CommSemiring).

instance : Zero MyNat where
  zero := 0

instance : AddCommMonoid MyNat where
  add_assoc := MyNat.add_assoc
  zero_add := MyNat.zero_add
  add_zero := MyNat.add_zero
  add_comm := MyNat.add_comm
  nsmul := nsmulRec

instance: One MyNat where
  one := 1

instance : CommSemiring MyNat where
  left_distrib := MyNat.mul_add
  right_distrib := MyNat.add_mul
  mul_assoc := MyNat.mul_assoc
  one_mul := MyNat.one_mul
  mul_one := MyNat.mul_one
  zero_mul := MyNat.zero_mul
  mul_zero := MyNat.mul_zero
  mul_comm := MyNat.mul_comm

example (a b c : MyNat) : (a + b) * (a + c) = a * a + (b + c) * a + b * c := by
  ring

MyNat can now use both the abel tactic and the ring tactic.

Defining multiplication for PreInt

To define multiplication for MyInt, we first define multiplication for PreInt. Expanding (m1 - m2) * (n1 - n2) gives m1 * n1 + m2 * n2 - (m1 * n2 + m2 * n1), so PreInt.mul can be defined as follows.

def PreInt.mul (m n : PreInt) : MyInt :=
  match m, n with
  | (m1, m2), (n1, n2) => ⟦(m1 * n1 + m2 * n2, m1 * n2 + m2 * n1)⟧

Defining multiplication for MyInt

We change the domain of PreInt.mul using Quotient.lift₂ to define multiplication for MyInt. To use Quotient.lift₂, we must prove that feeding equivalent inputs into PreInt.mul produces equal results.

In this proof, we set K = (p * c + q * d + q * c + p * d), rewrite both sides into the form lhs + K = rhs + K, and substitute using the hypotheses h1 and h2 to show the two sides are equal.

def MyInt.mul : MyInt → MyInt → MyInt := Quotient.lift₂ PreInt.mul <| by
  -- ⊢ ∀ (a₁ b₁ a₂ b₂ : PreInt), a₁ ≈ a₂ → b₁ ≈ b₂ → a₁.mul b₁ = a₂.mul b₂
  intro (a, b) (c, d) (p, q) (r, s) h1 h2
  dsimp [PreInt.mul]
  apply Quot.sound
  notation_simp at *
  -- h1 : a + q = b + p
  -- h2 : c + s = d + r
  -- ⊢ a * c + b * d + (p * s + q * r) = a * d + b * c + (p * r + q * s)

  generalize hl : a * c + b * d + (p * s + q * r) = lhs
  generalize hr : a * d + b * c + (p * r + q * s) = rhs

  have h3 : lhs + (p * c + q * d + q * c + p * d) = rhs + (p * c + q * d + q * c + p * d) := by
    calc
      lhs + (p * c + q * d + q * c + p * d)
        = a * c + b * d + (p * s + q * r) + (p * c + q * d + q * c + p * d) := by rw [← hl]
      _ = (a + q) * c + (b + p) * d + p * (c + s) + q * (d + r) := by ring
      _ = (b + p) * c + (a + q) * d + p * (d + r) + q * (c + s) := by rw [h1, h2]
      _ = a * d + b * c + (p * r + q * s) + (p * c + q * d + q * c + p * d) := by ring
      _ = rhs + (p * c + q * d + q * c + p * d) := by rw [← hr]

  exact MyNat.add_right_cancel h3

We register the multiplication we just defined with the Mul type class.

instance : Mul MyInt where
  mul := MyInt.mul

Registering simp lemmas for 0 and 1

We register the following lemmas so simp can automatically simplify multiplication by 0 and 1.

@[notation_simp]
theorem MyNat.toMyNat_one : MyNat.ofNat 1 = 1 := rfl

@[simp]
theorem MyInt.mul_one (m : MyInt) : m * 1 = m := by
  revert m
  unfold_int₁
  ring

@[simp]
theorem MyInt.one_mul (m : MyInt) : 1 * m = m := by
  revert m
  unfold_int₁
  ring

@[simp]
theorem MyInt.mul_zero (m : MyInt) : m * 0 = 0 := by
  revert m
  unfold_int₁

@[simp]
theorem MyInt.zero_mul (m : MyInt) : 0 * m = 0 := by
  revert m
  unfold_int₁
  ring

Proving commutativity, associativity, and distributivity

We prove commutativity, associativity, and distributivity for multiplication.

theorem MyInt.mul_comm (m n : MyInt) : m * n = n * m := by
  revert m n
  unfold_int₂
  ring

theorem MyInt.mul_assoc (m n k : MyInt) : m * n * k = m * (n * k) := by
  revert m n k
  unfold_int₃
  ring

theorem MyInt.left_distrib (m n k : MyInt) : m * (n + k) = m * n + m * k := by
  revert m n k
  unfold_int₃
  ring

theorem MyInt.right_distrib (m n k : MyInt) : (m + n) * k = m * k + n * k := by
  revert m n k
  unfold_int₃
  ring

Registering MyInt as a CommRing

Using the lemmas we have assembled so far, we register MyInt as a commutative ring (CommRing). This lets us use the ring tactic.

instance : CommRing MyInt where
  left_distrib := MyInt.left_distrib
  right_distrib := MyInt.right_distrib
  mul_assoc := MyInt.mul_assoc
  one_mul := MyInt.one_mul
  mul_one := MyInt.mul_one
  zero_mul := MyInt.zero_mul
  mul_zero := MyInt.mul_zero
  mul_comm := MyInt.mul_comm
  zsmul := zsmulRec
  neg_add_cancel := MyInt.neg_add_cancel

example (m n : MyInt) : (m - n) * (m + n) = m * m - n * n := by
  ring

Now that MyInt is registered as a CommRing, even fairly complex algebraic rewrites can be proved in a single call to the ring tactic.

The source code is available in the GitHub repository.