Building a Model's Domain

A structure fixes one domain : sort → Type that every theory component constrains at once. Theory.v explains why that cannot be built componentwise: pretheory_compose conjoins the two model predicates at a single structure, and SMTLIB.Theory.Seq alone asks for domain (τ_seq σ) = list (domain σ) at sorts it has never heard of. So the domain is chosen first, and only the interpretation composes. This file is that choice, for any signature whose stack closes with theory_init_seq. What a domain does at the *nullary* sort symbols is the caller's business. Which of them a signature declares is up to the signature, and which types they must denote is up to the theory components it is built from: a stack without SMTLIB.Theory.Strings pins nothing at σ_string, and one with a component this library has never heard of pins something here unknown. So the construction takes that assignment as a parameter, base, and extends it through the three sort constructors any stack reaching SMTLIB.Theory.Seq constrains. It meets, simultaneously:

• domain (SApp s []) = base s, away from the datatypes;
• domain (τ_map σ1 σ2) = domain σ1 → domain σ2 (structure itself);
• domain (τ_seq σ) = list (domain σ) (SMTLIB.Theory.Seq);
• domain δ = seq_ground_term Σ (fun σ _ ⇒ domain σ) δ at every datatype sort (seq_adt_axioms).

The last is not a fixpoint equation to be solved up to isomorphism: it asks the domain to *be* that inductive, on the nose. A caller combining several theories supplies as base the domains its theories pin, and reads the equations those theories owe off sort_domain_base.

The Two Passes

The obstruction is that the datatype equation defines the domain at δ from the domain at the generator sorts, which is not a subterm relation — the generators of δ's free algebra are sorts unrelated to δ. The way round is to notice that the algebra consults its generator parameter *only* at generator sorts, so a first pass that is correct there suffices to build it, and the second pass can then agree with the first exactly where the difference would show.

• adt_free_domain is the domain a signature with no datatypes would have, which is the correct one at every adt_free sort and a lie elsewhere;
• sort_domain is the real thing: the free algebra over adt_free_domain at a datatype sort, and adt_free_domain's own clauses elsewhere.

sort_domain_adt_free is the step the whole construction rests on: the two agree at every adt_free sort, hence at every generator_sort. It is provable only because SMTLIB.Theory.Seq's generators are the *datatype-free* sorts rather than Definition 9(3)'s "every sort that is not a datatype". Under the latter τ_map δ δ is a generator sort, where the first pass gives unit → unit and the second gives sort_domain δ → sort_domain δ; the two passes would have no sound step there. See domain_gen in Theory.v for that argument in full.

base is total in the sort symbol rather than restricted to Σ's own, because a sort is a symbol applied to arguments and nothing here knows which symbols are declared. At a symbol the caller does not care about, any inhabited type will do.

Pass one. Structural in the sort, and blind to the signature: the point is that it can be defined before any datatype's domain is. A datatype sort is nullary here like any other, so it lands on base, which is the deliberate lie sort_domain overrides.

Pass two. The datatype test comes first, so the equation it owes holds by decide_True alone; every other equation owes a proof that its sort is not a datatype, which is a condition on Σ and the caller's to discharge.

The Agreement

Where no datatype is mentioned the two passes are the same function. The induction is over the sort rather than over the adt_free derivation, since adt_free_app holds its premises in a Forall and the generated scheme offers no hypothesis about them.

The Equations

Each of the three non-datatype equations holds as soon as its sort is not a datatype. That is a real condition — a signature is free to declare a constructor at σ_int — and it is why these are stated with the premise rather than proved outright.

The datatype equation. sort_domain is the free algebra over adt_free_domain by definition; what has to be shown is that reading it as the algebra over sort_domain gives the *same type*, and that is an equality of the two generator parameters, by functional extensionality twice — once for the sort, once for the generator_sort proof the parameter is indexed by. sort_domain_adt_free is what makes the bodies equal, and it applies because the index is exactly a proof that the sort is datatype-free.

Inhabitation

interp is total: a structure gives a value at every rank, declared or not, so interp f [] σ is an element of the domain at every σ and no structure exists over a domain that is empty anywhere. Away from the datatype sorts that follows from base being inhabited, which is therefore what the caller owes here.

At a datatype sort it is not free, and the obligation does not reduce further: the free algebra at δ is empty unless some constructor of δ has every field sort inhabited, which is a well-foundedness condition on the datatype declarations rather than anything this construction can supply. It is taken as a parameter and owed by whoever builds Σ.