The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Mon, Nov 7, 2011 at 6:08 PM, Alexandre Pilkiewicz <alexandre.pilkiewicz AT polytechnique.org> wrote:

2011/11/7 Victor Porton <porton AT narod.ru>:
> The problem stays if we use simple Structures.
>
> Record S := {

>  x_record: nat;
>  cond_record: x_record = 0
> }.
>

> This creates a [cond_record] function which is in my opinion is entirely meaningless because it takes an argument of type C and returns True iff it is of type C, that is always return True.

Any member of your type S is a dependent pair of an integer and a
proof that this integer is equal to zero. The keyword "Record",
contrary to the simpler one Inductive, alors automatically defines to
functions, x_record and cond_record that project that pair (you can
think of them as being fst and snd, but for the type S. That is what I
showed in my precedent exemple, but I can show it again:

It might also help to think of cond_record as the result, automatically proved by Coq, that whenever s is an element of type S, then the x value of s is in fact equal to 0.  So, for example, you can apply this using:

Lemma Sx_plus_idem: forall s:S, x_record s + x_record s = x_record s.
Proof.
intros.
rewrite cond_record.
reflexivity.
Qed.

The interpretation Alexandre suggested relies on an understanding of the Howard-Curry correspondence, which underlies the meta-theory of Coq.  It will eventually be very useful to gain this understanding, as it allows you to do many things more concisely.  However, it does take a while to get used to it.
--
Daniel Schepler