Skip to content

Tactics Reference

Complete & detailed reference: list of tactics

summary

tactic description
intros move hypotheses/variables from goal to context
reflexivity finish the proof (when the goal looks like e = e)
apply prove goal using a hypothesis, lemma, or constructor
apply... in H apply a hypothesis, lemma, or constructor to a hypothesis in the context (forward reasoning)
apply... with... explicitly specify values for variables that cannot be determined by pattern matching
simpl simplify computations in the goal
simpl in H ... or a hypothesis
rewrite use an equality hypothesis (or lemma) to rewrite the goal
rewrite ... in H ... or a hypothesis
symmetry changes a goal of the form t=u into u=t
symmetry in H changes a hypothesis of the form t=u into u=t
transitivity y prove a goal x=z by proving two new subgoals, x=y and y=z
unfold replace a defined constant by its right-hand side in the goal
unfold... in H ... or a hypothesis
destruct... as... case analysis on values of inductively defined types
destruct... eqn specify the name of an equation to be added to the context, recording the result of the case analysis
induction... as... induction on values of inductively defined types
injection reason by injectivity on equalities between values of inductively defined types
discriminate reason by disjointness of constructors on equalities between values of inductively defined types
assert (H e) (or assert (e) as H)
generalize dependent x move the variable x (and anything else that depends on it) from the context back to an explicit hypothesis in the goal formula
f_equal change a goal of the form f x = f y into x = y
exfalso to change the goal to [False]; short of ex_falso_quodlibet

apply

apply term

  • this tactic applies to any goal
  • matches the current goal against the conclusion of the type of term
  • term being applied must match the goal exactly
  • on successful match it returns as many subgoals as the number of non-dependent premises of the type of term
  • on failure to match the goal and the conclusion is an inductive type isomorphic to a tuple type, then each component of the tuple is recursively matched to the goal in the left-to-right order.
1
2
3
4
5
6
7
Theorem apply_example : forall (n m o p : nat),
  n = m ->
  (n = m -> [n,o] = [m,p]) ->
  [n,o] = [m,p].
Proof.
intros n m o p eq1 eq2.
apply eq2. apply eq1. Qed.

apply in

apply X -> Y in H

  • applied to a hypothesis
  • X -> Y is some conditional statement with such form
  • matches H against X and, if successful, replaces it with Y.
1
2
3
4
5
6
7
8
9
Theorem apply_in_example : forall (n : nat),
  (n == 5 = true -> (S (S n)) == 7 = true) ->
  true = (n == 5) ->
  true = ((S (S n)) == 7).
Proof.
  intros n eq H.
  symmetry in H. apply eq in H. symmetry in H.
  apply H.
Qed.

discriminate

discriminate term

  • two terms beginning with different constructors can never be equal
  • discriminate is used on a hypothesis involving an equality between different constructors, and it solves the current goal immediately
1
2
3
4
5
6
7
Theorem nonsense : forall n,
0 == n = true -> n = 0.
Proof.
intros n. destruct n as [| n'] eqn:E.
  - intros H. reflexivity.
  - intros H. discriminate H.
Qed.

injection

injection term

  • constructors of inductive types are injective → if \(c\) is a constructor of an inductive type and \(c\) \(t_1\) and \(c\) \(t_2\) are equal then \(t_1\) and \(t_2\) are equal too.
  • using injection H without as clause turns all equations into hypotheses at the beginning of the goal
1
2
3
4
5
6
Theorem injective_example : forall (n m : nat),
  S n = S m ->  n = m.
Proof.
  intros n m H.
  injection H as Hnm. apply Hnm.
Qed.

simpl in

simpl in term

  • performs simplification on the hypothesis term in the context
1
2
3
4
5
6
7
Theorem simpl_hypothesis : forall (n m : nat) (b : bool),
  (S n) == (S m) = b -> n == m = b.
Proof.
  intros n m b H.
  simpl in H.
  apply H.
Qed.

symmetry

symmetry

  • applies to a goal that has the form t = u and changes it into u = t
1
2
3
4
5
Theorem silly_swap: forall (n m:nat), 1 + n = S (n).
Proof.
    symmetry. (* just to show use *)
    reflexivity.
Qed.

transitivity

transitivity term

  • applies to a goal that has the form t=u and transforms it into the two subgoals t=term and term=u.
1
2
3
4
5
6
7
8
9
Example transativity_example :
forall (a b c d e f : nat),
  [a,b] = [c,d] ->
  [c,d] = [e,f] ->
  [a,b] = [e,f].
Proof.
  intros a b c d e f eq1 eq2.
  transitivity [c,d].
  apply eq1. apply eq2. Qed.

unfold

unfold qualid

  • applies to any goal
  • qualid must denote a defined transparent constant or local definition
  • unfold applies the \(δ\) rule to each occurrence of the constant to which qualid refers in the current goal and then replaces it with its \(βι\)-normal form
 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
Definition square n := n * n.


Theorem unfold_example: forall n m,
  square (n * m) = square n * square m.
Proof.
  intros n m.
  simpl.          (* square (n * m) = square n * square m *)
  unfold square.  (* n * m * (n * m) = n * n * (m * m) *)
  (* rest... *)
Admitted.