数学の証明を書く

分野の記法、calc!、proof!、タクティクを使い分けて、数学の証明を読みやすく書きます。

17a.1 どの道具をいつ使うか

13〜17章の証明は、match と Eq::trans・Eq::congr を手で組み合わせていました。等式が長くなる数学の証明では、同じ内容を次の道具で、紙の上の証明に近い形で書けます。どの道具を使っても、最後に受理するかどうかを決めるのは、これまでと同じカーネルです。

17a.2 calc! で等式を連ねる

calc!(`$a = $b from $p = $c from $q`) は、式 a から始めて、一行ごとに「次の式」と「その一行の証明」を書く構文マクロです。import std::Calc { calc } で読み込みます。式と証明は、ほかの構文マクロと同じく $ で埋め込みます。std/Nat.taut の Nat::add_swap も、この形で書かれています。

import std::Base { Nat }
import std::Calc { calc }
import std::Nat { Nat }

theorem add_swap_ex(a: Nat, b: Nat, c: Nat): Nat::add(Nat::add(a, b), c) = Nat::add(Nat::add(a, c), b) {
  calc!(```
    $Nat::add(Nat::add(a, b), c)
    = $Nat::add(a, Nat::add(b, c)) from $Nat::add_assoc(a, b, c)
    = $Nat::add(a, Nat::add(c, b)) from $Eq::congr(⟦Nat::add(a, □)⟧, Nat::add_comm(b, c))
    = $Nat::add(Nat::add(a, c), b) from $Eq::sym(Nat::add_assoc(a, c, b))
    ```)
}

// 結合律、交換律、結合律の逆向き、の三行で式を入れ替える

✓ theorem add_swap_ex : ∀ a: Nat. ∀ b: Nat. ∀ c: Nat. Nat::add(Nat::add(a, b), c) = Nat::add(Nat::add(a, c), b)

各行の from の右には、その行の等式 前の式 = 次の式 の証明を書きます。この例の三行は、順に結合律、b + c を c + b に替える交換律、結合律の逆向きです。calc! は、これらを右結合の Eq::trans の入れ子に展開します。カーネルが受け取る項は、手で Eq::trans を並べたものと変わりません。

二行目の ⟦Nat::add(a, □)⟧ は合同の文脈です。□ は一つだけ書け、式の中でそこだけを別の式に差し替えます。この例では b + c = c + b を、a + □ の穴に入れて a + (b + c) = a + (c + b) に持ち上げています。(z: Nat) => Nat::add(a, z) という λ を Eq::congr に渡すのと同じです。

定義から等しい行も、from Refl と書いて省きません。計算で等しいことを、読み手がその場で確かめられるようにするためです。

calc! は = のほかに ↔ の連鎖も書けます。

import std::Calc { calc }

theorem iff_chain(P: Prop, Q: Prop, R: Prop, pq: P ↔ Q, qr: Q ↔ R): P ↔ R {
  calc!(```
    $P
    ↔ $Q from $pq
    ↔ $R from $qr
    ```)
}

// ↔ の連鎖

✓ theorem iff_chain : ∀ P: Prop. ∀ Q: Prop. ∀ R: Prop. (Iff(P, Q)) -> (Iff(Q, R)) -> Iff(P, R)

= と ↔ を一つの連鎖に混ぜることや、≤・< を連ねることは、まだできません。

17a.3 構文マクロで分野の記法を作る

Eq(Nat, Nat::add(n, m), Nat::add(m, n)) と書く代わりに、n + m = m + n と書きたい。数学の分野ごとの記法は、構文マクロで作ります。言語に分野の記法を足すのではなく、ライブラリが自分の記法を定義して、証明が import します。

examples/nat/Lib.taut は、自然数の命題の記法 nat! を定義します（以下の三つのコードは、このファイルからの抜粋です）。まず syntax! で文法を書きます。

syntax!(nat, ```par
%start Stmt
%title "nat"
%%
Stmt: Disj [Arrow Stmt];
Disj: Conj { OrTok Conj };
Conj: Rel { AndTok Rel };
Rel: Sum RelTail;
RelTail: EqTail | LeTail | LtTail | DvdTail;
EqTail: Equals Sum;
LeTail: LeTok Sum;
LtTail: LtTok Sum;
DvdTail: Bar Sum;
Sum: Prod { Plus Prod };
Prod: Atom { Star Atom };
Atom: Num | Paren | Embed;
Paren: LParen Sum RParen;
Embed: TautoExpr;
Num: /[0-9]+/;
Equals: '=';
LeTok: '<=';
LtTok: '<';
Bar: '|';
Arrow: '->';
AndTok: 'and';
OrTok: 'or';
Plus: '+';
Star: '*';
LParen: '(';
RParen: ')';
```) => enum Atom, struct Conj, struct Conj_Rep1, struct Disj, struct Disj_Rep1,
  struct DvdTail, struct EqTail, struct LeTail, struct LtTail, struct Paren,
  struct Prod, struct Prod_Rep1, struct Rel, enum RelTail, struct Stmt,
  struct Stmt_Opt1, struct Sum, struct Sum_Rep1, fn parse

文法から、各規則に対応する型付きの構文木（nat::Sum、nat::Rel など）が作られます。=> … の一覧は、作られる宣言の完全な一覧です。足りない名前や余った名前があるとエラーになります。Embed: TautoExpr は、$n や $Succ(k) のように、Tauto の式を記法の中に埋め込むための規則です。分野の記号（+、*、=、<=、|）は、この文法の中にだけ書かれ、言語には組み込まれていません。

次に、構文木から Tauto の式を作る関数と、マクロの入口を書きます。

pub fn nat_rel(r: nat::Rel): SynExpr ! {macro_error, Div} {
  let l := nat_sum(r.sum)
  match r.rel_tail {
    EqTail(t) => {
      let x := nat_sum(t.sum)
      quote { Eq(Nat, $l, $x) }
    }
    LeTail(t) => {
      let x := nat_sum(t.sum)
      quote { Le($l, $x) }
    }
    LtTail(t) => {
      let x := nat_sum(t.sum)
      quote { Lt($l, $x) }
    }
    DvdTail(t) => {
      let x := nat_sum(t.sum)
      quote { Dvd($l, $x) }
    }
  }
}

quote { … } は式を作る構文で、$l と $x に作った式を差し込みます。= が Eq(Nat, …)、<= が Le、< が Lt、| が Dvd（割り切り）になります。and と or は And と Or、-> は関数型（含意）に展開されます。この展開は、既存の項（Eq、Le、…）の呼び出しに限られます。カーネルに新しい規則は加わらないので、記法を増やしても信頼する範囲は広がりません。

pub macro fn nat(s: nat::Stmt): SynExpr ! {macro_error, Div} {
  let l := nat_disj(s.disj.conj, s.disj.rep)
  match s.opt {
    None => l
    Some(o) => {
      let r := nat(o.stmt)
      ExPi(Cons(SynParam { name: None, ty: l }, Nil), r, None, s.span)
    }
  }
}

これで nat!(`$n + $m = $m + $n`) は Eq(Nat, n + m, m + n) と読まれます。記法の文字列は、バッククォートで囲みます。

作られた型は、tauto syntax show で確かめられます。リポジトリのルートで実行します。

tauto syntax show examples/nat nat

enum nat::Atom {
  Num(SynToken)
  Paren(nat::Paren)
  Embed(SynExpr)
}
struct nat::Conj { span: SynSpan, rel: nat::Rel, rep: List(nat::Conj_Rep1) }
…

使う側では、定理の命題が数式のままになります。16章で見た add_comm が、その例です。examples/nat の Add・Mul・Order・Dvd・More は、すべて nat! で書かれています。

17a.4 proof! で文章に近い形に書く

proof! は、英語の証明の文章と、その文章から証明項を組み立てる短いプログラムを受け取って、証明項を作る構文マクロです。文章の側は、数学の証明が述べることをそのまま並べます。プログラムの側は、文章に書かれていない残りだけを書きます。探索はせず、同じ入力からは必ず同じ項ができます。作られた項は、通常どおりカーネルが検査します。プログラムが間違っていても、誤った定理が受理されることはありません。

今の std には、proof! が二つの形であります。

• std::proof::Lang の proof!：ラベル付きの文を木に並べ、各文を Forms の文型（By induction on …、We have …）が証明項に変える形。
• std::proof::Proof の proof!：文章のあとに %% を置き、続けて構築プログラムを書く形。examples/nat/proof/Add.taut が使っています。

Lang の proof!

子の文は、親の文より深くインデントして書きます。By induction on n. の子の文が、構成子ごとの場合になります。ラベル（[1] など）は、後ろから参照する文にだけ付けます。

import std::Base { Nat }
import std::proof::Lang { proof }
import std::proof::Forms { proof_by, proof_case, proof_we }

theorem add_zero_left(n: Nat): Nat::add(0, n) = n {
  proof!(```
    By induction on n.
      Case Zero. By Refl.
      Case Succ(k). We have Nat::add(0, Succ(k)) = $Succ(0 + k) = Succ(k) by the induction hypothesis.
  ```)
}

// 帰納法の仮定で場合 Succ(k) を閉じる

✓ theorem add_zero_left : ∀ n: Nat. Nat::add(0, n) = n

We have a = b = c by R. は等式の連鎖です。各段を Eq::trans でつなぎ、理由の書かれていない段は、計算で等しいもの（Refl）として扱います。最後の段の理由 the induction hypothesis は、Succ(k) の場合の帰納法の仮定です。式のうち、$ で始まる部分は Tauto の式の埋め込みです。$Succ(0 + k) のように、呼び出しの括弧の中には演算子も書けます。

文型は、利用する側が import します。ここでは proof_by（By …）、proof_case（Case …）、proof_we（We have …）です。

文型には、ほかに次のようなものがあります。

h が矛盾している場合は、This contradicts h. と書きます。

import std::Base { Nat }
import std::proof::Lang { proof }
import std::proof::Forms { proof_this }

theorem no_succ_le_zero(n: Nat, h: Nat::le(Succ(n), Zero) = true): False {
  proof!(```
    This contradicts h.
  ```)
}

// h が矛盾していれば何でも導ける

✓ theorem no_succ_le_zero : ∀ n: Nat. ¬(Nat::le(Succ(n), Zero) = true)

等式の連鎖に名前を付けて、後ろの文で使うこともできます。名前を付けた連鎖は、プログラム（%% の後ろ）で渡します。

import std::proof::Lang { proof }
import std::proof::Forms { proof_by, proof_we }

theorem named<A>(
  op: (A, A) -> A,
  unit: A,
  a: A,
  b: A,
  h1: op(a, b) = a,
  h2: a = unit
): unit = op(a, b) {
  proof!(```
    [1] We have h: op(a, b) = a by h1 = unit by h2. By Eq::sym.
    %%
    [1] h
  ```)
}

// 連鎖に h と名前を付け、プログラムで渡す

✓ theorem named : ∀ A: Type. ∀ op: (A) -> (A) -> A. ∀ unit: A. ∀ a: A. ∀ b: A. (op(a, b) = a) -> (a = unit) -> unit = op(a, b)

h1 は op(a, b) = a の理由、h2 は a = unit の理由です。連鎖 op(a, b) = a = unit に h と名前を付け、最後の By Eq::sym. に h を渡して、ゴール unit = op(a, b) を閉じています。

Proof の proof!

もう一つの形は、1 つの文章と 1 つのプログラムを %% で区切ります。examples/nat/proof/Add.taut の証明を見ましょう。

pub theorem succ_inj<a: Nat, b: Nat>(h: Succ(a) = Succ(b)): a = b {
  proof!(```
    [main] We have $a = $pred(Succ(a)) = $pred(Succ(b)) = $b.

    %%
    main:calc(conv,congr($pred,$h),conv)
    ```)
}

✓ theorem succ_inj : ∀ a: Nat. ∀ b: Nat. (Succ(a) = Succ(b)) -> a = b

文章の We have $a = … = $b. は、17a.2 の calc と同じ等式の列です。プログラムの main:calc(conv,congr($pred,$h),conv) は、隣り合う式の組ごとの理由を、順に並べたものです。

• conv：計算だけで等しい。pred(Succ(a)) は a に簡約されます。
• congr($pred,$h)：h: Succ(a) = Succ(b) を、pred で持ち上げる。
• app：式を埋め込んだ証拠（$succ_cong(ih) など）を使う。

ラベル main は文章のラベルです。プログラムは、文章の各ラベルに命令を割り当てます。次の帰納法の証明は、文が複数のラベルを持つ例です。

pub theorem add_zero_l(n: Nat): nat!(`0 + $n = $n`) {
  proof!(```
    [main] We prove $nat!(`0 + $n = $n`) by induction on $n.
    [zero] Case Zero is immediate.
    [succ] Case Succ($k).
      Assume $k: $Nat, $ih: $nat!(`0 + $k = $k`).
      We have $(0 + Succ(k)) = $Succ(0 + k) = $Succ(k).

    %%
    main:ind(zero:refl,succ:calc(conv,congr($Succ,$ih)))
    ```)
}

✓ theorem add_zero_l : ∀ n: Nat. 0 + n = n

main:ind(zero:refl,succ:calc(…)) は、main の文が帰納法で、zero の場合が refl、succ の場合が calc だと述べています。Assume $k: $Nat, $ih: … は、場合の変数と帰納法の仮定の名前を、型つきで書き下しています。型は文章に書かれるので、読み手は仮定が何かを、プログラムを読まずに知れます。

プログラムの命令は次のとおりです。

add_comm の証明は、sym・rewrite・calc を組み合わせた例です。

pub theorem add_comm(n: Nat, m: Nat): nat!(`$n + $m = $m + $n`) {
  proof!(```
    [main] We prove $nat!(`$n + $m = $m + $n`) by induction on $m.
    [zero] Case Zero.
      We prove $(n + Zero = Zero + n).
      By symmetry of [left].
    [left] We prove $(0 + n = n).
      By $add_zero_l(n).
    [succ] Case Succ($k).
      Assume $k: $Nat, $ih: $(n + k = k + n).
      We prove $nat!(`$n + $Succ(k) = $Succ(k) + $n`).
      Using $add_succ_l(k, n): $nat!(`$Succ(k) + $n = $Succ(k + n)`), rewrite the goal to
      $nat!(`$n + $Succ(k) = $Succ(k + n)`).
    [cong] We have $(n + Succ(k)) = $Succ(n + k) = $Succ(k + n).

    %%
    main:ind(zero:sym(left:app),succ:rewrite(cong:calc(conv,app($succ_cong(ih)))))
    ```)
}

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

rewrite の文章は、使う等式と、書き換え後のゴールの両方を書きます。16章の rewrite! と同じく、どこをどう書き換えるかが、読み手に見えます。なお、この例の命題は、17a.3 の nat! で書かれています。分野の記法と proof! は、このように組み合わせます。

17a.5 算術の等式を一手で閉じるタクティク

ring のように、等式を正規形で比べる証明は nat_norm! が行います。+・*・Succ・数のリテラル、それ以外の項を変数と見て、両辺が同じ正規形になることを、Nat::norm_eq 定理の適用として示します。

import std::Tactic { nat_norm }

theorem square_sum(a: Nat, b: Nat): (a + b) * (a + b) = a * a + 2 * a * b + b * b {
  by nat_norm!(): (a + b) * (a + b) = a * a + 2 * a * b + b * b {}
}

// 両辺が同じ正規形になるので、腕は書かない

✓ theorem square_sum : ∀ a: Nat. ∀ b: Nat. (a + b) * (a + b) = a * a + 2 * a * b + b * b

タクティクが信頼されるのではありません。読み取りが間違っていれば、カーネルが Refl を受け取らず、証明は通りません。ゴールを残さないタクティクなので、腕（{} の中身）は書きません。不等式 l <= r = true と l < r = true には nat_le! があります。

仮定を使う必要がある等式は、nat_norm! では閉じません。calc! や rewrite! の一歩で仮定を使い、残りの算術を nat_norm! に任せる、という使い分けになります。

17a.6 書きかけと読み直し

証明は、一気には書けません。ゴールの穴 ?名前 を置くと、検査はその宣言を「未完」として扱い、受理せずに、穴のゴールと文脈を教えてくれます。

import std::Base { Nat }

theorem add_zero_right(n: Nat): Nat::add(n, 0) = n {
  ?todo
}

// 穴を残した宣言は、受理されず未完になる

… theorem add_zero_right : ∀ n: Nat. Nat::add(n, 0) = n

?todo  (4:3)
  n : Nat
⊢ Nat::add(n, 0) = n

tauto goals src/todo.taut

?todo in add_zero_right (src/todo.taut:5:3)
  n : Nat
⊢ Nat::add(n, 0) = n

次に何を書くか迷うとき、tauto suggest FILE --hole todo は、ゴールに当てはまる補題の候補を挙げます。--verify を付けると、候補を実際に検査します。

書き終えた証明は、tauto proof が自然な文章にして読み上げます。calc! で書いた 17a.2 の証明を読ませてみます。

tauto proof src/calc.taut add_swap_ex --format natural

add_swap_ex
Assume a: Nat, b: Nat, c: Nat.
We prove Nat::add(Nat::add(a, b), c) = Nat::add(Nat::add(a, c), b).

Nat::add(Nat::add(a, b), c) = Nat::add(a, Nat::add(b, c))    (Nat::add_assoc(a, b, c))
 = Nat::add(a, Nat::add(c, b))    (Nat::add_comm(b, c) and congruence)
 = Nat::add(Nat::add(a, c), b)    (Nat::add_assoc(a, c, b) in reverse)

証明項から作られる文章なので、書き手の意図ではなく、実際に受理された項が何をしているかを表します。AI が書いた証明を人間が確かめるときは、この出力を読みます。tauto assumptions FILE NAME は、その定理が公理や外部関数に頼っていないかを、一覧にします。

17a.7 どれを選ぶか

• 式を一行ずつ変形する等式の証明は、まず calc!。
• 同じ分野の定理を何本も書くなら、その分野の記法を構文マクロで作る。
• 帰納法や場合分けを含み、人に読んでもらいたい証明は、proof!。
• 加算と乗算だけの恒等式は、nat_norm!。
• 迷ったら穴 ?名前 を置き、tauto goals でゴールを見る。

演習 17a.1：17a.2 の add_swap_ex を、Nat::add_assoc と Nat::add_comm を Eq::trans で直接つないで書き直してください。calc! を使うと、何が読みやすくなりますか。

演習 17a.2：Nat::add(a, b) = Nat::add(b, a) を、17a.4 の Lang の proof! で、b に関する帰納法で書いてみてください。うまくいかない箇所に ?todo を置いて、tauto goals で何が必要かを調べましょう。