\[\begin{split}\newcommand{\as}{\kw{as}} \newcommand{\case}{\kw{case}} \newcommand{\cons}{\textsf{cons}} \newcommand{\consf}{\textsf{consf}} \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}[3]{\kw{Ind}~[#1]\left(#2\mathrm{~:=~}#3\right)} \newcommand{\Indp}[4]{\kw{Ind}_{#4}[#1](#2:=#3)} \newcommand{\Indpstr}[5]{\kw{Ind}_{#4}[#1](#2:=#3)/{#5}} \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{\ModImp}[3]{{\kw{Mod}}({#1}:{#2}:={#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 command defines types similar to records in programming languages. Those types describe tuples whose components, called fields, can be accessed with projections. Records can also be used to describe mathematical structures, such as groups or rings, hence the synonym Structure.

Defining record types

Command Record​Structure record_definition
record_definition::=>? ident_decl binder* : sort? := ident? { record_field*; ;? } as ident??record_field::=#[ attribute*, ]* name field_spec? | natural?field_spec::=binder* of_type_inst|binder* := term|binder* of_type_inst := termof_type_inst::=:​:>​::​::> type

Defines a non-recursive record type, creating projections for each field that has a name other than _. The field body and type can depend on previous fields, so the order of fields in the definition may matter.

Use the Inductive and CoInductive commands to define recursive (inductive or coinductive) records. These commands also permit defining mutually recursive records provided that all of the types in the block are records. These commands automatically generate induction schemes. Enable the Nonrecursive Elimination Schemes flag to enable automatic generation of elimination schemes for Record. See Generation of induction principles with Scheme.

The Class command can be used to define records that are also Typeclasses, which permit Coq to automatically infer the inhabitants of the record.

>?

If specified, the constructor is declared as a coercion from the class of the last field type to the record name. See Implicit Coercions.

ident_decl

The ident within is the record name.

binder*

binders may be used to declare the inductive parameters of the record.

: sort

The sort the record belongs to. The default is Type.

:= ident?

ident is the name of the record constructor. If omitted, the name defaults to Build_ident where ident is the record name.

as ident?

Specifies the name used to refer to the argument corresponding to the record in the type of projections. If not specified, the name is the first letter of the record name converted to lowercase (see example). In constrast, Class command uses the record name as the default (see example).

In record_field:

attribute, if specified, can only be canonical.

name is the field name. Since field names define projections, you can't reuse the same field name in two different records in the same module. This example shows how to reuse the same field name in multiple records.

field_spec can be omitted only when the type of the field can be inferred from other fields. For example: the type of n can be inferred from npos in Record positive := { n; npos : 0 < n }.

| natural

Specifies the priority of the field. It is only allowed in Class commands.

:

Specifies the type of the field.

:>

If specified, the field is declared as a coercion from the record name to the class of the field type. See Implicit Coercions. Note that this currently does something else in Class commands.

::

If specified, the field is declared a typeclass instance of the class of the field type. See Typeclasses.

::>

Acts as a combination of :: and :>.

:= term, if present, gives the value of the field, which may depend on the fields that appear before it. Since their values are already defined, such fields cannot be specified when constructing a record.

The Record command supports the universes(polymorphic), universes(template), universes(cumulative), private(matching) and projections(primitive) attributes.

Example: Defining a record

The set of rational numbers may be defined as:

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

The Rat_* fields depend on top and bottom. Rat_bottom_nonzero is a proof that bottom (the denominator) is not zero. Rat_irreducible is a proof that the fraction is in lowest terms.

Example: Reusing a field name in multiple records

Module A. Record R := { f : nat }. End A.
Interactive Module A started R is defined f is defined Module A is defined
Module B. Record S := { f : nat }. End B.
Interactive Module B started S is defined f is defined Module B is defined
Check {| A.f := 0 |}.
{| A.f := 0 |} : A.R
Check {| B.f := 0 |}.
{| B.f := 0 |} : B.S

Example: Using the "as" clause in a record definition

Record MyRecord := { myfield : nat } as VarName.
MyRecord is defined myfield is defined
About myfield. (* observe the MyRecord variable is named "VarName" *)
myfield : MyRecord -> nat myfield is not universe polymorphic Arguments myfield VarName myfield is transparent Expands to: Constant Top.myfield
(* make "VarName" implicit without having to rename the variable,    which would be necessary without the "as" clause *)
Arguments myfield {VarName}. (* make "VarName" an implicit parameter *)
Check myfield.
myfield : nat where ?VarName : [ |- MyRecord]
Check (myfield (VarName:={| myfield := 0 |})).
myfield : nat

Example: Argument name for a record type created using Class

Compare to Record in the previous example:

Class MyClass := { myfield2 : nat }.
MyClass is defined myfield2 is defined
About myfield2. (* Argument name defaults to the class name and is marked implicit *)
myfield2 : MyClass -> nat myfield2 is not universe polymorphic Arguments myfield2 {MyClass} myfield2 is transparent Expands to: Constant Top.myfield2
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 Record command. Use the Inductive or CoInductive command instead.

Error ident already exists

The fieldname ident is already defined as a global.

Warning ident1 cannot be defined because the projection ident2 was not defined

The type of the projection ident1 depends on previous projections which themselves could not be defined.

Warning ident cannot be defined.

The projection cannot be defined. This message is followed by an explanation of why it's not possible, such as:

  1. The body of ident uses an incorrect elimination for ident (see Fixpoint and Destructors).

Warning identfield cannot be defined because it is informative and identrecord is not

The projection for the named field identfield can't be defined. For example, Record R:Prop := { f:nat } generates the message "f cannot be defined ... and R is not". Records of sort Prop must be non-informative (i.e. indistinguishable). Since nat has multiple inhabitants, such as {| f := 0 |} and {| f := 1 |}, the record would be informative and therefore the projection can't be defined.

See also

Coercions and records in section Classes as Records.

Note

Records exist in two flavors. In the first, a record ident with parameters binder*, constructor ident0, and fields name field_spec* is represented as a variant type with a single constructor: Variant ident binder* : sort := ident0 ( name field_spec )* and projections are defined by case analysis. In the second implementation, records have primitive projections: see Primitive Projections.

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

Constructing records

term_record::={| field_val*; ;? |}field_val::=qualid binder* := term

Instances of record types can be constructed using either record form (term_record, shown here) or application form (see term_application) using the constructor. The associated record definition is selected using the provided field names or constructor name, both of which are global.

In the record form, the fields can be given in any order. Fields that can be inferred by unification or by using obligations (see Program) may be omitted.

In application form, all fields of the record must be passed, in order, as arguments to the constructor.

Example: Constructing 1/2 as a record

Constructing the rational \(1/2\) using either the record or application syntax:

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
(* Record form: top and bottom can be inferred from other fields *)
Definition half :=   {| negative := false;      Rat_bottom_nonzero := O_S 1;      Rat_irreducible := one_two_irred |}.
half is defined
(* Application form: use the constructor and provide values for all the fields    in order.  "mkRat" is defined by the Record command *)
Definition half' := mkRat true 1 2 (O_S 1) one_two_irred.
half' is defined

Accessing fields (projections)

term_projection::=term0 .( qualid univ_annot? arg* )|term0 .( @ qualid univ_annot? term1* )

The value of a field can be accessed using projection form (term_projection, shown here) or with application form (see term_application) using the projection function associated with the field. Don't forget the parentheses for the projection form. Glossing over some syntactic details, the two forms are:

where the args are the parameters of the inductive type. If @ is specified, all implicit arguments must be provided.

In projection form, since the projected object is part of the notation, it is always considered an explicit argument of qualid, even if it is formally declared as implicit (see Implicit arguments).

Example: Accessing record fields

(* projection form *)
Eval compute in half.(top).
= 1 : nat
(* application form *)
Eval compute in top half.
= 1 : nat

Example: Matching on records

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

Example: Accessing anonymous record fields with match

Record T := const { _ : nat }.
T is defined
Definition gett x := match x with const n => n end.
gett is defined
Definition inst := const 3.
inst is defined
Eval compute in gett inst.
= 3 : nat

Settings for printing records

The following settings let you control the display format for record 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 record 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.

Flag Printing Projections

Activates the projection form (dot notation) for printing projections (off by default).

Example

Check top half. (* off: application form *)
top half : nat
Set Printing Projections.
Check top half. (* on:  projection form *)
half.(top) : nat

Primitive Projections

Note: the design of primitive projections is still evolving.

When the Primitive Projections flag is on or the projections(primitive) attribute is supplied for a Record definition, its match construct is disabled. To eliminate the record type, one must use its defined primitive projections.

For compatibility, the parameters still appear 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:

  1. 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.

  2. 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. Dependent elimination is not available for such types; you must use non-dependent case analysis for these.

For both cases the Primitive Projections flag must be set or the projections(primitive) attribute must be supplied.

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 extend 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.

Attribute projections(primitive= yes​no?)

This boolean attribute can be used to override the value of the Primitive Projections flag for the record type being defined.

Flag Printing Primitive Projection Parameters

This compatibility flag (off by default) reconstructs internally omitted parameters at printing time (even though they are absent in the actual AST manipulated by the kernel).

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.

Unfolded primitive projections can be built using the compatibility match syntax for primitive records, or by reducing the compatibility constant.

User-written match constructs on primitive records are desugared using the unfolded primitive projections and let bindings.

Example

#[projections(primitive)] Record Sigma A B := sigma { p1 : A; p2 : B p1 }.
Sigma is defined p1 is defined p2 is defined
Arguments sigma {_ _} _ _.
Check fun x : Sigma nat (fun _ => nat) =>   match x with sigma v _ => v + v end.
fun x : Sigma nat (fun _ : nat => nat) => let x0 := x in let v := p1 _ _ x0 in let p2 := p2 _ _ x0 in v + v : Sigma nat (fun _ : nat => nat) -> nat
Check fun x : Sigma nat (fun x => x = 0) =>   match x return exists y, y = 0 with     sigma v e => ex_intro _ v e   end.
fun x : Sigma nat (fun x : nat => x = 0) => let x0 := x in let v := p1 _ _ x0 in let e : v = 0 := p2 _ _ x0 in ex_intro (fun y : nat => y = 0) v e : Sigma nat (fun x : nat => x = 0) -> exists y : nat, y = 0

Matches which are equivalent to just a projection have adhoc handling to avoid generating useless let:

Arguments p1 {_ _} _.
Check fun x : Sigma nat (fun x => x = 0) =>   match x return x.(p1) = 0 with sigma v e => e end.
fun x : Sigma nat (fun x : nat => x = 0) => p2 _ _ x : forall x : Sigma nat (fun x : nat => x = 0), p1 x = 0
Flag Printing Unfolded Projection As Match

By default this flag is off and unfolded primitive projections are printed the same as folded primitive projections. By setting this flag, unfolded primitive projections are instead printed as let-style matches in the form let '{| p := p |} := c in p.

Compatibility Constants for Projections

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. They cannot be distinguished if the record has no parameters.