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 RecordStructure 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
::=
::>::::> typeDefines 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
andCoInductive
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 theNonrecursive Elimination Schemes
flag to enable automatic generation of elimination schemes forRecord
. 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 toBuild_ident
whereident
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 becanonical
.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 ofn
can be inferred fromnpos
inRecord 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.
::
If specified, the field is declared a typeclass instance of the class of the field type. See Typeclasses.
::>
Acts as a combination of
::
and:>
.
binder+ : of_type_inst
is equivalent to: forall binder+ , of_type_inst
binder+ of_type_inst := term
is equivalent to: forall binder+ , type := 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.The
Record
command supports theuniverses(polymorphic)
,universes(template)
,universes(cumulative)
,private(matching)
andprojections(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 ontop
andbottom
.Rat_bottom_nonzero
is a proof thatbottom
(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
- (* 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
- 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 theRecord
command. Use theInductive
orCoInductive
command instead.
- 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:
The body of
ident
uses an incorrect elimination forident
(seeFixpoint
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 sortProp
must be non-informative (i.e. indistinguishable). Sincenat
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 parametersbinder*
, constructorident0
, and fieldsname 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* := termInstances of record types can be constructed using either record form (
term_record
, shown here) or application form (seeterm_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 (seeterm_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
andRemove
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
andRemove
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:
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
andCoInductive
commands, when the body of the definition is a record declaration of the formBuild_
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
andCoInductive
commands). Primitive projections extend the Calculus of Inductive Constructions with a new binary term constructorr.(p)
representing a primitive projectionp
applied to a record objectr
(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= yesno?)¶
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.