Coqとの対話では、人間が伝えるメッセージを「tactics」と呼びます。tacticsは具体的な「証明の指示」であり、論理式の証明には自動的に選択されます。このセッションでは、論理式の証明に慣れることを目標としています。しかし、数学の証明には「等号を含んだ数式の証明」や「数学的帰納法を使う証明」など、別のtacticsが必要です。それらについては後続のセッションで取り上げます。
Coqを使って数学の証明を行う際、人間は様々なtacticsを指示する必要があります。ただし、証明を完成させることと証明の正しさを検証することは異なる問題です。数学的な推論では、すべての命題の証明が必要ではありません。そのため、誤った証明を作成する可能性があります。
Coqを利用すると、証明の実行だけでなく、証明の正しさも検証することができます。これは数学と証明に関する課題を解決する可能性を秘めています。詳細は「21世紀 数学的証明での「形式的証明」の拡大」などのショートムービーで説明されています。また、「人間はCoqに何を伝えたか？」というショートムービーも公開されています。
Bing AIの説明
Coqにおけるtacticsの使い方について説明します。
tacticsは、証明の構築を支援するために使用されるコマンドです。tacticsは、証明の状態を変更することができます。tacticsは、証明の構築を効率的に行うために使用されます。
以下は、tacticsの一例です。
・intros: 仮定を導入する。
・apply: 定理を適用する。
・destruct: 構造的帰納法を行う。
・simpl: 式を簡約する。
https://maruyama097.blogspot.com/2023/06/coq_13.html
 | カシオ 関数電卓 微分積分・統計計算・数学自然表示 394関数・機能 fx-375ESA-N 新品価格 |
