# Module `Constr`

This file defines the most important datatype of Coq, namely kernel terms, as well as a handful of generic manipulation functions.

`type pconstant`

`= Names.Constant.t Univ.puniverses`

###### Simply type aliases

`type pinductive`

`= Names.inductive Univ.puniverses`

`type pconstructor`

`= Names.constructor Univ.puniverses`

`type metavariable`

`= int`

###### Existential variables

`type case_style`

`=`

`|`

`LetStyle`

`|`

`IfStyle`

`|`

`LetPatternStyle`

`|`

`MatchStyle`

`|`

`RegularStyle`

infer printing form from number of constructor

###### Case annotation

`type case_printing`

`=`

`{`

`ind_tags : bool list;`

tell whether letin or lambda in the arity of the inductive type

`cstr_tags : bool list array;`

tell whether letin or lambda in the signature of each constructor

`style : case_style;`

`}`

`type case_info`

`=`

`{`

`ci_ind : Names.inductive;`

`ci_npar : int;`

`ci_cstr_ndecls : int array;`

`ci_cstr_nargs : int array;`

`ci_relevance : Sorts.relevance;`

`ci_pp_info : case_printing;`

`}`

`type 'constr pcase_invert`

`=`

###### The type of constructions

`type t`

`type constr`

`= t`

`types`

is the same as`constr`

but is intended to be used for documentation to indicate that such or such function specifically works with*types*(i.e. terms of type a sort). (Rem:plurial form since`type`

is a reserved ML keyword)

`type types`

`= constr`

###### Functions for dealing with constr terms.

The following functions are intended to simplify and to uniform the manipulation of terms. Some of these functions may be overlapped with previous ones.

###### Term constructors.

`val mkRel : int -> constr`

Constructs a de Bruijn index (DB indices begin at 1)

`val mkVar : Names.Id.t -> constr`

Constructs a Variable

`val mkArray : (Univ.Instance.t * constr array * constr * types) -> constr`

Constructs an array

`val mkMeta : metavariable -> constr`

Constructs an patvar named "?n"

`val mkEvar : existential -> constr`

`val mkSort : Sorts.t -> types`

Construct a sort

`val mkSProp : types`

`val mkProp : types`

`val mkSet : types`

`val mkType : Univ.Universe.t -> types`

`type cast_kind`

`=`

`|`

`VMcast`

`|`

`NATIVEcast`

`|`

`DEFAULTcast`

This defines the strategy to use for verifiying a Cast

`val mkCast : (constr * cast_kind * constr) -> constr`

Constructs the term

`t1::t2`

, i.e. the term t_{1}casted with the type t_{2}(that means t2 is declared as the type of t1).

`val mkProd : (Names.Name.t Context.binder_annot * types * types) -> types`

Constructs the product

`(x:t1)t2`

`val mkLambda : (Names.Name.t Context.binder_annot * types * constr) -> constr`

Constructs the abstraction [x:t

_{1}]t_{2}

`val mkLetIn : (Names.Name.t Context.binder_annot * constr * types * constr) -> constr`

Constructs the product

`let x = t1 : t2 in t3`

`val mkApp : (constr * constr array) -> constr`

`mkApp (f, [|t1; ...; tN|]`

constructs the application (f t_{1}... t_{n})`$(f~t_1\dots f_n)$`

.

`val map_puniverses : ('a -> 'b) -> 'a Univ.puniverses -> 'b Univ.puniverses`

`val mkConst : Names.Constant.t -> constr`

Constructs a Constant.t

`val mkConstU : pconstant -> constr`

`val mkProj : (Names.Projection.t * constr) -> constr`

Constructs a projection application

`val mkInd : Names.inductive -> constr`

Constructs the ith (co)inductive type of the block named kn

`val mkIndU : pinductive -> constr`

`val mkConstruct : Names.constructor -> constr`

Constructs the jth constructor of the ith (co)inductive type of the block named kn.

`val mkConstructU : pconstructor -> constr`

`val mkConstructUi : (pinductive * int) -> constr`

`val mkRef : Names.GlobRef.t Univ.puniverses -> constr`

Make a constant, inductive, constructor or variable.

`type 'constr pcase_branch`

`= Names.Name.t Context.binder_annot array * 'constr`

Names of the indices + name of self

`type 'types pcase_return`

`= Names.Name.t Context.binder_annot array * 'types`

Names of the branches

`type ('constr, 'types, 'univs) pcase`

`= case_info * 'univs * 'constr array * 'types pcase_return * 'constr pcase_invert * 'constr * 'constr pcase_branch array`

`type case_invert`

`= constr pcase_invert`

`type case_return`

`= types pcase_return`

`type case_branch`

`= constr pcase_branch`

`type case`

`= (constr, types, Univ.Instance.t) pcase`

`type ('constr, 'types) prec_declaration`

`= Names.Name.t Context.binder_annot array * 'types array * 'constr array`

If

`recindxs = [|i1,...in|]`

`funnames = [|f1,.....fn|]`

`typarray = [|t1,...tn|]`

`bodies = [|b1,.....bn|]`

then`mkFix ((recindxs,i), funnames, typarray, bodies)`

constructs the`$`

i`$`

th function of the block (counting from 0)`Fixpoint f1 [ctx1] = b1 with f2 [ctx2] = b2 ... with fn [ctxn] = bn.`

where the length of the

`$`

j`$`

th context is`$`

ij`$`

.

`type ('constr, 'types) pfixpoint`

`= (int array * int) * ('constr, 'types) prec_declaration`

The array of

`int`

's tells for each component of the array of mutual fixpoints the number of lambdas to skip before finding the recursive argument (e.g., value is 2 in "fix f (x:A) (y:=t) (z:B) (v:=u) (w:I)`struct w`

"), telling to skip x and z and that w is the recursive argument); The second component`int`

tells which component of the block is returned

`type ('constr, 'types) pcofixpoint`

`= int * ('constr, 'types) prec_declaration`

The component

`int`

tells which component of the block of cofixpoint is returned

`type cofixpoint`

`= (constr, types) pcofixpoint`

If

`funnames = [|f1,.....fn|]`

`typarray = [|t1,...tn|]`

`bodies = [b1,.....bn]`

then`mkCoFix (i, (funnames, typarray, bodies))`

constructs the ith function of the block`CoFixpoint f1 = b1 with f2 = b2 ... with fn = bn.`

`val mkCoFix : cofixpoint -> constr`

###### Concrete type for making pattern-matching.

`type 'constr pexistential`

`= Evar.t * 'constr list`

`constr list`

is an instance matching definitional`named_context`

in the same order (i.e. last argument first)

`type ('constr, 'types, 'sort, 'univs) kind_of_term`

`=`

`|`

`Rel of int`

Gallina-variable introduced by

`forall`

,`fun`

,`let-in`

,`fix`

, or`cofix`

.`|`

`Var of Names.Id.t`

Gallina-variable that was introduced by Vernacular-command that extends the local context of the currently open section (i.e.

`Variable`

or`Let`

).`|`

`Meta of metavariable`

`|`

`Evar of 'constr pexistential`

`|`

`Sort of 'sort`

`|`

`Cast of 'constr * cast_kind * 'types`

`|`

`Prod of Names.Name.t Context.binder_annot * 'types * 'types`

Concrete syntax

`"forall A:B,C"`

is represented as`Prod (A,B,C)`

.`|`

`Lambda of Names.Name.t Context.binder_annot * 'types * 'constr`

Concrete syntax

`"fun A:B => C"`

is represented as`Lambda (A,B,C)`

.`|`

`LetIn of Names.Name.t Context.binder_annot * 'constr * 'types * 'constr`

Concrete syntax

`"let A:C := B in D"`

is represented as`LetIn (A,B,C,D)`

.`|`

`App of 'constr * 'constr array`

Concrete syntax

`"(F P1 P2 ... Pn)"`

is represented as`App (F, [|P1; P2; ...; Pn|])`

. The`mkApp`

constructor also enforces the following invariant:`F`

itself is not`App`

- and
`[|P1;..;Pn|]`

is not empty.

`|`

`Const of Names.Constant.t * 'univs`

Gallina-variable that was introduced by Vernacular-command that extends the global environment (i.e.

`Parameter`

, or`Axiom`

, or`Definition`

, or`Theorem`

etc.)`|`

`Ind of Names.inductive * 'univs`

A name of an inductive type defined by

`Variant`

,`Inductive`

or`Record`

Vernacular-commands.`|`

`Construct of Names.constructor * 'univs`

A constructor of an inductive type defined by

`Variant`

,`Inductive`

or`Record`

Vernacular-commands.`|`

`Case of case_info * 'univs * 'constr array * 'types pcase_return * 'constr pcase_invert * 'constr * 'constr pcase_branch array`

`Case (ci,u,params,p,iv,c,brs)`

is a`match c return p with brs`

expression.`c`

lives in inductive`ci.ci_ind`

at universe instance`u`

and parameters`params`

. If this match has case inversion (ie match on a 1 constructor SProp inductive with proof relevant return type) the indices are in`iv`

.The names in

`p`

are the names of the bound indices and inductive value (ie the`in`

and`as`

clauses).The names in the

`brs`

are the names of the variables bound in the respective branch.`|`

`Fix of ('constr, 'types) pfixpoint`

`|`

`CoFix of ('constr, 'types) pcofixpoint`

`|`

`Proj of Names.Projection.t * 'constr`

`|`

`Int of Uint63.t`

`|`

`Float of Float64.t`

`|`

`Array of 'univs * 'constr array * 'constr * 'types`

`Array (u,vals,def,t)`

is an array of`vals`

in type`t`

with default value`def`

.`u`

is a universe containing`t`

.

`val kind : constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term`

`val of_kind : (constr, types, Sorts.t, Univ.Instance.t) kind_of_term -> constr`

`val kind_nocast_gen : ('v -> ('v, 'v, 'sort, 'univs) kind_of_term) -> 'v -> ('v, 'v, 'sort, 'univs) kind_of_term`

`val kind_nocast : constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term`

`val isRel : constr -> bool`

###### Simple case analysis

`val isRelN : int -> constr -> bool`

`val isVar : constr -> bool`

`val isVarId : Names.Id.t -> constr -> bool`

`val isRef : constr -> bool`

`val isRefX : Names.GlobRef.t -> constr -> bool`

`val isInd : constr -> bool`

`val isEvar : constr -> bool`

`val isMeta : constr -> bool`

`val isEvar_or_Meta : constr -> bool`

`val isSort : constr -> bool`

`val isCast : constr -> bool`

`val isApp : constr -> bool`

`val isLambda : constr -> bool`

`val isLetIn : constr -> bool`

`val isProd : constr -> bool`

`val isConst : constr -> bool`

`val isConstruct : constr -> bool`

`val isFix : constr -> bool`

`val isCoFix : constr -> bool`

`val isCase : constr -> bool`

`val isProj : constr -> bool`

`val is_Prop : constr -> bool`

`val is_Set : constr -> bool`

`val isprop : constr -> bool`

`val is_Type : constr -> bool`

`val iskind : constr -> bool`

`val is_small : Sorts.t -> bool`

###### Term destructors

`val destRel : constr -> int`

Destructs a de Bruijn index

`val destMeta : constr -> metavariable`

Destructs an existential variable

`val destVar : constr -> Names.Id.t`

Destructs a variable

`val destSort : constr -> Sorts.t`

Destructs a sort.

`is_Prop`

recognizes the sort`Prop`

, whether`isprop`

recognizes both`Prop`

and`Set`

.

`val destProd : types -> Names.Name.t Context.binder_annot * types * types`

Destructs the product

`$`

(x:t_1)t_2`$`

`val destLambda : constr -> Names.Name.t Context.binder_annot * types * constr`

Destructs the abstraction

`$`

`x:t_1`

t_2`$`

`val destLetIn : constr -> Names.Name.t Context.binder_annot * constr * types * constr`

Destructs the let

`$`

`x:=b:t_1`

t_2`$`

`val decompose_app : constr -> constr * constr list`

Decompose any term as an applicative term; the list of args can be empty

`val destConst : constr -> Names.Constant.t Univ.puniverses`

Destructs a constant

`val destEvar : constr -> existential`

Destructs an existential variable

`val destInd : constr -> Names.inductive Univ.puniverses`

Destructs a (co)inductive type

`val destConstruct : constr -> Names.constructor Univ.puniverses`

Destructs a constructor

`val destCase : constr -> case`

Destructs a

`match c as x in I args return P with ... | Ci(...yij...) => ti | ... end`

(or`let (..y1i..) := c as x in I args return P in t1`

, or`if c then t1 else t2`

)- returns
`(info,c,fun args x => P,[|...|fun yij => ti| ...|])`

where`info`

is pretty-printing information

`val destProj : constr -> Names.Projection.t * constr`

Destructs a projection

`val destFix : constr -> fixpoint`

Destructs the

`$`

i`$`

th function of the block`Fixpoint f{_ 1} ctx{_ 1} = b{_ 1} with f{_ 2} ctx{_ 2} = b{_ 2} ... with f{_ n} ctx{_ n} = b{_ n}`

, where the length of the`$`

j`$`

th context is`$`

ij`$`

.

`val destCoFix : constr -> cofixpoint`

`val destRef : constr -> Names.GlobRef.t Univ.puniverses`

###### Equality

`val equal : constr -> constr -> bool`

`equal a b`

is true if`a`

equals`b`

modulo alpha, casts, and application grouping

`val eq_constr_univs : constr UGraph.check_function`

`eq_constr_univs u a b`

is`true`

if`a`

equals`b`

modulo alpha, casts, application grouping and the universe equalities in`u`

.

`val leq_constr_univs : constr UGraph.check_function`

`leq_constr_univs u a b`

is`true`

if`a`

is convertible to`b`

modulo alpha, casts, application grouping and the universe inequalities in`u`

.

`val eq_constr_univs_infer : UGraph.t -> constr -> constr -> bool Univ.constrained`

`eq_constr_univs u a b`

is`true`

if`a`

equals`b`

modulo alpha, casts, application grouping and the universe equalities in`u`

.

`val leq_constr_univs_infer : UGraph.t -> constr -> constr -> bool Univ.constrained`

`leq_constr_univs u a b`

is`true`

if`a`

is convertible to`b`

modulo alpha, casts, application grouping and the universe inequalities in`u`

.

###### Extension of Context with declarations on constr

`type rel_declaration`

`= (constr, types) Context.Rel.Declaration.pt`

`type named_declaration`

`= (constr, types) Context.Named.Declaration.pt`

`type compacted_declaration`

`= (constr, types) Context.Compacted.Declaration.pt`

`type rel_context`

`= rel_declaration list`

`type named_context`

`= named_declaration list`

`type compacted_context`

`= compacted_declaration list`

###### Relocation and substitution

`val exliftn : Esubst.lift -> constr -> constr`

`exliftn el c`

lifts`c`

with lifting`el`

###### Functionals working on expressions canonically abstracted over a local context (possibly with let-ins)

`val map_branches : (constr -> constr) -> case_branch array -> case_branch array`

`val map_return_predicate : (constr -> constr) -> case_return -> case_return`

`val map_branches_with_binders : ('a -> 'a) -> ('a -> constr -> constr) -> 'a -> case_branch array -> case_branch array`

`val map_return_predicate_with_binders : ('a -> 'a) -> ('a -> constr -> constr) -> 'a -> case_return -> case_return`

###### Functionals working on the immediate subterm of a construction

`val fold : ('a -> constr -> 'a) -> 'a -> constr -> 'a`

`val fold_invert : ('a -> 'b -> 'a) -> 'a -> 'b pcase_invert -> 'a`

`val map : (constr -> constr) -> constr -> constr`

`val map_invert : ('a -> 'a) -> 'a pcase_invert -> 'a pcase_invert`

`val fold_map : ('a -> constr -> 'a * constr) -> 'a -> constr -> 'a * constr`

`val fold_map_invert : ('a -> 'b -> 'a * 'b) -> 'a -> 'b pcase_invert -> 'a * 'b pcase_invert`

`val iter : (constr -> unit) -> constr -> unit`

`val iter_invert : ('a -> unit) -> 'a pcase_invert -> unit`

`val compare_head : constr constr_compare_fn -> constr constr_compare_fn`

`type 'univs instance_compare_fn`

`= (Names.GlobRef.t * int) option -> 'univs -> 'univs -> bool`

Convert a global reference applied to 2 instances. The int says how many arguments are given (as we can only use cumulativity for fully applied inductives/constructors) .

`val compare_head_gen : Univ.Instance.t instance_compare_fn -> (Sorts.t -> Sorts.t -> bool) -> constr constr_compare_fn -> constr constr_compare_fn`

`val compare_head_gen_leq_with : ('v -> ('v, 'v, 'sort, 'univs) kind_of_term) -> ('v -> ('v, 'v, 'sort, 'univs) kind_of_term) -> 'univs instance_compare_fn -> ('sort -> 'sort -> bool) -> 'v constr_compare_fn -> 'v constr_compare_fn -> 'v constr_compare_fn`

`val compare_head_gen_with : ('v -> ('v, 'v, 'sort, 'univs) kind_of_term) -> ('v -> ('v, 'v, 'sort, 'univs) kind_of_term) -> 'univs instance_compare_fn -> ('sort -> 'sort -> bool) -> 'v constr_compare_fn -> 'v constr_compare_fn`

`compare_head_gen_with k1 k2 u s f c1 c2`

compares`c1`

and`c2`

like`compare_head_gen u s f c1 c2`

, except that`k1`

(resp.`k2`

) is used,rather than`kind`

, to expose the immediate subterms of`c1`

(resp.`c2`

).

`val compare_head_gen_leq : Univ.Instance.t instance_compare_fn -> (Sorts.t -> Sorts.t -> bool) -> constr constr_compare_fn -> constr constr_compare_fn -> constr constr_compare_fn`

`val eq_invert : ('a -> 'a -> bool) -> 'a pcase_invert -> 'a pcase_invert -> bool`