\[\begin{split}\newcommand{\as}{\kw{as}} \newcommand{\Assum}[3]{\kw{Assum}(#1)(#2:#3)} \newcommand{\case}{\kw{case}} \newcommand{\cons}{\textsf{cons}} \newcommand{\consf}{\textsf{consf}} \newcommand{\Def}[4]{\kw{Def}(#1)(#2:=#3:#4)} \newcommand{\emptyf}{\textsf{emptyf}} \newcommand{\End}{\kw{End}} \newcommand{\kwend}{\kw{end}} \newcommand{\even}{\textsf{even}} \newcommand{\evenO}{\textsf{even}_\textsf{O}} \newcommand{\evenS}{\textsf{even}_\textsf{S}} \newcommand{\Fix}{\kw{Fix}} \newcommand{\fix}{\kw{fix}} \newcommand{\for}{\textsf{for}} \newcommand{\forest}{\textsf{forest}} \newcommand{\Functor}{\kw{Functor}} \newcommand{\In}{\kw{in}} \newcommand{\Ind}[4]{\kw{Ind}[#2](#3:=#4)} \newcommand{\ind}[3]{\kw{Ind}~[#1]\left(#2\mathrm{~:=~}#3\right)} \newcommand{\Indp}[5]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)} \newcommand{\Indpstr}[6]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)/{#6}} \newcommand{\injective}{\kw{injective}} \newcommand{\kw}[1]{\textsf{#1}} \newcommand{\length}{\textsf{length}} \newcommand{\letin}[3]{\kw{let}~#1:=#2~\kw{in}~#3} \newcommand{\List}{\textsf{list}} \newcommand{\lra}{\longrightarrow} \newcommand{\Match}{\kw{match}} \newcommand{\Mod}[3]{{\kw{Mod}}({#1}:{#2}\,\zeroone{:={#3}})} \newcommand{\ModA}[2]{{\kw{ModA}}({#1}=={#2})} \newcommand{\ModS}[2]{{\kw{Mod}}({#1}:{#2})} \newcommand{\ModType}[2]{{\kw{ModType}}({#1}:={#2})} \newcommand{\mto}{.\;} \newcommand{\nat}{\textsf{nat}} \newcommand{\Nil}{\textsf{nil}} \newcommand{\nilhl}{\textsf{nil\_hl}} \newcommand{\nO}{\textsf{O}} \newcommand{\node}{\textsf{node}} \newcommand{\nS}{\textsf{S}} \newcommand{\odd}{\textsf{odd}} \newcommand{\oddS}{\textsf{odd}_\textsf{S}} \newcommand{\ovl}[1]{\overline{#1}} \newcommand{\Pair}{\textsf{pair}} \newcommand{\plus}{\mathsf{plus}} \newcommand{\SProp}{\textsf{SProp}} \newcommand{\Prop}{\textsf{Prop}} \newcommand{\return}{\kw{return}} \newcommand{\Set}{\textsf{Set}} \newcommand{\Sort}{\mathcal{S}} \newcommand{\Str}{\textsf{Stream}} \newcommand{\Struct}{\kw{Struct}} \newcommand{\subst}[3]{#1\{#2/#3\}} \newcommand{\tl}{\textsf{tl}} \newcommand{\tree}{\textsf{tree}} \newcommand{\trii}{\triangleright_\iota} \newcommand{\Type}{\textsf{Type}} \newcommand{\WEV}[3]{\mbox{$#1[] \vdash #2 \lra #3$}} \newcommand{\WEVT}[3]{\mbox{$#1[] \vdash #2 \lra$}\\ \mbox{$ #3$}} \newcommand{\WF}[2]{{\mathcal{W\!F}}(#1)[#2]} \newcommand{\WFE}[1]{\WF{E}{#1}} \newcommand{\WFT}[2]{#1[] \vdash {\mathcal{W\!F}}(#2)} \newcommand{\WFTWOLINES}[2]{{\mathcal{W\!F}}\begin{array}{l}(#1)\\\mbox{}[{#2}]\end{array}} \newcommand{\with}{\kw{with}} \newcommand{\WS}[3]{#1[] \vdash #2 <: #3} \newcommand{\WSE}[2]{\WS{E}{#1}{#2}} \newcommand{\WT}[4]{#1[#2] \vdash #3 : #4} \newcommand{\WTE}[3]{\WT{E}{#1}{#2}{#3}} \newcommand{\WTEG}[2]{\WTE{\Gamma}{#1}{#2}} \newcommand{\WTM}[3]{\WT{#1}{}{#2}{#3}} \newcommand{\zeroone}[1]{[{#1}]} \end{split}\]

Record types¶

The Record construction is a macro allowing the definition of records as is done in many programming languages. Its syntax is described in the grammar below. In fact, the Record macro is more general than the usual record types, since it allows also for “manifest” expressions. In this sense, the Record construction allows defining “signatures”.

Command RecordStructure record_definition with record_definition*¶

record_definition::=>? ident_decl binder* : sort? := ident? { record_field*; ;? }?record_field::=#[ attribute*, ]* name field_body? | natural? decl_notations?field_body::=binder* of_type|binder* of_type := term|binder* := termterm_record::={| field_def*; ;? |}field_def::=qualid binder* := term

Each record_definition defines a record named by ident_decl. The constructor name is given by ident. If the constructor name is not specified, then the default name Build_ident is used, where ident is the record name.

If sort is omitted, the default sort is Type. Notice that the type of an identifier can depend on a previously-given identifier. Thus the order of the fields is important. binder parameters may be applied to the record as a whole or to individual fields.

>?: If provided, the constructor name is automatically declared as a coercion from the class of the last field type to the record name (this may fail if the uniform inheritance condition is not satisfied). See Implicit Coercions.

Notations can be attached to fields using the decl_notations annotation.

Record and Structure are synonyms.

This command supports the universes(polymorphic), universes(template), universes(cumulative), and private(matching) attributes.

More generally, a record may have explicitly defined (a.k.a. manifest) fields. For instance, we might have: Record ident binder* : sort := { ident₁ : type₁ ; ident₂ := term₂ ; ident₃ : type₃ }. in which case the correctness of type₃ may rely on the instance term₂ of ident₂ and term₂ may in turn depend on ident₁.

Example

The set of rational numbers may be defined as:

Record Rat : Set := mkRat { sign : bool ; top : nat ; bottom : nat ; Rat_bottom_cond : 0 <> bottom ; Rat_irred_cond : forall x y z:nat, (x * y) = top /\ (x * z) = bottom -> x = 1 }.: Rat is defined sign is defined top is defined bottom is defined Rat_bottom_cond is defined Rat_irred_cond is defined

Note here that the fields Rat_bottom_cond depends on the field bottom and Rat_irred_cond depends on both top and bottom.

Let us now see the work done by the Record macro. First the macro generates a variant type definition with just one constructor: Variant ident binder* : sort := ident₀ binder*.

To build an object of type ident, provide the constructor ident₀ with the appropriate number of terms filling the fields of the record.

Example

Let us define the rational $1/2$:

Theorem one_two_irred : forall x y z:nat, x * y = 1 /\ x * z = 2 -> x = 1.
1 goal ============================ forall x y z : nat, x * y = 1 /\ x * z = 2 -> x = 1

Admitted.
one_two_irred is declared

Definition half := mkRat true 1 2 (O_S 1) one_two_irred.
half is defined

Check half.
half : Rat

Alternatively, the following syntax allows creating objects by using named fields, as shown in this grammar. The fields do not have to be in any particular order, nor do they have to be all present if the missing ones can be inferred or prompted for (see Program).

Definition half' := {| sign := true; Rat_bottom_cond := O_S 1; Rat_irred_cond := one_two_irred |}.: half' is defined

The following settings let you control the display format for types:

Flag Printing Records¶: When this flag is on (this is the default), use the record syntax (shown above) as the default display format.

You can override the display format for specified types by adding entries to these tables:

Table Printing Record qualid¶: This table specifies a set of qualids which are displayed as records. Use the Add and Remove commands to update the set of qualids.

Table Printing Constructor qualid¶: This table specifies a set of qualids which are displayed as constructors. Use the Add and Remove commands to update the set of qualids.

This syntax can also be used for pattern matching.

Eval compute in ( match half with | {| sign := true; top := n |} => n | _ => 0 end).: = 1 : nat

The macro generates also, when it is possible, the projection functions for destructuring an object of type ident. These projection functions are given the names of the corresponding fields. If a field is named _ then no projection is built for it. In our example:

Eval compute in top half.: = 1 : nat
Eval compute in bottom half.: = 2 : nat
Eval compute in Rat_bottom_cond half.: = O_S 1 : 0 <> bottom half

An alternative syntax for projections based on a dot notation is available:

Eval compute in half.(top).: = 1 : nat

Flag Printing Projections¶

This flag activates the dot notation for printing.

Example

Set Printing Projections.
Check top half.: half.(top) : nat

term_projection::=term0 .( qualid arg* )|term0 .( @ qualid term1* )
Syntax of Record projections

The corresponding grammar rules are given in the preceding grammar. When qualid denotes a projection, the syntax term0.(qualid) is equivalent to qualid term0, the syntax term0.(qualid arg+) to qualid arg+ term0. and the syntax term0.(@qualid term0+) to @qualid term0+ term0. In each case, term0 is the object projected and the other arguments are the parameters of the inductive type.

Note

Records defined with the Record keyword are not allowed to be recursive (references to the record's name in the type of its field raises an error). To define recursive records, one can use the Inductive and CoInductive keywords, resulting in an inductive or co-inductive record. Definition of mutually inductive or co-inductive records are also allowed, as long as all of the types in the block are records.

Note

Induction schemes are automatically generated for inductive records. Automatic generation of induction schemes for non-recursive records defined with the Record keyword can be activated with the Nonrecursive Elimination Schemes flag (see Generation of induction principles with Scheme).

Warning ident cannot be defined.¶

It can happen that the definition of a projection is impossible. This message is followed by an explanation of this impossibility. There may be three reasons:

The name ident already exists in the global environment (see Axiom).
The body of ident uses an incorrect elimination for ident (see Fixpoint and Destructors).
The type of the projections ident depends on previous projections which themselves could not be defined.

Error Records declared with the keyword Record or Structure cannot be recursive.¶: The record name ident appears in the type of its fields, but uses the keyword Record. Use the keyword Inductive or CoInductive instead.

Error Cannot handle mutually (co)inductive records.¶: Records cannot be defined as part of mutually inductive (or co-inductive) definitions, whether with records only or mixed with standard definitions.

During the definition of the one-constructor inductive definition, all the errors of inductive definitions, as described in Section Inductive types, may also occur.

Primitive Projections¶

Flag Primitive Projections¶: This flag turns on the use of primitive projections when defining subsequent records (even through the Inductive and CoInductive commands). Primitive projections extended the Calculus of Inductive Constructions with a new binary term constructor r.(p) representing a primitive projection p applied to a record object r (i.e., primitive projections are always applied). Even if the record type has parameters, these do not appear in the internal representation of applications of the projection, considerably reducing the sizes of terms when manipulating parameterized records and type checking time. On the user level, primitive projections can be used as a replacement for the usual defined ones, although there are a few notable differences.

Flag Printing Primitive Projection Parameters¶: This compatibility flag reconstructs internally omitted parameters at printing time (even though they are absent in the actual AST manipulated by the kernel).

Primitive Record Types¶

When the Primitive Projections flag is on, definitions of record types change meaning. When a type is declared with primitive projections, its match construct is disabled (see Primitive Projections though). To eliminate the (co-)inductive type, one must use its defined primitive projections.

For compatibility, the parameters still appear to the user when printing terms even though they are absent in the actual AST manipulated by the kernel. This can be changed by unsetting the Printing Primitive Projection Parameters flag.

There are currently two ways to introduce primitive records types:

Through the Record command, in which case the type has to be non-recursive. The defined type enjoys eta-conversion definitionally, that is the generalized form of surjective pairing for records: r = Build_R (r.(p$_{1}$) … r.(p$_{n}$)). Eta-conversion allows to define dependent elimination for these types as well.
Through the Inductive and CoInductive commands, when the body of the definition is a record declaration of the form Build_R { p$_{1}$ : t$_{1}$; … ; p$_{n}$ : t$_{n}$ }. In this case the types can be recursive and eta-conversion is disallowed. These kind of record types differ from their traditional versions in the sense that dependent elimination is not available for them and only non-dependent case analysis can be defined.

Reduction¶

The basic reduction rule of a primitive projection is p$_{i}$ (Build_R t$_{1}$ … t$_{n}$) ${\rightarrow_{\iota}}$ t$_{i}$. However, to take the δ flag into account, projections can be in two states: folded or unfolded. An unfolded primitive projection application obeys the rule above, while the folded version delta-reduces to the unfolded version. This allows to precisely mimic the usual unfolding rules of constants. Projections obey the usual simpl flags of the Arguments command in particular. There is currently no way to input unfolded primitive projections at the user-level, and there is no way to display unfolded projections differently from folded ones.

Compatibility Projections and `match`¶

To ease compatibility with ordinary record types, each primitive projection is also defined as an ordinary constant taking parameters and an object of the record type as arguments, and whose body is an application of the unfolded primitive projection of the same name. These constants are used when elaborating partial applications of the projection. One can distinguish them from applications of the primitive projection if the Printing Primitive Projection Parameters flag is off: For a primitive projection application, parameters are printed as underscores while for the compatibility projections they are printed as usual.

Additionally, user-written match constructs on primitive records are desugared into substitution of the projections, they cannot be printed back as match constructs.

Record types¶

Primitive Projections¶

Primitive Record Types¶

Reduction¶

Compatibility Projections and match¶

Compatibility Projections and `match`¶