こんなときどうする? タクティッククイックリファレンス

基本タクティクス

こんなとき使おう タクティック名 使った後

   ...
  ============================
   forall x : ほげ, むが

intro x.
(複数の場合はintros)

   x : ほげ
  ============================
   むが
   

   ...
  ============================
   ほげほげ -> むがむが

intro H.
(複数の場合はintros)

   H : ほげほげ
  ============================
   むがむが
   

   H : ほげ1 -> ほげ2 -> ほげ3 -> むがむが
  ============================
   むがむが

apply H.


   ...
  ============================
   ほげ1

subgoal 2 is:
   ほげ2

subgoal 3 is:
   ほげ3

等式を扱うタクティクス

こんなとき使おう タクティック名 使った後

   ...
  ============================
   むがむが = むがむが

reflexivity.

Proof completed.

   ...
   H : ほげ = むが
  ============================
   もぐもぐ

rewrite H.

もぐもぐ の中に含まれている ほげ を
むが に書き換える。

   ...
   H : ほげ = むが
  ============================
   もぐもぐ

rewrite <- H.

もぐもぐ の中に含まれている むが を
ほげ に書き換える。

その他のタクティクス

induction inductiveterm.:数学的帰納法を使う
unfold term (in H).:定義に従って展開する
fold term (in H).:unfoldの逆
simpl term (in H).:計算できるところだけ計算する

証明を扱うコマンド達

Theorem name : predicate.
証明モードへ移行する
(Lemma, Remark, Definition, Goal, Fact, Corollary, Proposition でも同様)

Proof.
証明をこれから始めるべく、気合いを入れる

Abort.
証明をあきらめて、もとのモードに戻る

Undo n.
証明をnステップ前に戻す

Restart.
証明を最初からやり直す

Qed.
証明を終えて、もとのモードに戻る