The Coq mailing list

[Kevin Sullivan <sullivan.kevinj AT gmail.com>]

One of my undergraduate students came to me wanting to know more about what's going on with the apply tactic. Having looked at his thought processes and the Coq materials available to beginners (mainly Benjamin's book) I understand the confusion. The issue is that Coq's unification algorithm isn't summarized in a way (or at all) to make it clear to a novice what it's actually doing or when it applies. So my question is where can I find the best, most accessible write-up on this issue?

The example in SF where this first came up is in Prop.v

Inductive gorgeous : nat -> Prop :=

  g_0 : gorgeous 0

| g_plus3 : forall n, gorgeous n -> gorgeous (3+n)

| g_plus5 : forall n, gorgeous n -> gorgeous (5+n).

(** **** Exercise: 1 star (gorgeous_plus13) *)

Theorem gorgeous_plus13: forall n, 

  gorgeous n -> gorgeous (13+n).

Proof.

The issue in this case is that it wasn't obvious to the student that it was valid to apply g_plus5 (or g_plus3) to the goal, because it "doesn't look like it matches." Indeed it appears that it does match only because some computation is being done on both 13+n and 5+n' to expand them both into (S (S (S ...))), at which point the matching and rewriting of the goal become clear. 

For what it's worth, this is what I told the student. Benjamin, if you're reading this, and it checks, you might consider adding something like this to your book at the designated spot.

==============

Proof. 

intros.

(** 

SULLIVAN. The key observation here is that the goal, [13+n], will 

"match" with the conclusion of either the [g_plus3] "rule" or with

the [g_plus5] rule: i.e., with the term [3+n] (a different n, by 

the way) or with the term [5+n]. Thus applying either the [g_plus3] 

or [g_plus5] rule will rewrite the current goal. Check it out.

*)

apply g_plus5.

(** What does *match* actually mean? The essential concept is 

that of *unification*. Unification is an algorithm that takes

a pattern term (such as the conclusion of a constructor rule)

and a target term (such as the current goal) and that either 

fails to find a "match" or that returns a match in the form of

a list of "matches" between pattern and target sub-terms, such

that the list of substitutions, if applied to the pattern, would

turn it into the target term. 

*)

(**

What the [apply] tactic does is (1) take the conclusion of the 

specified rule as a pattern, (2) try to unify it with the goal, 

and (3) if the unification succeeds, to replace the goal with

the premises of the rule suitably rewritten using the matching

results of the unification.

How did that work in the case that we just saw? Let's try to

line up the goal and the pattern (replacing the "n" variable

in the pattern with a different name, to keep the distinction

clear.)

GOAL:       13 + n

PATTERN:    5 + n'

GOAL:    (S (S (S (S (S (S (S (S (S (S (S (S (S n)))))))))))))

PATTERN: (S (S (S (S (S m)))))

MATCH               m = (S (S (S (S (S (S (S (S n))))))))

PREMISE: gorgeous m

Because unification succeeded, the task of proving the goal is 

thus reduced to the task of proving the premise, as rewritten

using the matching discovered by the unification process. 

*)

Qed.

==============

Kind regards,

Kevin