2.1 Record types

2.1 Record types

The Record function is a macro allowing the definition of records as is done in many programming languages. Its syntax is described on figure 2.1.

sentence ::= record
     
record ::= Record ident [ params ] : sort := [ident] { [field ; ... ; field] } .
     
field ::= ident : term


Figure 2.1:Syntax for the definition of Record


In the command ``Record ident [ params ] : sort := ident0 { ident1 : term1; ...identn : termn }.'', the identifier ident is the name of the defined record and sort is its type. The identifier ident0 is the name of its constructor. The identifiers ident1, .., identn are the names of its fields and term1, .., termn their respective types. Records can have parameters.


Example: The set of rational numbers may be defined as:
Coq < Record Rat : Set := mkRat {
Coq < top : nat;
Coq < bottom : nat;
Coq < Rat_cond : (gt bottom O) }.
Rat_ind is defined
Rat_rec is defined
Rat_rect is defined
Rat is defined


A field may depend on other fields appearing before it. For instance in the above example, the field Rat_cond depends on the field bottom. Thus the order of the fields is important.

Let us now see the work done by the Record macro. First the macro generates a inductive definition with just one constructor:


Inductive ident [ params ] : sort :=
  ident0 : (ident1:term1) .. (identn:termn)(ident params).


To build an object of type ident, one should provide the constructor ident0 with n terms filling the fields of the record.

Let us define the rational 1/2.

Coq < Theorem two_is_positive : (gt (S (S O)) O).

Coq < Repeat Constructor.

Coq < Save.

Coq < Definition half := (mkRat (S O) (S (S O)) two_is_positive).
Coq < Check half.
half
     : Rat


The macro generates also, when it is possible, the projection functions for destructuring an object of type ident. These projection functions have the same name that the corresponding field. In our example:

Coq < Eval Compute in (top half).
     = (S O)
     : nat

Coq < Eval Compute in (bottom half).
     = (S (S O))
     : nat

Coq < Eval Compute in (Rat_cond half).
     = two_is_positive
     : (gt (bottom half) O)


In the case where the definition of a projection function is impossible, a warning is printed.


Warnings:
  1. Warning: identi cannot be defined.
    This message is followed by an explanation of this impossibility.
    There may be three reasons:
    1. The name identi already exists in the environment (see section 1.3.1).
    2. The body of identi uses a incorrect elimination for ident (see sections 1.3.4 and 4.5.4).
    3. The projections [ idents ] were not defined.
      The body of termi uses the projections idents which are not defined for one of these three reasons listed here.



Error messages:
  1. A record cannot be recursive
    The record name ident appears in the type of its fields. During the definition of the one-constructor inductive definition, all the errors of inductive definitions, as described in section 1.3.3, may occur.



Variants:
  1. Record ident [ params ] : sort := {
          ident1 : term1;
      ...
          identn : termn }.
    One can omit the constructor name in which case the system will use the name Build_ident.


Retrieved by Memoweb from http://pauillac.inria.fr/coq/doc/node.0.1.0.html at 8/10/98