CoqCheatSheet

CoqCheatSheet

目次

[][]Coq CheatSheet

@nifty:@homepage:エラーを補完する形で。

前提が

A /\ Bdestruct?, decompose[and], elim
A \/ Bdestruct?, decompose[or],elim
~Pelim
forall x:A, ...specialize
exists x:P, ...decompose[ex],elim
C x y .. = C a b ..injection?
C x y .. = D a b ..discriminate
x = yrewrite
Falsecontradiction,elim

ゴールが

A -> B intro, intros
A /\ Bsplit
A \/ B left, right
~Pintro
forall x:A, ...intro, intros
exits x:P, ...exists
x = xreflexivity
Trueapply I.