Here's a list of tactics that should be sufficient to solve the problems in
this assignment. You're free to use any tactics except in sections that give
explicit restrictions, though. In particular, all of that stuff you did
manually in HW1 should be left to automation now, through liberal use of
tactics like |
intuition (described below). Whenever a goal has some
non-trivial propositional structure, starting off with
following a named
arguments) is a sound idea.
More detailed information on tactics can be found in
the manual's tactic index.
Basic goal manipulation:
Transform a goal with implications and/or universal quantifications into a
simpler goal, where the assumptions and quantified variables have moved
into the assumptions above the double line.
intros with no arguments
performs this for all implications and
foralls visible in the goal, while
intros followed by a space-separated list of names performs this
simplification as many times as there are names, using your list to pick the
names of new assumptions instead of assigning them itself. You'll often
want to use the named form of
intros for goals involving negation and
other syntactic abbreviations for implications. (Remember that
P -> False.)
Apply the named lemma/theorem
name to the current goal, adding the
premises of that lemma as subgoals, if there are any premises.
When the goal is some term
e', switch to proving
e' must be equivalent through the computational reductions.
Prove any equality between two equivalent terms.
Rewrite the goal using the equality proved by hypothesis
H. You can also
rewrite H1 in H2 to do the rewriting in
H2, and you can follow
<- to use the equality to rewrite from right to left
instead of left to right.
Try to simplify the goal using computational reduction rules. You may also
simpl in H to simplify hypothesis
simpl in * to simplify the
goal and all hypotheses.
name is a symbol assigned a meaning earlier in a
expand all occurrences of that name in the goal into the definition. The
same alternate syntaxes that work with
simpl apply here, too.
When considering using
unfold, keep in mind that it can sometimes make
the goal/hypothesis more complicated than it was before.
simpl is generally better about avoiding that kind of thing.
Working with inductive types:
Perform a case analysis on the expression
e of inductive type. The goal
is split into one subgoal per constructor of
e's type, with
by a generic application of that constructor to fresh variables. If
the name of a variable bound in the goal rather than a variable bound in the
assumptions above the double line, then
intros is used automatically to
move that variable and those that come before it above the double line.
destruct e, but the subgoals also have additional assumptions
corresponding to inductive hypotheses where appropriate. You may also use
induction on variables quantified in the goal.
Prove any formula, given that your assumptions include an equality between
terms built with different constructors of an inductive type.
H is a hypothesis equating two values built with the same
constructor of an inductive type, add all of the equalities that this
Prove a very obvious goal. The best way to get a handle on what this means
is through experience.
Prove any propositional tautology. Remember that we're working in
constructive logic, so not every formula that can be proved "true" using
truth tables is actually true constructively!
A version of
tauto that lets you take advantage of partial success.
In particular, when it can't prove the goal completely, it will often split
it into a set of simpler subgoals based on properties of the logical
intuition that has a limited ability to automate proofs in
Prove a goal whose truth follows from the definition of equality and basic
properties of inductive type constructors.
Prove any goal that follows from properties of linear arithmetic.
For some of the theorems in this assignment, it will be very useful to use
some of the ways of combining tactics.
- The notation
t1; t2 means "run
t1 on the current goal and then run
on all of the subgoals generated by
- The notation
try t means "try running
t1 on the goal; if it fails,
silently roll back to where we started instead of signaling an error to the
Finally, don't forget these other general theorem proving tools:
- You can introduce a definition with
Definition name := e.
- When you want to define a recursive function, it's easiest to use
- Often a theorem will be easiest to prove if you prove some lemmas first.
These are introduced with
, followed by a proof
Lemma name : formula.
, just as for
. (In fact,
are synonyms, with the choice of which to use serving only as