Tactics

This is a very useful chapter about tactics in Coq. Now it is less tedious, and we can proceed towards doing more complex proofs.

We have learned new tactics.

• 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: simplify computations in a hypothesis
• rewrite: use an equality hypothesis (or lemma) to rewrite the goal
• rewrite ... in H: use an equality hypothesis (or lemma) to rewrite 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: replace a defined constant by its right-hand side in the goal 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
• 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

31/36. Skipped one and stuck on split_combine.

N/A

I liked this chapter. It was slightly more challenging because of the expanded move-set but still easy. A bit more creativity is needed now. I quickly solved them, except that one problem combine_split. I was sick recently and so I finished this slightly late. We are also talking about a new project: formalization of metatheory. I will steer the independent study towards that direction as well.

(Excerpted from Coq documentation.) L_tac is the tactic language of Coq. L_tac2 is a modernization of L_tac. It aims for a more predictable semantics and more expressivity by including a type system and standard datatypes. It is a member of the ML family of languages. L_tac2 is naturally effectfu, since it changes the state of the proof engine. Proof manipulation lives in a monad. L_tac2 has notations - providing a way to extend the syntax of L_tac2 tactics.