The Coq mailing list

[Kristopher Micinski <krismicinski AT gmail.com>]

On Sat, Nov 23, 2013 at 10:51 AM, David MENTRÉ 
<dmentre AT linux-france.org>
 wrote:
> Thank you for this example and the explanations.
>
> I can use it through a simple "Eval compute in plus_0_r 2."
>
> If I understood correctly, "plus_0_r n" recursively computes a coq term(?)
> of value "eq_refl n" and of type "n + 0 = n".
>
> "eq_refl" itself takes any element "x" and builds a predicate (aka Prop)
> that "x = x".

That's not quite right.

`eq` is the constructor for the proposition for (intensional) equality.

So the answer is that `eq` builds a predicate that some x equals some
y (when you give instances for x and y).

    Coq < Check eq.
    eq
         : ?3 -> ?3 -> Prop
    Coq < Check eq 1.
    eq 1
         : nat -> Prop
    Coq < Check eq 1 1.
    1 = 1
         : Prop

Now, those build props.  The prop is the theorem, `eq_refl x` builds a
*proof* that proves that x = x.

So `eq` builds the theorem, `eq_refl` builds the proof.

This mirrors something like a datatype:  list X builds a datatype that
represents lists of things of type X.  By contrast cons and nil build
terms of that type.  So list constructs the type, and cons/nil build
terms of that type.

(Using `eq` you are using intensional equality, meaning that the only
things that are "equal" are those things that are (roughly) "the same
thing" as defined by Coq's term equivalences.  Hence sparking
Homotopy, but that's slightly tangential for someone trying to
understand this at a basic level.)

Kris