\[\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? decl_notations?``field_spec`::=`binder* of_type_inst`````|`binder* := term`````|`binder* of_type_inst := term``of_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 Rocq 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*`

    `binder`s 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.

  > `decl_notations?`

  >   Defines notations that are active in subsequent fields, not in the field itself, until the end of the `Record` (see example). Note that `where` clauses cannot be added at the record level.

  > - `binder+ : of_type_inst` is equivalent to `: forall binder+ , of_type_inst`

  > - `binder+ := term` is equivalent to `:= fun binder+ => term`

  > - `binder+ of_type_inst := term` is equivalent to `: forall binder+ , of_type_inst := fun binder+ => term`

  > `:= 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.

  > `:`

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

  > `::`

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

  > `::>`

  >   Acts as a combination of `::` and `:>`.

  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 myfield is a projection of MyRecord Arguments myfield VarName myfield is transparent Expands to: Constant Top.myfield Declared in toplevel input, characters 469-476
> (* 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 myfield2 is a projection of MyClass Arguments myfield2 {MyClass} myfield2 is transparent Expands to: Constant Top.myfield2 Declared in toplevel input, characters 843-851

> Example: Using a `where` clause in a record field

> Reserved Notation "a & b" (at level 40, left associativity).
> Record nat_comoid := { op : nat -> nat -> nat where "a & b" := (op a b); identity : nat; identity_cond : forall n, identity & n = n; comm: forall a b, a & b = b & a; assoc: forall a b c, a & (b & c) = a & b & c }.
>   nat_comoid is defined op is defined identity is defined identity_cond is defined comm is defined assoc is defined
> Error Error: "where" clause not supported for records.

>   `where` clauses are only supported for `record_field`s, not for the overall record definition.

> 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`::=`term1 .( qualid univ_annot? arg* )`````|`term1 .( @ 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:

> - `qualidrecord.( @? qualidfield arg*)` (projection) and

> - `@? qualidfield arg* qualidrecord` (application)

> where the `arg`s 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.

Other versions v: 9.2

Versions
  dev
  stable
  9.2
  9.1
  9.0
  8.20
  8.19
  8.18
  8.17
  8.16
  8.15
  8.14
  8.13
  8.12
  8.11
  8.10
  8.9
  8.8
  8.7
  8.6
  8.5
  8.4
  8.3
  8.2
  8.1
  8.0

Downloads
  PDF