7. タクティクによる証明（Tactic Proofs）🔗

タクティク言語は証明を構築するための特別な目的のプログラミング言語です。Lean では、 命題 は型によって表現され、証明はこれらの型に住んでいる項です。 命題については 命題の節 で詳しく説明しています 項が型の特定の住人を示すのに便利なように設計されているのに対して、タクティクは型に住人がいることを示すのに便利なように設計されています。この区別が存在するのは、定義では関心のある対象を正確に選び出してプログラムが意図した結果を返すことが重要ですが、証明の irrelevance によってある証明を別の証明の中から選りすぐる 技術的な 理由は無いからです。例えば、ある型の2つの仮定が与えられた時、プログラムは正しい方を使うように注意深く書かなければならない一方で、証明はどちらを使っても構いません。

タクティクは 証明状態 （proof state）を修正する命令型プログラムです。証明状態は ゴール （goal）の順序付けられた列から構成されます。これは住人がいるべき型と一緒になった局所的な仮定のコンテキストです；タクティクはさらなるゴール（ サブゴール 、subgoal と呼ばれます）の空である可能性のある列によって 成功 するか、処理が進まない場合は 失敗 します。タクティクがサブゴールが無い状態で成功すれば証明は完了です。1つ以上のサブゴールで成功した場合、それらのサブゴールが証明された時にそのゴールが証明されます。証明状態における最初のゴールを メインゴール （main goal）と呼びます。 ほとんどのタクティクはメインゴールだけに影響しますが、 <;> や all_goals などの演算子は、タクティクを多くのゴールに適用するために使用することができ、ブレット・ next ・ case などの演算子は後続のタクティクの焦点を証明状態の単一のゴールだけに絞ることができます。

裏では、タクティクは 証明項 を構築します。証明項とは、Lean の型理論で書かれた定理の真理について独立にチェック可能な根拠です。各証明は カーネル でチェックされ、独立に実装された外部チェッカで検証できるため、タクティクのバグによる最悪の結果は間違った照明ではなく混乱したエラーメッセージです。タクティク証明の各ゴールは証明項の不完全な部分に対応します。

  1. 7.1. タクティクの実行（Running Tactics）
  2. 7.2. 証明状態の読み方（Reading Proof States）
    1. 7.2.1. 証明と大きな項の非表示（Hiding Proofs and Large Terms）
    2. 7.2.2. メタ変数（Metavariables）
  3. 7.3. タクティク言語（The Tactic Language）
    1. 7.3.1. 制御構造（Control Structures）
      1. 7.3.1.1. 成功と失敗（Success and Failure）
      2. 7.3.1.2. 分岐（Branching）
      3. 7.3.1.3. ゴールの選択（Goal Selection）
        1. 7.3.1.3.1. 順序実行（Sequencing）
        2. 7.3.1.3.2. 複数のゴールに作用する（Working on Multiple Goals）
      4. 7.3.1.4. 焦点をあてる（Focusing）
      5. 7.3.1.5. 繰り返しと反復（Repetition and Iteration）
    2. 7.3.2. 名前と健全性（Names and Hygiene）
      1. 7.3.2.1. 仮定へのアクセス（Accessing Assumptions）
    3. 7.3.3. 仮定の管理（Assumption Management）
    4. 7.3.4. ローカル定義と証明（Local Definitions and Proofs）
    5. 7.3.5. 設定（Configuration）
    6. 7.3.6. 名前空間とオプション管理（Namespace and Option Management）
      1. 7.3.6.1. 展開のコントロール（Controlling Unfolding）
  4. 7.4. オプション
  5. 7.5. タクティクリファレンス（Tactic Reference）
    1. 7.5.1. 仮定（Assumptions）
    2. 7.5.2. 量化子（Quantifiers）
    3. 7.5.3. 関係（Relations）
      1. 7.5.3.1. 等価性（Equality）
    4. 7.5.4. 補題（Lemmas）
    5. 7.5.5. 偽（Falsehood）
    6. 7.5.6. ゴールの管理（Goal Management）
    7. 7.5.7. キャストの管理（Cast Management）
    8. 7.5.8. 外延性（Extensionality）
    9. 7.5.9. 単純化（Simplification）
    10. 7.5.10. 書き換え（Rewriting）
    11. 7.5.11. 帰納型（Inductive Types）
      1. 7.5.11.1. 帰納法（Introduction）
      2. 7.5.11.2. 除去（Elimination）
    12. 7.5.12. ライブラリ検索（Library Search）
    13. 7.5.13. ケース分析（Case Analysis）
    14. 7.5.14. 決定手続き（Decision Procedures）
      1. 7.5.14.1. SAT ソルバの統合（SAT Solver Integration）
    15. 7.5.15. フロー制御（Control Flow）
    16. 7.5.16. 項エラボレーションのバックエンド（Term Elaboration Backends）
    17. 7.5.17. デバッグ用ユーティリティ（Debugging Utilities）
    18. 7.5.18. その他（Other）
  6. 7.6. conv によるターゲットの書き換え（Targeted Rewriting with conv ）
    1. 7.6.1. 制御構造（Control Structures）
    2. 7.6.2. ゴールの選択（Goal Selection）
    3. 7.6.3. 移動（Navigation）
    4. 7.6.4. ゴールの変更（Changing the Goal）
      1. 7.6.4.1. 簡約（Reduction）
      2. 7.6.4.2. 単純化（Simplification）
      3. 7.6.4.3. 書き換え（Rewriting）
    5. 7.6.5. 入れ子のタクティク（Nested Tactics）
    6. 7.6.6. デバッグ用ユーティリティ（Debugging Utilities）
    7. 7.6.7. その他（Other）
  7. 7.7. カスタムタクティク（Custom Tactics）
    1. 7.7.1. タクティクマクロ（Tactic Macros）
      1. 7.7.1.1. 拡張可能なタクティクマクロ（Extensible Tactic Macros）
    2. 7.7.2. タクティクモナド（The Tactic Monad）
      1. 7.7.2.1. 制御（Control）
      2. 7.7.2.2. 式（Expressions）
      3. 7.7.2.3. ソース位置（Source Locations）
      4. 7.7.2.4. ゴール（Goals）
      5. 7.7.2.5. 項エラボレーション（Term Elaboration）
      6. 7.7.2.6. 低レベル操作（Low-Level Operations）
        1. 7.7.2.6.1. モナドクラスの実装（Monad Class Implementations）
        2. 7.7.2.6.2. マクロ展開（Macro Expansion）
        3. 7.7.2.6.3. ケース分析（Case Analysis）
        4. 7.7.2.6.4. 単純化器（Simplifier）
        5. 7.7.2.6.5. 属性（Attributes）