MyIntに足し算を定義する

前回はMyIntを定義するためにPreIntとその同値関係を用意しました。今回はそのMyIntに足し算を定義していきます。本記事は「ゼロから始めるLean言語入門 手を動かして学ぶ形式数学ライブラリ開発」を参考にしています。

PreIntへの足し算の定義

まずは商を取る前のPreIntに足し算を定義します。PreIntは自然数のペアなので、対応する成分同士を足すだけです。

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

Quotient.lift₂によるMyIntの足し算の定義

MyIntの足し算を定義するために、Quotient.lift₂を使ってPreInt.addの定義域を商に持ち上げます。足し算は引数を二つ取るため、Quotient.liftではなくQuotient.lift₂を使用します。Quotient.lift₂を使うには、代表元の取り方に依存せず結果が一致すること、つまり同値関係が保たれることを証明する必要があります。

証明はQuotient.soundを適用してPreIntの世界に戻し、notation_simpで足し算の世界に変換したあとは等式変換で完了します。

def MyInt.add : MyInt → MyInt → MyInt := Quotient.lift₂ PreInt.add <| by
  -- ⊢ ∀ (a₁ b₁ a₂ b₂ : PreInt), a₁ ≈ a₂ → b₁ ≈ b₂ → a₁.add b₁ = a₂.add b₂
  intro (m1, m2) (n1, n2) (m'1, m'2) (n'1, n'2) rm rn
  dsimp [PreInt.add]
  -- rm : (m1, m2) ≈ (m'1, m'2)
  -- rn : (n1, n2) ≈ (n'1, n'2)
  -- ⊢ Quotient.mk PreInt.sr (m1 + n1, m2 + n2) = Quotient.mk PreInt.sr (m'1 + n'1, m'2 + n'2)
  apply Quotient.sound -- ⊢ (m1 + n1, m2 + n2) ≈ (m'1 + n'1, m'2 + n'2)
  notation_simp at *
  -- rm : m1 + m'2 = m2 + m'1
  -- rn : n1 + n'2 = n2 + n'1
  -- ⊢ m1 + n1 + (m'2 + n'2) = m2 + n2 + (m'1 + n'1)
  have : m1 + n1 + (m'2 + n'2) = m2 + n2 + (m'1 + n'1) := calc
    _ = (m1 + m'2) + (n1 + n'2) := by ac_rfl
    _ = (m2 + m'1) + (n1 + n'2) := by rw [rm]
    _ = (m2 + m'1) + (n2 + n'1) := by rw [rn]
    _ = m2 + n2 + (m'1 + n'1) := by ac_rfl
  assumption

instance instAddMyInt : Add MyInt where
  add := MyInt.add

#check (3 + 4 : MyInt)

足し算をsimpに登録する

足し算もsimpに登録しておきます。教科書ではdsimpで証明していましたが、エラーになったためrflを使用しています。

@[simp]
theorem MyInt.add_def (x1 x2 y1 y2 : MyNat)
  : ⟦(x1, y1)⟧ + ⟦(x2, y2)⟧ = (⟦(x1 + x2, y1 + y2)⟧ : MyInt) := by rfl

ゼロを足しても変わらないことの証明

整数にゼロを足しても値が変わらないことを証明し、simpに登録します。証明にはQuotient.inductionOnを使います。Quotient.inductionOnは、商型Quotient sの要素mに関する命題を証明するには、その代表元aについて証明すればよいという帰納法（同値類からの値の取り出し）の原理です。

mを与えて?_を残すと、Quotient.inductionOn mの第2引数である「任意の代表元aに対して命題が成り立つこと」を示す証明部分が新たなサブゴールとして生成されます。結果として、ゴールはm + 0 = mから代表元a（PreInt型）についての式に変化します。

@[simp]
theorem MyInt.add_zero (m : MyInt) : m + 0 = m := by
  refine Quotient.inductionOn m ?_
  -- ∀ (a : PreInt), Quotient.mk PreInt.sr a + 0 = Quotient.mk PreInt.sr a

  intro (a1, a2)
  apply Quot.sound
  notation_simp
  -- a1 a2 : MyNat
  -- ⊢ a1 + 0 + a2 = a2 + 0 + a1

  ac_rfl

@[simp]
theorem MyInt.zero_add (m : MyInt) : 0 + m = m := by
  refine Quotient.inductionOn m ?_
  intro (a1, a2)
  apply Quot.sound
  notation_simp
  ac_rfl

マクロによる証明の共通化

これまでの証明で何度も出てきた、整数についての問題を自然数についての問題に帰着させる手順をマクロにまとめます。次のコードのように、変数mのようなスコープ外の変数を直接参照するとエラーになります。これはマクロ衛生と呼ばれる仕組みによるものです。

section
  local macro "unfold_int₁" : tactic => `(tactic| focus
    refine Quotient.inductionOn m ?_
    intro (a1, a2)
    apply Quot.sound
    notation_simp
  )

  example (m : MyInt) : m + 0 = m := by
    fail_if_success unfold_int₁
    sorry
end

set_option hygiene falseでエラーを抑止することもできますが、望ましくありません。代わりにrevert mでローカルコンテキストからmを取り除いて⊢ ∀ (m : MyInt), 0 + m = mという形にし、マクロ側ではintroで改めてmを宣言することでこの問題を解決します。

macro "unfold_int₁" : tactic => `(tactic| focus
  intro m
  refine Quotient.inductionOn m ?_
  intro (a1, a2)
  apply Quot.sound
  notation_simp
)

example (m : MyInt) : 0 + m = m := by
  revert m -- ⊢ ∀ (m : MyInt), 0 + m = m
  unfold_int₁
  ac_rfl

結合法則と交換法則の証明

同様にunfold_int₂とunfold_int₃を作成し、足し算の結合法則と交換法則を証明してインスタンスとして登録します。

macro "unfold_int₂" : tactic => `(tactic| focus
  intro m n
  refine Quotient.inductionOn₂ m n ?_
  intro (a1, a2) (b1, b2)
  apply Quot.sound
  notation_simp
)

macro "unfold_int₃" : tactic => `(tactic| focus
  intro m n k
  refine Quotient.inductionOn₃ m n k ?_
  intro (a1, a2) (b1, b2) (c1, c2)
  apply Quot.sound
  notation_simp
)

theorem MyInt.add_assoc (m n k : MyInt) : m + n + k = m + (n + k) := by
  revert m n k
  unfold_int₃
  ac_rfl

theorem MyInt.add_comm (m n : MyInt) : m + n = n + m := by
  revert m n
  unfold_int₂
  ac_rfl

instance : Std.Associative (α := MyInt) (· + ·) where
  assoc := MyInt.add_assoc

instance : Std.Commutative (α := MyInt) (· + ·) where
  comm := MyInt.add_comm

ソースコード全体はGitHubで公開しています。