By introducing a variable you are saying for a “particular” instance of that variable. Not for all such instances of the variable.
Thus, when introducing more than necessary prior to induction you may unintentionally weaken the induction hypothesis that you will get, making it impossible to prove your goal.
destruct a compound expression you lose what the original equation was. For instance:
destruct (beq_nat 3 n).
will give you two subgoals. One where
(beq_nat 3 n) is replaced with
true, and one where it is replaced with
Sometimes, however, you actually need the fact that
(beq_nat 3 n)
= true in that branch of the proof, or that
(beq_nat 3 n) =
false in the other branch of the proof. You can keep this information with:
destruct (beq_nat 3 n) eqn:Hbeq3.
Which will introduce in the context a hypothesis
Hbeq3 which will be
beq_nat 3 n = true in the
true branch of the proof, and
beq_nat 3 n = false in the false branch.
Introduces variables and hypothesis. This takes them out of the goal and puts them in the context.
Does reflexivity. If a goal has
x = y it will try to simplify (by normalization) both
y. If their normal forms are syntactically identical, then this tactic will succeed and the goal will be completed.
1 + 1 = 2
Reflexivity will solve this because
1 + 1 will evaluate to
2 = 2 is obviously true because each side of the equality is syntactically identical.
Attempts to simplify the goal. This essentially just evaluates to weak head normal form. Useful for seeing next steps in a proof (hard to unwind definitions in your head sometimes), and it can be used to facilitate rewrites.
1 + 1 = 2
simpl will transform this to
2 = 2.
When we have
x = y it can be used to replace
y in a goal, or vice versa.
H : x = y ========= x = y
rewrite H will leave us with the goal
y = y, and
rewrite <- H will leave us with
x = x.
Used to solve a goal by applying a theorem which has an identical conclusion to the current goal. Any hypothesis of the theorem will be added to the context.
This tactic can also be used on hypothesis in the context which then matches on the hypothesis of the theorem being applied and gives you a hypothesis in the context matching the goal of the theorem being applied.
H : x = y ========= x = y
apply H will solve the goal.
H : x = y -> y = z H0 : x = y ================== y = z
You could solve this in two ways with
apply Hwill use the theorem
Hto show that
y = zif
x = y, so it leaves you with
x = yin your goal. This can then be solved by applying
apply H in H0will use
H : x = y -> y = zto transform
H0 : x = yto
y = z. After this we can apply
H0to our goal.
Reverses an equality. Using
symmetry will flip
x = y to
y = x.
This is useful for when you need to
apply a theorem, but the goal is in a different order than the theorem.
destruct tactic is used to perform case analysis in Coq. It will break a possible value into all cases for that type (one for each constructor of the type). This gives you multiple goals to prove; one for each constructor.
This can be used on variables, or compound expressions.
When using destruct on a compound expression it is also possible to save the original expression.
destruct (f (x + y)) eqn:Hfxy
induction tactic is very similar to
destruct, except that it brings an induction hypothesis into the context for recursive data types.
inversion provides reasoning with constructors taking into account the fact that constructors are injective and disjoint.
A x = A ymeans that
x = yas well.
B, then you know that
Adoes not equal
Thus the inversion tactic has several uses.
H : A x = A y ============= x = y
inversion in H this gives us a new hypothesis,
H : A x = A y H1 : x = y ============= y = y
It will also perform rewrites with the new hypothesis automatically, so our goal changed to
y = y as well, since it rewrote
y using the new hypothesis
Inversion will apply this injective reasoning across multiple arguments in a constructor, and even recursively. So, if you have lists of three items that are equal you will get a hypothesis representing the equality of each item in the first list, with the equivalent item in the second list.
We can name the equations as well.
inversion in H as [Hxy] will give:
H : A x = A y Hxy : x = y ============= y = y
If we have values constructed with two different constructors
B, then we know that the values must be different. So if we have a hypothesis in the context with disjoint constructors, like so:
H: A x = B y ============ false = true
We can use
inversion H which will conclude that
H is a false hypothesis, and since we have a contradiction in our set of assumptions we may conclude the goal via the principle of explosion.
generalize dependent tactic can be used to place a variable in the context back into the goal. This can be useful when you only want to introduce certain variables, like when you want to keep your induction hypothesis strong.
This tactic is used to expand a definition.
Definition square n := n * n
square (n * m) = square n * square m
unfold square will yield
(n * m) * (n * m) = (n * n) * (m * m)
which will actually display as
n * m * (n * m) = n * n * (m * m)
due to the associativity of the operators.
This tactic will introduce a hypothesis into the context, and then split the goal into two subgoals. The first subgoal is to prove that this hypothesis is true, and the second subgoal is the original goal.