HOL Light チュートリアル
HOL Light Tutorial (hol-light.github.io)
要約
HOL Lightは、初心者が習得するのが難しい定理証明システムです。このチュートリアルは、複雑な背景知識を吸収する前に、段階的な例を通じてシステムの基本的な使い方を迅速に習得するための、代替的な「クイックスタート」ガイドを提供します。
全文翻訳
HOL Lightチュートリアル
2026年9月26日
要旨
HOL Light定理証明器は、使い始めるのが難しい場合があります。マニュアルは非常に詳細で包括的ですが、ユーザーが何か面白いことをする前に吸収しなければならない背景情報の量が intimidating です。ここでは、段階的な例を通じてシステムの基本的な使い方を迅速に教えることを目的とした、代替の「クイックスタート」ガイドを提供します。読者によっては、こちらの方が理解しやすいかもしれません。そうでない場合は、結局標準マニュアルを参照してください。
目次
1 インストール
1.1 Windowsユーザー向け: WSLとCygwin
1.2 OCaml
1.3 HOL Light
1.3.1 パッケージマネージャーからHOL Lightをインストールする
1.3.2 ソースコードからHOL Lightをインストールする
1.4 エディタ
1.5 HOLの他のバージョン
2 OCamlトップレベルの基本
2.1 HOL Lightの証明をコンパイルする
3 HOLの基本
3.1 項
3.2 型
3.3 定理
3.4 派生規則
4 命題論理
4.1 トートロジーの証明
4.2 低レベル論理規則
4.3 論理設計と検証
5 方程式と関数
5.1 カリー化関数
5.2 ペアリング
5.3 等式推論
5.4 定義
6 抽象化と量化子
6.1 量化子
6.2 一階論理推論
7 変換と書き換え
7.1 変換子
7.2 深さ変換
7.3 マッチング
7.4 書き換え
7.5 定理の検索
8 タクティクスとタクティカル
8.1 ゴールスタック
8.2 和に関する帰納的証明
9 HOLの数体系
9.1 算術的決定手続き
9.2 非線形推論
9.3 量化子消去
10 帰納的定義
10.1 バグパズル
10.2 並行プログラムの検証
11 健全帰納法
11.1 √2の無理数性
11.2 健全性
12 証明スタイルの変更
12.1 より読みやすい証明に向けて
12.2 例
12.3 適切なスタイルか？
13 再帰的定義
13.1 二項係数
13.2 二項定理
14 集合と関数
14.1 選択公理とselect演算子
14.2 関数計算
14.3 いくつかの基数算術
15 帰納的データ型
15.1 列挙型
15.2 再帰型
15.3 ファノ平面
15.4 レコード型
16 プログラミング言語の意味論
16.1 言語の意味論
16.2 決定性
16.3 弱先行条件
16.4 公理的意味論
17 浅い埋め込み
17.1 状態と式
17.2 コマンド
17.3 ホーア規則
17.4 検証条件
17.5 洗練
18 数論
18.1 合同式
18.2 フェルマーの小定理
18.3 RSA暗号
19 実解析
19.1 チェビシェフ多項式
19.2 サルコフスキーの定理の自明な部分
19.3 微分
20 論理の埋め込み
20.1 様相論理
20.2 深い埋め込み
20.3 様相スキーマ
20.4 浅い埋め込み
21 関数型プログラミング言語としてのHOL
21.1 if-then-else式の正規化
21.2 性質の証明
21.3 定理証明器
21.4 実行
22 ベクトル
22.1 3次元ベクトル
22.2 外積
23 カスタムタクティクス
23.1 コッヘン・スペッカーのパラドックス
23.2 HOLでの形式化
24 新しい型の定義
24.1 ゼロでない3次元ベクトル
24.2 射影平面の再訪
24.3 商型
25 カスタム推論規則
25.1 LPOを用いた順序付き書き換え
25.2 クリティカルペア
25.3 完了の例
26 外部ツールとの連携
26.1 Maxima
26.2 HOLとMaximaのインターフェース
26.3 因数分解
26.4 原始関数と積分
A HOL Lightの進化
A.1 LCF
A.2 HOL
A.3 開発と応用
A.4 hol90, ProofPower, および HOL Light
1 インストール
HOL Lightは、ほとんどの最新コンピュータで比較的簡単に動作させることができます。最初のバージョン（Harrison 1996a）以降、ビルドプロセスは大幅に簡略化されました。以下では、LinuxのようなUnixライクな環境を想定することがあります。読者がLinuxマシンにアクセスでき、それに慣れている場合は、その使用を推奨します。しかし、Windowsユーザーも絶望する必要はありません。なぜなら、必要なすべてのUnixツール、さらに多くの便利なツールがCygwinの一部として無料で利用可能だからです。Windows 10以降では、Windows Subsystem for Linux（WSL）をインストールし、好みのLinuxディストリビューションを選択することもできます。Windowsユーザー以外、または「ネイティブ」で作業することを決意したWindowsユーザーは、次のサブセクションをスキップできます。
1.1 Windowsユーザー向け: WSLとCygwin
Windows 10以降を使用している場合は、Microsoft Windowsの公式機能であるWindows Subsystem for Linuxをインストールできます。そのインストール手順はhttps://learn.microsoft.com/en-us/windows/wsl/installで入手できます。インストール後、Microsoft StoreからWSLに追加するLinuxディストリビューションを選択できます。
WSLがWindowsでサポートされていない場合は、Cygwinを試すことができます。Cygwinは、通常のWindowsの使用を妨げることなく、Windows内で実行できるLinuxライクな環境です。とりわけ、通常のUnix/Linuxソフトウェアツールが利用可能な従来のシェルを提供します。Cygwinはhttp://www.cygwin.com/から無料でダウンロードできます。特にすべてのパッケージインストールオプションを選択した場合、システムは大きくなるため、ダウンロードとインストールには時間がかかることがあります。しかし、通常は簡単で問題なく進むようです。
Cygwinをインストールしたら、単に「Bashシェル」を起動します。私のWindowsマシンでは、例えば、スタート → すべてのプログラム → Cygwin → Cygwin bash shell のメニューシーケンスをたどります。このアプリケーションは「シェル」（Unixの専門用語で、Windowsのコマンドプロンプトに似たもの）であり、そこから以下のコマンドをLinux内のように呼び出すことができます。以降、「Linux」という言葉は、Linux、その他のUnixバージョン、またはWindows内のCygwinを意味するものとします。
1.2 OCaml
HOL Lightは、関数型プログラミング言語であるObjective CAML（「OCaml」）の上に構築されています。より正確には、HOL LightはOCamlで書かれており、OCamlのread-eval-printループがHOL Lightと対話する通常の手段です。したがって、OCamlのインストールはHOL Lightを使用するための前提条件です。さらに、OCamlは、幅広い他のアプリケーションに推奨される点が多い、強力でモダンなプログラミング言語です。
http://caml.inria.fr/ocaml/english.en.htmlのWebサイトの手順に従うことで、OCamlは幅広いアーキテクチャにインストールできます。私は通常、Cygwin上でもシステムをソースから再構築します（数回の短いコマンドで済みます）が、多くのプラットフォームで事前コンパイル済みのバイナリが利用可能です。
1.3 HOL Light
ついにHOL Light自体をインストールする準備ができました。HOL Lightは、パッケージマネージャーを使用するか、ソースコードからビルドすることによってインストールできます。パッケージマネージャーを使用してHOL Lightをインストールする方が簡単ですが、少し古いバージョンになる可能性があります。ソースコードからビルドするのはより困難ですが、最新の機能を取得できることが保証されます。
1.3.1 パッケージマネージャーからHOL Lightをインストールする
HOL LightはOCamlパッケージマネージャーであるOPAMで利用可能です。お使いのコンピュータにOPAMがインストールされている場合（https://opam.ocaml.org/doc/Install.htmlで手順を確認できます）、次のコマンドを実行してHOL Lightをインストールできます。
opam install hol_light
DebianベースのLinuxディストリビューションを使用している場合は、HOL Lightと便利な補助ツールをまとめてhol-lightパッケージをインストールすることで入手できます。
sudo apt-get install hol-light
ただし、Ubuntuを使用している場合、apt-getから取得したHOL Lightシステムは、このチュートリアルには古すぎます。この場合、OPAMを使用してHOL Lightをインストールすることを検討してください。
1.3.2 ソースコードからHOL Lightをインストールする
HOL LightのGithubリポジトリhttps://github.com/jrh13/hol-light/をクローンすることでシステムをダウンロードできます。Githubリポジトリのクローンは、シェルの現在のディレクトリで次のコマンドを実行することで行えます。
git clone https://github.com/jrh13/hol-light.git
または、gitが利用できない場合は、アーカイブファイルhttps://github.com/jrh13/hol-light/archive/refs/heads/master.zipをダウンロードできます。Webブラウザはこれをhol-light-master.zipにダウンロードします。unzipコマンドを使用してhol-lightに展開します。
unzip hol-light-master.zip -d hol-light
シェルプロンプト（Linux）またはコマンドプロンプトで、次のコマンドを実行して適切なディレクトリに移動します。
cd hol-light
最初のステップは、HOL Lightシステムが使用するOCamlライブラリをインストールすることです。各ライブラリは、パッケージマネージャーを使用するか、ソースコードから手動でビルドしてインストールできます。ソースコードからOCamlライブラリをビルドするための手順は、このチュートリアルでは説明しません。なぜなら、ライブラリ自体に優れた指示がある可能性が高いからです。パッケージマネージャーについては、オペレーティングシステムでネイティブにサポートされているパッケージマネージャー（macOSの場合はhomebrew、Ubuntuの場合はapt）または、複数のオペレーティングシステムで同一のユーザーインターフェースをサポートする公式のOCamlパッケージマネージャーであるOPAMを選択できます。
どのパッケージマネージャーを使用すべきでしょうか？長所と短所があります。OPAMの場合、事前に追加の手順でインストールする必要があります。しかし、セットアップ後、HOL Lightが提供するMakefileコマンドを使用して必要なパッケージを迅速にインストールできます。ネイティブパッケージマネージャーの場合、HOL Lightはまだそのような利便性を提供していません。しかし、パッケージマネージャーに対応するパッケージ名を見つけることで、ライブラリをインストールできます。OCamlパッケージのリストは(_opam)ファイルに記載されています。HOL Lightは、どちらのパッケージマネージャーを選択しても機能するはずです。
お使いのコンピュータにOPAMが利用可能な場合は、OCamlバージョンの好みに応じて、次のいずれかのコマンドを実行してください。
make switch # OCaml 4のローカルセットアップを作成します
make switch-5 # OCaml 5のローカルセットアップを作成します
これにより、hol-lightディレクトリ内にローカルなOPAM環境が作成され、その中にパッケージがインストールされます。次に、ターミナルで次のようにローカル環境セットアップをアクティブ化します。
eval $(opam env)
次のステップは、HOL LightがOCaml内での解析と印刷を処理するために使用する特別なファイルを作成することです。Linuxでは次のように実行するだけです。
make
次に、次のようにしてインタラクティブなOCamlセッションを開始します。
./hol.sh
HOL Lightがロードされると大量の出力が表示され、特に多くの定理とその名前付けが行われます。コンピュータの速度にもよりますが、約2分後、最後の数行の出力とOCamlプロンプトが表示されるはずです。
0..0..0..solved at 3
* HOL-Light syntax in effect *
Camlp5 parsing version (HOL-Light) 8.03.01
#
これでシステムの使用を開始する準備が整いました。
1.4 エディタ
お好みのエディタを使用できますが、HOL Lightが初めての場合は、Visual Studio CodeのHOL Lightプラグインが良い選択肢となるでしょう。Visual Studio Codeの拡張機能タブでHOL Lightを検索することで、プラグインを見つけてインストールできます。このプラグインは以下の機能を提供しており、その一部はHOL Serverがオンになっている場合に有効になります。
- シンタックスハイライト。
- 次のタクティック/OCamlステートメントをターミナルに送信。
- 最後に成功したタクティック/ステートメントをハイライトし、証明ステップを元に戻す。
- バインディングまたは定数の定義を表示。
- キーワードのHOL Lightドキュメントをツールチップとして表示。
1.5 HOLの他のバージョン
良くも悪くも、HOL4、HOL Light、Isabelle/HOL、ProofPowerなど、いくつかのHOLライクな定理証明器が活発に使用されています（Web検索でいずれかのWebページを簡単に見つけることができます）。これらのシステムの基盤となる論理的基礎、および多くの他のアイデアは、1980年代にMike Gordonによって書かれたオリジナルのHOLシステムに由来しており、その最初の洗練され安定したリリースがHOL88（Gordon and Melham 1993）でした。以下のグラフは、アイデアやコードの流れの概略を示そうとしています。
［画像: PICT］
ここで議論されていることの多くは、他のHOLバージョン、そして一般的に他の定理証明システムにも同様に適用可能です。付録では、HOLの進化とその定理証明器の世界における位置づけについて、より詳細に説明します。
2 OCamlトップレベルの基本
HOL Lightがロードされた後、あなたは通常のOCamlのread-eval-printループに戻ります。唯一の違いは、多数の定理と定理証明のためのツールがロードされていることです。1 実装言語を対話環境として使用することで、完全にオープンで、クリーンかつ均一な方法で拡張可能なシステムが得られます。それにもかかわらず、最初はやや異質に感じるかもしれません。他の多くの同等の定理証明器やコンピュータ代数システムは、Mizar（Rudnicki 1992）のような個別のインターフェースを提供しており、プログラム可能な環境がありません。または、Mapleのように独自のカスタム言語をread-eval-printループに使用しています。2
HOL-Lightに固有のことに移る前に、OCamlのトップレベルループの使用方法を基本的な用語で理解しておく価値があります。大まかに言うと、OCamlのトップレベルループでは3つのことができます。ディレクティブの発行、式の評価、定義の作成です。初心者がしばらくの間必要とする可能性のある唯一のディレクティブは次のとおりです。
#use "filename";;
これは、filenameという名前のファイルからOCamlソースを、トップレベルにタイプされたかのようにロードします。これは、HOLをロードするために行ったこととまったく同じです。さらに、2 + 2;;の例は、式の評価の例でした。出力をもっと詳しく見てみましょう。
val it : int = 4
OCamlは式の結果（4）で応答しますが、それに型int（整数、つまり全数であることを意味します）を割り当て、結果の省略名itを導入します。これで、評価結果、つまり4の省略名としてitを使用できます。例えば：
# it * it;;
val it : int = 16
これでitはその式の結果、つまり16を表します。ただし、これはOCamlが最後の式の結果に与えるデフォルトの名前です。ユーザーは、次の形式の定義を使用して、任意の名前を付けることができます。
let <name> = <expression>;;
その後、その名前を後続の式で使用し、複合式を他の名前にバインドできます。例えば：
# let a = 741;;
val a : int = 741
# let b = 147;;
val b : int = 147
# let c = a - b;;
val c : int = 594
# let d = 495 + c;;
val d : int = 1089
整数（全数）だけでなく、CAMLでは他の型の式も評価できます。例えば、文字列（文字の有限シーケンス）は二重引用符で囲んで入力でき、+が数値を加算するのと同じように、文字列を連結する（結合する）^のような関数を使用して操作できます。
# let x = "no";;
val x : string = "no"
# let y = "body";;
val y : string = "body"
# let z = x^y;;
val z : string = "nobody"
読者は他の例もいくつか試してみることをお勧めします。インタラクティブなループにいることの利点の一つは、実験して結果をすぐに確認できることです。
基本的な値だけでなく、OCamlでは関数に名前を付けることもできます。関数は1つ以上のパラメータ、または引数を取り、対応する結果を計算します。このような関数を定義するには、定義を作成するときに関数名の後に引数を追加するだけです。例えば、次のものは引数を2乗する関数の定義です。
# let square x = x * x;;
val square : int -> int = <fun>
型int -> intは、squareが整数から整数への関数であることを意味します。関数は、関数名の後に引数を記述して、特定の引数に適用できます。
# square 0;;
val it : int = 0
# square 8;;
val it : int = 64
通常の数学表記では関数引数を括弧で囲むことが必須ですが（非公式な数学ではfxではなくf(x)と書きます）、OCamlではオプションであり、ほとんどの人は使用しません。しかし、他の状況と同様に、優先順位を確立するために常に括弧を使用することもできますし、単に慣れのために使用することもできます。
# square(2 + 2);;
val it : int = 16
# square(2) + 2;;
val it : int = 6
関数は、次々と書かれた複数の引数を持つことができます。OCamlが印刷する型については後で詳しく説明しますが、今のところは、2つの整数を取り、別の整数を返す関数だと考えてください。
# let pythag x y = square x + square y;;
val pythag : int -> int -> int = <fun>
# pythag 3 4;;
val it : int = 25
2.1 HOL Lightの証明をコンパイルする
OCamlコンパイラを使用してHOL Lightの証明をコンパイルし、作成されたバイナリを実行することもできます。コンパイルされた証明を実行することには、複数の利点があります。第一に、特にネイティブコンパイラバージョン（ocamlopt）を使用する場合、コンパイルされたバイナリはREPLを使用するよりも高速に実行できます。第二に、ソースコードのビルドは、証明を実行する前に、証明内の構文エラーを迅速に報告します。第三に、コンパイルされたモジュールは、他のOCamlプログラムによってインポートおよび使用できます。
詳細については、HOL LightのREADMEファイルの「Compiling HOL Light」セクションを参照してください。
3 HOLの基本
前のセクションでは、数値や文字列を含む式を評価しました。HOL — 以下では単に「HOL」 — は、項（数学的表現または論理的断言を表す）と定理（証明された断言を表す）を含む式の評価のためのツールのスイートです。
3.1 項
システムに項を入力するには、バッククォートで囲んで入力できます。
# `x + 1`;;
val it : term = `x + 1`
表面上は、これは文字列との類似した対話のように見えるかもしれません。
# "x + 1";;
val it : string = "x + 1"
項は文字列のように、純粋に記号的な式として操作されます。しかし、項は単なる文字のシーケンスとして表現されるのではなく、よりリッチなツリー構造の表現、つまり「抽象構文木」のようなものを使用して表現されます。OCamlのトップレベルは、バッククォート内のものを自動的に内部表現に解析しようとし、同様の方法でそれを表示しますが、これは人間の便宜のためだけです。例えば、入力のいくつかの表面的なバリエーションは、同じ内部表現にマッピングされ、同じように表示されますが、いくつかの不正な形式の式はまったく解析されません。
# `(x) + 1`;;
val it : term = `x + 1`
# `(x + (1))`;;
val it : term = `x + 1`
# `x + +`;;
Exception: Failure "term after binary operator expected".
内部形式は通常、人間にはあまり好ましくありません。次のOCamlディレクティブを使用して自動的な prettyprinting を無効にするとわかります。
# #remove_printer pp_print_colored_qterm;;
# `x + 1`;;
val it : term =
Comb (Comb (Const ("+", `:num->num->num`), Var ("x", `:num`)),
Comb (Const ("NUMERAL", `:num->num`),
Comb (Const ("BIT1", `:num->num`), Const ("_0", `:num`))))
内部表現については後で詳しく見ていきます。システムの高度な使用には重要だからです。しかし、今のところはそれを無視し、次のコマンドで通常の動作を復元します。
# #install_printer pp_print_colored_qterm;;
HOLは項を操作するための多くの操作を提供します。例えば、substは、ある項を別の項で置き換えることができます。例えば、「x + 1」という項の「1」を「2」に置き換えます。構文は、数学的な表記法[2/1](x + 1)または(x + 1)[2/1]に似ています。
# subst [`2`,`1`] `x + 1`;;
val it : term = `x + 2`
# subst [`y + 2`,`x:num`] `x + 5 * x`;;
val it : term = `(y + 2) + 5 * (y + 2)`
「x:num」と入力する理由、「x」だけではない理由は、HOLの型システムにあり、次に説明します。
3.2 型
HOLの重要な特徴は、すべての項が明確に定義された型を持つことです。大まかに言うと、型は項がどのような種類の数学的対象を表すかを示します（数値、集合、関数など）。項の可能な型は、別のシンボリックデータ型hol_typeを使用して表され、これらも同様にバッククォート内でコロンを先頭に付けて自動的に解析および表示されます。3
# `:num`;;
val it : hol_type = `:num`
type_of演算子を項に適用することで、項の型を見つけることができます。
# type_of `1`;;
val it : hol_type = `:num`
# type_of `x + 1`;;
val it : hol_type = `:num`
# type_of `x + 1 < x + 2`;;
val it : hol_type = `:bool`
項「1」と「x + 1」の型は:numであり、これらは自然数、つまり非負の整数を表すことを意味します。（より一般的な数学用語では、HOLの型割り当ての情報を捉えるために、1 ∈ℕおよびx + 1 ∈ℕと書くでしょう。）一方、項「x + 1 < x + 2」は型bool（ブール値）であり、これは真または偽になりうる断言であることを意味します（この場合は真です）。HOLが項に型を割り当てることができるが、一意に決定されない場合、一般的な型が自動的に割り当てられます。
# `x`;;
Warning: inventing type variables
val it : term = `(x:?142527)`
# type_of it;;
val it : hol_type = `:?142527`
しかし、項の後に:<type>と記述することで、選択した型を任意の項に強制することができます。
# `x:num`;;
val it : term = `x`
# `x:bool`;;
val it : term = `x`
（このように、同じ名前を持ちながら異なる型を持つ変数は、完全に異なると見なされます。）加算演算子の両方のオペランドが同じ型でなければならないため、複合項「x + 1」では型「num」が定数1に自動的に割り当てられ、xにも同じ型が推論されるため、注釈は必要ありませんでした。しかし、必要または単に強調のために、複合項のサブ項に型注釈を付けることができます。
# `(x:num) = y`;;
val it : term = `x = y`
# `(x:num) + 1`;;
val it : term = `x + 1`
型付けのため、構文的には正しくても型付けできない項があります。例えば、ここではブール型のものと数値型のものを加算しようとしています。
# `(x < y) + 2`;;
Exception:
Failure
"typechecking error (initial type assignment):
2 cannot have type num and bool simultaneously".
型の値は、これらの「無意味な」項を最初からフィルタリングし、「nは数値を表す」といった直感的な制約を特別なユーザーガイダンスなしに追跡できることです。否定的な側面としては、時には柔軟性に欠けることがあります。例えば、自然数と実数を直接加算することはできません。HOLはこれらを異なる型として扱うため、直感的にはℕ ⊆ℝを想像するかもしれませんが、そうはなりません。
# `(x:num) + (y:real)`;;
Exception:
Failure
"typechecking error (initial type assignment):
y cannot have type num and real simultaneously".
3.3 定理
型boolの項、しばしば公式と呼ぶもの、は真または偽である可能性があります。例えば、直感的には最初の項は（xの値に関係なく）真であり、2番目の項は偽です。
# `x + 1 < x + 2`;;
val it : term = `x + 1 < x + 2`
# `2 + 2 = 5`;;
val it : term = `2 + 2 = 5`
HOLは「真理」または「偽り」の概念を直接使用しません。しかし、公式が受け入れられている証明方法を使用して証明されたという概念は持っています。そして、これらの方法は、証明可能なものはすべて真であるように選ばれていることは言うまでもありません。4 HOLを使用する通常の目的は、断言を形式論理で正確に述べ、それを証明することです。
伝統的な形式論理では、公式はいくつかの初期公理に対して定義された構文規則のセットを適用することによって証明されます。pが証明可能であることを意味するために⊢ pと書き、より一般的にはp1,…,pnが仮説p1,…,pnから証明可能であることを意味するためにp1,…,pn ⊢ pと書きます。HOLでは、同様の概念がより計算的な形式で導入されています。特別な型thm（「定理」）は、証明された — 実際に証明された、単に証明できるだけでなく — 公式に使用されます。最初に、OCamlオブジェクトで型thmを持つのはHOLの公理のみであり、新しいthmオブジェクトを作成する唯一の方法は、限られた数の原始推論規則を適用することです。（公理と原始規則の完全なリストは非常に短い。）私たちがHOLで「推論規則」と呼ぶものは、定理の型（またはその複合型、例えばペアまたは定理のリスト）を返すOCaml関数に他なりません。
例えば、おそらくHOL論理の最も単純な推論規則は等式の反射性です。HOLでは、この規則は関数REFLによって実装されており、項tを受け取り、定理⊢ t = tを返します。（出力からわかるように、定理は通常の「ターンスタイル」表記のASCII近似を使用して prettyprint されます。）
# REFL `x:real`;;
val it : thm = |- x = x
# let th1 = REFL `x + 1`;;
val th1 : thm = |- x + 1 = x + 1
同様に単純な別の規則はASSUMEで、これは自身を仮定して何でも推論することを可能にします。公式pを与えると、定理p ⊢ pを返します。ブール型でない項を与えると、対応する「定理」が無意味であるため失敗します。
# ASSUME `2 + 2 = 5`;;
val it : thm = 2 + 2 = 5 |- 2 + 2 = 5
# let th2 = ASSUME `2 * n = n + n`;;
val th2 : thm = 2 * n = n + n |- 2 * n = n + n
# ASSUME `1`;;
Exception: Failure "ASSUME: not a proposition".
少し複雑な原始推論規則はINST（インスタンス化）です。これは、定理内の変数を特定の項に設定します。実際、これは項に対するsubstが行っていたことを定理レベルで実行しています。これは論理的に有効なステップです。なぜなら、自由変数を持つHOL定理は、それらが持つ可能性のあるすべての値に対して成り立つからです。
# let th3 = INST [`2`,`x:num`] th1;;
val th3 : thm = |- 2 + 1 = 2 + 1
これは、仮説内の変数も同様にインスタンス化することに注意してください。これは一般的に論理的に健全であるために必要です。
# INST [`2`,`n:num`] th2;;
val it : thm = 2 * 2 = 2 + 2 |- 2 * 2 = 2 + 2
さらに、INSTはsubstとは異なり、非変数を置換することを拒否します。これは一般的に論理的に有効なステップではありません。例えば、2 ⋅ n
n + n が成り立つという事実から、nを2 ⋅ nに置換しても論理的に有効であるとは限りません。
# INST [`2`,`2 * n`] th2;;
Exception: Failure "vsubst: Bad substitution list".
定理は証明によってのみ構築できますが、常にそれを結論と仮説に分解することは自由です。例えば、concl関数は定理の結論を項として返します（常にブール型になります）。
# concl;;
val it : thm -> term = <fun>
# concl th1;;
val it : term = `x + 1 = x + 1`
通常の形式では、HOLはすべての定理を証明によって生成しますが、証明は具体的なオブジェクトとして構築されません。しかし、Proofrecordingサブディレクトリには、Steven Obuaによるシステムがあり、証明が明示的に構築され、XMLベースの形式でファイルにダンプできるため、他のシステム（例えば、個別の証明チェッカー）への入力に適しています。
3.4 派生規則
この低レベルで非自明な定理を証明するのは非常に苦痛です。しかし、HOL Lightには、非自明な定理のいくつかのクラスを自動的に証明できる、より強力な推論規則が多数付属しています。これらの多くは後続で説明しますが、一例として、ARITH_RULEは、自然数に対する単純な代数的操作または不等式推論を必要とする多くの公式を証明できます。例えば、次の愛らしい公式（「x EXP n」はxnを表します）です。
# ARITH_RULE
`(a * x + b * y + a * y) EXP 3 + (b * x) EXP 3 +
(a * x + b * y + b * x) EXP 3 + (a * y) EXP 3 =
(a * x + a * y + b * x) EXP 3 + (b * y) EXP 3 +
(a * y + b * y + b * x) EXP 3 + (a * x) EXP 3`;;
val it : thm =
|- (a * x + b * y + a * y) EXP 3 +
(b * x) EXP 3 +
(a * x + b * y + b * x) EXP 3 +
(a * y) EXP 3 =
(a * x + a * y + b * x) EXP 3 +
(b * y) EXP 3 +
(a * y + b * y + b * x) EXP 3 +
(a * x) EXP 3
しかし、重要な点は、これらが表面下では依然としてREFLとINSTレベルの低レベル規則によって証明されているということです。このため、これらの複雑な派生規則でさえ非常に信頼性が高いと言えます。これらは単にthm型の何かを「作成」するのではなく、それを証明しなければなりません。もちろん、それは完全に自明ではありませんが、ユーザーの視点からはアトミックな操作のように見えるように、すべてARITH_RULEにカプセル化されています。そして、システムの高度な使用では、特別な状況のためにカスタム派生規則を書くことができることは非常に価値があります。
通常、HOLでの証明は次のように進行します。ユーザーは問題に対する特別な洞察を用いて、それを比較的単純なサブ問題のシリーズに分解します。サブ問題が十分に単純になるか、または十分に限定されたドメインに収まると、それらはHOLによって自動的に処理できます。一般的に、HOLがギャップを埋めることができるようになる前に必要な詳細レベルは、ほとんどの人が慣れているよりも高くなります。一方で、比較的長い手作業の証明を単一の自動HOLステップに置き換えることができる、心地よい例外もあります。
4 命題論理
指数がEXPと呼ばれるなど、マイナーな構文上の詳細を除けば、HOLのパーサーが自然数上の算術をサポートする表記法は、かなり馴染みのあるものに見えるはずです。名前付き変数、数値定数、および通常の優先順位規則を持つさまざまなインフィックス演算子を使用できます。式は、強調のため、または優先順位規則をオーバーライドするために括弧で囲むことができます。
次に、よりリッチな論理構造を持つ公式を操作するために、基本的な公式から「論理結合子」を使用して複合論理式を構築するためにHOLが使用する類似の表記法を習得することが重要です。読者は、おそらく「plus」という単語の代わりに「+」のような記号を使用することに慣れているでしょう。同様に、数学的な結果を述べるときに、「and」、「or」、「not」のような特別な論理単語の代わりに記号を使用することに慣れる必要があります。ここでは、いわゆる命題（またはブール）結合子の従来の表記法、およびHOLのASCII近似とそれらの近似的な英語の読み方を示す表を示します。
| ⊥ | F または false | 偽 |
| ⊤ | T または true | 真 |
| ¬ | ~ | Not |
| ∧ | `/ | |
| ` | And | |
| ∨ | ` | |
| /` | Or | |
| ⇒ | ==> | Implies（「if … then …」） |
| ⇔ | <=> | Iff（「… if and only if …」） |
通常の代数表記との類似性を強調する価値があります。真と偽は、0や42のような特定の数値に類似した、論理定数であり、論理的な命題を表します。上記の2つのASCIIスペルはそれぞれ、HOLが入力で相互に受け入れます。短いTとFは、このチュートリアル全体でタイプするものです。しかし、例で見るように、HOLが出力する項は、長いtrueとfalseです。7 論理否定は、数値の算術否定と同様に、単項演算です。他の結合子はすべて、加算、乗算などと同様の二項演算です。算術演算子とは異なり、可能な引数は有限個（すべて真または偽のいずれか）であるため、各引数の組み合わせに対応する結果を示す真理値表を使用して、結合子の意味を明示的に表示できます。否定演算子は、次の非常に単純な真理値表を持ちます。
| p | ¬ p |
| false | true |
| true | false |
二項結合子の場合、2^2 = 4つの可能な真値の組み合わせに対して、4行が必要です。スペースを節約するために、すべての結合子を同じ表の異なる列に配置します。
| p | q | p ∧ q | p ∨ q | p ⇒ q | p ⇔ q |
| false | false | false | false | true | true |
| false | true | false | true | true | false |
| true | false | false | true | false | false |
| true | true | true | true | true | true |
「or」は包括的な意味で解釈されることに注意してください。「p ∨ q」は「pまたはq、または両方」を意味します。含意の定義は、ほとんどの人にとって最初は直感に反するように思えますが、しばらくすると自然に思えるようになるでしょう。
基本的な「原子」公式で、より複雑な公式を構築するために使用できるものは、ブール型の変数です。
# `p
/ ~p`;;
val it : term = `p
/ ~p`
# ASSUME `p /
q`;;
val it : thm = p /
q |- p /
q
または、次の例のように、他の非ブールコンポーネントを含む場合があります。2番目の例では、自然数上の通常の順序の基本的なプロパティを推論するためにARITH_RULEを使用しています。つまり、任意のx、y ∈ℕに対して、x < yまたはy ≤ xのいずれかが成り立ちます。
# `x < 1 ==> p`;;
val it : term = `x < 1 ==> p`
# ARITH_RULE `x < y
/ y <= x`;;
val it : thm = |- x < y
/ y <= x
複合式では、さまざまな二項結合子の優先順位は上記の表の順であり、「and」が最も強く、「iff」が最も弱い順です。例えば、a ∧ b ⇒ c ∨ d ∧ e は (a ∧ b) ⇒ (c ∨ (d ∧ e)) を意味します。それらはすべて右結合性であるため、例えばp ∧ q ∧ rはp ∧ (q ∧ r)を意味します。HOLのすべてのインフィックス演算子のリストとその優先順位および結合性を取得するには、「infixes()」と入力します。または、特定のシンボルの状態を「get_infix_status "<symbol">」で取得できます。例えば。
# get_infix_status "==>";;
val it : int * string = (4, "right")
# get_infix_status "-";;
val it : int * string = (18, "left")
また、parse_as_infixを使用して、自分で選択した他のシンボルをインフィックスにしたり、既存のインフィックスの優先順位を変更したりすることもできます。
# parse_as_infix("<>",(12,"right"));;
val it : unit = ()
# parse_as_infix("+",(1,"left"));;
val it : unit = ()
ただし、既存のインフィックスの優先順位を変更すること（2番目の例のように）は推奨されません。なぜなら、既存の優先順位は他のソースファイルでしばしば想定されているからです。例えば、x < x + 1は(x < x) + 1として解析され、型チェックに失敗します。
# `x < x + 1`;;
Exception:
Failure
"typechecking error (initial type assignment):
1 cannot have type num and bool simultaneously".
したがって、通常のサービスを次のように復元しましょう。
# parse_as_infix("+",(16,"right"));;
val it : unit = ()
注：HOLは、数学の表記法がしばしば行うように、「連鎖」した二項演算子x < y < zを「x < y かつ y < z」を意味するように特別に解釈しません。その試みは型チェックで失敗しますが、p ==> q ==> rは受け入れられますが、p ⇒ (q ⇒ r)に論理的に等しく、(p ⇒ q) ∧ (q ⇒ r)ではありません。
4.1 トートロジーの証明
読者が命題論理結合子に慣れていない場合は、それらを使用して論理式を記述することに慣れるために時間を費やす価値があります。特に、どのブール変数から構築された公式がトートロジーであるか、つまり変数の真偽値の任意の値に対して真であるかを確認することは有益です。HOLの演繹システムは、証明可能なものはすべてトートロジーであり、それらを自動的に証明する単純な派生規則TAUTさえ存在します。例えば、次のトートロジーはいわゆる「排中律」であり、任意の公式pに対して、「p」または「not p」のいずれかが成り立つことを示しています。
# TAUT `p
/ ~p`;;
val it : thm = |- p
/ ~p
次のものは、「p if and only if q」が「if p then q」と「if q then p」の組み合わせと同等であることを示しています。
# TAUT `(p <=> q) <=> (p ==> q) /
(q ==> p)`;;
val it : thm = |- (p <=> q) <=> (p ==> q) /
(q ==> p)
一方、一般に「ド・モルガンの法則」として知られるものは、「and」と「or」の間の興味深い二重性を示しています。例えば、「私はスウェーデン語を話せないし、フィンランド語も話せない」は「私はスウェーデン語かフィンランド語のどちらも話せない」と同等です。
# TAUT `~(p /
q) <=> ~p
/ ~q`;;
val it : thm = |- ~(p /
q) <=> ~p
/ ~q
# TAUT `~(p
/ q) <=> ~p /
q`;;
val it : thm = |- ~(p
/ q) <=> ~p /
q
一部のトートロジーは、慣れていないと少し驚くかもしれませんが、各命題変数が「真」または「偽」の値を取るすべての可能なケースを網羅的に検討し、各ケースの結果を計算するために真理値表を使用することで、常に自分自身を納得させることができます。例えば、「iff」演算子は「連想的」です。
# TAUT `(p <=> (q <=> r)) <=> ((p <=> q) <=> r)`;;
val it : thm = |- (p <=> q <=> r) <=> (p <=> q) <=> r
ほとんどの人は含意の真理値表定義を不自然だと感じるため、最も奇妙に見えるトートロジーの多くが含意を含むことは驚くことではありません。例えば、次のものは、2つの命題pとqに対して、一方はいずれか一方が他方を含意することを示しています。
# TAUT `(p ==> q)
/ (q ==> p)`;;
val it : thm = |- (p ==> q)
/ (q ==> p)
一方、次のものは伝統的にピアスの法則として知られています。
# TAUT `((p ==> q) ==> p) ==> p`;;
val it : thm = |- ((p ==> q) ==> p) ==> p
ここでは、優先順位規則を混同するユーザー向けの別の例を示します。
# TAUT `(a <=> b
/ c) ==> (a <=> b)
/ c`;;
val it : thm = |- (a <=> b
/ c) ==> (a <=> b)
/ c
ユーザーがトートロジーでないものをTAUTに渡した場合、単に定理を返さずに失敗します。
# TAUT `p
/ q ==> p /
q`;;
Exception: Failure "TAUT `p \/ q ==> p /\ q`: cannot solve".
この場合、明示的な反例（「pが真でqが偽の場合に失敗する」）を与えるようにTAUTを変更することは、それほど難しくありません。そして、TAUTは一般的に複合項を原始ブール式ではなく受け入れることに満足していますが。
# TAUT `x < 1 /
y > 0 ==> x < 1`;;
val it : thm = |- x < 1 /
y > 0 ==> x < 1
それは単に原子式（ここではx < 1とy > 0）を別個かつ原始的なものとして扱い、それらの間のリンクを利用することはできません。
# TAUT `0 < x /
x < 7 ==> 1 <= x /
x <= 6`;;
Exception:
Failure "TAUT `0 < x /\ x < 7 ==> 1 <= x /\ x <= 6`: cannot solve".
その目標は、算術的内容を実際に分析するARITH_RULEによって自動的に解決できます。
# ARITH_RULE `0 < x /
x < 7 ==> 1 <= x /
x <= 6`;;
val it : thm = |- 0 < x /
x < 7 ==> 1 <= x /
x <= 6
しかし、一般的には、このような場合における妥当性を確立するために、任意に複雑な推論が必要になることがあります。例えば、次の項はフェルマーの最終定理のステートメントであり、人類に多大な苦労をかけたことを考えると、HOLに自動的に証明することを期待するのは難しいです。
# ARITH_RULE `x EXP n + y EXP n = z EXP n /
n >= 3
==> x = 0
/ y = 0`;;
Exception:
Failure "ARITH_RULE `... (* string length 546; truncated *)."
4.2 低レベル論理規則
TAUTのような高レベルの自動規則に加えて、HOLは、定理に対する繊細な推論パターンを実行するための、より基本的な操作の完全なセットを提供します。一般的に、各論理結合子には、それを「導入」および「除去」するための対応する規則のセットがあります。例えば、推論規則CONJは、pとqを別々に与えられた場合、p ∧ qを推論することを可能にします。より正確には、それは2つの定理Γ ⊢ pとΔ ⊢ qを受け取り、定理Γ ∪Δ ⊢ p ∧ qを返します。なぜなら、使用された仮説のセットは常に維持する必要があるからです。
# let thp = ASSUME `p:bool`;;
val thp : thm = p |- p
# let thq = ASSUME `q:bool`;;
val thq : thm = q |- q
# let thpq = CONJ thp thq;;
val thpq : thm = p, q |- p /
q
一方、二項の規則CONJUNCT1とCONJUNCT2は、それぞれp ∧ qからpとqを推論することを可能にします。
# CONJUNCT1 thpq;;
val it : thm = p, q |- p
# CONJUNCT2 thpq;;
val it : thm = p, q |- q
別の非常に重要な低レベル規則はMPです。これは、p ⇒ qとpからqへの推移を可能にし、これはしばしば定理をリンクする非常に有用な方法です。この名前は「modus ponens」（ラテン語で「肯定の方法」）という伝統的だが曖昧な名前の省略形です。
# let th1 = ARITH_RULE `x <= y ==> x < y + 1`;;
val th1 : thm = |- x <= y ==> x < y + 1
# let th2 = ASSUME `x <= y`;;
val th2 : thm = x <= y |- x <= y
# MP th1 th2;;
val it : thm = x <= y |- x < y + 1
4.3 論理設計と検証
命題論理に関心がある理由の1つは、それがデジタル回路で使用される構造、例えばHOLを実行しているコンピュータの構造と非常によく対応していることです。合理的な近似として、特定の時間におけるデジタル回路の各ワイヤは、「偽」（0または「ロー」）と「真」（1または「ハイ」）のいずれかの電圧レベルのいずれか1つを持ちます。論理的なビルディングブロックは、命題論理の基本的な結合子を模倣した動作を持つ回路要素です。例えば、(2入力)「ANDゲート」は、2つの入力と1つの出力を持つ回路であり、両方の入力が「真」の場合にのみ出力が「真」になるというもので、命題結合子「∧」に対応します。
ほとんどの最新マイクロプロセッサのゲート自体は、トランジスタと呼ばれるさらに基本的なコンポーネントから構築されています。トランジスタは電圧制御スイッチの一種です。より正確には、3端子デバイスであり、「ソース」と「ドレイン」の2つの端子間の電流の流れは、「ゲート」入力の電圧レベルによって制御されます。n型トランジスタでは、ゲート電圧が高い場合にソースとドレイン間の電流が流れ、ソースとドレインの電圧が等しくなりますが、それ以外の場合はそれらの間に高い抵抗があり、ソースとドレインの電圧は任意に異なることができます。この動作をHOLでモデル化できます。
# `gate ==> (source <=> drain)`;;
val it : term = `gate ==> (source <=> drain)`
同様に、p型トランジスタでは、ゲート電圧が低い場合にのみ電流が流れ、ソースとドレインの電圧が等しくなります。これを次のようにモデル化できます。
# `~gate ==> (source <=> drain)`;;
val it : term = `~gate ==> (source <=> drain)`
CMOS8配置を使用して、トランジスタから論理ゲートが通常どのように構築されるかを見てみましょう。例えば、図1は、論理関数「not or」、つまりoutput ⇔¬ (inputa ∨ inputb)を実現するためのCMOS NORゲートを示しています。ゲートに小さな円が付いている上の2つのトランジスタはp型、下の2つはn型です。上の2つのトランジスタ間の内部ワイヤをinternalと呼びましょう。V ddとV ssとマークされたワイヤは、固定の高電圧および低電圧ワイヤを表します（大まかに言うと、電源の正極と負極）、これはブールモデルの「真」と「偽」に対応します。これで、回路接続によって暗示されるすべての制約が、実際に入力と出力の間に正しい「NOR」関係が得られることを意味すると主張するHOL公式を書き、TAUTを使用して検証できます。
［画像: PIC］
図1: CMOS NORゲート
# TAUT
`(~input_a ==> (internal <=> T)) /
(~input_b ==> (output <=> internal)) /
(input_a ==> (output <=> F)) /
(input_b ==> (output <=> F))
==> (output <=> ~(input_a
/ input_b))`;;
val it : thm =
|- (~input_a ==> (internal <=> true)) /
(~input_b ==> (output <=> internal)) /
(input_a ==> (output <=> false)) /
(input_b ==> (output <=> false))
==> (output <=> ~(input_a
/ input_b))
この例は手作業で検証するのはそれほど難しくありませんでした。一方、HOLのトートロジーチェッカーは、人間が混乱しやすい、やや大きな例にも対応できます。例えば、回路設計における次のパズル（Wos 1998, Wos and Pieper 1999）を考えてみましょう。
3つの入力i1、i2、i3と3つの出力を持つデジタル回路を構築する方法を示してください。出力はそれぞれi1、i2、i3の否定o1 = ¬ i1、o2 = ¬ i2、o3 = ¬ i3です。ANDゲートとORゲートは任意に使用できますが、NOTゲート（インバータ）は最大2つまでです。
注意してください、このパズルは驚くほど難しいです。読者は、自分で考える楽しみのために、以下の解決策から目をそらしたいかもしれません。（ただし、ちらっと見ても強い直感は得られないでしょう。）かなりの努力の末、私は次の解決策を思いつきましたが、それは十分に複雑で、その正しさはまったく明らかではありません。しかし、HOLで簡単に検証できます。TAUTで使用されるアルゴリズムは非常に単純なため、数秒かかりますが、手作業で行うよりも間違いなく優れています。
# TAUT
`(i1 /
i2 <=> a) /\n (i1 /
i3 <=> b) /\n (i2 /
i3 <=> c) /\n (i1 /
c <=> d) /\n (m /
r <=> e) /\n (m /
w <=> f) /\n (n /
w <=> g) /\n (p /
w <=> h) /\n (q /
w <=> i) /\n (s /
x <=> j) /\n (t /
x <=> k) /\n (v /
x <=> l) /\n (i1
/ i2 <=> m) /\n (i1
/ i3 <=> n) /\n (i1
/ q <=> p) /\n (i2
/ i3 <=> q) /\n (i3 /
a <=> r) /\n (a /
w <=> s) /\n (b /
w <=> t) /\n (d /
h <=> u) /\n (c /
w <=> v) /\n (~e <=> w) /\n (~u <=> x) /\n (i
/ l <=> o1) /\n (g
/ k <=> o2) /\n (f
/ j <=> o3)
==> (o1 <=> ~i1) /
(o2 <=> ~i2) /
(o3 <=> ~i3)`;;
このようにデジタル回路検証を行うことには、内部ワイヤの割り当てが実際に一貫しているかどうかのチェックがないという批判があります。例えば、インバータの出力が入力に接続されていると主張した場合、何でも推論できます。（異なる電圧を持つ2つのワイヤを接続することが電気的に何を意味するかは、物理的な詳細に依存します。コンポーネントは一方の値でロックされるか、発振するか、燃え尽きる可能性があります。）
# TAUT `(~output <=> output) ==> the_moon_is_made_of_cheese`;;
val it : thm = |- (~output <=> output) ==> the_moon_is_made_of_cheese
しかし、主張された内部ワイヤの割り当てが一貫していることを示す方法については、後で見ていきます。
5 方程式と関数
前のセクションでは、数、算術演算、数詞、ブール関数などを含むさまざまなHOL項を見てきました。これらすべてのエンティティやそれ以上のものを表現できるため、HOLの項構造は非常に複雑だと想像するかもしれません。それどころか、最低レベルではそれは単純そのものです。HOL項には4種類しかありません。
- 変数
- 定数
- 関数適用
- 抽象化
「x:bool」や「n:num」のような変数、および「true」（「true」）や「false」（「false」）のような定数は、おそらく読者が期待するようなものです。10 関数を引数に適用することを、関数と引数の項から構築された複合項と呼びます。例えば、「not p」を表す項、「~p」は、否定演算子を表す定数をブール変数に適用したものです。否定演算子を単独で項として入力できます。
# `~`;;
val it : term = `(~)`
アプリケーションの2つのコンポーネント（演算子とオペランドとも呼ぶ）について、それぞれrator（演算子=関数）とrand（オペランド=引数）という慣習的な専門用語を使用します。アプリケーションをその演算子とオペランドに分解する、または組み合わせでない場合に失敗する、対応する名前の関数が項にあります。
# rator `~p`;;
val it : term = `(~)`
# rand `~p`;;
val it : term = `p`
# rand `n:num`;;
Exception: Failure "rand: Not a combination".
OCamlと同様に、関数への引数を括弧で囲む必要はありません。ただし、優先順位を強制するために必要な場合を除きます。強調のために括弧を使用することを選択する場合もありますが、HOLは通常、追加の括弧を使用せずに表示します。もちろん、内部表現は、項がどのように入力されたかの特定の詳細を抽象化し、単に抽象構文木として扱います。
# `~(p)`;;
val it : term = `~p`
HOLにおけるアプリケーションの重要な点は、OCamlと同様に、演算子が型α → β（型αの引数を型βの結果にマッピングする関数）を持ち、オペランドが対応する型αを持つ場合にのみアプリケーションが形成できることです。その場合、組み合わせ全体は型βを持ちます。例えば、予想されるように、否定演算子は型bool -> boolを持ちます。
# type_of `(~)`;;
val it : hol_type = `:bool->bool`
5.1 カリー化関数
HOLの項表現は、複数の引数を持つ関数に特別な配慮をしていません。しかし、関数は1つの引数を受け取り、別の関数を生成することができます。これは、論理学者Haskell Curryにちなんでカリー化として知られるトリックを利用して、同じ効果を得ることができます。例えば、自然数の加算を二項関数ℕ ×ℕ →ℕと見なす代わりに、ℕ → (ℕ →ℕ) の関数と見なします。これは単一の引数aを受け取り、その引数にaを加える新しい関数を生成します。この中間関数は、2番目の引数bに適用され、最終結果a + bを生成します。言い換えれば、a + bと書くものは、HOLでは((+)a)(b)として表現されます。そして、infixの通常の表面構文が使用された場合でも、その文字列を明示的に入力できます。基盤となる項はまったく同じです。
# `((+) x) 1`;;
val it : term = `x + 1`
# `((+) x) 1` = `x + 1`;;
val it : bool = true
正確に同じカリー化表現がOCaml自体でも二項関数に一般的であることに注意してください。
# (+);;
val it : int -> int -> int = <fun>
# (+) 1;;
val it : int -> int = <fun>
カリー化はやや難解な表現トリックのように思えるかもしれませんが、カリー化された関数の部分適用から生じる中間関数を、それ自体で考慮すると便利な場合があります。例えば、後続操作を定義して別々に使用できます。
# let successor = (+) 1;;
val successor : int -> int = <fun>
# successor 5;;
val it : int = 6
# successor 100;;
val it : int = 101
カリー化は非常に一般的な操作であるため、OCamlとHOLの両方で、カリー化された関数を扱う際に必要な括弧の数を減らすために同じ規約を採用しています。関数適用は左結合性であるため、f a bはf(a(b))ではなく(f a) bを意味します。多くの初心者は、これに慣れるのに時間がかかるでしょう。
# (+) 1 2;;
val it : int = 3
# `(+) 1 2`;;
val it : term = `1 + 2`
また、反復関数型は右結合性であるため、二項カリー化関数の型α → β → γはα → (β → γ)を意味します。
5.2 ペアリング
これで、定数、変数、および適用のみを使用して、より複雑な項が内部的にどのように表現されるかを見始めることができます。例えば、この項の入力方法は、含意、等式、および加算の定数と変数x、y、z、Pからどのように適用によって構築されるかをより明確に示しています。HOLは、ユーザーが通常好む数学的表記法に近い方法でそれを表示します。
# `(==>) ((=) ((+) x y) z) (P z)`;;
val it : term = `x + y = z ==> P z`
ほとんどのインフィックス演算子はHOLとOCamlでカリー化されていますが、どちらも順序対の型を持っています。HOLの型α#β、またはOCamlのα*βは、最初の要素が型α、2番目の要素が型βを持つペアの型を表します。言い換えれば、型を集合と見なす場合、ペア型は構成集合のデカルト積です。OCamlとHOLの両方で、順序対は二項インフィックス演算子「,」を適用することによって構築されます。
# `1,2`;;
val it : term = `1,2`
# type_of it;;
val it : hol_type = `:num#num`
# 1,2;;
val it : int * int = (1, 2)
関数適用と同様に、慣習的な周囲の括弧は不要ですが、多くのユーザーは通常の数学的表記法との整合性のために括弧を含めることを好みます。OCamlはHOLとは異なり、括弧で表示することさえあります。括弧のない順序対は馴染みがないように見えるかもしれませんが、コンマを単なる二項インフィックス演算子と見なし、「魔法の」構文ではないという概念的な経済性があります。11 もちろん、HOLでは少なくとも、ペアリング操作自体はペアリングに基づいて定義できないため、カリー化されている必要があります。実際、HOLの定義済みの二項インフィックス演算子のすべて、およびOCamlのほとんどはカリー化されています。これは、カリー化が論理的に基本的であり、関数の部分適用が可能であることが非常に役立つ場合があるためです。しかし、OCamlのHOL構文操作の一部はペアを使用して定義されています。例えば、関数と引数から適用を構築するmk_combは、引数のペアを取ります。型が互換性のない項を組み合わせることを拒否することに注意してください。定理と同様に、項自体は型付けされていない「項」が除外される抽象型です。
# mk_comb(`(+) x`,`y:num`);;
val it : term = `x + y`
# mk_comb(`(+) 1`,`true`);;
Exception: Failure "mk_comb: types do not agree".
同様に、推論規則CONJ_PAIRは、共役定理を定理のペアに分解します。
# CONJ_PAIR(ASSUME `p /
q`);;
val it : thm * thm = (p /
q |- p, p /
q |- q)
一方、MK_COMBは、定理Γ ⊢ f = gとΔ ⊢ x = yのペアを取り、Γ ∪Δ ⊢ f(x) = g(y)を返します。
# (ASSUME `(+) 2 = (+) (1 + 1)`,ARITH_RULE `3 + 3 = 6`);;
val it : thm * thm =
((+) 2 = (+) (1 + 1) |- (+) 2 = (+) (1 + 1), |- 3 + 3 = 6)
# MK_COMB it;;
val it : thm = (+) 2 = (+) (1 + 1) |- 2 + 3 + 3 = (1 + 1) + 6
OCamlには、順序対の2つのコンポーネントを選択するための関数fst（「最初」）とsnd（「2番目」）があります。同様に、HOLには同じものがありますが、大文字（特に理由はありません）です。
# fst(1,2);;
val it : int = 1
# snd(1,2);;
val it : int = 2
5.3 等式推論
方程式はHOLにおいて、数学全般よりもさらに基本的です。HOLの少数の原始推論規則のほとんど（上記のMK_COMBなど）は等式のみを含み、他のすべての論理概念は等式に基づいて定義されています。実際、「⇔」はブール型のオブジェクト間の等式に他なりません。HOLは、概念的に明確に見えるため、また論理記号の優先順位を低く設定して、例えばp ∧ x = 1 ⇔ qを括弧なしでp ∧ (x = 1) ⇔ qとして解析できるようにするために、それを異なる方法で解析および表示します。
# `p /
x = 1 <=> q`;;
val it : term = `p /
x = 1 <=> q`
# `(p /
x = 1) = q`;;
val it : term = `p /
x = 1 <=> q`
# `p /
x = 1 = q`;;
val it : term = `p /
(x <=> 1 = q)`
等式が（（=）s）tの形式の項にすぎないことは、おそらく読者が理解するまでにはしばらく時間がかかるでしょう。しかし、それらは十分に重要であるため、方程式の構築と分解のために特別な派生構文操作が定義されています。名前と以下の例から、4つの操作mk_eq、dest_eq、lhs（左辺）、およびrhs（右辺）のアイデアが得られることを願っています。
# mk_eq(`1`,`2`);;
val it : term = `1 = 2`
# dest_eq it;;
val it : term * term = (`1`, `2`)
# lhs `1 = 2`;;
val it : term = `1`
# rhs `1 = 2`;;
val it : term = `2`
等号関係の3つの基本的な性質は、それが反射的（t = tは常に成り立つ）、対称的（s = tならばt = s）、および推移的（s = tかつt = uならばs = u）であることです。これらの各性質には対応するHOL推論規則があります。反射性の規則（REFL）はすでに見てきました。ここでは対称性（SYM）と推移性（TRANS）の規則も動作中です。
# REFL `1`;;
val it : thm = |- 1 = 1
# SYM (ARITH_RULE `1 + 1 = 2`);;
val it : thm = |- 2 = 1 + 1
# SYM (ARITH_RULE `2 + 2 = 4`);;
val it : thm = |- 4 = 2 + 2
# TRANS (ARITH_RULE `1 + 3 = 4`) it;;
val it : thm = |- 1 + 3 = 2 + 2
前に見た合同規則MK_COMBは、もう1つの同様の単純な規則EQ_MPです。これは、定理Γ ⊢ p ⇔ q（つまり、ブール値pとqの場合、Γ ⊢ p = q）と別の定理Δ ⊢ pを受け取り、Γ ∪Δ ⊢ qを返します。ここで、SYMが原始的でない方法でどのように定義されているかを見るのは有益かもしれません。まず、まだ言及していないOCamlのいくつかの機能について説明する必要があります。OCamlの定義は特定の式にローカルにすることができます。そのため、式と定義は任意に深く絡み合わせることができます。これは、次の抽象構文の観点から理解できます。
<binding> ::= <pattern> = <expression>
<bindings> ::= <binding>
| <binding> and <bindings>
<definition> ::= let <bindings>
<expression> ::= <basic expression>
| <definition> in <expression>
例えば、トップレベルでxとyを定義すると、それらは後で利用可能になります。
# let x = 1 and y = 2;;
val x : int = 1
val y : int = 2
# x + y;;
val it : int = 3
または、uとvの定義を式u + vにローカルに制限すると、それらは後で不可視になります（または、以前の値が保持されます）。
# let u = 1 and v = 2 in u + v;;
val it : int = 3
# u;;
Error: Unbound value "u"
# let x = 10 and y = 20 in x + y;;
val it : int = 30
# x;;
val it : int = 1
もう1つの便利な機能は、バインディングの左辺が単なる変数ではなく、より一般的なパターンである可能性があることです。例えば、次の後。
# let pair = (1,2);;
val pair : int * int = (1, 2)
コンポーネントにアクセスするためにfstとsndを使用する必要はありません。
# let x = fst pair and y = snd pair;;
val x : int = 1
val y : int = 2
しかし、直接次のように書くことができます。
# let x,y = pair;;
val x : int = 1
val y : int = 2
# let x = fst pair and y = snd pair;;
val x : int = 1
val y : int = 2
派生推論規則SYMの定義を考えてみましょう。
let SYM th =
let tm = concl th in
let l,r = dest_eq tm in
let lth = REFL l in
EQ_MP (MK_COMB(AP_TERM (rator (rator tm)) th,lth)) lth;;
これや同様の派生規則の定義を理解するには、単純な「汎用」インスタンスステップをステップバイステップでトレースする価値があります。したがって、結論l = rを持つ定理を作成し、それをthという名前を付けて、引数と一致させましょう。
# let th = ASSUME `l:num = r`;;
val th : thm = l = r |- l = r
これで、推論規則の動作をステップバイステップでトレースし、最終的な結論r = lを持つ定理をどのように取得できるかを確認できます。ローカル定義を模倣するだけでなく、最後の行の大きな式を中間値を保持するために使用して分解します。
# let tm = concl th;;
val tm : term = `l = r`
# let l,r = dest_eq tm;;
val l : term = `l`
val r : term = `r`
# let lth = REFL l;;
val lth : thm = |- l = l
# rator (rator tm);;
val it : term = `(=)`
# AP_TERM it th;;
val it : thm = l = r |- (=) l = (=) r
# MK_COMB(it,lth);;
val it : thm = l = r |- l = l <=> r = l
# EQ_MP it lth;;
val it : thm = l = r |- r = l
これは少し曖昧でしたが、今や任意の等式に適用できる一般的な規則SYMとしてカプセル化されたので、その内部動作を気にする必要はなくなりました。
5.4 定義
HOLでは新しい定数を定義できます。新しい定数cを項tの省略名として定義したい場合は、単純に関数new_definitionを、変数vが目的の名前を持つ方程式v = tに適用します。この関数は定数cを定義し、cが定数になった対応する定理⊢ c = tを返します。
# let wordlimit = new_definition `wordlimit = 2 EXP 32`;;
val wordlimit : thm = |- wordlimit = 2 EXP 32
new_definition関数は、定義の論理的一貫性を確保するためにいくつかの制限を課します。例えば、既存の定数を異なるものとして再定義することはできません。
# let wordlimit' = new_definition `wordlimit = 2 EXP 64`;;
Exception: Failure "new_basic_definition: 'wordlimit' is already defined".
これは論理的な矛盾につながるためです。定理⊢ c = 2^32と⊢ c = 2^64から、⊢ 2^32 = 2^64、したがって⊢⊥を推論できます。OCamlと同様に、引数を取る関数を定義することもできます。
# let wordlim = new_definition `wordlim n = 2 EXP n`;;
val wordlim : thm = |- forall n. wordlim n = 2 EXP n
また、関数引数に同様のパターンマッチングを使用することもできます。
# let addpair = new_definition `addpair(x,y) = x + y`;;
val addpair : thm = |- forall x y. addpair (x,y) = x + y
再帰と高度なパターンマッチングを使用した、はるかに一般的な形式の定義が可能であり、後で検討します。
6 抽象化と量化子
前のセクションで、HOLには4種類の項があると述べました。変数、定数、および適用については十分に見てきましたが、抽象化についてはどうでしょうか？これまでのところ、変数は初等代数の起源に沿って、任意の値を表すために使用されてきました。このような場合、変数は自由であると言われます。なぜなら、それらを好きなものに置き換えることができるからです。推論規則INSTはこの概念を形式化します。変数を含む定理を証明できる場合、その任意のインスタンスを証明できます。例えば。
# let th = ARITH_RULE `x + y = y + x`;;
val th : thm = |- x + y = y + x
# INST [`1`,`x:num`; `z:num`,`y:num`] th;;
val it : thm = |- 1 + z = z + 1
しかし、数学における変数はしばしば異なる方法で使用されます。∑ n=1∞1∕n^2のような和では、nは自由変数ではありません。同様に、∫ 0^1 e^{-x^2} dxのxや、{k^2∣k ∈ℕ}のような集合内包のkも同様です。むしろ、このような場合、変数は異なる部分間の対応を示すために内部的に使用されます。そのような変数は束縛されていると言われます。λx.tのような束縛構造の中にラップされると、それは、いわば「キャプチャ」され、外部での独立した意味を持ちません。束縛変数は、通常の言語における代名詞にいくぶん似ています。これは、以前に確立された名詞を参照するためにローカルに使用されますが、外部での意味はありません。例えば、「彼は本を閉じてバッグに入れた」という文では、「それ」の意味は、この文にローカルであり、「本」という名詞の以前の使用によって確立されます。次の文では、「それ」という言葉は異なるものを参照する可能性があります：「彼は本を閉じてバッグに入れた。天気は良く、彼は外に出て楽しみたいと思った。」
数学には多くの変数束縛構造があります。HOLは原始的な変数束縛概念の豊富さを持っていませんが、それらをただ1つ、抽象化（関数適用とは逆の操作）に基づいてすべて表現します。変数xと項t（xを含む場合も含まない場合もある）を与えると、いわゆるラムダ抽象λx.tを構築できます。これは「xの関数でtを生成するもの」を意味します。HOLのASCII構文では、バックスラッシュが使用されます。例えば、λx.x + 1は引数に1を加える関数であり、HOL項として次のように記述できます。
# `
x. x + 1`;;
val it : term = `
x. x + 1`
# type_of it;;
val it : hol_type = `:num->num`
「ラムダ」記号は、慣れる必要がある標準的な論理専門用語です。OCamlでは、類似の構造は「λ」の代わりにfunキーワードを使用し、ドットの代わりに->を使用します。
# fun x -> x + 1;;
val it : int -> int = <fun>
# it 82;;
val it : int = 83
抽象化と適用がHOLで逆操作である正確な意味は、原始推論規則BETAが存在することです。これは⊢ (λx.t)x = tを教えてくれます。例えば。
# let th = BETA `(
x. x + 1) x`;;
val th : thm = |- (
x. x + 1) x = x + 1
ラムダ項「λx.⋯」内の変数のインスタンスはすべて束縛されていると見なされ、インスタンス化によってそのまま残されます。インスタンス化は自由変数を置き換えるだけです。例えば。
# subst [`1`,`x:num`] `
x. x + 1`;;
val it : term = `
x. x + 1`
# INST [`1`,`x:num`] (REFL `
x. x + 1`);;
val it : thm = |- (
x. x + 1) = (
x. x + 1)
より興味深いことに、上記の定理thにインスタンス化を適用した場合に何が起こるかに注意してください。
# INST [`y:num`,`x:num`] th;;
val it : thm = |- (
x. x + 1) y = y + 1
束縛されたxのインスタンスはそのまま残されましたが、2つの自由インスタンスはyにインスタンス化されたことに注意してください。したがって、2つのステップで、抽象化を任意の引数に適用し、抽象化の本体の適切に置換されたインスタンスを取得するという、より一般的な概念を得ることができます。
OCamlとHOLの両方で、引数を持つ定義は、ラムダ式の基本的な定義の省略名として単純に考慮できます。例えば、OCamlではこれらは完全に同等です。
# let successor x = x + 1;;
val successor : int -> int = <fun>
# let successor = fun x -> x + 1;;
val successor : int -> int = <fun>
6.1 量化子
Pが何らかのαに対する型α → boolの項であると仮定します。このような型の項を述語と呼びます。述語は集合と見なすことも、より正確には型の部分集合と見なすこともできます。実際、HOLは集合の別個の概念を定義せず、通常の「∈」に対応するinfix集合メンバーシップ記号INを単にx IN s <=> s xと定義します。したがって、述語を、同じ項内でも、関数からブール値への変換として、または集合として考えることは、正常であり、しばしば便利です。
述語がその引数のすべての値に対して真である（値⊤ を生成する）こと、または真となる引数が存在すること、あるいは一意に存在する引数が存在することを言えることは、しばしば有用です。12 伝統的な「一階論理」（Enderton 1972またはMendelson 1987で良い入門書を参照）では、述語は他の関数とは別に考慮され、「すべて」のようなことを言う特別な「量化子」は言語の原始的な概念です。これらの特別な措置は必要なく、量化のすべての種類をより原始的な概念を使用して定義できます。
例えば、Pがすべての引数に対して成り立つと言うことは、それが定数関数（値が「真」）である（等しい）こと、つまりP = λx.⊤ を言うことと同じです。13 したがって、通常∀ と書かれ、「すべて」と発音される普遍量化子を、Pに対して、(∀ )P ⇔ (P = λx.⊤ )と定義できます。
(∀ ) = λP.P = λx.⊤
これは実際、HOLで定義されているとおりです。∀ はASCII文字ではないため、HOLは量化子を記述するために2つの方法を提供します。感嘆符!とforallという英語の単語です。どちらもまったく同じ定数を表し、HOL Lightが項を表示するときに使用する単語です。例えば、定義方程式（⊤ は前述のようにtrueと表示されます）を示す次の定理です。
# FORALL_DEF;;
val it : thm = |- (forall) = (\P. P = (\x. true))
実際には、量化子を適用したい述語は通常ラムダ式です。例えば、「すべてのnに対して、n < n + 1」と言うには、∀ (λn.n < n + 1)を使用します。これは非常に一般的な構成であるため、∀ n.n < n + 1と単純に記述すると便利です。これは一階論理の伝統的な表記法に近いです。HOLは、この形式を解析および表示しますが、!で書かれた入力はforallと表示され、基盤となる項は抽象化に適用される定数で構成されることに注意してください。
# `!n. n < n + 1`;;
val it : term = `forall n. n < n + 1`
# dest_comb it;;
val it : term * term = (`(forall)`, `\n. n < n + 1`)
!のような定数は、抽象化に適用されたときに省略された形式で解析および表示されるため、バインダーと呼ばれます（ただし、厳密にはそうではありません。それは基盤となる抽象化がそれを行うからです）。今のところ、3つの重要なものは3つの量化子であり、それぞれが上記の普遍量化子と同様に、シンボルまたは英語の単語のいずれかで記述できます。
| ∀ | ! または forall | For all |
| ∃ | ? または exists | There exists |
| ∃ ! | ?! または existsunique | There exists a unique |
入力にはどちらのスペルも使用でき、HOL Lightは英語のスペルを表示します。14
ラムダ抽象および他のすべてのバインダー構造に適用されるもう1つの便利な構文省略形は、反復適用を圧縮できることです。例えば、λx.λy.x + yと書く代わりに、λxy.x + yと書くことができ、同様に同じ種類の複数の量化子についても同様です。しかし、いつものように、これは単なる便利な表面構文であり、基盤となる項はコア構造が反復されています。
# `!m n. m + n = m + m`;;
val it : term = `forall m n. m + n = m + m`
# dest_comb it;;
val it : term * term = (`(forall)`, `\m. forall n. m + n = m + m`)
すべての量化子には、定義から派生した導入規則と除去規則があります。普遍量化子の場合、2つの主要な規則は、自由変数を普遍的に量化するGEN（一般化）と、その逆操作であるSPEC（特殊化）であり、普遍量化された変数をインスタンス化します。例えば、ここで変数を一般化してから再び特殊化します。これは、同じ効果をINSTを直接使用して得ることができるため、ここではやや無意味です。
# let th = ARITH_RULE `x + 1 = 1 + x`;;
val th : thm = |- x + 1 = 1 + x
# GEN `x:num` th;;
val it : thm = |- forall x. x + 1 = 1 + x
# SPEC `y + z` it;;
val it : thm = |- (y + z) + 1 = 1 + y + z
一般化しようとしている変数が仮説に出現する場合（自由変数として）、GENは適用できないことに注意してください。これは論理的一貫性を確保するために必要であり、派生規則としてのGENの実装から自然に生じます。
# ASSUME `x + 1 = 1 + x`;;
val it : thm = x + 1 = 1 + x |- x + 1 = 1 + x
# GEN `x:num` it;;
Exception: Failure "ABS".
複数の変数を一緒に特殊化および一般化できる「リスト」バージョンSPECLとGENLもありますが、これらは適切な順序でより基本的な関数の反復適用を省略したものと見なすことができます。
# SPEC `1` (SPEC `2` ADD_SYM);;
val it : thm = |- 2 + 1 = 1 + 2
# SPECL [`1`; `2`] ADD_SYM;;
val it : thm = |- 1 + 2 = 2 + 1
6.2 一階論理推論
量化子をネストして使用することで、変数間のより興味深い依存関係を表現できます。ネストの順序はしばしば重要です。例えば、loves(x,y)を「xはyを愛している」と考えると：
- ∀ x.∃ y.loves(x,y) は、すべての人が愛する誰かを持っていることを意味します。
- ∀ y.∃ x.loves(x,y) は、すべての人が自分を愛する誰かを持っていることを意味します。
- ∃ y.∀ x.loves(x,y) は、ある（固定された）人がすべての人に愛されていることを意味します。
より数学的な例として、関数f : ℝ →ℝの連続性と一様連続性のε-δ定義を考えてみましょう。連続性は、任意のε > 0に対して、各xに対してあるδ > 0が存在し、|x'− x| < δならば、|f(x') − f(x)| < εも成り立つことを主張します。
∀ ε.ε > 0 ⇒∀ x.∃ δ.δ > 0 ∧∀ x′.|x′− x| < δ ⇒|f(x′) − f(x)| < ε
一方、一様連続性は、任意のε > 0に対して、xに依存しないあるδ > 0が存在し、すべてのxおよびx'に対して、|x'− x| < δならば、|f(x') − f(x)| < εも成り立つことを主張します。量化の順序が変更されると、主張されるプロパティが根本的に変化することに注意してください。
∀ ε.ε > 0 ⇒∃ δ.δ > 0 ∧∀ x.∀ x′.|x′− x| < δ ⇒|f(x′) − f(x)| < ε
トートロジー証明器TAUTは非自明な量化子推論を処理できませんが、MESONというより強力な自動ツールがあり、非常に便利です。量化子論理における妥当性の決定は決定不能問題ですが、MESONは「モデル除去」と呼ばれる自動証明探索方法を使用します（Loveland 1968, Stickel 1988）。これはしばしば妥当な公式で成功します。（通常はループし続けるか、深さ制限に達して失敗しますが、公式が無効であることを示すわけではありません。）例えば、古典的な「三段論法」を証明できます。
# MESON[] `(!(x:A). man(x) ==> mortal(x)) /
man(Socrates) ==> mortal(Socrates)`;;
0..0..1..solved at 4
val it : thm =
|- (forall x. man x ==> mortal x) /
man Socrates ==> mortal Socrates
MESONは、次のパズルで示されるような、量化子を伴う複雑だが本質的に単純な推論を自動化するのに非常に便利なツールです。これはPeter Andrewsによるものです。
# MESON[]
`((?x. !y. P(x) <=> P(y)) <=> ((?x. Q(x)) <=> (!y. Q(y)))) <=>
((?x. !y. Q(x) <=> Q(y)) <=> ((?x. P(x)) <=> (!y. P(y))))`;;
時には、MESONは人々がそれほど明白ではないと考えるものさえ自動的に証明できます。例えば、Łoś（Rudnicki 1987）に帰せられる次の例です。これは、集合（型）A上の2つの二項関係PとQが両方とも推移的で、少なくとも一方が対称的であり、それらの和が集合A × A全体をカバーする場合、一方または他方の関係がすでにA × A全体であると主張しています。機械は私よりもはるかに速くこれを証明します。
# MESON[]
`(!x y z. P x y /
P y z ==> P x z) /
(!x y z. Q x y /
Q y z ==> Q x z) /
(!x y. P x y ==> P y x) /
(!x y. P x y
/ Q x y)
==> (!x y. P x y)
/ (!x y. Q x y)`;;
しかし、MESONは純粋に論理的な事実のみを証明できます。つまり、定数の解釈が何であれ成り立つ事実です。例えば、「≤」が反射的であることや、2 + 2 = 4であることを証明するために使用しようとすると失敗します。
# MESON[] `!x. x <= x`;;
...Exception: Failure "solve_goal: Too deep".
理由は、その事実が一般的な二項関係には当てはまらない、不等号関係の特別な性質に依存しているからです。一方、次の、はるかに明白ではない問題 — Dijkstra（1989）がHoareに帰したものです — は即座に解決されます。
# let ewd1062 = MESON[]
`(!x. x <= x) /
(!x y z. x <= y /
y <= z ==> x <= z) /
(!x y. f(x) <= y <=> x <= g(y))
==> (!x y. x <= y ==> f(x) <= f(y)) /
(!x y. x <= y ==> g(x) <= g(y))`;;
ポイントは、これが通常の不等号関係を使用している場合でも、これは本質的ではなく、任意の二項関係に置き換えても同様に有効であるということです。
# let ewd1062 = MESON[]
`(!x. R x x) /
(!x y z. R x y /
R y z ==> R x z) /
(!x y. R (f x) y <=> R x (g y))
==> (!x y. R x y ==> R (f x) (f y)) /
(!x y. R x y ==> R (g x) (g y))`;;
MESONが特別に扱う主な定数は論理結合子と等号関係です。後者は、「一意存在」量化子を扱うために anyway 必要です。次の問題のように15。
# MESON[] `(?!x. g(f x) = x) <=> (?!y. f(g y) = y)`;;
これは、他の定数について推論するためにMESONを使用できないという意味ではありません。単に、それらの定数の必要なプロパティを提供する必要があるということです。これらのプロパティは単純に定義であるか、またはより可能性が高いのはそれに関するより高レベルの結果です。例えば、加算が結合的で可換であるとMESONに伝えると、結果として他の定理を推論できます。
# MESON [ADD_ASSOC; ADD_SYM] `m + (n + p) = n + (m + p)`;;
7 変換と書き換え
しばしば、一連の中間段階を経由して、体系的な変換プロセスを使用してある項が別の項に等しいことを示したい場合があります。最終的に、初期項と最終項が等しいことを証明する正式なHOL定理が必要な場合、等式定理を維持しながら変換プロセスを整理するには、少し注意が必要です。これを容易にするために、HOLは変換の体系的なフレームワークを提供します（Paulson 1983）。
A conversion is simply an inference rule of type term -> thm that when given a term t, always returns (assuming it doesn’t fail) an equational theorem of the form ⊢ t = t', that is, it proves that the term it was given is equal to some other term, possibly the same as the original. For example, we can think of the primitive inference rule REFL as the 'trivial' or 'identity' conversion because given a term t it always, without fail, returns the reflexive theorem ⊢ t = t. A slightly more interesting one is BETA_CONV, which reduces a beta-redex (λx.s[x])t and gives the theorem ⊢ (λx.s[x])t = s[t]. (It is implemented by stringing together BETA and INST much as we did manually above.)
# BETA_CONV `(
x. x + 2) 1`;;
val it : thm = |- (
x. x + 2) 1 = 1 + 2
数詞上の算術演算を含む式の「評価」を実行するための変換のファミリーが、各算術演算子ごとに存在します。例えば。
# NUM_ADD_CONV `2 + 2`;;
val it : thm = |- 2 + 2 = 4
# NUM_MULT_CONV `9 * 6`;;
val it : thm = |- 9 * 6 = 54
# NUM_EXP_CONV `2 EXP 8`;;
val it : thm = |- 2 EXP 8 = 256
7.1 変換子
変換の均一なアプローチの利点は、基本的な変換をより複雑な変換にまとめるための汎用関数、しばしば「変換子」と呼ばれるものがあることです。例えば、THENCはインフィックスとして2つの変換を取り、最初の変換を適用し、次に結果に2番目の変換を適用することから得られる新しい変換を返します。等式定理を維持する必要があることを考えると、これは単に関数の合成よりも複雑ですが、実装はそれほど難しくありません。本質的には次のとおりです。
# let (THENC) =
fun conv1 conv2 t ->
let th1 = conv1 t in
let th2 = conv2 (rand(concl th1)) in
TRANS th1 th2;;
例えば、ベータ変換を実行し、次に結果に加算を実行する変換を構築できます。
# let BETA_ADD_CONV = BETA_CONV THENC NUM_ADD_CONV;;
val BETA_ADD_CONV : term -> thm = <fun>
# BETA_ADD_CONV `(
x. x + 2) 1`;;
val it : thm = |- (
x. x + 2) 1 = 1 + 2
もう1つの有用なビルディングブロックは、インフィックス変換子ORELSECです。これは最初の変換を試しますが、失敗した場合（例外を生成した場合）、代わりに2番目の変換を試します。例えば、加算、乗算、または指数を評価する変換を次のように構築できます。
# let NUM_AME_CONV = NUM_ADD_CONV ORELSEC NUM_MULT_CONV ORELSEC NUM_EXP_CONV;;
何もできない場合、多くの変換は自然に例外を生成します。他のものは反射定理を返します。TRY_CONVを使用して、一方の動作をもう一方の動作に簡単に交換できます。これは変換を試みますが、失敗した場合は反射定理を喜んで返します。
# TRY_CONV NUM_ADD_CONV `1 + 2`;;
val it : thm = |- 1 + 2 = 3
# TRY_CONV NUM_ADD_CONV `7 - 3`;;
val it : thm = |- 7 - 3 = 7 - 3
そして、CHANGED_CONVは、引数変換が反射定理を返した場合に失敗を生成します。また、REPEATCを使用して、変換が失敗するまで繰り返し適用することもできます。例えば。
# BETA_CONV `(
x. (
y. x + y) 2) 1`;;
val it : thm = |- (
x. (
y. x + y) 2) 1 = (
y. 1 + y) 2
# REPEATC BETA_CONV `(
x. (
y. x + y) 2) 1`;;
val it : thm = |- (
x. (
y. x + y) 2) 1 = 1 + 2
7.2 深さ変換
他の有用な変換子は、変換を項のサブ項に適用することを可能にします。基本的なものは、RAND_CONVであり、変換を組み合わせのrandに適用します。
# RAND_CONV NUM_ADD_CONV `1 + 2 + 3`;;
val it : thm = |- 1 + 2 + 3 = 1 + 5
RATOR_CONVは、変換をratorに適用します。
# RATOR_CONV BETA_CONV `(
x y. x + y) 1 2`;;
val it : thm = |- (
x y. x + y) 1 2 = (
y. 1 + y) 2
そしてABS_CONVは、変換を抽象化の本体に適用します。
# ABS_CONV BETA_CONV `
x. (
y. x + y) 2`;;
val it : thm = |- (
x. (
y. x + y) 2) = (
x. x + 2)
それら基本的なものから、LAND_CONV（二項演算子の左引数に適用）、BINDER_CONV（量化子などのバインダーの本体に適用）、BINOP_CONV（二項演算子の両方の引数に適用）など、他のいくつかの変換が定義されています。項の特定の部分に変換を指示するには、これらのプリミティブを合成するだけです。例えば。
# (RAND_CONV o RAND_CONV o LAND_CONV) NUM_ADD_CONV
`f(1 + 2,3 + 4) + g(5 + 6,7 + 8)`;;
val it : thm =
|- f (1 + 2,3 + 4) + g (5 + 6,7 + 8) = f (1 + 2,3 + 4) + g (11,7 + 8)
適切な変換子のシリーズを特定するのは苦痛になる可能性があります。おそらくより便利な代替手段はPAT_CONVです。これは、変換を適用する場所を示す抽象項を取ります。パターン内の特定の名前と型は、構造を識別する限り無関係です。
# PAT_CONV `
x. f(c,x) + g(x,x)` NUM_ADD_CONV
`f(1 + 2,3 + 4) + g(5 + 6,7 + 8)`;;
Warning: inventing type variables
val it : thm = |- f (1 + 2,3 + 4) + g (5 + 6,7 + 8) = f (1 + 2,7) + g (11,15)
次のクラスの変換子は、より「自動的」な方法で適用可能なサブ項に変換を適用します。例えば、ONCE_DEPTH_CONVは、項のトップダウン走査で最初に適用可能な項に変換を適用します。それより深い項は検査されませんが、最初に遭遇した適用可能な項が互いに素である場合、複数の項が変換されます。
# ONCE_DEPTH_CONV NUM_AME_CONV `1 + (2 + 3)`;;
val it : thm = |- 1 + 2 + 3 = 1 + 5
# ONCE_DEPTH_CONV NUM_AME_CONV `(1 + 1) * (1 + 1)`;;
val it : thm = |- (1 + 1) * (1 + 1) = 2 * 2
NUM_AME_CONVのような変換は、複合式を評価するために、ボトムアップ方式で再帰的に使用するのが最も自然です。これはDEPTH_CONVで実行できます。
# DEPTH_CONV NUM_AME_CONV `(2 EXP 8 + 1) * (3 * 2 EXP 5 + 1)`;;
val it : thm = |- (2 EXP 8 + 1) * (3 * 2 EXP 5 + 1) = 24929
実際、HOLにはNUM_REDUCE_CONVという事前定義関数があり、本質的に同じ実装を使用していますが、減算などの他のすべての算術演算も処理されます。
# NUM_REDUCE_CONV `2 EXP (32 + (22 DIV 7)) - 7 * (121 - 4 EXP (1 + 1))`;;
val it : thm =
|- 2 EXP (32 + 22 DIV 7) - 7 * (121 - 4 EXP (1 + 1)) = 34359737633
しかし、DEPTH_CONVは常に必要なものではありません。時には、あるレベルで変換を適用するという行為が、下位で新しい適用可能な項を作成することがあります。この場合、DEPTH_CONVはそれらを再検査しません。他の2つの変換子、TOP_DEPTH_CONVとREDEPTH_CONVは、変換を可能な限りすべての項に適用し続けます。
# DEPTH_CONV BETA_CONV `(
x f. f x) (
y. y + 1)`;;
val it : thm = |- (
x f. f x) (
y. y + 1) = (
x. (
y. y + 1) x)
# REDEPTH_CONV BETA_CONV `(
x f. f x) (
y. y + 1)`;;
val it : thm = |- (
x f. f x) (
y. y + 1) = (
x. x + 1)
# TOP_DEPTH_CONV BETA_CONV `(
x f. f x) (
y. y + 1)`;;
val it : thm = |- (
x f. f x) (
y. y + 1) = (
x. x + 1)
これらの2つの深さ変換の違いは、主なスイープがそれぞれトップダウンとボトムアップであることです。これにより、一部の状況では、一方が他方よりも好ましい場合があります。主に効率上の理由からです。
7.3 マッチング
読者は、「modus ponens」推論規則MPを覚えているかもしれません。これは、⊢ p ⇒ qと⊢ pから⊢ qへの推移を可能にします。しかし、定理は正確に同じpに一致する必要があります。16
# LT_IMP_LE;;
val it : thm = |- forall m n. m < n ==> m <= n
# MP LT_IMP_LE (ARITH_RULE `1 < 2`);;
Exception: Failure "dest_binary".
# MP (SPECL [`1`; `2`] LT_IMP_LE) (ARITH_RULE `1 < 2`);;
val it : thm = |- 1 <= 2
このような場合、1つの定理をもう一方に一致させるために、正しいインスタンス化を選択するタスクをHOLに委任する方が便利です（SPECL、INSTなどを使用）。より強力な規則MATCH_MPはまさにそれを実行します。2番目の引数定理は固定と見なされ、最初の定理はそれに一致するようにインスタンス化されます。
# MATCH_MP LT_IMP_LE (ARITH_RULE `1 < 2`);;
val it : thm = |- 1 <= 2
マッチング規則REWR_CONV（「書き換え変換」）もあります。これは、等式定理⊢ s = tを受け取り、sに一致できる項s'に適用されたときに、対応する定理⊢ s' = t'を返し、それ以外の場合は失敗する変換を生成します。
# REWR_CONV ADD_SYM `7 + 8`;;
val it : thm = |- 7 + 8 = 8 + 7
HOLでは「もしかつもし」が単なる等式でもあるため、これも⊢ p ⇔ qの形式の定理に使用できます。これは、多くの論理変換も書き換えによって実装できることを意味します。例えば。
# LE_LT;;
val it : thm = |- forall m n. m <= n <=> m < n
/ m = n
# REWR_CONV LE_LT `1 <= x`;;
val it : thm = |- 1 <= x <=> 1 < x
/ 1 = x
マッチングは単純なインスタンス化よりもわずかに一般的です。それは、より多くのものを一致させるために、ベータ変換を使用して項を少しシャッフルすることもできます。（これは一般的に「高階マッチング」と呼ばれます。）例えば、次の定理を使用することを考えてみましょう。これは、すべてのxがPを満たすということは、Pを満たさないxが存在するということではないことを示す、一種の無限ド・モルガンの法則です。
# NOT_FORALL_THM;;
val it : thm = |- forall P. ~(forall x. P x) <=> (exists x. ~P x)
# let NOT_FORALL_CONV = REWR_CONV NOT_FORALL_THM;;
val NOT_FORALL_CONV : term -> thm = <fun>
その変換を定義した後、さまざまな一致可能な項に適用できます。
# NOT_FORALL_CONV `~(!n. EVEN n)`;;
val it : thm = |- ~(forall n. EVEN n) <=> (exists n. ~EVEN n)
# NOT_FORALL_CONV `~(!s:num->bool. FINITE s)`;;
val it : thm = |- ~(forall s. FINITE s) <=> (exists s. ~FINITE s)
すべて期待どおりに機能します。おそらく少し驚くべきは次のとおりです。
# NOT_FORALL_CONV `~(!n. n * n = n + n)`;;
val it : thm = |- ~(forall n. n * n = n + n) <=> (exists n. ~(n * n = n + n))
単純なマッチングを使用すると、これは機能しません。P xをn * n = n + nに一致させる必要があります。これは、基盤となる項構造を考えると、Pを(=) (n * n)に、xをn + nに設定することを意味します。しかし、後者の代入はxが束縛変数であるため不可能であり、実際には最初のものも機能しません。17 HOLが実際に行うことは、項を一致可能にするための逆ベータ還元の一種であり、その後、手動で行うのと同様に、元の形式に戻すためのターゲットベータ変換です。
# NOT_FORALL_CONV `~(!n. (
k. k * k = k + k) n)`;;
val it : thm =
|- ~(forall n. (
k. k * k = k + k) n) <=>
(exists n. ~(
k. k * k = k + k) n)
# CONV_RULE(ONCE_DEPTH_CONV BETA_CONV) it;;
val it : thm = |- ~(forall n. n * n = n + n) <=> (exists n. ~(n * n = n + n))
7.4 書き換え
REWR_CONVを深さ変換子と組み合わせて使用することで、一連の等式定理を使用して項を可能な限り書き換えることができます。例えば、加算の結合性を使用して項を繰り返し書き換えると、完全に左結合形式が得られます。
# TOP_DEPTH_CONV(REWR_CONV ADD_ASSOC)
`(a + b) + ((c + d) + e) + f + g + h`;;
val it : thm =
|- (a + b) + ((c + d) + e) + f + g + h =
((((((a + b) + c) + d) + e) + f) + g) + h
実際、結果を最も見栄え良くするには、逆方向に書き換える方が良いです。加算は右結合性であるため、最小の括弧が得られます。ADD_ASSOC定理にSYMを直接適用することはできませんが、わずかに一般化されたGSYM（一般化対称性）は、普遍量化子を下降させます。
# ADD_ASSOC;;
val it : thm = |- forall m n p. m + n + p = (m + n) + p
# GSYM it;;
val it : thm = |- forall m n p. (m + n) + p = m + n + p
# TOP_DEPTH_CONV(REWR_CONV it)
`(a + b) + (((c + d) + e) + (f + g + h))`;;
val it : thm =
|- (a + b) + ((c + d) + e) + f + g + h = a + b + c + d + e + f + g + h
書き換えは非常に一般的な操作であるため、HOLは、定理のスイート全体での書き換えを容易にするための、いくつかの高レベルな書き換え変換子を提供します。最も一般的なのは次のとおりです。
GEN_REWRITE_CONV convl [th1; ...; thn]
successive matching の一部の最適化を除いて、これは基本的に次のものと同じです。
convl(REWR_CONV th1 ORELSEC ... ORELSEC thn)
ただし、1つの重要な一般化があります。定理のリストには、個々の書き換えに分解される等式の連鎖を含めることができます。これはREWR_CONVでは処理されません。
# ADD_CLAUSES;;
val it : thm =
|- (forall n. 0 + n = n) /
(forall m. m + 0 = m) /
(forall m n. SUC m + n = SUC (m + n)) /
(forall m n. m + SUC n = SUC (m + n))
# REWR_CONV ADD_CLAUSES;;
Exception: Failure "dest_eq".
# GEN_REWRITE_CONV REDEPTH_CONV [ADD_CLAUSES];;
val it : conv = <fun>
# it `SUC(0 + SUC(SUC 0 + 0))`;;
val it : thm = |- SUC (0 + SUC (SUC 0 + 0)) = SUC (SUC (SUC 0))
# GEN_REWRITE_CONV(PAT_CONV `
x. f(c,x) + g(x,x)`) [ADD_SYM]
`f(1 + 2,3 + 4) + g(5 + 6,7 + 8)`;;
Warning: inventing type variables
val it : thm =
|- f (1 + 2,3 + 4) + g (5 + 6,7 + 8) = f (1 + 2,4 + 3) + g (6 + 5,8 + 7)
最も一般的な走査戦略はTOP_DEPTH_CONVであり、これはPURE_REWRITE_CONVにハードコードされています。これは基本的にGEN_REWRITE_CONV TOP_DEPTH_CONVと同じです。最も短い名前の書き換え変換子REWRITE_CONVは、PURE_REWRITE_CONVと同じ基本的な戦略を持っていますが、標準的な書き換えルールのスイートが、それに渡されたリストに加えて常に書き換えに含まれている点が異なります。これらをリストとして取得するには、次のようにします。
# basic_rewrites();;
以前に、加算の結合性を使用して項を左結合および右結合バリアントに強制するために繰り返し書き換える例を挙げました。乗算（⊢ x + y = y + x）の可換性による書き換えを試みると、より問題が発生します。任意の項s + tを与えると、x + yをそれに一致させてt + sに書き換えることができます。しかし、その後、それを再び書き換えてs + tに戻すことも同様にできます。このプロセスは無限に継続でき、2つの項を前後にフリップします。しかし、HOLは多くの場合、このような状況でループを回避します（ただし、ループする組み合わせを考案するのはそれほど難しくありません）。最も平凡には、LHSがRHS内に正確に含まれる書き換え（例：⊢ x = x + 0）は単に無視されます。置換書き換えの場合、LHSがRHSと一致可能であり、その逆も同様である場合（可換性の主張のように）、HOLはもう少し巧妙なことを行います。書き換えを適用しますが、インスタンス化されたバージョンが、実質的に任意の一意な構文順序に従って、LHSがRHSよりも大きい場合にのみ適用されます。18 可換性のケースでは、任意の加算s + tおよびt + sは、実質的に任意ですが、1つの固定された向きに正規化されます。
# REWRITE_CONV[ADD_SYM] `(a + b) + (b + a) + (c + d) + (b + a) + (d + c)`;;
val it : thm =
|- (a + b) + (b + a) + (c + d) + (b + a) + d + c =
(a + b) + (a + b) + (c + d) + (a + b) + c + d
実際、HOLの構文順序は、次の定理のスイートで書き換えると、加算の和が完全に標準的な形式に書き換わるように定義されています。
# ADD_AC;;
val it : thm =
|- m + n = n + m /
(m + n) + p = m + n + p /
m + n + p = n + m + p
# REWRITE_CONV[ADD_AC] `(a + b) + (b + a) + (c + d) + (b + a) + d + c`;;
val it : thm =
|- (a + b) + (b + a) + (c + d) + (b + a) + d + c =
a + a + a + b + b + b + c + c + d + d
特に、これは組み込みの反射性書き換えと組み合わせることで、結合的および可換な法則の下での同値性の証明のタスクを処理します。
# REWRITE_CONV[ADD_AC]
`(a + b) + (b + a) + (c + d) + (b + a) + d + c =
c + a + d + b + b + c + a + a + b + d`;;
val it : thm =
|- (a + b) + (b + a) + (c + d) + (b + a) + d + c =
c + a + d + b + b + c + a + a + b + d <=>
true
加算と乗算を使用した代数式の正規化のより洗練された例として、ここではまず分配法則を使用して項を「展開」し、次に積を正規化し、最後に和を正規化して、完全な「積の和」（SOP）形式を取得します。すべてのステップを接続するためにTHENCを使用します。これらのステップすべてを単一の書き換えに投げ込むことも可能ですが、ルールの間の相互作用が冗長なステップを引き起こす可能性があるため、遅くなる可能性があります。例えば、加算に関して正規化された和s + tでは、sとt内の変更により順序が変更され、t + sへのスワップが必要になる場合があります。
# let SOP_CONV =
REWRITE_CONV[LEFT_ADD_DISTRIB; RIGHT_ADD_DISTRIB] THENC
REWRITE_CONV[MULT_AC] THENC
REWRITE_CONV[ADD_AC];;
val SOP_CONV : term -> thm = <fun>
# SOP_CONV `(a + b) * (c + d) + (a + c) * (b + d)`;;
val it : thm =
|- (a + b) * (c + d) + (a + c) * (b + d) =
a * b + a * c + a * d + a * d + b * c + b * c + b * d + c * d
同様の「AC」定理は、多くの結合的および可換な演算子に対して証明されています。例えば、整数加算用のINT_ADD_ACと実数乗算用のREAL_MUL_ACがあります。一部の演算子「⊗」は冪等でもあり、x ⊗ x = xを意味します。この場合、対応するより強力なスイートがあり、その名前は_ACIで終わります。例えば。
# CONJ_ACI;;
val it : thm =
|- (p /
q <=> q /
p) /
((p /
q) /
r <=> p /
q /
r) /
(p /
q /
r <=> q /
p /
r) /
(p /
p <=> p) /
(p /
p /
q <=> p /
q)
これは次のように使用されるかもしれません。
# REWRITE_CONV[CONJ_ACI] `x < 2 /
y < 3 /
x < 2 /
z < 4 /
y < 3`;;
val it : thm =
|- x < 2 /
y < 3 /
x < 2 /
z < 4 /
y < 3 <=> x < 2 /
y < 3 /
z < 4
順序付き書き換えを使用して代数式を正規化するより興味深い例については、「4平方」と「8平方」の恒等式をExamples/lagrange_lemma.mlで参照してください。
7.5 定理の検索
書き換え変換子を効果的に使用するには、適用する適切な定理を見つけることが重要です。HOL Lightは、構文パターンを受け取り、結論にパターンのインスタンスであるサブ項を持つ定理を返す検索機能を提供します。例えば、CONJ_ACIを見つけるには、「search [a /
a <=> a]」を使用できます。
# search [`a /
a <=> a`];;
val it : (string * thm) list =
[("AND_CLAUSES",
|- forall t.
(true /
t <=> t) /
(t /
true <=> t) /
(false /
t <=> false) /
(t /
false <=> false) /
(t /
t <=> t));
("CONJ_ACI",
|- (p /
q <=> q /
p) /
((p /
q) /
r <=> p /
q /
r) /
(p /
q /
r <=> q /
p /
r) /
(p /
p <=> p) /
(p /
p /
q <=> p /
q))]
検索関数に複数のパターンが渡された場合、結果の定理はすべてのパターンを満たす必要があります。
searchは、omit、exactly、nameの構文関数から作成された特別な項を取ることができます。「omit pat」は、パターンpatを満たさない定理を検索します。「exactly t ``」は、項tとアルファ等価な定理を検索します。「name "str"」は、名前がstrを部分文字列として含む定理を検索します。「help "search"`」を実行すると、さらに例が表示されます。
# search [name "AC"; `(+):num->num->num`];;
val it : (string * thm) list =
[("ADD_AC",
|- m + n = n + m /
(m + n) + p = m + n + p /
m + n + p = n + m + p)]
8 タクティクスとタクティカル
原理的には、CONJやMPのような基本的な前方推論規則を組み合わせて、HOLで定理を証明できます。これは可能ですが、中間結果を常にML識別子にバインドするのは少し面倒です。さらに、逆方向で作業し、目標をより単純な「サブ目標」に分解して、それらが自明になるまで分解する方が概念的に自然な場合があります。HOLは、前方および後方証明を混合するための非常に一般的なメカニズムを、ゴールタクティクスに基づいてサポートしています。また、対話的に証明を作成し、少しずつ試すためのいくつかの単純だが便利な関数も提供しています。
最初の重要な概念はゴールです。大まかに言うと、これは証明したい事実です。しかし、それは単なる項以上のものです。それは、仮定できるさまざまな仮説とともに、項です。HOLは、元のゴールを解決するために証明する必要があるゴールの「ゴールスタック」を提供します。
A tactic takes a goal and reduces it to a list of subgoals. But it also keeps track of how to construct a proof of the main goal if the user succeeds in proving the subgoal; this is simply an ML function. So the user can keep applying tactics, and the forward proof is reconstructed by HOL. It’s rather as if the machine automatically reverses the user’s proof and converts it to the standard primitive inferences. The user can perform the proof via a mixture of forward and backward steps, as desired.
8.1 ゴールスタック
ゴールスタックを使用して対話的に証明を発見できます。これにより、タクティックステップを実行し、必要に応じて元に戻して修正できます。ユーザーはgを使用して初期ゴールを設定します。例えば。
# g `2 <= n /
n <= 2 ==> f(2,2) + n < f(n,n) + 7`;;
Warning: Free variables in goal: f, n
val it : goalstack = 1 subgoal (1 total)
`2 <= n /
n <= 2 ==> f (2,2) + n < f (n,n) + 7`
そして、e（「展開」）関数を介してタクティクスを使用してサブゴールに還元します。1つの単純なタクティックはDISCH_TACであり、これは含意ゴールの先行詞を仮説のリストに入れます。これで、p ∧ q ⇒ pを証明するのではなく、p ∧ qを仮定した状態でのpという微妙に異なるゴールを証明する必要があります。
# e DISCH_TAC;;
val it : goalstack = 1 subgoal (1 total)
0 [`2 <= n /
n <= 2`]
`f (2,2) + n < f (n,n) + 7`
気が変わったり、間違いに気づいたりした場合は、「b()」（「バックアップ」）でステップを「元に戻す」ことができ、以前のゴールスタックを復元できます。
# b();;
val it : goalstack = 1 subgoal (1 total)
`2 <= n /
n <= 2 ==> f (2,2) + n < f (n,n) + 7`
タクティックの内部で何が起こるかをよりよく理解するため、また命名規則を理解するためには、類似の推論規則DISCHを検討する価値があります。これは、Γ ⊢ qの形式の定理を受け取り、Γ −{p}⊢ p ⇒ qを生成します（ここでpは通常Γにありますが、必須ではありません）。DISCH_TACが推論規則DISCHの自然なパートナーと見なされる理由を理解することが重要です。それらが逆の変換を行うように見えても、名前はそうです。
推論規則を定理thに適用して別の定理th'を取得する場合、th'がthから従うことを示します。一方、タクティックを適用してゴールgからサブゴールg'に移動する場合、対応する主張はgがg'から従うことですが、必ずしも逆ではありません。つまり、タクティックの適用から生じるサブゴールの真理は、最初のゴールが成り立つには十分ですが、必要ではない場合があります。例えば、非常に大きな式EとE'のE + E' = E' + Eというゴールを、より強いがより単純なゴール∀ xy.x + y = y + xに還元することがあります。もちろん、証明可能なゴールを証明不可能なゴールに還元しないように注意する必要があります。
CONV_TACを変換に適用することで、タクティックを取得する非常に便利な方法があります。これは、対応する変換をゴールの結論に適用するタクティックを生成します。これは特に魅力的な機能を持っており、元のゴールとサブゴールが同等であることがわかっているため、証明可能なゴールを証明不可能なものに置き換えることは決してありません。例えば。
# CONV_TAC;;
val it : conv -> tactic = <fun>
# CONV_TAC(REWRITE_CONV[LE_ANTISYM]);;
val it : tactic = <fun>
# e it;;
val it : goalstack = 1 subgoal (1 total)
`2 = n ==> f (2,2) + n < f (n,n) + 7`
書き換えは非常に一般的な要件であるため、REWRITE_TACというタクティックがあります。これはCONV_TAC o REWRITE_CONVとして定義されています。また、より強力なSIMP_TACもあり、文脈情報を活用します。例えば、ここで適用すると、後件を書き換えるために先行詞2 = nを使用します。
# e(SIMP_TAC[]);;
val it : goalstack = 1 subgoal (1 total)
`2 = n ==> f (n,n) + n < f (n,n) + 7`
同様に、ONCE_REWRITE_TACはONCE_REWRITE_CONVを適用します。
# e(ONCE_REWRITE_TAC[EQ_SYM_EQ]);;
val it : goalstack = 1 subgoal (1 total)
`n = 2 ==> f (n,n) + n < f (n,n) + 7`
すべての書き換えタクティクスには、ASM_で始まるバリアントがあり、これらはすべての仮説も書き換えに使用します。例えば、ここでSIMP_TACを使用する代わりに、次のようにできます。
# e DISCH_TAC;;
val it : goalstack = 1 subgoal (1 total)
0 [`n = 2`]
`f (n,n) + n < f (n,n) + 7`
# e(ASM_REWRITE_TAC[]);;
val it : goalstack = 1 subgoal (1 total)
0 [`n = 2`]
`f (2,2) + 2 < f (2,2) + 7`
ゴールが単にtrueに還元されると、HOLはそれを解決済みと見なします。例えば、ここでARITH_RULEを使用できます。EQT_INTRO o ARITH_RULEが必要だと感じるかもしれません。なぜなら、⊢ p = trueではなく⊢ pになるからです。なぜなら、後者だけが適切な変換の動作だからです。しかし、CONV_TACはそのようなニュアンスなしでゴールの解決を受け入れるように設定されています。（実際、ARITH_TACはこのように定義されていますが、変換または証明手順をCONV_TACでタクティックに常に変換できることに注意する価値があります。
# e(CONV_TAC ARITH_RULE);;
val it : goalstack = No subgoals
したがって、完了しました。証明すべきサブゴールはもうありません。そして、述べたように、残りのサブゴールの証明から（この場合はなし）、HOLは原始推論を適用することによって元のゴールの証明を再構築できます。すべてのサブゴールが証明された後、最終的な定理を取得するにはtop_thm()を使用します。その後、通常の通り定理を名前にバインドできます。
# let trivial = top_thm();;
val trivial : thm = |- 2 <= n /
n <= 2 ==> f (2,2) + n < f (n,n) + 7
したがって、証明の対話的な構築はここまでです。次に、ファイルをファイルに保存して後で再生したい場合、ステップのシーケンスを忠実に書き写すだけです。
g `2 <= n /
n <= 2 ==> f(2,2) + n < f(n,n) + 7`;;
e DISCH_TAC;;
b();;
e(CONV_TAC(REWRITE_CONV[LE_ANTISYM]));;
e(SIMP_TAC[]);;
e(ONCE_REWRITE_TAC[EQ_SYM_EQ]);;
e DISCH_TAC;;
e(ASM_REWRITE_TAC[]);;
e(CONV_TAC ARITH_RULE);;
let trivial = top_thm();;
最初のステップは間違いで、b()はその修正だったので、それらを削除するかもしれません（連鎖の交換も削除するかもしれませんが、ここでは何らかの理由でそれを望んでいたと仮定しましょう）。そして次のようになります。
g `2 <= n /
n <= 2 ==> f(2,2) + n < f(n,n) + 7`;;
e(CONV_TAC(REWRITE_CONV[LE_ANTISYM]));;
e(SIMP_TAC[]);;
e(ONCE_REWRITE_TAC[EQ_SYM_EQ]);;
e DISCH_TAC;;
e(ASM_REWRITE_TAC[]);;
e(CONV_TAC ARITH_RULE);;
let trivial = top_thm();;
代わりに、ステップを次々と実行するのではなく、THENを使用してタクティクスを接続できます。この関数はタクティカルと呼ばれます：tac1 THEN tac2はゴールにタクティックtac1を適用し、次に結果のすべてのサブゴールにtac2を適用します。（この場合、サブゴールは1つだけでした。）したがって、次も機能します。
g `2 <= n /
n <= 2 ==> f(2,2) + n < f(n,n) + 7`;;
e(CONV_TAC(REWRITE_CONV[LE_ANTISYM]) THEN
SIMP_TAC[] THEN ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN
DISCH_TAC THEN ASM_REWRITE_TAC[] THEN CONV_TAC ARITH_RULE);;
let trivial = top_thm();;
さらに、対話的に証明を生成していない場合、ゴールスタックを設定してタクティクスを適用する必要はありません。prove(tm,tac)関数を使用して、ゴールtmをタクティックtacで証明できます。実際、HOLで証明を開発するときは、通常、この種のタクティクススクリプトをエディタで明示的に作成し、進捗を確認するために部分をゴールスタックにコピーして、正しい軌道に乗っていることを確認します。
# let trivial = prove
(`2 <= n /
n <= 2 ==> f(2,2) + n < f(n,n) + 7`,
CONV_TAC(REWRITE_CONV[LE_ANTISYM]) THEN
SIMP_TAC[] THEN ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN
DISCH_TAC THEN ASM_REWRITE_TAC[] THEN CONV_TAC ARITH_RULE);;
書き換えタクティクスのASM_バリアントはすべて、すべての仮説を使用して書き換えることも言及しました。同様に、MESON_TACはMESONのタクティックバージョンであり、ASM_MESON_TACはすべての仮説を使用するバリアントです。しかし、仮説をより繊細に使用することについてはどうでしょうか？ここで、いくつかの他のタクティクスとともに、これを例示するために別のゴールを設定しましょう。
# g `!x y:real. &0 < x * y ==> (&0 < x <=> &0 < y)`;;
GEN_TACタクティックは普遍量化子を剥がし、REPEATタクティカルはそれを可能な限り何度も適用します。
# e(REPEAT GEN_TAC);;
val it : goalstack = 1 subgoal (1 total)
`&0 < x * y ==> (&0 < x <=> &0 < y)`
STRIP_TACタクティックは、ゴールの最も外側の接続詞に応じて、GEN_TAC（外側の普遍量化子を削除）、CONJ_TAC（連言を2つのゴールに分割）、またはDISCH_TACの展開バージョン（STRIP_ASSUME_TACを使用して分解した後、含意の先行詞をゴールの仮説に変換）の効果があります。
# e STRIP_TAC;;
val it : goalstack = 1 subgoal (1 total)
0 [`&0 < x * y`]
`&0 < x <=> &0 < y`
一方、EQ_TACは、if-and-only-ifゴールを2つの含意に分割します。
# e EQ_TAC;;
val it : goalstack = 2 subgoals (2 total)
0 [`&0 < x * y`]
`&0 < y ==> &0 < x`
0 [`&0 < x * y`]
`&0 < x ==> &0 < y`
仮説は実際には定理であることを忘れないでください。既存の定理があれば、ASSUME_TACを使用して仮説に追加できます。
# e(ASSUME_TAC(SPECL [`x:real`; `--y`] REAL_LE_MUL));;
val it : goalstack = 1 subgoal (2 total)
0 [`&0 < x * y`]
1 [`&0 <= x /
&0 <= --y ==> &0 <= x * --y`]
`&0 < x ==> &0 < y`
逆に、仮説を明示的に使用して、いつでも1つを使用できます。タクティックメカニズムは、これが機能することを自動的に確認します。
# e(ASSUME_TAC(ONCE_REWRITE_RULE[GSYM REAL_NOT_LE] (ASSUME `&0 < x * y`)));;
val it : goalstack = 1 subgoal (2 total)
0 [`&0 < x * y`]
1 [`&0 <= x /
&0 <= --y ==> &0 <= x * --y`]
2 [`~(x * y <= &0)`]
`&0 < x ==> &0 < y`
しかし、当然のことながら、存在しないものを仮定することはできません。
# e(REWRITE_TAC[ASSUME `&0 < x <=> ~(x <= &0)`]);;
Exception: Failure "VALID: Invalid tactic".
ASSUME_TACは定理タクティックの例です。これは定理を受け取り、タクティックを生成するために使用します。ASSUME_TACはそれを仮説に置きますが、MP_TACはそれを結論の先行詞として追加します。
# e(MP_TAC(ASSUME `~(x * y <= &0)`));;
val it : goalstack = 1 subgoal (2 total)
0 [`&0 < x * y`]
1 [`&0 <= x /
&0 <= --y ==> &0 <= x * --y`]
2 [`~(x * y <= &0)`]
`~(x * y <= &0) ==> &0 < x ==> &0 < y`
一方、DISJ_CASES_TACはケース分割を実行し、結果の仮説を追加します。
# e(DISJ_CASES_TAC(REAL_ARITH `&0 < y
/ &0 <= --y`));;
val it : goalstack = 2 subgoals (3 total)
0 [`&0 < x * y`]
1 [`&0 <= x /
&0 <= --y ==> &0 <= x * --y`]
2 [`~(x * y <= &0)`]
3 [`&0 <= --y`]
`~(x * y <= &0) ==> &0 < x ==> &0 < y`
0 [`&0 < x * y`]
1 [`&0 <= x /
&0 <= --y ==> &0 <= x * --y`]
2 [`~(x * y <= &0)`]
3 [`&0 < y`]
`~(x * y <= &0) ==> &0 < x ==> &0 < y`
これらのサブゴールの1つは自明です。
# e(ASM_REWRITE_TAC[]);;
val it : goalstack = 1 subgoal (2 total)
0 [`&0 < x * y`]
1 [`&0 <= x /
&0 <= --y ==> &0 <= x * --y`]
2 [`~(x * y <= &0)`]
3 [`&0 <= --y`]
`~(x * y <= &0) ==> &0 < x ==> &0 < y`
どちらにしても、このゴールを終わらせましょう。
# e(FIRST_X_ASSUM MP_TAC THEN MP_TAC(SPECL [`--x`; `y:real`] REAL_LE_MUL) THEN
REAL_ARITH_TAC);;
val it : goalstack = No subgoals
そして、実際、この証明全体を次のように行うことができました。十分な非線形部分に関する補題を提供するだけで十分です。
# let trivial = prove
(`!x y:real. &0 < x * y ==> (&0 < x <=> &0 < y)`,
REPEAT GEN_TAC THEN MP_TAC(SPECL [`--x`; `y:real`] REAL_LE_MUL) THEN
MP_TAC(SPECL [`x:real`; `--y`] REAL_LE_MUL) THEN REAL_ARITH_TAC);;
注釈は、ゴールがxとyの間で実際に対称的であることについてです。そのような状況では、次の補題のようなものを使用してケースの数を減らすことができます。
# REAL_WLOG_LE;;
val it : thm =
|- (forall x y. P x y <=> P y x) /
(forall x y. x <= y ==> P x y)
==> (forall x y. P x y)