Lean 4でMyIntの掛け算を定義する

前回の記事ではMyIntの足し算を定義し、可換群(AddCommGroup)として登録することでabelタクティクが使用できるようになりました。今回はMyIntの掛け算を定義し、可換環(CommRing)として登録することでringタクティクを使用できるようにします。参考書籍はゼロから始めるLean言語入門 手を動かして学ぶ形式数学ライブラリ開発です。

MyNatをCommSemiringとして登録する

掛け算に関する証明でringタクティクを使うためには、まず自然数MyNatを可換モノイド(AddCommMonoid)かつ可換半環(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に対してabelタクティクとringタクティクの両方が使用できるようになりました。

PreIntの掛け算を定義する

MyIntの掛け算を定義するために、まずPreIntに対する掛け算を定義します。(m1 - m2) * (n1 - n2) を展開すると m1 * n1 + m2 * n2 - (m1 * n2 + m2 * n1) となるため、PreInt.mulは以下のように定義できます。

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

MyIntの掛け算を定義する

PreInt.mulの定義域をQuotient.lift₂で変更し、MyIntの掛け算を定義します。Quotient.lift₂を使用するには、同値な入力をPreInt.mulに渡したときに結果も等しくなることを証明する必要があります。

この証明では、K = (p * c + q * d + q * c + p * d) とおき、lhs + K = rhs + K という形に持ち込んで、仮定h1, h2で置き換えることで両辺が等しいことを示します。

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

作成した掛け算をMul型クラスに登録します。

instance : Mul MyInt where
  mul := MyInt.mul

0と1に関するsimp補題を登録する

0や1との掛け算をsimpで自動的に簡約できるように、以下の補題を登録します。

@[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

交換法則・結合法則・分配法則を示す

掛け算に関する交換法則、結合法則、分配法則を証明します。

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

MyIntをCommRingとして登録する

ここまでで揃えた補題を使い、MyIntを可換環(CommRing)として登録します。これでringタクティクが使用できるようになります。

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

MyIntがCommRingとして登録されたことで、複雑な式変形もringタクティク一発で証明できるようになりました。

ソースコードはGitHubリポジトリで公開しています。