Here are some additional tactics beyond those listed at the start of
HW2 that you may find useful for this assignment.
As before, you are free to use any additional tactics if you like, and the Coq
index may be helpful.
constructor: This proves a goal that is an application of an
inductively-defined predicate if the goal matches the conclusion of one of
the rules used to define the predicate.
constructor won't work if the
candidate rule involves one or more quantified variables whose values can't
be determined just by looking at the form of the goal. To use such rule
apply name with arg1 ... argN: A simpler form of
apply appeared at the
start of HW2. There it was mentioned as a tool for applying lemmas, but it
works just as well with constructors of inductive predicates. Use this long
form of apply when the constructor or lemma that you are applying has some
quantified variables whose instantiations aren't clear from the form of
your goal. The space-separated list of arguments should contain the right
value for each of these variables, in the order that the variables are
quantified in the lemma or constructor definition. The argument list should
not contain entries for variables whose values are implied by the
form of the goal. Alternatively, you can use the form
apply (name arg1 ...
argN), where you treat the lemma or constructor like a function (which it
is!) and specify the arguments to pass to it. You often need to specify
more arguments explicitly with this version, since it can't take advantage
of argument values that are apparent from the goal.
inversion H: Where
H is a hypothesis stating an instance of an
inductively-defined predicate, this tactic considers the ways that instance
may have been derived and adds a subgoal for each case.
differs from simple
induction in an important way: the
latter two ignore the structure of the arguments to the predicate, while
inversion takes them into account by adding new assumptions of equalities
between the formal arguments (i.e., those that appear in the predicate's
definition) and the actual arguments (i.e., those that appear in
After a few inversions, these equality assumptions can come to dominate the
context, and so it's usually a good idea to chain
with a semicolon, so that every equality with a variable on its lefthand or
righthand side is eliminated.
Your main new tools for this assignment are inductively-defined predicates
and proofs by induction over their derivations.