The Coq mailing list

[David MENTRÉ <dmentre AT linux-france.org>]

Hello,

Sorry for my late reply.

2013-11-23 17:11, Kristopher Micinski:
> `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.

OK. Thank you for the explanations.

> 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.

This is clear for my for languages like OCaml. But for Coq, I am still 
have issues linking the types to the corresponding kind of object 
(theorem, proof).

I am correct in saying that if something like "eq" has type that ends in 
"-> Prop", it is a theorem and if it has a "formula" in type like 
"forall (A : Type) (x : A), x = x" for "eq_refl", then it builds a proof?

Best regards,
david