Tactics So Far

We’ve reached a point where we’ve got enough tactics to do some real work. Here are tactics that we’ve seen in class as of 2024-20-20:

• 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… as…: 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): introduce a “local lemma” e and call it H

There are many more tactics and we’ve not learned much about automation, but this is a good start.