One of the strong points of Coq is its powerful proof automation facility embodied in the tactic language \(\mathcal{L}_{tac}\). Instead of having to write new tactics in ML, compiling them, and jumping through all sorts of hoops in the process, we can simply write down new tactics as part of a proof development. In this post I will develop a small tactic that solves propositions of the \(\wedge, \vee, \forall, \Rightarrow\) subset of first order predicate logic automatically.

What would we do to proof a goal involving conjunction, disjunction, implication and universal quantifiaction manually using only the built-in tactics? First of all, we'd introduce all quantified variables and premises into the context with the intros tactic. Then we'd repeatedly apply a set of rules according to the current goal and context. This approach can be directly transcribed as an Ltac definition.

Ltac FO := intros; repeat
  match goal with
    | [ H: ?P |- ?P ] => apply H
    | [ H: ?P /\ ?Q |- ?P ] => inversion H as [HP _]; apply HP
    | [ H: ?P /\ ?Q |- ?Q ] => inversion H as [_ HQ]; apply HQ
    | [ |- ?P /\ ?Q ] => split
    | [ H: ?P \/ ?Q |- _ ] => inversion H as [HP | HQ]
    | [ H: ?P |- ?P \/ ?Q ] => left; FO
    | [ H: ?Q |- ?P \/ ?Q ] => right; FO
  end.

The main part is the match goal with ... end pattern matching construct. It performs case analysis on the current state of the proof. Metavariables are prefixed by question marks and the syntax [ C |- G ] gives a pattern C to be matched against the context (the hypotheses from which the goal is to be derived) and on the right hand side of the ASCII turnstyle symbol |- a pattern to be matched against the current goal.

So far this tactic deals with most of the cases we'll encounter in a manual proof, but what if the current goal is P and the context contains an implication with multiple premises A -> B -> ... -> P or the current goal itself is an implication or a universally quantified term? Let us only consider the first case for now. We could write down a series of patterns for implications with one, two, three or more premises like so:

  | [ H : _ -> ?P |- ?P ] => apply H
  | [ H : _ -> _ -> ?P |- ?P ] => apply H
  | [ H : _ -> _ -> _ -> ?P |- ?P ] => apply H

But this is not only tedious but incomplete. What we need is a so-called context pattern which matches a subterm. We then reformulate our rules for implications with multiples premises by factoring out the part they have in common into a context pattern:

  | [ H : context [_ -> ?P] |- ?P ] => apply H

This pattern matches whenever the context contains a hypotheses H that contains a subterm of the form A -> P and the goal is exactly P. We can solve the second case mentioned earlier in much the same way.

  | [ |- context [_ -> _] ] => intros

Now, we have a complete automatic tactic:

Ltac FO := intros; repeat
  match goal with
    | [ H: ?P |- ?P ] => apply H
    | [ H: ?P /\ ?Q |- ?P ] => inversion H as [HP _]; apply HP
    | [ H: ?P /\ ?Q |- ?Q ] => inversion H as [_ HQ]; apply HQ
    | [ |- ?P /\ ?Q ] => split
    | [ H: ?P \/ ?Q |- _ ] => inversion H as [HP | HQ]
    | [ H: ?P |- ?P \/ ?Q ] => left; FO
    | [ H: ?Q |- ?P \/ ?Q ] => right; FO
    | [ |- context [_ -> _] ] => intros
    | [ H : context [_ -> ?P] |- ?P ] => apply H
  end.