MyNatに分配法則を追加してdistribタクティクを作る

今回は分配法則をうまく使って、多項式の同値な式を ac_rfl で証明できるところまで変形する方法を考えます。Mathlibには可換環の恒等式を自動的に証明する ring というタクティクがありますが、そのミニ版を自分で組み立ててみるようなイメージです。教材には引き続き「ゼロから始めるLean言語入門 手を動かして学ぶ形式数学ライブラリ開発」です。

rwで分配法則を適用する

まずは、すべて展開した多項式の和の形に変形する方法から考えます。rw タクティクに分配法則を渡すと、1回だけ適用されて止まってしまいます。

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

rw に分配法則を2回渡すことで、多項式の和の形まで変形できます。

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

simpでまとめて展開する

simp を使うと、適用可能な箇所をまとめて変形してくれるので、分配法則を何度も書く必要がなくなります。

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

つまり 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
  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

distribタクティクを作る

ring の代わりになる distrib というタクティクを作って、多項式の和の形に変換する処理をまとめてみます。macro コマンドを使うと、既存のタクティクの組み合わせに名前を付けて新しいタクティクとして定義できます。

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

ここまでの distrib だけでは、上の例を完全に証明することはできません。さらに変形が必要です。2や3を 1 + 1 + 1 のような形に変形して mul_one や one_mul を適用できるようにし、最後に 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

これらのタクティクを focus でまとめると、distrib だけで証明できるようになります。

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

3より大きい数値に対応する

今のままでは3より大きい数値を含む命題を証明できません。これを解決するために、別のマクロ expand_num を作ります。まず定理 unfoldNatList で x + 2 = x + 1 + 1 を証明し、OfNat.ofNat を使って Nat を MyNat に変換できるようにします。教科書では expand_num に simp only [Nat.reduceAdd] も追加されていましたが、なくても証明が通るためここでは外しています。

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]

distrib に expand_num を組み込むことで、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

tryで進捗なしエラーを回避する

現状の distrib だと、simp が何も変換できない場合にエラーになってしまいます。

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

そこで try を付けて、進捗がなくても無視するようにします。

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