Chapter 5 More Basic Tactics

The apply Tactic

The apply tactic uses implications to transform goals and hypotheses. When apply-ing a lemma to the goal, Coq will match the goal against the conclusion of the lemma, try to instantiate unknown variables, and replace the goal with the premises of the lemma.

The apply with Tactic

Sometimes apply cannot instantiate all unknown variables, we need to manually determine variables in the lemma by using apply with.

The injection and discriminate Tactics

The principle of explosion states that a contradictory hypothesis entails anything, even false things.

All constructors of a data-type are injective. We use injection to “undo” one application of the constructor.

Any two constructors of a data-type are disjoint, and no two terms beginning with different constructors can be equal. Use discriminate on hypotheses involving such inequalities to solve the goal.

Using Tactics on Hypotheses

Most tactics in Coq work on the goal and leave the context unchanged. However, we could perform a tactic on a statement in the context, by using the in qualifier.

The informal proofs tend to use forward reasoning, while the idiomatic use of Coq favors backward reasoning.

Varying the Induction Hypothesis

Be careful which of the universally quantified variables to introduce before starting the induction. It is crucial to leave some variables generic. Hypotheses that are too specific are weak: we may end up with a goal which the induction hypothesis is not generic enough to apply to.

Use generalize dependent to put an argument back to goal.

Unfolding Definitions

Coq does definition unfolding automatically, but it is also conservative and we sometimes need to unfold the definitions manually using unfold.

Using destruct on Compound Expressions

When using destruct on compound expression, we need to retain the equality by adding the eqn: qualifier.