In proving properties about extensible languages, each module may introduce its own properties, providing some portion of a proof for them, as well as providing some portion of the proof for properties from the modules it imports. Extensibella ensures the proof work provided by each module will work together so a full proof of each property can be built using this modular proof work without needing human intervention.
There are two pieces to ensuring the modular proof work will be valid for proving the property for any composed language:
We want the proof fragments written in the context of a single module and the modules on which it builds to remain valid in the composed language, meaning it proves the same sequents. The difference between the two contexts is that the latter's language may include more language constructs, relations, and rules for existing relations, as well as that we might have more properties we may use as lemmas in the composition. Then the only actions we might take in a proof that could have different effects in the composed language are those that rely on the language specification.
Using a rule to prove something (e.g. using a typing rule for addition to find an addition has an integer type) is not affected by the composition, as all rules included in the context of a module are also included in a composition using it.
The only proof operation that might change is a case analysis on a derivation of a relation. Since more rules may exist in a composed language than in the context of a module, a naive case analysis may create more cases in the context of a composed language than in the context of a module and its imports. This would be a problem, as the extra cases would not have proofs to handle them, and the composed language would not have a full proof.
To ensure this does not happen, we restrict case analysis within the proofs written for modules. Specifically, we restrict it to analyze only derivations where the primary component of the relation derived is built by a known constructor. Recall from our discussion of extensible languages that new rules written for an imported relation in a module must have the primary component built by new syntax constructors also from that module. This prevents new rules from being added in further extension modules that will apply to known syntax, and thus we know, in the context of a module and its imports, all the rules that might apply in such a case even when we move to the context of a composed language.
In Extensibella, language properties are proven arguing by induction and case analysis on the derivation of a relation. The cases arising from this case analysis are distributed across the modules that know the property, with how they are distributed depending on the relation between the modules introducing the property, the relation on which it carries out its top-level case analysis, and the primary component of this relation.
If the property, relation, and its primary component are all introduced by the same module, each module introducing a new constructor of the primary component will also introduce the rules defining the relation for it. Additionally, each module will know the property exists. Then we can distribute the proof work across all the modules knowing the relation.
Each module is responsible for providing modular proof fragments showing the property holds in the cases arising from the rules it introduces. Since each case in the language composition arises from a rule that is given by one of the modules, and the module giving it must have provided a modular proof fragment showing the property holds in that case, each case is proven in the composed language.
If the property and relation are introduced in the same module but the relation's primary component is introduced in an imported module, other modules may add constructors of the primary component where the relation is defined by the default rule introduced by the module introducing the relation and the property. Additionally, other modules may build on the one introducing the relation and property, adding new constructors of the primary component and rules for the relation for them.
In this situation, a subset of the cases will be known by modules knowing the property, those for rules introduced in the module introducing the property, as well as those in modules that build on the one introducing the property. The module introducing the property writes proof fragments for the rules it knows, with the cases for modules building on it having proof fragments written by those modules.
The cases for constructors introduced by other modules are grouped together as a single proof case for the module introducing the property to prove. The idea is to show the property holds for any constructor of the primary component introduced by another module that does not know the relation. In this case, the relation is defined for the unknown constructors by the default rule. We handle this in Extensibella by a special generic constructor for the primary component type where the relation is explicitly defined by the default rule. This proof fragment can then be used for each instantiation of the default rule in the composition.
If the relation and its primary component are introduced together but the property is introduced in a module building on that one, each module introducing a new constructor of the primary component will also introduce the rules defining the relation for it. However, not every module will know the property exists, so we cannot distribute the proof work across all the modules knowing the relation.
In this situation, a subset of the cases will be known by modules knowing the property, those for rules introduced in the module introducing the property and any modules it imports, as well as those in modules that build on the one introducing the property. The module introducing the property writes proof fragments for the rules it knows, with the cases for modules building on it having proof fragments written by those modules.
The cases for rules introduced by other modules are grouped into a
generic proof case for the module introducing the property
to prove as before, using a different generic constructor than the
previous case. Here the rules for the unknown cases are each
introduced by the other modules, and are thus unknown to the
module introducing the property. The module introducing the
relation must have given a special property, introduced in
Extensibella by Ext_Ind, showing what can be expected
of a rule introduced by another extension. This relies on a rule
introduced in Sterling using Extensibella_Stand_In,
with Ext_Ind showing this rule is a valid way to view
the behavior other extensions will introduce. The
generic proof fragment proves the property holds for this
rule, and the Ext_Ind property will allow us to lift
this to any actual rule in the composition.
If each was introduced in a separate module, there can be constructors of the primary component where the relation is not known, so the default rule is used to define it for them. Additionally, there can be rules written for the relation in modules where the property is not known.
As with the previous two cases, some of the rules are known in modules where the property is known, and these can be proven in the same way.
However, we also have unknown cases, but now there are two types of cases in the composition that are unknown in the module introducing the property:
Extensibella also introduces the concept of fixed
properties. Unlike extensible properties, introduced
by Extensible_Theorem and discussed above, fixed
properties do not have cases from a top-level case analysis to
distribute. Instead the full proof will be given by the module
introducing the property. The restrictions on case analysis from
above are still enforced, preventing new cases from being added to
the proof in the composition and ensuring its validity in there.