Corresponds to Sec. 5.3, structures and satisfiability, and Sec. 5.4, theories. A structure is Definition 7's Σ-structure. Its domain field is indexed by sort rather than being a single untyped universe, so a term of sort σ evaluates to something of type domain σ. interp gives a value to every function symbol at every rank, including ranks the signature does not declare; the model conditions constrain only the declared ones. A rank carries a list of argument sorts, so an interpretation is a curried function rather than a value: interpretation is its type, hlist is a list of argument values sorted pointwise by the rank, and interp_apply applies the one to the other. adt_axioms holds the conditions a structure owes where the signature declares datatypes — Definition 8's absolutely free structure for the domain and for the constructor interpretations, and Definition 9's selector and tester conditions. It is deliberately not a field of structure for ergonomic theory composition. A theory is Definition 12 — a signature together with the class of structures that model it. It is reached from a pretheory, which is the same pair without the datatype condition: pretheory_compose combines two whose signatures compose, and a model of the result is a structure modelling both, while theory_init closes the result off by conjoining the datatype condition at the signature reached.

Interpretations and Heterogeneous Lists

The type of an interpretation of one rank, the arguments it is applied to, and the application itself.

Case analysis on an hlist whose index is a known list shape. dependent destruction reaches these too, but by a route that needs eq_rect_eq; a dependent match on the index does not.

The inverse of interp_apply: the interpretation of a rank read off a function on its argument lists.

Operations on hlist

The values of an hlist, each tagged with its sort: the form a finite map from variables stores them in.

Type-valued "every element satisfies P".

The hlist_ForallT payload is a nested tuple, which is what a Type-level definition wants. A proof wants it indexed, to match the hlist_lookup lemmas above.

Replacements for dependent destruction on an hlist at a known index shape, so that the lemmas above carry the case analysis rather than eq_rect_eq. hlist_cons keeps the tail under the name the head variable had, as dependent destruction does.

hlist_map commutes with lookup: the ith element of the mapped list is the image of the ith element.

Ground Terms

The free term algebra over a signature's constructors: the domain that Definition 8 requires a datatype sort to have. A ground_term is either a generator — an element of a datatype-free domain — or a constructor applied to further ground terms. gen is quantified over generator sorts, taking the guard as an argument, rather than being a plain sort → Type. This is not decoration, and is necessary to ensure that structures (introduced below) remain constructable. Proof irrelevance makes the extra argument invisible in use. The guard is adt_free and not Definition 9(3)'s "not a datatype"; the argument is at domain_gen below, which is where 9(3) is transcribed.

Elimination

ground_term nests through hlist, so Rocq's generated eliminator gives no induction hypothesis for a constructor's arguments. These are the usable ones.

The recursion over the argument list has to be an inner fix. Written as a mutual Fixpoint the guard checker rejects it: hlist is not in the same inductive block as ground_term, so it cannot see an element of the list as a subterm of the term. Inlined, the subterm information propagates, because ws is passed vs and vs is a subterm of g.

Reading a Sort Off a Term

A ground term at σ witnesses that σ is one of the sorts a datatype's fields can be read back at: a leaf sits at a datatype-free sort, a constructor application at a datatype sort, and there is no third case. This is where the embeddable_sort premises below come from when the argument sorts are read off a term rather than off the signature.

Structures

Moving Between the Domain and the Term Algebra

Definition 9(3)'s generators, restricted. The standard takes them to be the domains of every sort that is not a datatype, and that is circular wherever such a sort has its domain fixed in terms of a datatype's. τ_seq δ is not a datatype, so 9(3) makes its domain a generator of the algebra that defines δ's domain, while SMTLIB.Theory.Seq fixes that same domain to be the lists over δ's; neither is prior to the other. Arrows do the same inside Definition 9 itself, 9(2) fixing the domain of σ → δ as a function space over δ's. Restricting the generators to the adt_free sorts breaks the circle. A generator at a sort mentioning a datatype could only reach a term as a constructor field at that sort, so the two readings build the same ground terms exactly when no constructor field buries a datatype (constructor_args_embeddable). §4.2.3(iv) forbids that only within a declaration group: a field Int → List of a datatype declared after List keeps to (iv), and builds a ground term under 9(3) but none here. At such a rank adt_interp_constructor and the selector condition below say nothing; see there.

adt_axioms' constructor condition has to equate a domain-level application with a term-level one, so it needs to send a constructor's arguments across. A datatype-sorted argument transports by the domain equation; a datatype-free one is a generator leaf. The choice between the two builds a term, so it cannot be made classically — adt_dec is what makes this a function. An argument sort that is neither — a datatype buried under another sort constructor — has no ground terms at all, so there is nothing to send it to. The crossing therefore takes an embeddable_sort proof, and the constructor condition below is stated only at the ranks that have one.

The left inverse. A leaf gives its generator back; a constructor application is a datatype element, so the domain equation transports it back. This is what takes a destructured GConstr's argument list back to domain elements.

The two round trips. ground_term_project is a genuine inverse, not merely a retraction, which is what lets a destructured GConstr be put back together after its arguments have been read off.

Crossing a Constructor's Argument List

ground_term_embed takes a proof, so the map over an argument list threads one per element. The Forall cannot be taken apart ahead of the recursion — it lives in Prop and the result in Type — so it is passed along as an argument and destructed one cons at a time, as the hlist is consumed.

The round trip on a whole argument list: what a destructured GConstr needs in order to be put back together after its arguments have been read off the domain.

The Selector and Tester Conditions

Definition 9's requirements on selectors and testers. They constrain the interpretation alone — no domain equation, no term algebra — so they are stated apart from adt_axioms and reused by a theory that reads the domain condition differently; Theory.Seq is one. The consequences below are proved against them for the same reason. A selector applied to a value built by its own constructor returns the corresponding argument. Selectors stay unconstrained off the range of that constructor. The condition is restricted to constructors for the same reason as the tester condition below: selectors_for_constructor is total on func, and nothing constrains it off constructors. It is also restricted to the ranks whose argument sorts satisfy E, the sorts at which the reading of the domain condition in force builds ground terms: embeddable_sort for adt_axioms, seq_embeddable_sort for Theory.Seq's. At any other rank the constructor contributes no ground term, so its datatype's domain has no room for its values, and asking its selectors to invert it would ask it to be injective into that domain. Where its argument domains are larger, as Seq List's is than List's under List ::= nil | wrap (Seq List), no interpretation would exist.

A tester holds exactly on the range of its constructor, at each sort the constructor builds. At any other sort the condition says nothing, as Definition 9(5) says nothing, so a tester the signature overloads at such a sort is left free there. The condition is about constructors and says nothing about any other symbol. It has to be restricted explicitly, because tester_for_constructor is a total function on func that a signature is free to define as the identity off constructors — as Σ_core and Σ_reals_ints both do. Read at such a symbol the condition would ask the symbol's own interpretation to recognise the symbol's own range, which no interpretation of a surjection can do: at f_not it asks negb to be true exactly on the range of negb.

The Constructor Condition

Definition 8, second bullet, and the constructor half of Definition 9's ADT requirement, relative to a domain equation Hdom: a constructor is interpreted as the term former it names, so applying its interpretation to arguments builds exactly the ground term built from them. Unlike the selector and tester conditions it is about ground_term, so a theory reading the domain condition differently states its own. Hσs is §4.2.3(iv), asked of one rank: the argument sorts are ones the crossing is defined at. A constructor whose argument sort buries a datatype under another sort constructor has no such rank, and this condition then says nothing about it — it is left uninterpreted rather than making the theory modelless. The premises are bound by name rather than as implications because the conclusion mentions their proofs: adt_intro and GConstr carry them.

Definition 8, first bullet, and the domain half of Definition 9's ADT requirement: the domain of a datatype sort is the free term algebra over the signature's constructors.

The constructor condition reads the domain through adt_domain; the selector and tester conditions do not mention ground_term, and are shared with the variants of the domain condition that other theories introduce.

Consequences of the Structure Axioms

What a client can conclude about a model without unfolding structure or adt_axioms. An inhabitant of every domain, obtained by interpreting the nullary application of the symbol IdSimple "" at result sort σ. Every structure interprets every symbol at every rank, so this always exists — a caller needing an element of A.(domain) σ never has to carry a non-emptiness side-condition to get one.

The tester condition with its lets reduced, in the form a caller applies.

What a Consumer of the Datatype Condition Needs

adt_axioms states the datatype condition as an equation on the domain, which pins it down exactly but names a particular inductive: ground_term is the standard's reading of Definition 8, in which a datatype may not appear below another sort constructor. A theory that extends the standard past that restriction states its own variant over its own inductive — Theory.Seq's seq_adt_axioms is one — and there is no reason to expect it to be the last. adt_constructed is what all such variants have in common, stated over the interpretation alone: no junk and no confusion. It is strictly weaker — it does not rule out a domain with infinite descent, which the equation does — but it is what a consumer reasoning about a match needs, and it is what such a consumer can *name*. Eval.v is below every variant, so eval_total cannot ask for adt_axioms without foreclosing the extended ones; it asks for this instead, and each variant supplies its own way in (adt_constructed_of_adt_axioms here).

No junk: every value of a datatype sort is built by one of that sort's constructors. A match with no variable pattern rests on this: it is what says one of the arms fires.

No confusion: two constructors of one sort that build a common value are the same constructor. Restates adt_interp_constructor_disjoint without naming adt_axioms.

adt_constructed does not read a signature's variable sorts, so it carries to any signature agreeing with it except on sorts.

No-confusion in the form a client of a tester wants: outside the range of its own constructor a tester is false. Stated against adt_constructed rather than adt_axioms, so it serves every reading of the domain condition.

Theories

Definition 12. A theory names a signature Σ together with a class of Σ-structures obeying some axioms; the members of that class are the theory's models. The datatype condition is not among those axioms until the signature is finished. adt_axioms is an equation about A.(domain) δ at every datatype sort of Σ, and ground_term Σ is indexed by Σ, so asserting it at a component's own signature says something about a different type from the condition Definition 9 places on the *combined* structure, with no transport between the two. A component therefore owes no datatype condition at all: the finished structure owes it once, at the signature its models are really about. pretheory is what a component is — a signature and a model predicate, composable and extensible by variable sortings. theory_init closes a pretheory into a theory by conjoining the datatype condition at the signature reached, and theory is what sat consumes. Composing past an init is then not merely discouraged but unrepresentable. A theory wanting the extended reading of the datatype condition closes with its own operation instead — see Theory.Seq's theory_init_seq.

Closing with the standard's reading of Definition 8: a datatype domain is the well-sorted ground terms, in which a datatype sort occurs as a constructor's argument sort and never below another sort constructor.

Model Construction

Exhibiting a model means producing one structure: a domain, and an interpretation of every symbol at every rank. For a theory assembled by pretheory_compose the interpretation can be built one component at a time, but the domain cannot. The domain is a single object that all the components constrain together, and some of those constraints reach beyond the component that makes them: Theory.Seq asks for domain (τ_seq σ) = list (domain σ) at every sort, including the sorts other components introduce. The domain is therefore chosen first, and everything below varies the interpretation over a domain held fixed. A component supplies two facts about itself, pretheory_local and pretheory_interpretable, and the theorems here assemble them. To build a model of a composed theory:

• construct a domain meeting every component's requirements;
• take each component's pretheory_interpretable at that domain and combine them with pretheory_compose_interpretable;
• discharge the datatype condition at the finished signature, which no component owes — see theory_init.

The structure with domain D and interpretation ι.

ι1 and ι2 give the same value at every rank of every symbol in fs.

Building an Interpretation

interp is total: a structure gives a value at every rank, whether or not the signature declares it. So an interpretation that pins a handful of ranks needs somewhere to send the rest, and building a structure at all needs the domain inhabited at every sort. Three combinators cover that: a base to fall through to, an override at one rank, and an override at one symbol — the last for a symbol like f_eq, whose ranks are not a finite list.

Ignore the arguments and return the domain's witness.

Override base at one rank, in the shape of stdpp's fn_insert: key, value, function.

Override base at one function symbol, at every rank.

pT's model conditions depend on the domain and on the symbols pT declares, and on nothing else — so interpreting another component's symbols leaves them standing. A component proves this of its own conditions; it is immediate when each condition names a single symbol.