今日の証明

Chapter4を読み進める。

Include "../lib/plus.g".

Classify
  induction(n:nat) return Forall(m:nat). { (plus n (S m)) = (S (plus n m)) } with
    Z =>
      foralli(m:nat).
        trans cong (plus * (S m)) n_eq
        trans join (plus Z (S m)) (S (plus Z m))
              cong (S (plus * m)) symm n_eq
  | S n' =>
      foralli(m:nat).
        trans cong (plus * (S m)) n_eq
        trans join (plus (S n') (S m)) (S (plus n' (S m)))
        trans cong (S *) [n_IH n' m]
        trans join (S (S (plus n' m))) (S (plus (S n') m))
              cong (S (plus * m)) symm n_eq
  end.

ここで、S n'の方の
n_eq
は、
n = S n'
になる。"n ="の右側はinductionで与えられた"S n'"が当てはまるだけ。

cong (plus * (S m)) n_eq
は
(plus n (S m)) = (plus (S n') (S m))
になる。*のところに、nとS n'が当てはまる。

join (plus (S n') (S m)) (S (plus n' (S m)))
は
(plus (S n') (S m)) = (S (plus n' (S m)))
になる。単に=で結ぶだけ。

[n_IH n' m]
は
(plus n' (S m)) = (S (plus n' m))
になる。仮定{ (plus n (S m)) = (S (plus n m)) }の、変数を、与えられたsubterm、n' mで置き換えるだけ。

cong (S *) [n_IH n' m]
は
(S (plus n' (S m))) = (S (S (plus n' m)))
ですね。

symm n_eq
は、
S n' = n
になる。単に右辺と左辺を置き換えるだけ。

こうやっていくと、最終的にできあがる式は、
(plus n (S m)) = (plus (S n') (S m))
(plus (S n') (S m)) = (S (plus n' (S m)))
(S (plus n' (S m))) = (S (S (plus n' m)))
(S (S (plus n' m))) = (S (plus (S n') m))
(S (plus (S n') m)) = (S (plus n m))
の５つ。
transは各式を推移的に結びつけるので、残るのは、
(plus n (S m)) = (S (plus n m))
となって、 証明すべき式が作れたことになる。

等式の証明をするときの基本戦略は、まず各変数から右辺、左辺を作り、
transできるように式を変形していくイメージかな。