こんなとき使おう | タクティック名 | 使った後 |
---|---|---|
|
intro x. (複数の場合は intros )
|
|
|
intro H. (複数の場合は intros )
|
|
|
apply H.
|
|
こんなとき使おう | タクティック名 | 使った後 |
---|---|---|
|
reflexivity.
|
|
|
rewrite 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.
証明を終えて、もとのモードに戻る