- Final Exam
- Imp and IndProp
- Homework Scores
- Homework Grading
- Final Homework Excercises
- Midterm Clarification
- Midterm Exam
- Midterm Exam Info
- Classes Fall 24
- Tactics So Far

Blog

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.