apply TacticThe 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.
apply with TacticSometimes apply cannot instantiate all unknown variables, we need to manually determine variables in the lemma by using apply with.
injection and discriminate TacticsThe 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.
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.
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.
Coq does definition unfolding automatically, but it is also conservative and we sometimes need to unfold the definitions manually using unfold.
destruct on Compound ExpressionsWhen using destruct on compound expression, we need to retain the equality by adding the eqn: qualifier.