4 実例①　定義をどこまで開くか

6.book の定義で、べき集合の和集合は元の集合、を示します。
⋃℘ … \(\bigcup ( \wp X ) = X\) \(\blacktriangleleft\) \(\mathbb{W}.\)
最初からこのprfが書けたわけではありません。試した順に並べます。
　⋃℘ / W. -| O p; … FAIL（Prover9 not_proved: No proof found）
　⋃℘ // W. -| O p; … FAIL（同じ）
　⋃℘ /// W. -| O p; … FAIL（同じ）。v; に替えても Vampire not_proved (CounterSatisfiable)
　⋃℘ //// W. -| O p; … OK（Prover9 に2本、それぞれ約0.01秒）
どれもすぐに落ちています。これは「探索が重い」ではなく「この形のままでは証明が見つからない」という落ち方です（第6章）。原因は、証明器に渡った goal を読むと分かります。/ の本数ごとに、goal には次の形が開かずに残っていました（Prover9 の入力を抜粋。wp は ℘、sub は ⊂）。
　/ … in(w1,Cup(wp(xX))) -> in(w1,xX)（⋃ の所属がまだ残る）
　// … exists w2 (in(w2,wp(xX)) & in(w1,w2)) -> in(w1,xX)（℘ の所属が残る）
　/// … exists w2 (sub(w2,xX) & in(w1,w2)) -> in(w1,xX)（⊂ が残る）
1本ごとに1層ずつ開いていきます。⊂ が開かないうちは「w2 ⊂ X かつ w1 ∈ w2 なら w1 ∈ X」が証明器には分からないので、示せません。
本数を増やすのをやめる目安：///// にしても、証明器に渡る入力は //// と1文字も変わりませんでした（もう開くものが無い）。入力が変わらなくなったら、本数を増やしても意味がありません。逆に開きすぎは、式が大きくなって timeout の元になります（最初の早見表）。
証明器に渡った入力は、査読画面で OK の印や FAIL の欄の「投げた入力を見る」を押すと見られます。CLI では review_cli.php <本の名前> --inputs と --inputs を付けると、FAIL した行の下に出ます。読み方は 1.book「CLIから査読する」・3.book「途中の段が落ちたとき」。slash の書き換えだけなら、証明器に投げずに slash_cli.php 0_tutorial_AI/6 '`⋃ (℘ X) = X` /// W.' で確かめられます（結果は前置記法で [∀ w1 [⇔ [∃ w2 [and [⊂ w2 X] [∈ w1 w2]]] [∈ w1 X]]]＝⊂ が残っている）。予測を立ててから本数を決めるのに使います。

5 実例②　前提が足りない・補題が要る

6.book では、対集合公理 ax_set2 を置換公理 ax_r から導きました。そこでは補題 le_set2（相異なる2元をもつ集合がある）を前提に加えています。この補題を外すと次のようになります。
　ax_set2 --| ax_r_atST v; … FAIL（Vampire timeout・約90秒）
　ax_set2 --| ax_r_atST , le_set2 v; … OK
今度は時間切れです。ax_r の実例は「相異なる s, t をもつ集合 C があれば、その像は \(\{u,v\}\)」と言っているので、証明器はそのような C を自分で見つけなければなりません。そのような C（例えば ℘ (℘ ∅)）を作るには ℘ と ∅ の定義が要りますが、この段の前提には入っていません。つまり、この段はそもそも前提から示せない可能性があります。示せない問題でも、すぐに「示せない」と返るとは限らず、timeout になることがあります。そこで「そういう C がある」を別の Thm（le_set2）として先に示し（6.book では ℘. , ∅. , ⊂. から）、前提に置きました。
このように、証明器に証人（存在を示すための具体的なもの）を自力で発明させている段は、timeout しやすいです。証人を明示した補題を立てると通ることが多いです。
補題の切り方の目安：
　・ 証人が要る所で切る（上の例）。
　・ 数学の場合分けで切る（x ∈ A のときと x ∉ A のとき、など）。1つの段の前提が減って速くなります。
　・ 「写像である」のような部分と「単射である」のような性質の部分を分け、前者は既に示したThmを前提に置く。
　・ 他の定理でも使いそうなら、prf の中のラベルではなく、Book の中の名前付きの Thm にして後で前提に引く。
　・ 数学の要の一点で切る。技術的な細部ではなく、仮定を引く段が1つで済み、残りの段がそこから出る補題を探す（standard_math/1-2 の CSBpiece の Lkey＝X∖A が g[Y∖f[A]] に一致する）。
　・ 補題の結論には、使う段が必要とするものだけを書く。余分な and があると、その分だけ証明器に投げる本数と前提が増える。同値（⟺）の補題は ⟹ と ⟸ に分け、使う段ごとに要る方だけ引く（使わない結論を1つ外しただけで、投げる本数が2本から1本になった例があります）。
　・ 1回しか使わない補題の段は、使う段にまとめる（articles1/25 では f' ∈ X →IS Y を示す段を置かず、goal が |X =# |Y の段で /// W.' を当てて直接示す。投げ先は v;）。

6 失敗の種類を見分ける

FAIL の文言は、大きく4種類に分かれます。種類によって次の一手が違います。
1. 証明器が動く前に落ちた（「本が紹介していない word」「翻訳不可」「Formとして消費されないword」など）：書き方か、関係（-| と --|）の選び方の問題です。数学の中身はまだ試されていません。文言が指す語・行を直します。
2. すぐに「示せない」（Prover9 の No proof found が短時間で出る、Vampire の CounterSatisfiable）：この前提とこの展開のままでは証明が見つからなかった、ということです（Prover9 は探索を制限しているので、「示せないことが確定した」とまでは言えません）。考えられるのは、定義が開ききっていない（実例①）、前提が足りない、主張が偽、のどれかです。CounterSatisfiable は、証明器に渡した問題（翻訳した後の式）に反例があるという意味で、元の主張が偽だとは限りません。開いていない記号が入力に残っていないか、足りない定義・補題が無いかを先に疑います。
3. 時間切れ（timeout）：探索が重い、ということです。開きすぎ（W.!〇. で特定の定義を開かないようにする）、証人を自力で探させている（実例②）、1つの段に詰め込みすぎ（補題に分ける）、のどれかを疑います。前提を削りすぎた場合も timeout になることがあります。
4. 証明器の段は通ったのに、最後の h; の段で落ちた：各段は示せていますが、それらを組み合わせても thm の主張にならない、ということです。多くは段どうしのつなぎ方の問題です。最後の段の goal・sos が thm の行と合っているか、途中で使った定義が W. に入っているか（入っていない定義で開いた段はつなげません）を確かめます。
投げ先（p; v; s;）の選び方は最初の早見表にあります。

6.1 実例：症状から直すまで

・ 2. すぐに示せない → / を足す。最初に書いた prf `X ⊂ X ∪ Y` / W. -| O p; `X ⊂ X ∪ Y` -| W. h; は「Prover9 not_proved: No proof found.」。--inputs で見た入力は formulas(sos).end_of_list.formulas(goals).(all w1 (in(w1,xX) -> in(w1,cup(xX,xY)))).end_of_list. で、⊂ は開いたが ∪ の所属 cup(xX,xY) が残っています。/ を2本にすると通ります。
\(X \subset X \cup Y\) \(\blacktriangleleft\) \(\mathbb{W}.\)
　ソース：thm `X ⊂ X ∪ Y` ◀ W.　prf `X ⊂ X ∪ Y` // W. -| O p; `X ⊂ X ∪ Y` -| W. h;
・ 1. 証明器が動く前に落ちた → 関係を替える。クラス変数の推移律に -| O p; と書くと「capsule-error: |0 翻訳不可: cvt+ 後に ∈_ が残っています。クラス変数への所属は述語に置き換えられません。」。{s,c}ソートのまま Vampire に投げると通ります（◀ O v; でも同じく OK＝実測）。
\(X \subset Y \subset Z \Longrightarrow X \subset Z\) \(\blacktriangleleft\) O
　ソース：thm `[ chain X_ ⊂_ Y_ ⊂_ Z_ ] ⟹ X_ ⊂_ Z_` ◀ O　prf `[ chain X_ ⊂_ Y_ ⊂_ Z_ ] ⟹ X_ ⊂_ Z_` --| O v;

7 通ったあとで

7.1 前提を最小にする

通ったら、前提を1つずつ外して試します。外しても通る前提は要らなかったものです。前提が少ないほど探索は速く、読む人にも何を使ったかが分かります。

7.2 前提が強すぎないかを点検する

前提に量化子で縛られていない変数を書くと、「すべての〜について」の意味になります。そのせいで前提が矛盾していると、何でも証明できてしまいます。4.book の例がそれです。
\({\perp}\) \(\blacktriangleleft\) \(x \neq y\)
前提から ⊥（偽）が示せてしまうなら、その前提は矛盾しています。思ったより簡単に通ったときは、goal を ⊥ に替えて同じ前提で試すと点検できます。ただし、矛盾していなくても強すぎる前提はあります。5.book の x ∈_ |B_ ◀ x ∈_ A_ の前提 x ∈_ A_ は「すべてのもの x がすべてのクラス A_ に属する」という式で、A_ に |B_ を入れれば goal そのものです。この前提から ⊥ は示せません（実測で反例あり）が、どんな y ∈_ |B_ も示せます。前提を O にすると反例が見つかって落ちます。また、⊥ が示せないことは、前提が矛盾していないことの証明にはなりません（見つからなかっただけかもしれません）。点検では ⊥ だけでなく、主張と関係の無い式も試します。変数の名前を替えただけの y ∈_ |B_ は goal と同じ意味（自由な変数は「すべての」）なので点検になりません。|a ∈_ |D_ のように、主張に出てこない定数についての式を試します（この前提からは示せてしまいます＝実測）。
集合版の完全な例：`|a ∈ |B` ◀ `x ∈ A` は -| `x ∈ A` p; で一瞬で通りますが、前提 x ∈ A は「すべての x がすべての A に属する」です。点検の式 `|c ∈ |D` ◀ `x ∈ A` も通ってしまう（実測）ので、前提が強すぎると分かります。「A の元はすべて B の元で、a は A の元」という意図なら、定数で書きます。
\(\mathrm{a} \in \mathrm{B}\) \(\blacktriangleleft\) \(\forall x ( x \in \mathrm{A} \Longrightarrow x \in \mathrm{B} )\) ，\(\mathrm{a} \in \mathrm{A}\)
　ソース：thm `|a ∈ |B` ◀ `∀ x (x ∈ |A ⟹ x ∈ |B)` , `|a ∈ |A`　prf `|a ∈ |B` -| `∀ x (x ∈ |A ⟹ x ∈ |B)` , `|a ∈ |A` p;

8 よく使う証明の形

articles の prf で何度も出てくる形です。例はどれも実際の本の行で、査読を通っています。

8.1 帰納法：IND𝕄 にクラスを代入する

「すべての k ∈ 𝕄 で P(k)」は、帰納法の公理 IND𝕄（0 ∈_ C_ で、m ∈_ C_ ⟹ m suc ∈_ C_ なら 𝕄 ⊂_ C_）の C_ に \{ cls k | P(k) \} を代入して示します。底の段 Lb と一歩の段 Ls を先に置き、代入した IND𝕄 と並べて sos に書きます。例：articles3/0-pa.book の +A（結合法則）。

　代入するクラスの中のほかの変数（ここでは x・y）は自由なままでかまいません。前提の自由変数は「すべての x・y について」の意味です（3.book・4.book「自由変数の罠」）。Lb・Ls の m・n と名前が違っても、どちらも「すべての」と読むので同じことです。集合で自然数を作る本（0-sn）では、IND𝕄 の代わりに INDC[D_:=…] を使います（58.book の choose∈𝕄）。

8.2 強い帰納法

「b より小さいすべての数で成り立てば b でも成り立つ」の形は、性質を [ ∀ z ∈ 𝕄 . (z < b ⟹ P(z)) ] にして普通の帰納法を使います。底は「z < 0 となる z は無い」、一歩は L<S（z < b suc ⟹ z < b or z = b）で場合を分けます。最後に L<s（n < n suc）で P(n) を取り出します。例：articles3/0-pa.book の SIND𝕄（性質をクラス変数 D_ への所属にしたもの・次の小節）。

8.3 強い帰納法を定理にする

強い帰納法を何度も使う本では、上の形を1つのクラス変数の Thm にしておくと、使う段は代入した実例を引く1段になります。段の末尾に {D_.-}（D_ への所属を新しい述語に置き替える・1.book の辞書）を付けると -| の段のまま示せ、h; で結べます（多ソートの段 --| … v; で示して -| … h[lift]; で結ぶ書き方もありますが、その〇は multisort→tfl に依存します・3.book「h; の段の関係」）。名前は prop/thm、自由なクラス変数は D_ にします（6.book「分出公理」の注意）。

　（この Thm は articles3/0-pa.book にあり、1・11・23-1・3b・60・69・69b・80-1・80 が使っています。）

8.4 𝕄 の上の段：閉包の補題と数字の定義を並べる

𝕄 に制限した量化子（[ ∀ m ∈ 𝕄 . … ]・[ m ; n col ∈ 𝕄 ]）を使う段では、式に出てくる m + n・m ⋅ n・N + 1 が 𝕄 に入ることを、証明器は前提からしか知りません。そこで前提に、閉包の補題（+∈𝕄・⋅∈𝕄）と 𝕄0s（0 ∈ 𝕄 と suc で閉じること）を並べ、数字を使うなら定義 1.・2. も並べます。例：articles3/0-pa.book の LA1。

　これらを1つ外しただけで timeout することがあります（外部の AI の試験では、0-pa の上で m ⋅ 1 = m（0-pa の隠し補題 L⋅1 と同じ式）を示す段から L0+ を外すと timeout しました）。段が落ちたら、まずこの並びが揃っているかを見ます。

8.5 等号を開かない：W.!=.

articles1/0.book は =. を X = Y ⟺ X =_ Y（外延の形）と定義しています。そのため / W. は等号もすべて ∀ w (w ∈ X ⟺ w ∈ Y) の形に開きます。Book 内定数の定義 |g =_ |g_ のように、証明で等号として置き換えに使いたい式まで開くと、証明器は置き換えに使えなくなります。
等号を残したいときは、=. を除いた W.!=.（所属の形で開くなら W.'!=.）を使います（4.book の W.!〇.）。例：58.book の Lgi -| hyg ///// W.'!=. , …。

8.6 goal と sos で形を揃える

slash で開くと、同じものが goal と sos で違う形になることがあります（goal は A ∈ ℘ X のまま、sos は A ⊂ X まで開いた、など）。2つを結ぶ定義が sos に無いと、証明器は証明できません。slash_cli で両方の開いた形を見て、残った方の定義（℘.'・⊂. など）を sos に足すか、両方を同じ深さまで開きます。

8.7 演算の強さは word ごと

演算の結合の強さは word ごとに DB で決まっています。数の演算は普通の数学と同じで、後置の suc が最も強く、↑（累乗・右結合）、⋅、+ の順です。例：2 ⋅ n ↑ 2 は 2 ⋅ (n ↑ 2)、m ⋅ n + j は (m ⋅ n) + j。ほかの語との組み合わせで迷ったら括弧を書くか、slash_cli.php の前置記法（[⋅ 2 [↑ n 2]]）で確かめます。

9 本を分ける：import と private theorem

何冊かで同じ準備を使うときは、準備を別の本にして import します。例：articles2/0-sn.book（集合と自然数）を 52a.book と 58.book が import し、どちらも主定理の周りだけの小さな本になりました。import した本は証明し直さず、保存された査読結果を使います。

9.1 import で運ぶもの・運ばないもの

運ぶ：紹介（word・prop・abbr・lower）と、証明済みの Thm（thm prop/thm let/thm、! 付きも）。goal は名前でも `式` でもかまいません。`式` の Thm は、使う側の sos に `式` と書いて引きます（52a.book の `0 ∈ 𝕄`・`2 ∈ 𝕄` は 0-sn.book の Thm）。let/thm の名前も引けます。import した本がさらに import した本の Thm も届きます。
運ばない：thm- 系（private theorem）の Thm と名前、sos に `式` を含む Thm（その本だけの定数に頼るかもしれない）、ヘッダの formel・thmel。
sos に let で置いた名前を含む Thm は、後の Thm からも使えません（同じ名前を後で置き直せるため）。

9.2 private theorem

thm- prop/thm- let/thm-（! 付きも）は、その本の中（後の Thm・後の頁）では使えて、import した本には運ばない Thm です。Lean の private theorem と同じ考え方です。! は表示するか、- は運ぶか、で別のことなので、!thm- と組み合わせられます。
使いどころ：準備の本の中だけで使う作業用の補題です。運ばなければ、import した本は同じ名前（L01・LD など）を自由に使えます。逆に、使う側の本で使いたい Thm には - を付けません。
例（説明のための形・実際の 0-sn.book では L01 は ∪=#+ の prf の中のラベル）：

　この本の中では ∪=#+ の prf が L01 を引けます。この本を import した本からは ∪=#+ は使えますが、L01 を sos に書くと FAIL: unintroduced sos name: L01 で落ちます。