coq tactics

LF Tactics review

  • intros: move hyp/vars from goat to ctx
  • reflexivity: finish proof when lhs = rhs in goal
  • apply: prove goal using hyp, lemma, constr.
  • simpl: simplify.
  • rewrite: use an equality in Hyp to rewrite the goal.
  • symmetry: swaps lhs and rhs
  • unfold: replace const with its rhs in goal
  • destruct... as...: case analysis. destruct... eqn:... records the result of the case analysis and adds it to the context.
  • induction... as...: induction
  • injection: injectivity on equalities
  • discriminate: reason by disjointness of constructors
  • assert (H: e): introduce a lemma locally
  • generalize dependent x: move x (and all dependencies) from ctx to goal.
  • apply ... in H: forward reasoning by applying to hyp in ctx
  • simpl in H.
  • rewrite ... in H
  • symmetry in H
  • unfold... in H

  • rewrite (plus_comm x y) applies plus_comm with the arguments x, y instantiated.
  • apply some_lema with (x := 42) applies the lemma with x instantiated as 42.

  • When proving correctness of the tail recursive rev. Induct on the first list. You’ll need a lemma that generalizes over the accumulator. When trying to prove that lemma, make sure you quantify over all accumulators (So don’t intro it). This is important to be able to apply the IH.

CUFP 2015

  • intros: Introduce variables into the context, giving them names.
  • simpl: Simplify the goal.
  • reflexivity: Prove that some expression x is equal to itself.
  • destruct: Consider all possible constructors of an inductive data type, generating subgoals that need to be solved separately.
  • rewrite: Replace one side of an equation by the other.
  • apply: Suppose that the current goal is Q. If H : Q, then apply H solves the goal. If H : P -> Q, then apply H replaces Q by P in the goal. If H has multiple hypotheses, H : P1 -> P2 -> ... -> Pn -> Q, then apply H generates one subgoal for each Pi.
  • induction: Argue by induction. It works as destruct, but additionally giving us an inductive hypothesis in the inductive case.
  • discriminate: Looks for an equation between terms starting with different constructors, and solves the current goal.
  • revert: The opposite of intros; removes variables and hypotheses from the context, putting them back in the goal.
  • clear: Remove hypotheses from the context (ex. needed to simplify the IH).
  • unfold: Calling unfold foo expands the definition of foo in the goal.
  • trivial: solves simple goals through reflexivity and by looking for assumptions in the context that apply directly. If it cannot solve the goal, it does nothing.
  • ;: An expression such as foo; bar first calls foo, then calls bar on all generated subgoals. A common idiom is foo; trivial, which solves the trivial subgoals and does nothing on the remaining ones.
  • try: Calling try foo tries to execute foo, doing nothing if foo raises any errors. In particular, if foo is a terminating tactic such as discriminate, try foo attempts to solve the goal, and does nothing if it fails.
  • destruct ... eqn: ...: Do case analysis on an expression while generating an equation.
  • lia: Short for “Linear Integer Arithmetic”; tries to solve goals that involve linear systems of inequalites on integers.
  • specialize: Instantiate a universally quantified hypothesis
  • assert: Introduce a new hypothesis in the context, requiring us to prove that it holds. The curly braces {} allow us to focus on the current subgoal, like + and -.