Three layers, in order: the symbol and identifier vocabulary shared by every other file in the package; the sort datatype (corresponding with Sec. 5.1, the language of sorts), with the induction principles its nested list argument makes necessary; and sort substitution, by which a polymorphic rank is instantiated at a monomorphic sort. Throughout, σ names a sort required to be monomorphic and τ one that is arbitrary.

Symbols

Identifiers & Indices

Identifiers can be indexed: see Sec. 3.3, identifiers.

A function symbol, in the head position of an application.

The head of an applied sort.

A sort variable, bound by the parameter list of a polymorphic rank.

With this in scope a bare string literal may be written wherever an identifier is expected, which is how the constants further down are defined.

Boolean Equality

The EqDecision instances above already decide equality, but they return a sumbool carrying a proof. These return a plain bool, which is what the hammer tactics and any if inside a definition want instead.

Sorts

A sort is a parameter or a sort symbol applied to a list of argument sorts. Nullary application is how a sort symbol of arity 0, such as Bool, is written as a sort.

Induction and Recursion Principles

SApp holds a list sort, so the scheme Rocq generates by default offers no hypothesis about the elements of that list and is useless for every proof in this file. Generation is switched off around the declaration above and the principles are supplied here instead. sort_ind is written directly, with the element hypothesis ∀ τ, τ ∈ τs → P τ. Since no automatic sort_ind exists, it is also what every later induction τ on a sort resolves to by name — a dependency that no `.glob` records and that no reordering may break. sort_rect is the Type analogue. It is derived rather than written out, from the well-founded subterm order sub_sort, and sort_rec is its Set instance.

sub_sort τ1 τ2 holds when τ1 is an immediate argument of τ2.

Decidable Equality and Countability

Countability goes through gen_tree identifier: a parameter becomes a leaf, and an application becomes a node holding its top symbol as a leaf followed by the encodings of its arguments.

Operations on Sorts

The parameters occurring anywhere in a sort. Empty exactly when the sort is monomorphic — see monomorphic_iff_sort_params_empty, which needs monomorphic and so is stated below it.

The top symbol of a sort, absent for a bare parameter.

Well-Formedness

A sort is well formed against a set S of declared sort symbols and an arity for each: every applied symbol is declared, and is applied to exactly as many arguments as its arity gives. A parameter is well formed unconditionally — nothing here constrains which parameters may appear. Well-formedness is conceptually a property of a sort against a *signature*, and that is how a client states it: sort_wf is this predicate at a signature's own sort symbols and arities. It is the base form because a signature is defined partly in terms of it — the well-formedness of a signature's sorts and of its ranks are both fields of the record — so nothing signature-shaped can be said until it exists.

Elementary Sorts

The sorts and sort symbols every signature carries, whatever theories it is built from: the boolean sort that every formula has, and the map sort constructor → of §3.9, whose sorts denote maps. A map is a value, and so has a sort; a function symbol has ranks instead, and is not one.

Sort Parameters

A fixed supply of parameter names, used to state the polymorphic ranks in the theory files. Unlike the sorts above these are an arbitrary choice rather than anything the standard fixes: any two distinct parameters would do, and the names are short only so the ranks read well.

Monomorphic Sorts

Sort Substitution

A sort_subst_map assigns sorts to sort parameters, and sort_subst applies one throughout a sort, leaving any parameter the map does not mention. This is how a polymorphic rank is brought to a particular sort: the two lemmas below say when two assignments cannot be told apart by doing so.

sort_subst θ1 and sort_subst θ2 agreeing on a sort τ forces them to agree on every parameter occurring in τ.

If sort_subst θ1 and sort_subst θ2 agree on τ and τ''s parameters are all among τ's, then they agree on τ' too.

Instantiation

instance_of θ τ τ' says τ' is what the polymorphic sort τ becomes under the parameter assignment θ. The monomorphic variant additionally demands that the result carry no parameters at all, which is what a rank must reach before a term can be given that sort.

A monomorphic sort is its own only instance: instance_of substitutes for sort parameters, and a monomorphic sort has none. This is how a proof reads a monomorphic rank off a declaration whose argument sorts are already concrete.