The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

Types can be considered as theorems.

Members(inhabitants) of types can be considered as proofs of those types.

Consider the following theorem.

\forall n:nat, \exists m:nat m such that m= n+1

With dependent types, this theorem can be expressed by the following type:

(n:nat) -> ( (m : nat) * ( m=n+1) )

Here * denotes dependent product. The type of rhs depends on the member of lhs type.

Members of dependent products are pairs.

The following function is a legitimate member of the above type and hence can be considered

as a proof of the corresponding theorem.

\lambda n. (n+1, eq_refl)

-- Abhishek

http://www.cs.cornell.edu/~aa755/

On Sun, Dec 1, 2013 at 1:25 PM, David MENTRÉ <dmentre AT linux-france.org> wrote:

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