Logical Foundations.
https://softwarefoundations.cis.upenn.edu/lf-current/index.html
$ coq_makefile -f _CoqProject -o Makefile
$ make
Tactics review:
intros
: move hypotheses/variables from goal to contextreflexivity
: finish the proof (when the goal looks likee=e
)apply
: prove goal using a hypothesis, lemma, or constructorapply... in H
: apply a hypothesis, lemma, or constructor to a hypothesis in the context (forward reasoning)apply... with...
: explicitly specify values for variables that cannot be determined by pattern matchingsimpl
: simplify computations in the goalsimpl in H
: ... or a hypothesisrewrite
: use an equality hypothesis (or lemma) to rewrite the goalrewrite ... in H
: ... or a hypothesissymmetry
: changes a goal of the formt=u
intou=t
symmetry in H
: changes a hypothesis of the formt=u
intou=t
transitivity y
: prove a goalx=z
by proving two new subgoals,x=y
andy=z
unfold
: replace a defined constant by its right-hand side in the goalunfold... in H
: ... or a hypothesisdestruct... as...
: case analysis on values of inductively defined typesdestruct... eqn:...
: specify the name of an equation to be added to the context, recording the result of the case analysisinduction... as...
: induction on values of inductively defined typesinjection... as...
: reason by injectivity on equalities between values of inductively defined typesdiscriminate
: reason by disjointness of constructors on equalities between values of inductively defined typesassert (H: e)
(orassert (e) as H
): introduce a "local lemma" e and call it Hgeneralize dependent x
: move the variablex
(and anything else that depends on it) from the context back to an explicit hypothesis in the goal formulaf_equal
: change a goal of the formf x = f y
intox = y