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 cannot instantiate all unknown variables, we need to manually determine variables in the lemma by using
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.
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
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.
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
destruct on compound expression, we need to retain the equality by adding the