今日のCoq
4章まで出て来たタクティーク一覧
- intros: 仮定や変数をゴールからコンテキストに移す
- reflexivity: 証明を完了させる（ゴールがe = eという形になっている場合）
- apply... （in H）: 仮定、補助定理、コンストラクタを使ってゴールを証明する
- apply... with...: パターンマッチだけで決定できなかった変数を、特定の値に明示的に結びつける
- simpl (in H): ゴール、もしくは仮定Hの式を簡約する
- compute (in H): ゴール、もしくは仮定Hの式をやや強力に簡約する
- rewrite ... （in H）: 等式の形をした仮定（もしくは定理）を使い、ゴールや仮定を書き換える
- unfold... (in H): 定義された定数を、ゴールや仮定の右側の式で置き換える
- destruct... as...: 帰納的に定義された型の値について、ケースごとに解析する
- induction... as...: 機能的に定義された型の値に帰納法を適用する
- inversion: コンストラクタの単射性と独立性を利用して証明を行う
- remember (e) as x: destruct xとすることで式を失わないようにするため、式(e)に名前(x)を与える
- assert (e) as H: 定義した補助定理(e)をHという名前でコンテキストに導入する
- generalize dependent... コンテキストに移した仮定や変数を元に戻す。
