The Coq mailing list

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

Matthieu,

Thanks a *lot* for this pointer.It's exactly what I needed. Really appreciate it.

Best,

Kevin

On Fri, Mar 7, 2014 at 11:54 AM, Matthieu Sozeau <matthieu.sozeau AT gmail.com> wrote:

Hi Kevin,

  it’s a late answer but not too late hopefully :) We’re working with Beta Ziliani
and colleagues on formalizing the unification algorithm used by refine (actually
an improvement thereof), which should become the only one in the future. The one
of apply is very ad-hoc as it distinguishes between two kind of existential
variables and its delta-reduction is restricted in some cases. We hope to have
something readable in the coming months. You can have a look at Claudio
Sacerdoti Coen’s thesis, chapter 10, which is the best reference I know on unification
for CIC and Abel and Pientka’s paper on dynamic pattern unification for some of the tricks
used in Coq (although their system is slightly different). Ziliani’s ICFP paper
with Gonthier also includes some detailed explanations about unification in Coq.

Best,
— Matthieu

On 16 févr. 2014, at 19:49, Ömer Sinan Ağacan <omeragacan AT gmail.com> wrote:

> 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