Leanにおける足し算の交換法則と結合法則

足し算の交換法則と結合法則を証明します。

交換法則も結合法則も数学的帰納法とsimpを使って証明できます。

-- 足し算の交換法則
theorem MyNat.add_comm (m n : MyNat) : m + n = n + m := by
  induction n with
  | zero => simp [ctor_eq_zero]
  | succ n ih =>
    simp [ih]

-- 足し算の結合法則
theorem MyNat.Int.add_assoc (l m n : MyNat) : l + m + n = l + (m + n) := by
  induction n with
  | zero => rfl
  | succ n ih =>
    simp [ih]

交換法則と結合法則を証明で使用するには、何に適用するかを指定しなければなりません。

example (l m n : MyNat) : l + m + n + 3 = m + (l + n) + 3 := calc
  _ = m + l + n + 3 := by rw [MyNat.add_comm l m]
  _ = m + (l + n) + 3 := by rw [MyNat.add_assoc m l n]

しかし、以下のようにライブラリの標準で用意されている演算の交換法則と結合法則を登録しておくことで、ac_rflタクティクを使用して証明できるようになります。

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

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

example (l m n : MyNat) : l + m + n + 3 = m + (l + n) + 3 := by
  ac_rfl