タクティクと証明のステップ

どの命題からどの命題へ進むかを、明示します。

16.1 自動化してもゴールは隠さない

証明が長くなると、等式を一つずつ書き換える作業が増えます。Tauto のタクティクは、その作業の一部を、証明項に展開するマクロです。ただし、書き換えの前後にどの命題があるかは、必ず書きます。

by rewrite!(e): 元のゴール {
  ⊢ 次のゴール from 次の証明
}

これは書式を示す図です。実際のコードでは、「元のゴール」と「次のゴール」に a = b などの命題を書きます。書き換えのモチーフを推論させず、書かれた二つのゴールから一つに決まるようにするのが、Tauto の方針です。

16.2 実際の書き換えを見る

リポジトリの examples/nat/Add.taut に、加算の交換法則の証明があります。命題を数式のまま書ける構文マクロ nat! を使っています。

pub theorem add_comm(n: Nat, m: Nat): nat!(`$n + $m = $m + $n`) {
  match m: nat!(`$n + $m = $m + $n`) {
    Zero => Eq::sym(add_zero_l(n))
    Succ(k) => by rewrite!(add_succ_l(k, n)): nat!(`$n + ${Succ(k)} = ${Succ(k)} + $n`) {
      ⊢ nat!(`$n + ${Succ(k)} = ${Succ(k + n)}`) from succ_cong(add_comm(n, k))
    }
  }
}

✓ theorem add_comm : ∀ n: Nat. ∀ m: Nat. n + m = m + n

nat! は、a = b に展開されます。$n は Tauto の変数 n を式に埋め込む書き方で、式を埋め込むときは ${Succ(k)} のように波括弧で囲みます。このファイルは、import "Lib.taut"（nat! の定義）と、add_zero_l、add_succ_l、succ_cong を同じファイルで先に証明しています。

rewrite! が何をしたかは、: のあとの元の等式と、⊢ のあとの次の等式を見比べると読めます。どちらかが実際のゴールと一致しなければ、カーネルに受け入れられません。

16.3 nat_norm! は算術を正規化する

pub theorem add_left_comm(a: Nat, b: Nat, c: Nat): nat!(`$a + ($b + $c) = $b + ($a + $c)`) {
  by nat_norm!(): nat!(`$a + ($b + $c) = $b + ($a + $c)`) {}
}

✓ theorem add_left_comm : ∀ a: Nat. ∀ b: Nat. ∀ c: Nat. a + (b + c) = b + (a + c)

nat_norm! は、自然数の加算・乗算などからなる式を正規化して、左辺と右辺の一致を証明するタクティクです。算術に、任意の性質を無条件で与えるわけではありません。

動かすには、リポジトリのルートで次のように検査します。

tauto check examples/nat/Add.taut

ok      add_comm
ok      add_assoc
ok      add_left_comm

（実際には、そのほかの定理も並びます。）

16.4 なぜ自動化を信頼しなくてよいのか

マクロが間違った証明項を生成しても、カーネルの検査を通らなければ、定理は受理されません。タクティクに許されるのは、証明の候補を作ることです。その候補が正しいかどうかを決めるのは、カーネルです。

演習 16.1：「自動化がバグを含んでいても、カーネルが健全なら、誤った定理の受理を防げる」と言える理由を、一文で書いてください。