The Coq mailing list

[Alexandre Pilkiewicz <alexandre.pilkiewicz AT polytechnique.org>]

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:

<<<<<<<
Set Printing All.
Record S := {
 x_record: nat;
 cond_record: x_record = 0
}.

(*let's define the same thing manually *)

Inductive S_manual : Type :=
  | BSM: forall n : nat, n = 0 -> S_manual.

Definition x_manual sm:=
  match sm with
    | BSM n _ => n
  end.

Definition cond_manual sm : (x_manual sm = 0) :=
  match sm as sm' return (x_manual sm' = 0) with
    | BSM _ H => H
  end.

(* Let us see if we find a difference *)

Print S.
(*Inductive S : Type :=
    Build_S : forall x_record : nat, @eq nat x_record O -> S

For Build_S: Argument scopes are [nat_scope _]
*)

Print S_manual.
(* Inductive S_manual : Type :=
    BSM : forall n : nat, @eq nat n O -> S_manual

For BSM: Argument scopes are [nat_scope _]*)


Print x_record.
(*x_record =
fun s : S => match s return nat with
             | Build_S x_record _ => x_record
             end
     : S -> nat
*)

Print x_manual.
(*x_manual =
fun sm : S_manual => match sm return nat with
                     | BSM n _ => n
                     end
     : S_manual -> nat*)


Print cond_record.
(*cond_record =
fun s : S =>
match s as s0 return (@eq nat (x_record s0) O) with
| Build_S x_record cond_record => cond_record
end
     : forall s : S, @eq nat (x_record s) O*)

Print cond_manual.
(*cond_manual =
fun sm : S_manual =>
match sm as sm' return (@eq nat (x_manual sm') O) with
| BSM n H => H
end
     : forall sm : S_manual, @eq nat (x_manual sm) O*)
>>>>>>>

You should familiarize yourself a bit more with dependent type and
similar things before you attack the formalization of a big theory in
Coq. Because the fact you think that a function of return type
"s.(x_record) = 0" returns "True"  (which is a proposition) when it in
fact returns à *proof* of the previous equality shows that your are
not familiar with the difference between proofs and proposition, which
can be an handicap to perform interesting proofs in Coq.

Cheers,
Alexandre Pilkiewicz