The Coq mailing list

[Ömer Sinan Ağacan <omeragacan AT gmail.com>]

Nice write-up, thanks. I also remember having trouble understanding
what exactly is apply tactic doing. I already knew unification from
Prolog and other type systems but "replacing conclusion with premises"
part took some time for me to realize. That part is either not
explained in SF book or I read it badly.

---
Ömer Sinan Ağacan
http://osa1.net


2014-02-16 18:31 GMT+02:00 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