This walkthrough introduces the structure of modular metatheory and the use of Extensibella for proving properties in modular metatheory. Extensibella is an interactive proof assistant that reasons about extensible languages built by separate modules. Much of the reasoning will look familiar to those familiar with Abella.
The language about which we will reason is built by three modules:
let bindings, along with defining typing and
evaluation for them.
Our host language's main property is type preservation, that a well-typed term that takes an evaluation step produces a term with the same type. To prove this, the host language will introduce several other properties it will use as lemmas. Each extension will then contribute to proving these properties. The big step extension will add its own property, that type preservation is also true for its big-step evaluation.
We will close with a discussion of proof composition, how the modular proofs can be used to build full proofs for a composed language.
Readers are encouraged to download the walkthrough skeleton tarball and follow along. Following along will require having Sterling installed to compile the specifications, as well as Extensibella to execute the proof steps. We recommend using Proof General to follow along; if not using Proof General, the commands can be entered into Extensibella on the terminal.
The proof can also be found as part of the examples.
Sterling contains a standard library with useful relations defined for use in writing language specifications, which is included in Sterling modules automatically. It has an accompanying Extensibella module with properties about these relations. To prepare for reasoning about our own modules, we need to compile the Sterling standard library for Extensibella.
To do this, go to the Sterling standard
library directory (sterling/stdLib) and run
$ ./build_extensibellaThis only needs to be done once to reason about all languages. It should be done again each time Sterling is updated in case the standard library has expanded.
We start by writing a specification of our host language in
Sterling. This will be
the walkthrough:host module. It
defines syntax categories and constructors for terms
(tm) and types
(ty). As discussed in
the Sterling tutorial,
each type must also declare its projection type.
The host language also declares its relations. It has small-step
evaluation (eval), substitution for
a variable (subst), a term being a
value (value), and typing
(typeOf). Each of these has its
primary component, explained as part of
our view of extensible
languages, marked with *.
These relations are then defined by inference rules. We also have
a special rule, T-Q, that is not part of the language
definition but which will play a part in reasoning. We will
discuss its use below.
Module walkthrough:host
tm ::= var(string)
| abs(string, ty, tm)
| app(tm, tm)
Projection tm : [(string, ty)]
ty ::= arrowTy(ty, ty)
| intTy
Projection ty :
Judgment eval : tm* tm
Judgment subst : string tm tm* tm
Judgment value : tm*
eval T1 T11
----------------------------- [E-App-Step1]
eval app(T1, T2) app(T11, T2)
value T1
eval T2 T21
----------------------------- [E-App-Step2]
eval app(T1, T2) app(T1, T21)
value T2
subst X T2 Body V
-------------------------------- [E-App-Subst]
eval app(abs(X, Ty, Body), T2) V
Extensibella_Stand_In {
Ctx |{tm}- T ~~> T_T
eval T_T T2
-------------------- [E-Q]
eval T T1
}
X != Y
----------------------- [S-Var-NEq]
subst X R var(Y) var(Y)
------------------ [S-Var-Eq]
subst X R var(X) R
X != Y
subst X R B S
------------------------------------- [S-Abs-NEq]
subst X R abs(Y, Ty, B) abs(Y, Ty, S)
------------------------------------- [S-Abs-Eq]
subst X R abs(X, Ty, B) abs(X, Ty, B)
subst X R T1 S1
subst X R T2 S2
--------------------------------- [S-App]
subst X R app(T1, T2) app(S1, S2)
------------------- [V-Abs]
value abs(X, Ty, T)
Judgment typeOf : [(string, ty)] tm* ty
lookup Ctx X Ty
-------------------- [T-Var]
typeOf Ctx var(X) Ty
typeOf (X, Ty1)::Ctx Body Ty2
---------------------------------------------- [T-Abs]
typeOf Ctx abs(X, Ty1, Body) arrowTy(Ty1, Ty2)
typeOf Ctx T1 arrowTy(Ty1, Ty2)
typeOf Ctx T2 Ty1
------------------------------- [T-App]
typeOf Ctx app(T1, T2) Ty2
In order to reason about this module using Extensibella, we must have Sterling compile it for Extensibella. We can do this by running the following command from the directory containing the contents of the tarball:
$ sterling --extensibella walkthrough:hostThis has Sterling translate the inference-rule-based definition into one in Extensibella's specification format and places it where Extensibella can find it.
The host language's properties can be found in the
host/host.xthm file, with the full file, including
proofs, reproduced here:
Module walkthrough:host.
Extensible_Theorem
typeOf_unique : forall Ctx T TyA TyB,
TyA : typeOf Ctx T TyA ->
TyB : typeOf Ctx T TyB ->
TyA = TyB
on TyA. [Show Proof]
Extensible_Theorem
ty_lookup : forall Ctx1 Ctx2 T Ty,
Ty : typeOf Ctx1 T Ty ->
L : (forall X XTy, lookup Ctx1 X XTy -> lookup Ctx2 X XTy) ->
typeOf Ctx2 T Ty
on Ty. [Show Proof]
Theorem empty_ty_any : forall T Ty Ctx,
typeOf [] T Ty -> typeOf Ctx T Ty. [Show Proof]
Extensible_Theorem
subst_type_preservation : forall T Ctx X XTy Ty R S,
TTy : typeOf ((X, XTy)::Ctx) T Ty ->
S : subst X R T S ->
RTy : typeOf [] R XTy ->
typeOf Ctx S Ty
on S. [Show Proof]
Extensible_Theorem
type_preservation : forall T Ty T',
Ty : typeOf [] T Ty ->
Ev : eval T T' ->
typeOf [] T' Ty
on Ev. [Show Proof]
Projection_Constraint proj_type_same : forall G T Ty T_T,
G |{tm}- T ~~> T_T -> typeOf G T Ty -> typeOf G T_T Ty.
Ext_Size eval T T'.
Proj_Rel eval T T'.
Ext_Ind forall G T T' Ty, eval T T' with Ty : typeOf G T Ty. [Show Proof]
We will look at each top-level declaration here in turn.
The first element is the module declaration. This lets Extensibella know about which language module we will be reasoning so it can locate and load the specification Sterling wrote.
The remainder of the top-level declarations in the file are properties to prove.
The first couple of declarations are extensible theorems, declared
with Extensible_Theorem.
Extensible theorems have their proofs organized around the
definition of a key relation, identified by
the on part of the declaration.
For example, for
the typeOf_unique property, the
first one in the file, its key relation is the typeOf
relation, and we are specifically focused on the first derivation
of it, typeOf Ctx T TyA, given
the named TyA by prefixing it
with TyA :. The
proof of the extensible theorem proceeds using induction and case
analysis on the key relation. For
the typeOf_unique property, this
means we have top-level proof cases for
when typeOf Ctx T TyA is derived
by
the T-Var, T-Abs,
and T-App rules. Showing the
proof in the file above will show these cases and their proofs.
The key point to note for extensible theorems is that the set of rules defining the key relation may grow by other extensions adding new rules, as our let extension will do. This is whence the extensible in extensible theorems arises. Extensions to the host language, like the let extension, will know the property exists and what its key relation is, so they can contribute to the proof, adding the proofs for the new cases they introduce.
We will leave the proofs
of typeOf_unique
and ty_lookup as exercises. For
now, they can be skipped.
The proof skeleton files
have the appropriate number of skip commands for
each. These can either be processed in Proof General without
changes, or the commands can be copied to Extensibella on the
commandline. Note, in the latter case, that each command must be
entered on its own line; multiple commands on one line will not be
accepted.
Our file contains one non-extensible
theorem, declared with Theorem,
empty_ty_any, stating that a
term typable with an empty context is typable with any context.
This particular non-extensible theorem is a corollary of the
extensible ty_lookup theorem.
Non-extensible theorems do not have proofs organized around the definitions of extensible relations, so extensions cannot add new proof cases to them. Their full proofs can thus be given in a single module, as we do here.
We also leave the proof of
empty_ty_any as an exercise. It
can be skipped as the extensible theorems were.
Type preservation, the main property our host language wants, is
an extensible theorem with evaluation as its key relation. In the
context of the host language, this gives us proof cases for the
E-App-Step1,
E-App-Step2, and
E-App-Subst rules. As with the
typeOf_unique property at which
we looked earlier, type preservation may have new proof cases
added by extensions and for which they will need to give their own
proofs. We will go through the proof of it here. Note we are
also leaving
subst_type_preservation as an
exercise, so it can be skipped as the others were.
We state our type preservation property as a term being typable
with an empty typing context and it taking an evaluation step to
T' means T' has the same type. We give
each assumption a name we will use to refer to it in the proof.
The clause on Ev declares we
will prove the property by induction on the derivation of
evaluation, the property's key relation, and by considering
the last rule by which the evaluation might have been derived:
< Extensible_Theorem
type_preservation : forall T Ty T',
Ty : typeOf [] T Ty ->
Ev : eval T T' ->
typeOf [] T' Ty
on Ev.
Subgoal 1:
Variables: Ty T2 T11 T1
IH : forall T Ty T', typeOf [] T Ty -> eval T T' * -> typeOf [] T' Ty
Ty : typeOf [] (app T1 T2) Ty
Ev : eval (app T1 T2) (app T11 T2) @
Ev1 : eval T1 T11 *
============================
typeOf [] (app T11 T2) Ty
After declaring the property, we are immediately dropped into the
case for the first rule, which here is
the E-App-Step1 rule. Before going into how we prove
this case, consider our induction scheme. Note we have the
inductive hypothesis in the context, using the
name IH, in addition to the Ty
and Ev assumptions from our declared property. The
second premise of IH, corresponding
to Ev in our original statement, is marked with
the * annotation, while the Ev
assumption is marked with the @ assumption.
The @ annotation denotes this is the size of
derivation with which we started, while the *
annotation denotes a smaller derivation. Thus the inductive
hypothesis can only be used with derivations marked as smaller.
We get smaller derivations by case analysis on derivations
annotated with @ or *. We see this
in Ev1, coming from the top-level case analysis on
the rules deriving Ev.
In this case, for rule E-App-Step1, we evaluate the
application by evaluating the first sub-term. The evaluation of
the sub-term is smaller, so we can use it with the inductive
hypothesis, but first we need a relevant typing derivation. The
top-level case analysis on Ev filled in the primary
component of Ty, so we can analyze the rules by which
this may have been derived using
the case tactic:
< Ty: case Ty. Subgoal 1: Variables: Ty T2 T11 T1 Ty1 IH : forall T Ty T', typeOf [] T Ty -> eval T T' * -> typeOf [] T' Ty Ev : eval (app T1 T2) (app T11 T2) @ Ev1 : eval T1 T11 * Ty : typeOf [] T1 (arrowTy Ty1 Ty) Ty1 : typeOf [] T2 Ty1 ============================ typeOf [] (app T11 T2) Ty
The case analysis gives us typing judgments for
both T1 and T2. Because we prefixed the
case analysis with the name Ty, the new typing
judgments are given names starting with Ty. We can now use the
apply tactic to use the
inductive hypothesis to get a typing judgment for the result of
evaluating the first sub-term:
< apply IH to Ty Ev1. Subgoal 1: Variables: Ty T2 T11 T1 Ty1 IH : forall T Ty T', typeOf [] T Ty -> eval T T' * -> typeOf [] T' Ty Ev : eval (app T1 T2) (app T11 T2) @ Ev1 : eval T1 T11 * Ty : typeOf [] T1 (arrowTy Ty1 Ty) Ty1 : typeOf [] T2 Ty1 H1 : typeOf [] T11 (arrowTy Ty1 Ty) ============================ typeOf [] (app T11 T2) Ty
The T-App rule now applies to H1
and Ty1. Extensibella will automatically apply this
rule when we use the search
tactic, finishing this case and moving to the next one:
< search. Subgoal 2: Variables: Ty T21 T1 T2 IH : forall T Ty T', typeOf [] T Ty -> eval T T' * -> typeOf [] T' Ty Ty : typeOf [] (app T1 T2) Ty Ev : eval (app T1 T2) (app T1 T21) @ Ev1 : value T1 Ev2 : eval T2 T21 * ============================ typeOf [] (app T1 T21) Ty
The next case, for rule E-App-Step2, is similar to
the first case and can be completed with the following three
commands (note if you are following along that each must be
entered individually on the Extensibella command line):
Ty: case Ty. apply IH to Ty1 Ev2. search.
This brings us to the last case in the host language, that for
the E-App-Subst rule:
Subgoal 3: Variables: Ty T' T2 Body Ty1 X IH : forall T Ty T', typeOf [] T Ty -> eval T T' * -> typeOf [] T' Ty Ty : typeOf [] (app (abs X Ty1 Body) T2) Ty Ev : eval (app (abs X Ty1 Body) T2) T' @ Ev1 : value T2 Ev2 : subst X T2 Body T' ============================ typeOf [] T' Ty
We want to use the subst_type_preservation theorem we
would have proven earlier. To do so, we will need a derivation of
typing for Body. First, we analyze the derivation of
typing again:
< Ty: case Ty. Subgoal 3: Variables: Ty T' T2 Body Ty1 X Ty2 IH : forall T Ty T', typeOf [] T Ty -> eval T T' * -> typeOf [] T' Ty Ev : eval (app (abs X Ty1 Body) T2) T' @ Ev1 : value T2 Ev2 : subst X T2 Body T' Ty : typeOf [] (abs X Ty1 Body) (arrowTy Ty2 Ty) Ty1 : typeOf [] T2 Ty2 ============================ typeOf [] T' Ty
This does not give us a derivation of typing for Body
directly, but it gives us a derivation of typing for the full
abstraction. Analyzing this again gives us the typing derivation
we need:
< Ty: case Ty. Subgoal 3: Variables: Ty T' T2 Body X Ty2 IH : forall T Ty T', typeOf [] T Ty -> eval T T' * -> typeOf [] T' Ty Ev : eval (app (abs X Ty2 Body) T2) T' @ Ev1 : value T2 Ev2 : subst X T2 Body T' Ty1 : typeOf [] T2 Ty2 Ty : typeOf [(X, Ty2)] Body Ty ============================ typeOf [] T' Ty
We can now use the apply tactic
to apply the subst_type_preservation lemma:
< apply subst_type_preservation to Ty Ev2 Ty1. Subgoal 3: Variables: Ty T' T2 Body X Ty2 IH : forall T Ty T', typeOf [] T Ty -> eval T T' * -> typeOf [] T' Ty Ev : eval (app (abs X Ty2 Body) T2) T' @ Ev1 : value T2 Ev2 : subst X T2 Body T' Ty1 : typeOf [] T2 Ty2 Ty : typeOf [(X, Ty2)] Body Ty H1 : typeOf [] T' Ty ============================ typeOf [] T' Ty
This gives us the exact same formula as our goal as an assumption.
The search tactic will find this and solve the goal,
and, as it is the last goal, finish the full proof as well.
< search. Proof completed.
Note in the final case in the host language proof for type
preservation we use the previous property,
subst_type_preservation, as a
lemma. This is the purpose of all the earlier properties; they
all acted as lemmas to prove later ones. Our modular metatheory
framework ensures modular proofs guarantee not only individual
properties are true for composed languages, but also that modular
proofs for a set of properties, with some possibly using others as
lemmas, guarantee the full set will hold for any composed
language.
The validity of full sets of properties is guaranteed by maintaining the order in which the properties are proven by the host language. The host language declares its properties in order, with the proofs of later properties able to use earlier properties as lemmas. Extensions then add their proofs in this order, ensuring all the modular proofs can be composed into full proofs for any composed language.
The antepenultimate declaration in the file is for a projection constraint, which is a special kind of extensible property. Projection constraints specify how the semantics of extension-introduced constructs must relate to their projections, their projections being defined by special rules in Sterling. For example, the projection constraint our host language introduces requires a term and its projection have the same type.
The key relation for a projection constraint is its first premise, which must be a projection of some term. Note that we have no proof for the projection constraint in the host language. Because its key relation is a projection and the host language does not introduce projecting syntax, there are no proof cases for the host language to prove.
Note that this projection constraint does not contribute to the proof of type preservation, which was the host language's main goal. Projection constraints can be viewed as a service to extension writers, as they don't generally help the host language prove its own properties, but they make it easier for extensions to prove their new properties.
The final three declarations are
for Ext_Size,
Proj_Rel,
and Ext_Ind for
the eval relation. The name Ext_Ind stands
for extension induction. When an extension
wants to prove a property using a relation introduced by the host
language as its key relation, there is a possibility other
extensions that will be included in a composed language will
introduce new rules defining that relation. The extension will
need to prove a generic case to handle these. The
generic case is given by
the Ext_Ind declaration for the
relation. Having a declaration of this is required for an
extension to use a host relation as its key relation, that is, to
use it for induction, hence the name.
The generic case the extension proves for its property is when the
key relation is derived using the stand-in rule given
above, X-Q:
Extensibella_Stand_In {
Ctx |{tm}- T ~~> T_T
eval T_T T2
-------------------- [E-Q]
eval T T1
}
This declaration also creates an obligation that must be proven by
the host language and each extension, that this rule is a valid
way of looking at the rules introduced by extensions, embodied in
the projection version of the eval relation
declared by the Proj_Rel declaration.
The Ext_Size declaration
introduces a new version of the eval relation that
will be useful for proving this.
The details of this are discussed more
in the context of the let extension below. We
leave the proof for the Ext_Ind
in the host language as an exercise, recommending returning to it
after reading the discussion of it for the let extension.
Because extensions are obligated to prove the host language's properties and maintain their order, we need to compile the host language's proof file before we can start proving properties for our extensions:
$ extensibella --compile host.xthmThe compilation process has Extensibella pull out the theorems in the proof file, give them order tags, and store them in a place it knows. When Extensibella goes to reason about an extension, it then reads this information so it knows the proof obligations the extension has for the properties from the host language, and the order in which they should occur. If an extension module builds on multiple modules, the order tags are used to combine the property orders from each into a shared order containing all the properties and relative orderings from both. Having such an ordering, Extensibella can then check the extension fulfills all its obligations, and that it maintains the orders from the modules on which it builds.
In general, when compiling a proof file, it is a good idea to combine the compilation and proof checking flags:
$ extensibella --check --compile host.xthmWith only the compilation flag, Extensibella assumes each property's proof is present and valid; when we add the proof checking flag, it verifies this before compiling it. This prevents mistakes from sneaking into the compiled form and affecting extensions. Checking is not a default part of compilation because it is much slower than the compilation alone, and is not needed if the file is already known to be valid.
Our first extension adds a new form for terms,
a let-binding, and defines the relations introduced
by the host language for the new form. It also defines its
projection in the Proj-Let rule,
projecting to an application of an abstraction.
Module walkthrough:let
Builds on walkthrough:host
tm ::= ...
| let(string, tm, tm)
typeOf Ctx T1 Ty
----------------------------------------------------- [Proj-Let]
Ctx |{tm}- let(X, T1, T2) ~~> app(abs(X, Ty, T2), T1)
eval T1 T11
----------------------------------- [E-Let-Step]
eval let(X, T1, T2) let(X, T11, T2)
value T1
subst X T1 T2 V
--------------------- [E-Let-Subst]
eval let(X, T1, T2) V
X != Y
subst X R T1 S1
subst X R T2 S2
--------------------------------------- [S-Let-NEq]
subst X R let(Y, T1, T2) let(Y, S1, S2)
subst X R T1 S1
--------------------------------------- [S-Let-Eq]
subst X R let(X, T1, T2) let(X, S1, T2)
typeOf Ctx T1 Ty1
typeOf (X, Ty1)::Ctx T2 Ty2
----------------------------- [T-Let]
typeOf Ctx let(X, T1, T2) Ty2
We can compile this module in the same manner as the host module so we can use it with Extensibella:
$ sterling --extensibella walkthrough:let
The Extensibella proofs for the let extension's properties can be
found in the let/let.xthm file, reproduced here:
Module walkthrough:let. Prove walkthrough:host:typeOf_unique. [Show Proof] Prove walkthrough:host:ty_lookup. [Show Proof] Prove walkthrough:host:subst_type_preservation. [Show Proof] Prove walkthrough:host:type_preservation. [Show Proof] Prove_Constraint walkthrough:host:proj_type_same. [Show Proof] Add_Ext_Size walkthrough:host:eval. Add_Proj_Rel walkthrough:host:eval. Prove_Ext_Ind walkthrough:host:eval. [Show Proof]
The proofs the let extension writes are all for new cases of
extensible host properties of the various kinds. Thus the
top-level declarations are all
the Prove
and Add versions of the host
language's declarations. When Extensibella reads the
module declaration, it finds the walkthrough:let
module builds on the walkthrough:host module. It
then reads the compiled set of properties from the host language,
along with their order, so it knows what the let extension needs
to prove here, and in what order it must be proven. Extensibella
checks this order is maintained by the let extension.
Note we do not have a command for the
empty_ty_any theorem from the
host language here. Because it is non-extensible, the let
extension does not need to add to its proof. If a proof needed it
as a lemma, it could still be used, but only after the
ty_lookup extensible theorem.
This is because the empty_ty_any
theorem is part of the order from the host language and the
validity of the proofs for a composed language is dependent on
maintaining this order.
We will look at the proofs given by the let extension for type
preservation, the projection constraint, and
Ext_Ind for typing. The earlier
properties can be skipped past as we saw in the host language,
returning to them later as exercises.
When the extension is ready to prove the type preservation
property, it declares so with
a Prove declaration using the
property's fully-qualified name that includes the module where it
was declared:
< Prove walkthrough:host:type_preservation. Subgoal 7: Variables: Ty T2 T11 X T1 IH : forall T Ty T', typeOf [] T Ty -> eval T T' * -> typeOf [] T' Ty Ty : typeOf [] (let X T1 T2) Ty Ev : eval (let X T1 T2) (let X T11 T2) @ Ev1 : eval T1 T11 * ============================ typeOf [] (let X T11 T2) Ty
This drops us into the first case for when Ev is
derived using a rule introduced by this extension, specifically
the E-Let-Step rule. This can be solved by a
sequence of tactics similar to those for
the E-App-Step1 and E-App-Step2 rules in
the host language:
Ty: case Ty. apply IH to Ty Ev1. search.
This brings us to the case for the
E-Let-Subst rule:
Subgoal 8: Variables: Ty T' T2 T1 X IH : forall T Ty T', typeOf [] T Ty -> eval T T' * -> typeOf [] T' Ty Ty : typeOf [] (let X T1 T2) Ty Ev : eval (let X T1 T2) T' @ Ev1 : value T1 Ev2 : subst X T1 T2 T' ============================ typeOf [] T' Ty
This is similar to the case for the E-App-Subst rule
from the host language and can be solved by a similar chain of
tactics:
Ty: case Ty. apply subst_type_preservation to Ty1 Ev2 Ty. search.
After proving type preservation, we are ready to prove the
projection constraint, and declare so with a
Prove_Constraint declaration:
< Prove_Constraint walkthrough:host:proj_type_same.
Variables: G Ty T1 T2 Ty1 X
Hyp : G |{tm}- let X T1 T2 ~~> app (abs X Ty1 T2) T1
Hyp1 : typeOf G (let X T1 T2) Ty
Hyp2 : typeOf G T1 Ty1
============================
typeOf G (app (abs X Ty1 T2) T1) Ty
This gives us the case for the projection being derived using
the Proj-Let rule. To show this, we
need to show the projection
app (abs X Ty1 T2) T1
has the same type as the original term
let X T1 T2. We can analyze the
typing derivation for the original term, since its primary
component is built by the let constructor:
< case Hyp1.
Variables: G Ty T1 T2 Ty1 X Ty2
Hyp : G |{tm}- let X T1 T2 ~~> app (abs X Ty1 T2) T1
Hyp2 : typeOf G T1 Ty1
H1 : typeOf G T1 Ty2
H2 : typeOf ((X, Ty2)::G) T2 Ty
============================
typeOf G (app (abs X Ty1 T2) T1) Ty
We need to know that T2 has type Ty
if X is assigned type Ty1 in its
context. To do this, we can use the type uniqueness property
introduced by the host language to show Ty1
and Ty2 must actually be the same:
< apply typeOf_unique to Hyp2 H1.
Variables: G Ty T1 T2 X Ty2
Hyp : G |{tm}- let X T1 T2 ~~> app (abs X Ty2 T2) T1
Hyp2 : typeOf G T1 Ty2
H1 : typeOf G T1 Ty2
H2 : typeOf ((X, Ty2)::G) T2 Ty
============================
typeOf G (app (abs X Ty2 T2) T1) Ty
This unified Ty1 and Ty2,
so we have the premises to use the T-App
and T-Abs rules to prove the conclusion:
< search. Proof completed.
For Ext_Ind,
each extension has an obligation to show the rules it introduces
are compatible with the stand-in rule defined by the host language.
For the eval relation, this is
Extensibella_Stand_In {
Ctx |{tm}- T ~~> T_T
eval T_T T2
-------------------- [E-Q]
eval T T1
}
This
compatibility for a relation rel
is defined by a relation <rel
{P}>, called the projection version
of rel. This relation is
declared by the Proj_Rel and
Add_Proj_Rel commands.
In our case, this relation is
<eval {P}>. Each rule
for this relation corresponds to one for the underlying relation,
with those introduced by extensions having the stand-in rule
incorporated. For example, the rule for the projection version
of eval corresponding to E-Let-Step is
<eval {P}> T1 T11
Ctx |{tm}- let(X, T1, T2) ~~> T_T
<eval {P}> T_T T3
----------------------------------------- [E-Let-Step {P}]
<eval {P}> let(X, T1, T2) let(X, T11, T2)
This rule incorporates both the standard premises of
the E-Let-Step rule and the premises of the stand-in rule
instantiated for the conclusion of E-Let-Step.
In order to prove the projection version of
the eval relation follows from the relation itself,
we need a way to show we will have <eval {P}>
hold for the projection of the primary component of any
extension-introduced rule even though we do not have a derivation
of the basic eval relation for it. The extension
size version of the eval relation,
written <eval {ES}>, will give us a way to do
this. The extension size version of a relation incorporates a
count of the number of extension-introduced rules in a derivation.
Both of these versions of relations, and how the extension size
version of a relation gives us a hook for showing the projection
version will hold on the projection, can be read about in
our paper.
What Ext_Ind shows is that we have a
derivation of the projection version of a relation whenever we
have a derivation of the relation itself, as well as a derivation
of typing for the original term. Because projection can rely on
typing, this extra premise is useful in the proof. When we have declared
the extension size version of the relation
using Ext_Size, as we have for eval,
Extensibella has us start from a derivation of the extension size
version of the relation rather than the relation itself. Thus
what we need to prove here is
forall G T T' Ty n, <eval {ES}> T T' n -> typeOf G T Ty -> <eval {P}> T T'
where n is the extension size of the original
derivation, that is, the number of extension-introduced rules used
in the derivation. We will prove this by induction on the extension
size n and the derivation
of <eval {ES}> T T' n.
The induction on n also requires a second premise,
acc n. The
acc predicate essentially
encodes strong induction on natural numbers by holding for a
number only if it holds for all non-negative integers less than
it.
We start by declaring we are ready to fulfill the proof obligation
for the Ext_Ind for the typeOf relation:
< Prove_Ext_Ind walkthrough:host:eval.
Subgoal 4:
Variables: N G Ty N2 T2 T11 X T1
IH : forall N G T T' Ty,
<eval {ES}> T T' N -> acc N * -> typeOf G T Ty -> <eval {P}> T T'
IH1 : forall N G T T' Ty,
<eval {ES}> T T' N ** -> acc N @ -> typeOf G T Ty -> <eval {P}> T T'
R : <eval {ES}> (let X T1 T2) (let X T11 T2) N @@
Acc : acc N @
Ty : typeOf G (let X T1 T2) Ty
R1 : 1 + N2 = N
R2 : <eval {ES}> T1 T11 N2 **
============================
<eval {P}> (let X T1 T2) (let X T11 T2)
This puts us into the proof case for when <eval
{ES}> is derived using the rule corresponding to
the T-Let-Step rule.
We then analyze acc n to unfold
its definition:
< Acc: case Acc.
Subgoal 4:
Variables: N G Ty N2 T2 T11 X T1
IH : forall N G T T' Ty,
<eval {ES}> T T' N -> acc N * -> typeOf G T Ty -> <eval {P}> T T'
IH1 : forall N G T T' Ty,
<eval {ES}> T T' N ** -> acc N @ -> typeOf G T Ty -> <eval {P}> T T'
R : <eval {ES}> (let X T1 T2) (let X T11 T2) N @@
Ty : typeOf G (let X T1 T2) Ty
R1 : 1 + N2 = N
R2 : <eval {ES}> T1 T11 N2 **
Acc : forall M, 0 <= M -> M < N -> acc M *
============================
<eval {P}> (let X T1 T2) (let X T11 T2)
This gives us a way to build a derivation
of acc suitable for use with the
inductive hypothesis, as seen by the * annotation on
its unfolded conclusion. We can use
the unfold tactic to see the
definition of <eval {P}> (let X
T1 T2) (let X T11 T2), and thus what we need to prove:
< unfold.
Subgoal 4:
Variables: N G Ty N2 T2 T11 X T1
IH : forall N G T T' Ty,
<eval {ES}> T T' N -> acc N * -> typeOf G T Ty -> <eval {P}> T T'
IH1 : forall N G T T' Ty,
<eval {ES}> T T' N ** -> acc N @ -> typeOf G T Ty -> <eval {P}> T T'
R : <eval {ES}> (let X T1 T2) (let X T11 T2) N @@
Ty : typeOf G (let X T1 T2) Ty
R1 : 1 + N2 = N
R2 : <eval {ES}> T1 T11 N2 **
Acc : forall M, 0 <= M -> M < N -> acc M *
============================
exists Ctx T_T T3,
<eval {P}> T1 T11 /\ (Ctx |{tm}- let X T1 T2 ~~> T_T /\ <eval {P}> T_T T3)
We see the first conjunct in the conclusion are those for the
premises of the E-Let-Step evaluation rule and the others are
for the stand-in rule, but now using the projection
version of the relation. Then we need to show the
original let projects, that its projection evaluates,
and that each of the premises can be turned into its
projection version.
We start with showing the projection exists. This requires a
typing derivation for T1, which we can get by
breaking down the typing derivation:
< Ty: case Ty.
Subgoal 4:
Variables: N G Ty N2 T2 T11 X T1 Ty1
IH : forall N G T T' Ty,
<eval {ES}> T T' N -> acc N * -> typeOf G T Ty -> <eval {P}> T T'
IH1 : forall N G T T' Ty,
<eval {ES}> T T' N ** -> acc N @ -> typeOf G T Ty -> <eval {P}> T T'
R : <eval {ES}> (let X T1 T2) (let X T11 T2) N @@
R1 : 1 + N2 = N
R2 : <eval {ES}> T1 T11 N2 **
Acc : forall M, 0 <= M -> M < N -> acc M *
Ty : typeOf G T1 Ty1
Ty1 : typeOf ((X, Ty1)::G) T2 Ty
============================
exists Ctx T_T T3,
<eval {P}> T1 T11 /\ (Ctx |{tm}- let X T1 T2 ~~> T_T /\ <eval {P}> T_T T3)
< assert G |{tm}- let X T1 T2 ~~> app (abs X Ty1 T2) T1.
Subgoal 4:
Variables: N G Ty N2 T2 T11 X T1 Ty1
IH : forall N G T T' Ty,
<eval {ES}> T T' N -> acc N * -> typeOf G T Ty -> <eval {P}> T T'
IH1 : forall N G T T' Ty,
<eval {ES}> T T' N ** -> acc N @ -> typeOf G T Ty -> <eval {P}> T T'
R : <eval {ES}> (let X T1 T2) (let X T11 T2) N @@
R1 : 1 + N2 = N
R2 : <eval {ES}> T1 T11 N2 **
Acc : forall M, 0 <= M -> M < N -> acc M *
Ty : typeOf G T1 Ty1
Ty1 : typeOf ((X, Ty1)::G) T2 Ty
H1 : G |{tm}- let X T1 T2 ~~> app (abs X Ty1 T2) T1
============================
exists Ctx T_T T3,
<eval {P}> T1 T11 /\ (Ctx |{tm}- let X T1 T2 ~~> T_T /\ <eval {P}> T_T T3)
The other portions of the conclusion are related, as evaluating the
projection ultimately requires the same premises as
the E-Let-Step rule. These will require using the
inductive hypothesis, which will in turn require a derivation of
acc for N2.
We start by building a derivation
of is_integer for N2. We can use
the ext_size_is_int_eval
property, also introduced by
the Ext_Size declaration but
which the user does not need to prove, as it can be proven
automatically.
< IsN2: apply ext_size_is_int_typeOf to R2.
Subgoal 4:
Variables: N G Ty N2 T2 T11 X T1 Ty1
IH : forall N G T T' Ty,
<eval {ES}> T T' N -> acc N * -> typeOf G T Ty -> <eval {P}> T T'
IH1 : forall N G T T' Ty,
<eval {ES}> T T' N ** -> acc N @ -> typeOf G T Ty -> <eval {P}> T T'
R : <eval {ES}> (let X T1 T2) (let X T11 T2) N @@
R1 : 1 + N2 = N
R2 : <eval {ES}> T1 T11 N2 **
Acc : forall M, 0 <= M -> M < N -> acc M *
Ty : typeOf G T1 Ty1
Ty1 : typeOf ((X, Ty1)::G) T2 Ty
H1 : G |{tm}- let X T1 T2 ~~> app (abs X Ty1 T2) T1
IsN2 : is_integer N2
============================
exists Ctx T_T T3,
<eval {P}> T1 T11 /\ (Ctx |{tm}- let X T1 T2 ~~> T_T /\ <eval {P}> T_T T3)
We can now use an Extensibella standard library property to
show N2 < N:
< L: apply lt_plus_one to R1 _.
Subgoal 4:
Variables: N G Ty N2 T2 T11 X T1 Ty1
IH : forall N G T T' Ty,
<eval {ES}> T T' N -> acc N * -> typeOf G T Ty -> <eval {P}> T T'
IH1 : forall N G T T' Ty,
<eval {ES}> T T' N ** -> acc N @ -> typeOf G T Ty -> <eval {P}> T T'
R : <eval {ES}> (let X T1 T2) (let X T11 T2) N @@
R1 : 1 + N2 = N
R2 : <eval {ES}> T1 T11 N2 **
Acc : forall M, 0 <= M -> M < N -> acc M *
Ty : typeOf G T1 Ty1
Ty1 : typeOf ((X, Ty1)::G) T2 Ty
H1 : G |{tm}- let X T1 T2 ~~> app (abs X Ty1 T2) T1
IsN2 : is_integer N2
L : N2 < N
============================
exists Ctx T_T T3,
<eval {P}> T1 T11 /\ (Ctx |{tm}- let X T1 T2 ~~> T_T /\ <eval {P}> T_T T3)
To show N2 is at least
zero, a requirement for acc, we
can use another property declared and automatically proven by
Ext_Size:
< PosN2: apply ext_size_pos_typeOf to R2.
Subgoal 4:
Variables: N G Ty N2 T2 T11 X T1 Ty1
IH : forall N G T T' Ty,
<eval {ES}> T T' N -> acc N * -> typeOf G T Ty -> <eval {P}> T T'
IH1 : forall N G T T' Ty,
<eval {ES}> T T' N ** -> acc N @ -> typeOf G T Ty -> <eval {P}> T T'
R : <eval {ES}> (let X T1 T2) (let X T11 T2) N @@
R1 : 1 + N2 = N
R2 : <eval {ES}> T1 T11 N2 **
Acc : forall M, 0 <= M -> M < N -> acc M *
Ty : typeOf G T1 Ty1
Ty1 : typeOf ((X, Ty1)::G) T2 Ty
H1 : G |{tm}- let X T1 T2 ~~> app (abs X Ty1 T2) T1
IsN2 : is_integer N2
L : N2 < N
PosN2 : 0 <= N2
============================
exists Ctx T_T T3,
<eval {P}> T1 T11 /\ (Ctx |{tm}- let X T1 T2 ~~> T_T /\ <eval {P}> T_T T3)
We can now build a derivation of acc N2:
< A: apply Acc to PosN2 L.
Subgoal 4:
Variables: N G Ty N2 T2 T11 X T1 Ty1
IH : forall N G T T' Ty,
<eval {ES}> T T' N -> acc N * -> typeOf G T Ty -> <eval {P}> T T'
IH1 : forall N G T T' Ty,
<eval {ES}> T T' N ** -> acc N @ -> typeOf G T Ty -> <eval {P}> T T'
R : <eval {ES}> (let X T1 T2) (let X T11 T2) N @@
R1 : 1 + N2 = N
R2 : <eval {ES}> T1 T11 N2 **
Acc : forall M, 0 <= M -> M < N -> acc M *
Ty : typeOf G T1 Ty1
Ty1 : typeOf ((X, Ty1)::G) T2 Ty
H1 : G |{tm}- let X T1 T2 ~~> app (abs X Ty1 T2) T1
IsN2 : is_integer N2
L : N2 < N
PosN2 : 0 <= N2
A : acc N2 *
============================
exists Ctx T_T T3,
<eval {P}> T1 T11 /\ (Ctx |{tm}- let X T1 T2 ~~> T_T /\ <eval {P}> T_T T3)
Using this, we can use the induction hypothesis to get a
derivation of <eval {P}> for T1:
< apply IH to R2 A Ty.
Subgoal 4:
Variables: N G Ty N2 T2 T11 X T1 Ty1
IH : forall N G T T' Ty,
<eval {ES}> T T' N -> acc N * -> typeOf G T Ty -> <eval {P}> T T'
IH1 : forall N G T T' Ty,
<eval {ES}> T T' N ** -> acc N @ -> typeOf G T Ty -> <eval {P}> T T'
R : <eval {ES}> (let X T1 T2) (let X T11 T2) N @@
R1 : 1 + N2 = N
R2 : <eval {ES}> T1 T11 N2 **
Acc : forall M, 0 <= M -> M < N -> acc M *
Ty : typeOf G T1 Ty1
Ty1 : typeOf ((X, Ty1)::G) T2 Ty
H1 : G |{tm}- let X T1 T2 ~~> app (abs X Ty1 T2) T1
IsN2 : is_integer N2
L : N2 < N
PosN2 : 0 <= N2
A : acc N2 *
H2 : <eval {P}> T1 T11
============================
exists Ctx T_T T3,
<eval {P}> T1 T11 /\ (Ctx |{tm}- let X T1 T2 ~~> T_T /\ <eval {P}> T_T T3)
This new assumption is what we need to complete the derivations, so we can finish the proof case:
< search.
Subgoal 5:
Variables: G T' Ty T2 T1 X
IH : forall N G T T' Ty,
<eval {ES}> T T' N -> acc N * -> typeOf G T Ty -> <eval {P}> T T'
IH1 : forall N G T T' Ty,
<eval {ES}> T T' N ** -> acc N @ -> typeOf G T Ty -> <eval {P}> T T'
R : <eval {ES}> (let X T1 T2) T' 1 @@
Acc : acc 1 @
Ty : typeOf G (let X T1 T2) Ty
R1 : value T1
R2 : subst X T1 T2 T'
============================
<eval {P}> (let X T1 T2) T'
This leaves us with the case for the E-Let-Subst
case. Because this rule does not have any evaluation premises,
only value and subst, its proof is
similar but simpler:
< unfold.
Subgoal 5:
Variables: G T' Ty T2 T1 X
IH : forall N G T T' Ty,
<eval {ES}> T T' N -> acc N * -> typeOf G T Ty -> <eval {P}> T T'
IH1 : forall N G T T' Ty,
<eval {ES}> T T' N ** -> acc N @ -> typeOf G T Ty -> <eval {P}> T T'
R : <eval {ES}> (let X T1 T2) T' 1 @@
Acc : acc 1 @
Ty : typeOf G (let X T1 T2) Ty
R1 : value T1
R2 : subst X T1 T2 T'
============================
exists Ctx T_T T3,
(value T1 /\ subst X T1 T2 T') /\
(Ctx |{tm}- let X T1 T2 ~~> T_T /\ <eval {P}> T_T T3)
< Ty: case Ty.
Subgoal 5:
Variables: G T' Ty T2 T1 X Ty1
IH : forall N G T T' Ty,
<eval {ES}> T T' N -> acc N * -> typeOf G T Ty -> <eval {P}> T T'
IH1 : forall N G T T' Ty,
<eval {ES}> T T' N ** -> acc N @ -> typeOf G T Ty -> <eval {P}> T T'
R : <eval {ES}> (let X T1 T2) T' 1 @@
Acc : acc 1 @
R1 : value T1
R2 : subst X T1 T2 T'
Ty : typeOf G T1 Ty1
Ty1 : typeOf ((X, Ty1)::G) T2 Ty
============================
exists Ctx T_T T3,
(value T1 /\ subst X T1 T2 T') /\
(Ctx |{tm}- let X T1 T2 ~~> T_T /\ <eval {P}> T_T T3)
< assert G |{tm}- let X T1 T2 ~~> app (abs X Ty1 T2) T1.
Subgoal 5:
Variables: G T' Ty T2 T1 X Ty1
IH : forall N G T T' Ty,
<eval {ES}> T T' N -> acc N * -> typeOf G T Ty -> <eval {P}> T T'
IH1 : forall N G T T' Ty,
<eval {ES}> T T' N ** -> acc N @ -> typeOf G T Ty -> <eval {P}> T T'
R : <eval {ES}> (let X T1 T2) T' 1 @@
Acc : acc 1 @
R1 : value T1
R2 : subst X T1 T2 T'
Ty : typeOf G T1 Ty1
Ty1 : typeOf ((X, Ty1)::G) T2 Ty
H1 : G |{tm}- let X T1 T2 ~~> app (abs X Ty1 T2) T1
============================
exists Ctx T_T T3,
(value T1 /\ subst X T1 T2 T') /\
(Ctx |{tm}- let X T1 T2 ~~> T_T /\ <eval {P}> T_T T3)
< search.
Proof completed.
Our other extension does not introduce any new syntax, only defining a new relation for big-step evaluation.
[Reduce File]
Module walkthrough:big_step
Builds on walkthrough:host
Judgment big_step : tm* tm
value T
------------ [Big-End]
big_step T T
eval T T1
big_step T1 T2
-------------- [Big-Step]
big_step T T2
[] |{tm}- T ~~> T_T
big_step T_T T1
------------------- [Big-D]*
big_step T T1
The big-step evaluation defined here is a bit odd, but we make it
so to make our example property easier to understand, making the
focus on the aspects of proving an extension-introduced property
rather than the specific property. The oddness here is that we
may step through multiple small-step evaluation steps
(eval steps) or we may project away any extension
syntax and step through the evaluation of its projection.
We can compile this for Extensibella as we did for the others:
$ sterling --extensibella walkthrough:big_step
The Extensibella proofs for the big step extension can be
found in the big_step/big_step.xthm file, reproduced
here:
Module walkthrough:big_step.
Prove walkthrough:host:typeOf_unique.
Prove walkthrough:host:ty_lookup.
Prove walkthrough:host:subst_type_preservation.
Prove walkthrough:host:type_preservation.
Prove_Constraint walkthrough:host:proj_type_same.
Add_Ext_Size walkthrough:host:eval.
Add_Proj_Rel walkthrough:host:eval.
Prove_Ext_Ind walkthrough:host:eval.
Extensible_Theorem
big_step_type_preservation : forall T Ty T',
Ty : typeOf [] T Ty ->
Big : big_step T T' ->
typeOf [] T' Ty
on Big. [Show Proof]
As we saw with the let extension, Extensibella knows
the walkthrough:big_step module builds on the host
language and thus expects the
Prove version of each extensible theorem
from the host language. Unlike in the let extension, the big step
extension does not introduce any new syntax or new rules for the
key relations of these theorems, and thus has nothing new to
prove for them. However, Extensibella still requires the
Prove declarations for two
reasons. First, it does not check whether there are new
rules until the Prove
declaration. Second, declaring the imported theorems makes it
clear where new theorems, such as
big_step_type_preservation,
belong in the order and what existing theorems they may use as
lemmas and, in more complex examples, what host properties may use
them as lemmas in the new proofs. We see this use of
existing properties as lemmas in proving a new theorem in the
proof of big_step_type_preservation, as we use
both the type_preservation
theorem and proj_type_same
projection constraint from the host language as lemmas.
The new
big_step_type_preservation
theorem in this extension is also declared using the
Extensible_Theorem keyword, just
like the host language's theorems, with its key relation
being the new big_step relation it introduces.
< Extensible_Theorem
big_step_type_preservation : forall T Ty T',
Ty : typeOf [] T Ty ->
Big : big_step T T' ->
typeOf [] T' Ty
on Big.
Subgoal 1:
Variables: Ty T'
IH : forall T Ty T', typeOf [] T Ty -> big_step T T' * -> typeOf [] T' Ty
Ty : typeOf [] T' Ty
Big : big_step T' T' @
Big1 : value T'
============================
typeOf [] T' Ty
Unlike the properties from the host language, there are two
extension points here. One is that new extensions may build on
this one and add new rules for it. This is the same as we saw for
the properties from the host language. The other extension point
here is that other extensions may introduce new constructs not
known here, but for which the big_step relation will
hold. We see this with the let extension; the big step extension
does not know the let construct exists, but the
big_step relation will still hold for it in a
composed language including both extensions.
This property has three cases, two for the known
rules Big-End and Big-Step, with the
third being a generic case that can be used for any constructs
from other extensions, such as let. The first one,
into which we drop immediately, is that for when the big-step
evaluation was derived using the Big-End rule. As
there is no evaluation here, the proof is immediate:
< search. Subgoal 2: Variables: T Ty T' T3 IH : forall T Ty T', typeOf [] T Ty -> big_step T T' * -> typeOf [] T' Ty Ty : typeOf [] T Ty Big : big_step T T' @ Big1 : eval T T3 Big2 : big_step T3 T' * ============================ typeOf [] T' Ty
The next case is that for when the big-step evaluation was derived
using the Big-Step rule. Here we can apply the type
preservation property of the host language to find T3
has the same type, then the inductive hypothesis to
find T' has the same type:
< apply type_preservation to Ty Big1.
Subgoal 2:
Variables: T Ty T' T3
IH : forall T Ty T', typeOf [] T Ty -> big_step T T' * -> typeOf [] T' Ty
Ty : typeOf [] T Ty
Big : big_step T T' @
Big1 : eval T T3
Big2 : big_step T3 T' *
H1 : typeOf [] T3 Ty
============================
typeOf [] T' Ty
< apply IH to _ Big2.
Subgoal 2:
Variables: T Ty T' T3
IH : forall T Ty T', typeOf [] T Ty -> big_step T T' * -> typeOf [] T' Ty
Ty : typeOf [] T Ty
Big : big_step T T' @
Big1 : eval T T3
Big2 : big_step T3 T' *
H1 : typeOf [] T3 Ty
H2 : typeOf [] T' Ty
============================
typeOf [] T' Ty
< search.
Subgoal 3:
Variables: Ty T' T_T
IH : forall T Ty T', typeOf [] T Ty -> big_step T T' * -> typeOf [] T' Ty
Ty : typeOf [] <unknown I tm> Ty
Big : big_step <unknown I tm> T' @
Big1 : [] |{tm}- <unknown I tm> ~~> T_T
Big2 : big_step T_T T' *
============================
typeOf [] T' Ty
The final case, which we see as the next goal after
the search tactic completing the
case for Big-Step, is the generic case. Because our
key relation is introduced by this extension, the generic case
uses the default rule introduced by the
module, Big-D, which is instantiated for each
construct introduced by another extension in a composition. For
the generic proof, it is instantiated for a special
term <unknown I tm>
representing this class of terms unknown in the context of
the current module.
Because this generic term is a stand-in for terms introduced by
other modules that will introduce their own semantics, we do not
know how existing relations, such as typeOf, are
defined for it and case analysis is disallowed. If we try, we get
an error message:
< case Ty.
Error: Cannot do case analysis on host extensible relation with unknown primary component
Subgoal 3:
Variables: Ty T' T_T
IH : forall T Ty T', typeOf [] T Ty -> big_step T T' * -> typeOf [] T' Ty
Ty : typeOf [] <unknown I tm> Ty
Big : big_step <unknown I tm> T' @
Big1 : [] |{tm}- <unknown I tm> ~~> T_T
Big2 : big_step T_T T' *
============================
typeOf [] T' Ty
Because case analysis is limited here, we instead rely on
projection constraints and other existing properties to show what
we want about the semantics
of <unknown I tm>. We can
start our proof of this case by using the projection constraint
from the host language to show the projection T_T
has the same type:
< apply proj_type_same to Big1 Ty.
Subgoal 3:
Variables: Ty T' T_T
IH : forall T Ty T', typeOf [] T Ty -> big_step T T' * -> typeOf [] T' Ty
Ty : typeOf [] <unknown I tm> Ty
Big : big_step <unknown I tm> T' @
Big1 : [] |{tm}- <unknown I tm> ~~> T_T
Big2 : big_step T_T T' *
H1 : typeOf [] T_T Ty
============================
typeOf [] T' Ty
This gives us the typing derivation we need for applying the inductive hypothesis, which we can do to complete the proof:
< apply IH to _ Big2.
Subgoal 3:
Variables: Ty T' T_T
IH : forall T Ty T', typeOf [] T Ty -> big_step T T' * -> typeOf [] T' Ty
Ty : typeOf [] <unknown I tm> Ty
Big : big_step <unknown I tm> T' @
Big1 : [] |{tm}- <unknown I tm> ~~> T_T
Big2 : big_step T_T T' *
H1 : typeOf [] T_T Ty
H2 : typeOf [] T' Ty
============================
typeOf [] T' Ty
< search.
Proof completed.
If an extension-introduced property is proven using a relation
from the host language as its key relation, instead of an
extension-introduced relation as we used here, the ideas behind
the proof will be similar. However, instead of the default rule
given by the module instantiated for the generic
term <unknown I tm> as the
rule giving rise to the case, it will have the stand-in rule given
by the host language instantiated for a generic
constructor <unknown K tm>
as the rule giving rise to the case.
Once each extension has completed its proofs, we know any composed language will have all properties introduced by all modules included in the composition. We can check this for a composition by using Extensibella to build a composed Abella proof for all the properties.
To build a composition, we need a Sterling module that composes
all the pieces. Make a directory named composed as a
sibling of the host, let,
and big_step directories, and put the following in a
file named composed.sos in it:
Module walkthrough:composed Builds on walkthrough:host Builds on walkthrough:let Builds on walkthrough:big_step
We will need to compile this twice, once for a regular Extensibella proof, the same way we have compiled the others, and once for the Extensibella composition, as these have slightly different requirements.
$ sterling --extensibella walkthrough:composed $ sterling --extensibellaFull walkthrough:composed
We also need to create an Extensibella file for the composed module. This is necessary for Extensibella to know what properties the modules in the composition add, if any. We can have Extensibella generate the file for us. To do this, we need to compile the files for the let and big step extensions so Extensibella knows what properties they add and the order in which they add them:
$ extensibella --compile walkthrough/let/let.xthm $ extensibella --compile walkthrough/big_step/big_step.xthm $ extensibella --generate walkthrough:composed walkthrough/composed/composed.xthmcomposed.xthm [Reduce File]
Module walkthrough:composed. Prove walkthrough:host:typeOf_unique. Prove walkthrough:host:ty_lookup. Prove walkthrough:host:subst_type_preservation. Prove walkthrough:host:type_preservation. Prove_Constraint walkthrough:host:proj_type_same. Add_Ext_Size walkthrough:host:eval. Add_Proj_Rel walkthrough:host:eval. Prove_Ext_Ind walkthrough:host:eval. Prove walkthrough:big_step:big_step_type_preservation.
When we generate the Extensibella file for the
walkthrough:composed module, Extensibella takes the
property orders from each module on which it builds and combines
them to form an order containing all the properties from all the
modules. This composed order maintains the order from each module
individually, so each use of a property as a lemma will still be
valid in the composition.
We now have all the pieces necessary to have Extensibella build the composition. To do so, we give the name of the file to be output, along with the module for which we are building the composition, and all the proof files for the modules included in the composition:
$ extensibella --compose walkthrough/out.thm walkthrough:composed walkthrough/host/host.xthm walkthrough/let/let.xthm walkthrough/big_step/big_step.xthm walkthrough/composed/composed.xthm path/to/sterling/stdLib/stdLib.xthmNote we need to include the Extensibella proof file for the Sterling standard library as well, since the standard library is included in all Sterling modules. Extensibella does not treat the Sterling standard library module specially, so its properties, which are all non-extensible, are also included in the Extensibella modules using them and their proofs are needed for the composition.
The produced Abella file, out.thm in our example,
contains the Abella specification of the language and Abella
proofs of each property from any module in the composition. We
show here a version of it edited for white space to fit better in
the page.
/******************************************************************** Extensibella Standard Library ********************************************************************/ Kind $lib__bool type. Kind $lib__nat type. Kind $lib__pair type -> type -> type. Import "/path/to/extensibella/stdLib/bools". Import "/path/to/extensibella/stdLib/integers". Import "/path/to/extensibella/stdLib/integer_addition". Import "/path/to/extensibella/stdLib/integer_multiplication". Import "/path/to/extensibella/stdLib/integer_division". Import "/path/to/extensibella/stdLib/integer_comparison". Import "/path/to/extensibella/stdLib/lists". Import "/path/to/extensibella/stdLib/strings". Import "/path/to/extensibella/stdLib/pairs". Import "/path/to/extensibella/stdLib/extSize_induction". /******************************************************************** Language Definition ********************************************************************/ Kind $ty__walkthrough-$-host-$-tm type. Kind $ty__walkthrough-$-host-$-ty type. Type walkthrough-$-let-$-let (list $char) -> ($ty__walkthrough-$-host-$-tm) -> ($ty__walkthrough-$-host-$-tm) -> $ty__walkthrough-$-host-$-tm. Type walkthrough-$-host-$-var (list $char) -> $ty__walkthrough-$-host-$-tm. Type walkthrough-$-host-$-abs (list $char) -> ($ty__walkthrough-$-host-$-ty) -> ($ty__walkthrough-$-host-$-tm) -> $ty__walkthrough-$-host-$-tm. Type walkthrough-$-host-$-app ($ty__walkthrough-$-host-$-tm) -> ($ty__walkthrough-$-host-$-tm) -> $ty__walkthrough-$-host-$-tm. Type walkthrough-$-host-$-arrowTy ($ty__walkthrough-$-host-$-ty) -> ($ty__walkthrough-$-host-$-ty) -> $ty__walkthrough-$-host-$-ty. Type walkthrough-$-host-$-intTy $ty__walkthrough-$-host-$-ty. Define $fix__sterling-$-stdLib-$-range : ($lib__integer) -> ($lib__integer) -> (list ($lib__integer)) -> prop by $fix__sterling-$-stdLib-$-range (Low) (High) (nil) := $greater_integer (Low) (High); $fix__sterling-$-stdLib-$-range (Low) (High) ((Low)::(Rest)) := exists PlusOne, ($lesseq_integer (Low) (High)) /\ (($plus_integer ($posInt ($succ ($zero))) (Low) (PlusOne)) /\ ($fix__sterling-$-stdLib-$-range (PlusOne) (High) (Rest))). Define $fix__sterling-$-stdLib-$-take : ($lib__integer) -> (list (Var_A)) -> (list (Var_A)) -> prop by $fix__sterling-$-stdLib-$-take ($posInt ($zero)) (L) (nil); $fix__sterling-$-stdLib-$-take (N) ((X)::(L)) ((X)::(F)) := exists N1, ($plus_integer ($posInt ($succ ($zero))) (N1) (N)) /\ ($fix__sterling-$-stdLib-$-take (N1) (L) (F)). Define $fix__sterling-$-stdLib-$-drop : ($lib__integer) -> (list (Var_A)) -> (list (Var_A)) -> prop by $fix__sterling-$-stdLib-$-drop ($posInt ($zero)) (L) (L); $fix__sterling-$-stdLib-$-drop (N) ((X)::(L)) (R) := exists N1, ($plus_integer ($posInt ($succ ($zero))) (N1) (N)) /\ ($fix__sterling-$-stdLib-$-drop (N1) (L) (R)). Define $fix__sterling-$-stdLib-$-zip : (list (Var_A)) -> (list (Var_B)) -> (list ($lib__pair (Var_A) (Var_B))) -> prop by $fix__sterling-$-stdLib-$-zip (nil) (nil) (nil); $fix__sterling-$-stdLib-$-zip ((A)::(ARest)) ((B)::(BRest)) (($pair_c (A) (B))::(Rest)) := $fix__sterling-$-stdLib-$-zip (ARest) (BRest) (Rest). Define $fix__sterling-$-stdLib-$-values : (list ($lib__pair (Var_A) (Var_B))) -> (list (Var_B)) -> prop by $fix__sterling-$-stdLib-$-values (nil) (nil); $fix__sterling-$-stdLib-$-values (($pair_c (A) (B))::(Rest)) ((B)::(VRest)) := $fix__sterling-$-stdLib-$-values (Rest) (VRest). Define $fix__sterling-$-stdLib-$-domain : (list ($lib__pair (Var_A) (Var_B))) -> (list (Var_A)) -> prop by $fix__sterling-$-stdLib-$-domain (nil) (nil); $fix__sterling-$-stdLib-$-domain (($pair_c (A) (B))::(Rest)) ((A)::(DRest)) := $fix__sterling-$-stdLib-$-domain (Rest) (DRest). Define $fix__sterling-$-stdLib-$-count : (Var_A) -> (list (Var_A)) -> ($lib__integer) -> prop by $fix__sterling-$-stdLib-$-count (X) (nil) ($posInt ($zero)); $fix__sterling-$-stdLib-$-count (X) ((X)::(Rest)) (N1) := exists N, ($fix__sterling-$-stdLib-$-count (X) (Rest) (N)) /\ ($plus_integer ($posInt ($succ ($zero))) (N) (N1)); $fix__sterling-$-stdLib-$-count (X) ((Y)::(Rest)) (N) := (((X) = (Y)) -> (false)) /\ ($fix__sterling-$-stdLib-$-count (X) (Rest) (N)). Define $fix__sterling-$-stdLib-$-select : (Var_Item) -> (list (Var_Item)) -> (list (Var_Item)) -> prop by $fix__sterling-$-stdLib-$-select (Item) (Rest) ((Item)::(Rest)); $fix__sterling-$-stdLib-$-select (Item) ((I)::(L1)) ((I)::(L2)) := $fix__sterling-$-stdLib-$-select (Item) (L1) (L2). Define $fix__sterling-$-stdLib-$-permutation : (list (Var_A)) -> (list (Var_A)) -> prop by $fix__sterling-$-stdLib-$-permutation (nil) (nil); $fix__sterling-$-stdLib-$-permutation ((A)::(Rest)) (L) := exists L2, ($fix__sterling-$-stdLib-$-select (A) (L2) (L)) /\ ($fix__sterling-$-stdLib-$-permutation (Rest) (L2)). Define $fix__sterling-$-stdLib-$-mem : (Var_Item) -> (list (Var_Item)) -> prop by $fix__sterling-$-stdLib-$-mem (Item) ((Item)::(Rest)); $fix__sterling-$-stdLib-$-mem (Item) ((I)::(Rest)) := $fix__sterling-$-stdLib-$-mem (Item) (Rest). Define $fix__sterling-$-stdLib-$-subset : (list (Var_A)) -> (list (Var_A)) -> prop by $fix__sterling-$-stdLib-$-subset (nil) (L); $fix__sterling-$-stdLib-$-subset ((X)::(Rest)) (Supset) := ($fix__sterling-$-stdLib-$-mem (X) (Supset)) /\ ($fix__sterling-$-stdLib-$-subset (Rest) (Supset)). Define $fix__sterling-$-stdLib-$-not_mem : (Var_Item) -> (list (Var_Item)) -> prop by $fix__sterling-$-stdLib-$-not_mem (Item) (nil); $fix__sterling-$-stdLib-$-not_mem (Item) ((I)::(Rest)) := (((I) = (Item)) -> (false)) /\ ($fix__sterling-$-stdLib-$-not_mem (Item) (Rest)). Define $fix__sterling-$-stdLib-$-no_lookup : (list ($lib__pair (Var_Key) (Var_Item))) -> (Var_Key) -> prop by $fix__sterling-$-stdLib-$-no_lookup (nil) (Key); $fix__sterling-$-stdLib-$-no_lookup (($pair_c (K) (V))::(Rest)) (Key) := (((K) = (Key)) -> (false)) /\ ($fix__sterling-$-stdLib-$-no_lookup (Rest) (Key)). Define $fix__sterling-$-stdLib-$-lookup : (list ($lib__pair (Var_Key) (Var_Item))) -> (Var_Key) -> (Var_Item) -> prop by $fix__sterling-$-stdLib-$-lookup (($pair_c (Key) (Value))::(Rest)) (Key) (Value); $fix__sterling-$-stdLib-$-lookup (($pair_c (K) (V))::(Rest)) (Key) (Value) := (((K) = (Key)) -> (false)) /\ ($fix__sterling-$-stdLib-$-lookup (Rest) (Key) (Value)). Define $ext__0__walkthrough-$-host-$-is_ty : ($ty__walkthrough-$-host-$-ty) -> prop by $ext__0__walkthrough-$-host-$-is_ty (walkthrough-$-host-$-arrowTy (Ty1) (Ty)) := ($ext__0__walkthrough-$-host-$-is_ty (Ty1)) /\ ($ext__0__walkthrough-$-host-$-is_ty (Ty)); $ext__0__walkthrough-$-host-$-is_ty (walkthrough-$-host-$-intTy). Define $ext__0__walkthrough-$-host-$-is_tm : ($ty__walkthrough-$-host-$-tm) -> prop by $ext__0__walkthrough-$-host-$-is_tm (walkthrough-$-host-$-var (S)) := is_string (S); $ext__0__walkthrough-$-host-$-is_tm (walkthrough-$-host-$-abs (S) (Ty) (Tm)) := (is_string (S)) /\ (($ext__0__walkthrough-$-host-$-is_ty (Ty)) /\ ($ext__0__walkthrough-$-host-$-is_tm (Tm))); $ext__0__walkthrough-$-host-$-is_tm (walkthrough-$-host-$-app (Tm1) (Tm)) := ($ext__0__walkthrough-$-host-$-is_tm (Tm1)) /\ ($ext__0__walkthrough-$-host-$-is_tm (Tm)); $ext__0__walkthrough-$-host-$-is_tm (walkthrough-$-let-$-let (S) (Tm1) (Tm)) := (is_string (S)) /\ (($ext__0__walkthrough-$-host-$-is_tm (Tm1)) /\ ($ext__0__walkthrough-$-host-$-is_tm (Tm))). Define $ext__1__walkthrough-$-host-$-typeOf : (list ($lib__pair (list $char) ($ty__walkthrough-$-host-$-ty))) -> ($ty__walkthrough-$-host-$-tm) -> ($ty__walkthrough-$-host-$-ty) -> prop by $ext__1__walkthrough-$-host-$-typeOf (Ctx) (walkthrough-$-host-$-var (X)) (Ty) := $fix__sterling-$-stdLib-$-lookup (Ctx) (X) (Ty); $ext__1__walkthrough-$-host-$-typeOf (Ctx) (walkthrough-$-host-$-abs (X) (Ty1) (Body)) (walkthrough-$-host-$-arrowTy (Ty1) (Ty2)) := $ext__1__walkthrough-$-host-$-typeOf (($pair_c (X) (Ty1))::(Ctx)) (Body) (Ty2); $ext__1__walkthrough-$-host-$-typeOf (Ctx) (walkthrough-$-host-$-app (T1) (T2)) (Ty2) := exists Ty1, ($ext__1__walkthrough-$-host-$-typeOf (Ctx) (T1) (walkthrough-$-host-$-arrowTy (Ty1) (Ty2))) /\ ($ext__1__walkthrough-$-host-$-typeOf (Ctx) (T2) (Ty1)); $ext__1__walkthrough-$-host-$-typeOf (Ctx) (walkthrough-$-let-$-let (X) (T1) (T2)) (Ty2) := exists Ty1, ($ext__1__walkthrough-$-host-$-typeOf (Ctx) (T1) (Ty1)) /\ ($ext__1__walkthrough-$-host-$-typeOf (($pair_c (X) (Ty1))::(Ctx)) (T2) (Ty2)). Define $ext__0__walkthrough-$-host-$-value : ($ty__walkthrough-$-host-$-tm) -> prop by $ext__0__walkthrough-$-host-$-value (walkthrough-$-host-$-abs (X) (Ty) (T)). Define $ext__2__walkthrough-$-host-$-subst : (list $char) -> ($ty__walkthrough-$-host-$-tm) -> ($ty__walkthrough-$-host-$-tm) -> ($ty__walkthrough-$-host-$-tm) -> prop by $ext__2__walkthrough-$-host-$-subst (X) (R) (walkthrough-$-host-$-var (Y)) (walkthrough-$-host-$-var (Y)) := ((X) = (Y)) -> (false); $ext__2__walkthrough-$-host-$-subst (X) (R) (walkthrough-$-host-$-var (X)) (R); $ext__2__walkthrough-$-host-$-subst (X) (R) (walkthrough-$-host-$-abs (Y) (Ty) (B)) (walkthrough-$-host-$-abs (Y) (Ty) (S)) := (((X) = (Y)) -> (false)) /\ ($ext__2__walkthrough-$-host-$-subst (X) (R) (B) (S)); $ext__2__walkthrough-$-host-$-subst (X) (R) (walkthrough-$-host-$-abs (X) (Ty) (B)) (walkthrough-$-host-$-abs (X) (Ty) (B)); $ext__2__walkthrough-$-host-$-subst (X) (R) (walkthrough-$-host-$-app (T1) (T2)) (walkthrough-$-host-$-app (S1) (S2)) := ($ext__2__walkthrough-$-host-$-subst (X) (R) (T1) (S1)) /\ ($ext__2__walkthrough-$-host-$-subst (X) (R) (T2) (S2)); $ext__2__walkthrough-$-host-$-subst (X) (R) (walkthrough-$-let-$-let (Y) (T1) (T2)) (walkthrough-$-let-$-let (Y) (S1) (S2)) := (((X) = (Y)) -> (false)) /\ (($ext__2__walkthrough-$-host-$-subst (X) (R) (T1) (S1)) /\ ($ext__2__walkthrough-$-host-$-subst (X) (R) (T2) (S2))); $ext__2__walkthrough-$-host-$-subst (X) (R) (walkthrough-$-let-$-let (X) (T1) (T2)) (walkthrough-$-let-$-let (X) (S1) (T2)) := $ext__2__walkthrough-$-host-$-subst (X) (R) (T1) (S1). Define $ext__0__walkthrough-$-host-$-eval : ($ty__walkthrough-$-host-$-tm) -> ($ty__walkthrough-$-host-$-tm) -> prop by $ext__0__walkthrough-$-host-$-eval (walkthrough-$-host-$-app (T1) (T2)) (walkthrough-$-host-$-app (T11) (T2)) := $ext__0__walkthrough-$-host-$-eval (T1) (T11); $ext__0__walkthrough-$-host-$-eval (walkthrough-$-host-$-app (T1) (T2)) (walkthrough-$-host-$-app (T1) (T21)) := ($ext__0__walkthrough-$-host-$-value (T1)) /\ ($ext__0__walkthrough-$-host-$-eval (T2) (T21)); $ext__0__walkthrough-$-host-$-eval (walkthrough-$-host-$-app (walkthrough-$-host-$-abs (X) (Ty) (Body)) (T2)) (V) := ($ext__0__walkthrough-$-host-$-value (T2)) /\ ($ext__2__walkthrough-$-host-$-subst (X) (T2) (Body) (V)); $ext__0__walkthrough-$-host-$-eval (walkthrough-$-let-$-let (X) (T1) (T2)) (walkthrough-$-let-$-let (X) (T11) (T2)) := $ext__0__walkthrough-$-host-$-eval (T1) (T11); $ext__0__walkthrough-$-host-$-eval (walkthrough-$-let-$-let (X) (T1) (T2)) (V) := ($ext__0__walkthrough-$-host-$-value (T1)) /\ ($ext__2__walkthrough-$-host-$-subst (X) (T1) (T2) (V)). Define $proj__walkthrough-$-host-$-ty : ($ty__walkthrough-$-host-$-ty) -> ($ty__walkthrough-$-host-$-ty) -> prop by $proj__walkthrough-$-host-$-ty (X257) (X258) := false. Define $proj__walkthrough-$-host-$-tm : (list ($lib__pair (list $char) ($ty__walkthrough-$-host-$-ty))) -> ($ty__walkthrough-$-host-$-tm) -> ($ty__walkthrough-$-host-$-tm) -> prop by $proj__walkthrough-$-host-$-tm (Ctx) (walkthrough-$-let-$-let (X) (T1) (T2)) (walkthrough-$-host-$-app (walkthrough-$-host-$-abs (X) (Ty) (T2)) (T1)) := $ext__1__walkthrough-$-host-$-typeOf (Ctx) (T1) (Ty). Define $ext__0__walkthrough-$-big_step-$-big_step : ($ty__walkthrough-$-host-$-tm) -> ($ty__walkthrough-$-host-$-tm) -> prop by $ext__0__walkthrough-$-big_step-$-big_step (T) (T) := $ext__0__walkthrough-$-host-$-value (T); $ext__0__walkthrough-$-big_step-$-big_step (T) (T2) := exists T1, ($ext__0__walkthrough-$-host-$-eval (T) (T1)) /\ ($ext__0__walkthrough-$-big_step-$-big_step (T1) (T2)); $ext__0__walkthrough-$-big_step-$-big_step (walkthrough-$-let-$-let (S) (Tm1) (Tm)) (T1) := exists T_T, ($proj__walkthrough-$-host-$-tm (nil) (walkthrough-$-let-$-let (S) (Tm1) (Tm)) (T_T)) /\ ($ext__0__walkthrough-$-big_step-$-big_step (T_T) (T1)). %Stand-In Rules Define $stand-in_rule__$ext__0__walkthrough-$-big_step-$-big_step : ($ty__walkthrough-$-host-$-tm) -> ($ty__walkthrough-$-host-$-tm) -> prop by $stand-in_rule__$ext__0__walkthrough-$-big_step-$-big_step (A1) (A2). Define $stand-in_rule__$ext__0__walkthrough-$-host-$-is_tm : ($ty__walkthrough-$-host-$-tm) -> prop by $stand-in_rule__$ext__0__walkthrough-$-host-$-is_tm (X) := exists A1 X_T, ($proj__walkthrough-$-host-$-tm (A1) (X) (X_T)) /\ ($ext__0__walkthrough-$-host-$-is_tm (X_T)). Define $stand-in_rule__$ext__0__walkthrough-$-host-$-is_ty : ($ty__walkthrough-$-host-$-ty) -> prop by $stand-in_rule__$ext__0__walkthrough-$-host-$-is_ty (X) := exists X_T, ($proj__walkthrough-$-host-$-ty (X) (X_T)) /\ ($ext__0__walkthrough-$-host-$-is_ty (X_T)). Define $stand-in_rule__$ext__1__walkthrough-$-host-$-typeOf : (list ($lib__pair (list $char) ($ty__walkthrough-$-host-$-ty))) -> ($ty__walkthrough-$-host-$-tm) -> ($ty__walkthrough-$-host-$-ty) -> prop by $stand-in_rule__$ext__1__walkthrough-$-host-$-typeOf (Ctx) (T) (Ty) := exists T_T, ($proj__walkthrough-$-host-$-tm (Ctx) (T) (T_T)) /\ ($ext__1__walkthrough-$-host-$-typeOf (Ctx) (T_T) (Ty)). Define $stand-in_rule__$ext__0__walkthrough-$-host-$-eval : ($ty__walkthrough-$-host-$-tm) -> ($ty__walkthrough-$-host-$-tm) -> prop by $stand-in_rule__$ext__0__walkthrough-$-host-$-eval (A1) (A2). Define $stand-in_rule__$ext__2__walkthrough-$-host-$-subst : (list $char) -> ($ty__walkthrough-$-host-$-tm) -> ($ty__walkthrough-$-host-$-tm) -> ($ty__walkthrough-$-host-$-tm) -> prop by $stand-in_rule__$ext__2__walkthrough-$-host-$-subst (A1) (A2) (A3) (A4). Define $stand-in_rule__$ext__0__walkthrough-$-host-$-value : ($ty__walkthrough-$-host-$-tm) -> prop by $stand-in_rule__$ext__0__walkthrough-$-host-$-value (A1). /******************************************************************** Proof-Level Definitions ********************************************************************/ Define $extSize__walkthrough-$-host-$-eval : $ty__walkthrough-$-host-$-tm -> $ty__walkthrough-$-host-$-tm -> $lib__integer -> prop by $extSize__walkthrough-$-host-$-eval ((walkthrough-$-host-$-app) (T1) (T2)) ((walkthrough-$-host-$-app) (T11) (T2)) (N) := exists N1, (N1 = N) /\ ($extSize__walkthrough-$-host-$-eval (T1) (T11) (N1) ); $extSize__walkthrough-$-host-$-eval ((walkthrough-$-host-$-app) (T1) (T2)) ((walkthrough-$-host-$-app) (T1) (T21)) (N) := exists N1, (N1 = N) /\ (($ext__0__walkthrough-$-host-$-value (T1)) /\ ($extSize__walkthrough-$-host-$-eval (T2) (T21) (N1) )); $extSize__walkthrough-$-host-$-eval ((walkthrough-$-host-$-app) ((walkthrough-$-host-$-abs) (X) (Ty) (Body)) (T2)) (V) (($posInt) ($zero)) := ($ext__0__walkthrough-$-host-$-value (T2)) /\ ($ext__2__walkthrough-$-host-$-subst (X) (T2) (Body) (V)); $extSize__walkthrough-$-host-$-eval ((walkthrough-$-let-$-let) (X) (T1) (T2)) ((walkthrough-$-let-$-let) (X) (T11) (T2)) (N) := exists N1, ($plus_integer (($posInt) (($succ) ($zero))) (N1) (N) ) /\ ($extSize__walkthrough-$-host-$-eval (T1) (T11) (N1) ); $extSize__walkthrough-$-host-$-eval ((walkthrough-$-let-$-let) (X) (T1) (T2)) (V) (($posInt) (($succ) ($zero))) := ($ext__0__walkthrough-$-host-$-value (T1)) /\ ($ext__2__walkthrough-$-host-$-subst (X) (T1) (T2) (V)). Define $projRel__walkthrough-$-host-$-eval : $ty__walkthrough-$-host-$-tm -> $ty__walkthrough-$-host-$-tm -> prop by $projRel__walkthrough-$-host-$-eval ((walkthrough-$-host-$-app) (T1) (T2)) ((walkthrough-$-host-$-app) (T11) (T2)) := $projRel__walkthrough-$-host-$-eval (T1) (T11); $projRel__walkthrough-$-host-$-eval ((walkthrough-$-host-$-app) (T1) (T2)) ((walkthrough-$-host-$-app) (T1) (T21)) := ($ext__0__walkthrough-$-host-$-value (T1)) /\ ($projRel__walkthrough-$-host-$-eval (T2) (T21)); $projRel__walkthrough-$-host-$-eval ((walkthrough-$-host-$-app) ((walkthrough-$-host-$-abs) (X) (Ty) (Body)) (T2)) (V) := ($ext__0__walkthrough-$-host-$-value (T2)) /\ ($ext__2__walkthrough-$-host-$-subst (X) (T2) (Body) (V)); $projRel__walkthrough-$-host-$-eval ((walkthrough-$-let-$-let) (X) (T1) (T2)) ((walkthrough-$-let-$-let) (X) (T11) (T2)) := exists Ctx T_T T3, ($projRel__walkthrough-$-host-$-eval (T1) (T11)) /\ (($proj__walkthrough-$-host-$-tm (Ctx) ((walkthrough-$-let-$-let) (X) (T1) (T2)) (T_T)) /\ ($projRel__walkthrough-$-host-$-eval (T_T) (T3))); $projRel__walkthrough-$-host-$-eval ((walkthrough-$-let-$-let) (X) (T1) (T2)) (V) := exists Ctx T_T T3, (($ext__0__walkthrough-$-host-$-value (T1)) /\ ($ext__2__walkthrough-$-host-$-subst (X) (T1) (T2) (V))) /\ (($proj__walkthrough-$-host-$-tm (Ctx) ((walkthrough-$-let-$-let) (X) (T1) (T2)) (T_T)) /\ ($projRel__walkthrough-$-host-$-eval (T_T) (T3))). /******************************************************************** Properties and Proofs ********************************************************************/ /*Start Theorem sterling:stdLib:lookup_unique*/ Theorem sterling-$-stdLib-$-lookup_unique[Key, Value] : forall L (Key : Key) (Value2 : Value) (Value1 : Value), ($fix__sterling-$-stdLib-$-lookup (L) (Key) (Value1)) -> ($fix__sterling-$-stdLib-$-lookup (L) (Key) (Value2)) -> Value1 = Value2. [Show Proof] /*End sterling:stdLib:lookup_unique*/ /*Start Theorem sterling:stdLib:no_lookup*/ Theorem sterling-$-stdLib-$-no_lookup[Key, Value] : forall L (Key : Key) (Value : Value), ($fix__sterling-$-stdLib-$-no_lookup (L) (Key)) -> ($fix__sterling-$-stdLib-$-lookup (L) (Key) (Value)) -> false. [Show Proof] /*End sterling:stdLib:no_lookup*/ /*Start Theorem sterling:stdLib:lookup_eq_or_not*/ Theorem sterling-$-stdLib-$-lookup_eq_or_not[Key, Value] : forall L (A : Key) (B : Key) (VB : Value) (VA : Value), ($fix__sterling-$-stdLib-$-lookup (L) (A) (VA)) -> ($fix__sterling-$-stdLib-$-lookup (L) (B) (VB)) -> (A = B) \/ ((A = B) -> false). [Show Proof] /*End sterling:stdLib:lookup_eq_or_not*/ /*Start Theorem sterling:stdLib:lookup_mem*/ Theorem sterling-$-stdLib-$-lookup_mem[Key, Value] : forall L (Key : Key) (Value : Value), ($fix__sterling-$-stdLib-$-lookup (L) (Key) (Value)) -> $fix__sterling-$-stdLib-$-mem (($pair_c) (Key) (Value)) (L). [Show Proof] /*End sterling:stdLib:lookup_mem*/ /*Start Theorem sterling:stdLib:no_lookup_mem*/ Theorem sterling-$-stdLib-$-no_lookup_mem[Key, Value] : forall L (Key : Key) (Value : Value), ($fix__sterling-$-stdLib-$-no_lookup (L) (Key)) -> ($fix__sterling-$-stdLib-$-mem (($pair_c) (Key) (Value)) (L)) -> false. [Show Proof] /*End sterling:stdLib:no_lookup_mem*/ /*Start Theorem sterling:stdLib:no_lookup_mem_pair*/ Theorem sterling-$-stdLib-$-no_lookup_mem_pair[Key, Value] : forall L (P : $lib__pair Key Value) K, ($fix__sterling-$-stdLib-$-no_lookup (L) (K)) -> ($fix__sterling-$-stdLib-$-mem (P) (L)) -> exists X Y, P = ($pair_c) (X) (Y). [Show Proof] /*End sterling:stdLib:no_lookup_mem_pair*/ /*Start Theorem sterling:stdLib:lookup_select*/ Theorem sterling-$-stdLib-$-lookup_select[Key, Value] : forall L (Key : Key) (Value : Value), ($fix__sterling-$-stdLib-$-lookup (L) (Key) (Value)) -> exists L', $fix__sterling-$-stdLib-$-select (($pair_c) (Key) (Value)) (L') (L). [Show Proof] /*End sterling:stdLib:lookup_select*/ /*Start Theorem sterling:stdLib:no_lookup_select*/ Theorem sterling-$-stdLib-$-no_lookup_select[Key, Value] : forall L (Key : Key) (Value : Value) R, ($fix__sterling-$-stdLib-$-no_lookup (L) (Key)) -> ($fix__sterling-$-stdLib-$-select (($pair_c) (Key) (Value)) (R) (L)) -> false. [Show Proof] /*End sterling:stdLib:no_lookup_select*/ /*Start Theorem sterling:stdLib:select_lookup*/ Theorem sterling-$-stdLib-$-select_lookup[Key, Value] : forall L (Key : Key) (K : Key) (Value : Value) (V : Value) R, ($fix__sterling-$-stdLib-$-lookup (L) (K) (V)) -> ($fix__sterling-$-stdLib-$-select (($pair_c) (Key) (Value)) (R) (L)) -> ((K = Key) -> false) -> $fix__sterling-$-stdLib-$-lookup (R) (K) (V). [Show Proof] /*End sterling:stdLib:select_lookup*/ /*Start Theorem sterling:stdLib:no_lookup_after_select_before*/ Theorem sterling-$-stdLib-$-no_lookup_after_select_before[Key, Value] : forall (Key : Key) (K : Key) (V : Value) Rest L, ($fix__sterling-$-stdLib-$-no_lookup (Rest) (Key)) -> ($fix__sterling-$-stdLib-$-select (($pair_c) (K) (V)) (Rest) (L)) -> ((K = Key) -> false) -> $fix__sterling-$-stdLib-$-no_lookup (L) (Key). [Show Proof] /*End sterling:stdLib:no_lookup_after_select_before*/ /*Start Theorem sterling:stdLib:no_lookup_before_select_after*/ Theorem sterling-$-stdLib-$-no_lookup_before_select_after[Key, Value] : forall (Key : Key) (P : $lib__pair Key Value) Rest L, ($fix__sterling-$-stdLib-$-no_lookup (L) (Key)) -> ($fix__sterling-$-stdLib-$-select (P) (Rest) (L)) -> $fix__sterling-$-stdLib-$-no_lookup (Rest) (Key). [Show Proof] /*End sterling:stdLib:no_lookup_before_select_after*/ /*Start Theorem sterling:stdLib:lookup_after_select_before*/ Theorem sterling-$-stdLib-$-lookup_after_select_before[Key, Value] : forall (K : Key) (Key : Key) (V : Value) (Value : Value) L R, ($fix__sterling-$-stdLib-$-lookup (R) (K) (V)) -> ($fix__sterling-$-stdLib-$-select (($pair_c) (Key) (Value)) (R) (L)) -> ((K = Key) -> false) -> $fix__sterling-$-stdLib-$-lookup (L) (K) (V). [Show Proof] /*End sterling:stdLib:lookup_after_select_before*/ /*Start Theorem sterling:stdLib:mem_select*/ Theorem sterling-$-stdLib-$-mem_select[Item] : forall L (X : Item), ($fix__sterling-$-stdLib-$-mem (X) (L)) -> exists L', $fix__sterling-$-stdLib-$-select (X) (L') (L). [Show Proof] /*End sterling:stdLib:mem_select*/ /*Start Theorem sterling:stdLib:select_mem*/ Theorem sterling-$-stdLib-$-select_mem[Item] : forall L (X : Item) L', ($fix__sterling-$-stdLib-$-select (X) (L') (L)) -> $fix__sterling-$-stdLib-$-mem (X) (L). [Show Proof] /*End sterling:stdLib:select_mem*/ /*Start Theorem sterling:stdLib:mem_after_select_before*/ Theorem sterling-$-stdLib-$-mem_after_select_before[Item] : forall L L' (Y : Item) (X : Item), ($fix__sterling-$-stdLib-$-select (X) (L') (L)) -> ($fix__sterling-$-stdLib-$-mem (Y) (L')) -> $fix__sterling-$-stdLib-$-mem (Y) (L). [Show Proof] /*End sterling:stdLib:mem_after_select_before*/ /*Start Theorem sterling:stdLib:mem_before_select_after*/ Theorem sterling-$-stdLib-$-mem_before_select_after[Item] : forall L L' (Y : Item) (X : Item), ($fix__sterling-$-stdLib-$-select (X) (L') (L)) -> ($fix__sterling-$-stdLib-$-mem (Y) (L)) -> ((X = Y) -> false) -> $fix__sterling-$-stdLib-$-mem (Y) (L'). [Show Proof] /*End sterling:stdLib:mem_before_select_after*/ /*Start Theorem sterling:stdLib:select_comm*/ Theorem sterling-$-stdLib-$-select_comm[Item] : forall L Rest Rest' (Y : Item) (X : Item), ($fix__sterling-$-stdLib-$-select (X) (Rest) (L)) -> ($fix__sterling-$-stdLib-$-select (Y) (Rest') (Rest)) -> exists R, ($fix__sterling-$-stdLib-$-select (Y) (R) (L)) /\ ($fix__sterling-$-stdLib-$-select (X) (Rest') (R)). [Show Proof] /*End sterling:stdLib:select_comm*/ /*Start Theorem sterling:stdLib:mem_append_left*/ Theorem sterling-$-stdLib-$-mem_append_left[A] : forall L1 L2 L (A : A), ($fix__sterling-$-stdLib-$-mem (A) (L1)) -> ($append (L1) (L2) (L)) -> $fix__sterling-$-stdLib-$-mem (A) (L). [Show Proof] /*End sterling:stdLib:mem_append_left*/ /*Start Theorem sterling:stdLib:mem_append_right*/ Theorem sterling-$-stdLib-$-mem_append_right[A] : forall L1 L2 L (A : A), ($fix__sterling-$-stdLib-$-mem (A) (L2)) -> ($append (L1) (L2) (L)) -> $fix__sterling-$-stdLib-$-mem (A) (L). [Show Proof] /*End sterling:stdLib:mem_append_right*/ /*Start Theorem sterling:stdLib:mem_append*/ Theorem sterling-$-stdLib-$-mem_append[A] : forall L1 L2 L (A : A), ($fix__sterling-$-stdLib-$-mem (A) (L)) -> ($append (L1) (L2) (L)) -> ($fix__sterling-$-stdLib-$-mem (A) (L1)) \/ ($fix__sterling-$-stdLib-$-mem (A) (L2)). [Show Proof] /*End sterling:stdLib:mem_append*/ /*Start Theorem sterling:stdLib:not_mem*/ Theorem sterling-$-stdLib-$-not_mem[A] : forall (A : A) L, ($fix__sterling-$-stdLib-$-not_mem (A) (L)) -> ($fix__sterling-$-stdLib-$-mem (A) (L)) -> false. [Show Proof] /*End sterling:stdLib:not_mem*/ /*Start Theorem sterling:stdLib:not_mem_select*/ Theorem sterling-$-stdLib-$-not_mem_select[A] : forall L (A : A) L', ($fix__sterling-$-stdLib-$-not_mem (A) (L)) -> ($fix__sterling-$-stdLib-$-select (A) (L') (L)) -> false. [Show Proof] /*End sterling:stdLib:not_mem_select*/ /*Start Theorem sterling:stdLib:not_mem_after_select_before*/ Theorem sterling-$-stdLib-$-not_mem_after_select_before[A] : forall L L' (Y : A) (X : A), ($fix__sterling-$-stdLib-$-select (X) (L') (L)) -> ($fix__sterling-$-stdLib-$-not_mem (Y) (L')) -> ((X = Y) -> false) -> $fix__sterling-$-stdLib-$-not_mem (Y) (L). [Show Proof] /*End sterling:stdLib:not_mem_after_select_before*/ /*Start Theorem sterling:stdLib:not_mem_before_select_after*/ Theorem sterling-$-stdLib-$-not_mem_before_select_after[A] : forall L L' (Y : A) (X : A), ($fix__sterling-$-stdLib-$-select (X) (L') (L)) -> ($fix__sterling-$-stdLib-$-not_mem (Y) (L)) -> $fix__sterling-$-stdLib-$-not_mem (Y) (L'). [Show Proof] /*End sterling:stdLib:not_mem_before_select_after*/ /*Start Theorem sterling:stdLib:not_mem_append*/ Theorem sterling-$-stdLib-$-not_mem_append[A] : forall L1 L2 L (A : A), ($fix__sterling-$-stdLib-$-not_mem (A) (L1)) -> ($fix__sterling-$-stdLib-$-not_mem (A) (L2)) -> ($append (L1) (L2) (L)) -> $fix__sterling-$-stdLib-$-not_mem (A) (L). [Show Proof] /*End sterling:stdLib:not_mem_append*/ /*Start Theorem sterling:stdLib:not_mem_append_back*/ Theorem sterling-$-stdLib-$-not_mem_append_back[A] : forall L1 L2 L (A : A), ($fix__sterling-$-stdLib-$-not_mem (A) (L)) -> ($append (L1) (L2) (L)) -> ($fix__sterling-$-stdLib-$-not_mem (A) (L1)) /\ ($fix__sterling-$-stdLib-$-not_mem (A) (L2)). [Show Proof] /*End sterling:stdLib:not_mem_append_back*/ /*Start Theorem sterling:stdLib:permutation_mem*/ Theorem sterling-$-stdLib-$-permutation_mem[Item] : forall (L : list Item) (M : list Item) I, ($fix__sterling-$-stdLib-$-permutation (L) (M)) -> ($fix__sterling-$-stdLib-$-mem (I) (L)) -> $fix__sterling-$-stdLib-$-mem (I) (M). [Show Proof] /*End sterling:stdLib:permutation_mem*/ /*Start Theorem sterling:stdLib:perm_lemma*/ Theorem sterling-$-stdLib-$-perm_lemma[Item] : forall A B B' (X : Item), ($fix__sterling-$-stdLib-$-permutation (B') (A)) -> ($fix__sterling-$-stdLib-$-select (X) (B') (B)) -> $fix__sterling-$-stdLib-$-permutation (B) ((X)::(A)). [Show Proof] /*End sterling:stdLib:perm_lemma*/ /*Start Theorem sterling:stdLib:permutation_symmetric*/ Theorem sterling-$-stdLib-$-permutation_symmetric[Item] : forall (M : list Item) (L : list Item), ($fix__sterling-$-stdLib-$-permutation (L) (M)) -> $fix__sterling-$-stdLib-$-permutation (M) (L). [Show Proof] /*End sterling:stdLib:permutation_symmetric*/ /*Start Theorem sterling:stdLib:no_lookup_permutation*/ Theorem sterling-$-stdLib-$-no_lookup_permutation[Key, Value] : forall (L : list ($lib__pair Key Value)) (P : list ($lib__pair Key Value)) (Key : Key), ($fix__sterling-$-stdLib-$-no_lookup (L) (Key)) -> ($fix__sterling-$-stdLib-$-permutation (L) (P)) -> $fix__sterling-$-stdLib-$-no_lookup (P) (Key). [Show Proof] /*End sterling:stdLib:no_lookup_permutation*/ /*Start Theorem sterling:stdLib:count_is_integer*/ Theorem sterling-$-stdLib-$-count_is_integer[Item] : forall (I : Item) L N, ($fix__sterling-$-stdLib-$-count (I) (L) (N)) -> is_integer (N). [Show Proof] /*End sterling:stdLib:count_is_integer*/ /*Start Theorem sterling:stdLib:count_geq_0*/ Theorem sterling-$-stdLib-$-count_geq_0[Item] : forall (I : Item) L N, ($fix__sterling-$-stdLib-$-count (I) (L) (N)) -> $greatereq_integer (N) (($posInt) ($zero)). [Show Proof] /*End sterling:stdLib:count_geq_0*/ /*Start Theorem sterling:stdLib:select_count*/ Theorem sterling-$-stdLib-$-select_count[Item] : forall (I : Item) L Rest N N', ($fix__sterling-$-stdLib-$-count (I) (L) (N)) -> ($fix__sterling-$-stdLib-$-select (I) (Rest) (L)) -> ($minus_integer (N) (($posInt) (($succ) ($zero))) (N')) -> $fix__sterling-$-stdLib-$-count (I) (Rest) (N'). [Show Proof] /*End sterling:stdLib:select_count*/ /*Start Theorem sterling:stdLib:count_select*/ Theorem sterling-$-stdLib-$-count_select[Item] : forall (I : Item) L Rest N' N, ($fix__sterling-$-stdLib-$-count (I) (Rest) (N')) -> ($fix__sterling-$-stdLib-$-select (I) (Rest) (L)) -> ($plus_integer (($posInt) (($succ) ($zero))) (N') (N)) -> $fix__sterling-$-stdLib-$-count (I) (L) (N). [Show Proof] /*End sterling:stdLib:count_select*/ /*Start Theorem sterling:stdLib:select_count_neq*/ Theorem sterling-$-stdLib-$-select_count_neq[Item] : forall (I : Item) (J : Item) L Rest N, ($fix__sterling-$-stdLib-$-count (I) (L) (N)) -> ($fix__sterling-$-stdLib-$-select (J) (Rest) (L)) -> ((I = J) -> false) -> $fix__sterling-$-stdLib-$-count (I) (Rest) (N). [Show Proof] /*End sterling:stdLib:select_count_neq*/ /*Start Theorem sterling:stdLib:count_select_neq*/ Theorem sterling-$-stdLib-$-count_select_neq[Item] : forall (I : Item) (J : Item) L Rest N, ($fix__sterling-$-stdLib-$-count (I) (Rest) (N)) -> ($fix__sterling-$-stdLib-$-select (J) (Rest) (L)) -> ((I = J) -> false) -> $fix__sterling-$-stdLib-$-count (I) (L) (N). [Show Proof] /*End sterling:stdLib:count_select_neq*/ /*Start Theorem sterling:stdLib:count_unique*/ Theorem sterling-$-stdLib-$-count_unique[Item] : forall (I : Item) NA NB L, ($fix__sterling-$-stdLib-$-count (I) (L) (NA)) -> ($fix__sterling-$-stdLib-$-count (I) (L) (NB)) -> NA = NB. [Show Proof] /*End sterling:stdLib:count_unique*/ /*Start Theorem sterling:stdLib:count_mem*/ Theorem sterling-$-stdLib-$-count_mem[Item] : forall (I : Item) N L, ($fix__sterling-$-stdLib-$-count (I) (L) (N)) -> ($greater_integer (N) (($posInt) ($zero))) -> $fix__sterling-$-stdLib-$-mem (I) (L). [Show Proof] /*End sterling:stdLib:count_mem*/ /*Start Theorem sterling:stdLib:count_not_mem*/ Theorem sterling-$-stdLib-$-count_not_mem[Item] : forall (I : Item) L, ($fix__sterling-$-stdLib-$-count (I) (L) (($posInt) ($zero))) -> ($fix__sterling-$-stdLib-$-mem (I) (L)) -> false. [Show Proof] /*End sterling:stdLib:count_not_mem*/ /*Start Theorem sterling:stdLib:count_greater_0*/ Theorem sterling-$-stdLib-$-count_greater_0[Item] : forall (I : Item) L N, ($fix__sterling-$-stdLib-$-count (I) ((I)::(L)) (N)) -> $greater_integer (N) (($posInt) ($zero)). [Show Proof] /*End sterling:stdLib:count_greater_0*/ /*Start Theorem sterling:stdLib:subset_mem*/ Theorem sterling-$-stdLib-$-subset_mem[A] : forall (Sub : list A) (Sup : list A) A, ($fix__sterling-$-stdLib-$-subset (Sub) (Sup)) -> ($fix__sterling-$-stdLib-$-mem (A) (Sub)) -> $fix__sterling-$-stdLib-$-mem (A) (Sup). [Show Proof] /*End sterling:stdLib:subset_mem*/ /*Start Theorem sterling:stdLib:subset_trans*/ Theorem sterling-$-stdLib-$-subset_trans[A] : forall (B : list A) (C : list A) (A : list A), ($fix__sterling-$-stdLib-$-subset (A) (B)) -> ($fix__sterling-$-stdLib-$-subset (B) (C)) -> $fix__sterling-$-stdLib-$-subset (A) (C). [Show Proof] /*End sterling:stdLib:subset_trans*/ /*Start Theorem sterling:stdLib:subset_add_right*/ Theorem sterling-$-stdLib-$-subset_add_right[A] : forall Sub Sup (A : A), ($fix__sterling-$-stdLib-$-subset (Sub) (Sup)) -> $fix__sterling-$-stdLib-$-subset (Sub) ((A)::(Sup)). [Show Proof] /*End sterling:stdLib:subset_add_right*/ /*Start Theorem sterling:stdLib:permutation_counts*/ Theorem sterling-$-stdLib-$-permutation_counts[Item] : forall L P (I : Item) NL NP, ($fix__sterling-$-stdLib-$-permutation (L) (P)) -> ($fix__sterling-$-stdLib-$-count (I) (L) (NL)) -> ($fix__sterling-$-stdLib-$-count (I) (P) (NP)) -> NL = NP. [Show Proof] /*End sterling:stdLib:permutation_counts*/ /*Start Theorem sterling:stdLib:domain_mem*/ Theorem sterling-$-stdLib-$-domain_mem[A, B] : forall L (A : A) (B : B) D, ($fix__sterling-$-stdLib-$-mem (($pair_c) (A) (B)) (L)) -> ($fix__sterling-$-stdLib-$-domain (L) (D)) -> $fix__sterling-$-stdLib-$-mem (A) (D). [Show Proof] /*End sterling:stdLib:domain_mem*/ /*Start Theorem sterling:stdLib:mem_domain*/ Theorem sterling-$-stdLib-$-mem_domain[A, B] : forall (L : list ($lib__pair A B)) A D, ($fix__sterling-$-stdLib-$-domain (L) (D)) -> ($fix__sterling-$-stdLib-$-mem (A) (D)) -> exists B, $fix__sterling-$-stdLib-$-mem (($pair_c) (A) (B)) (L). [Show Proof] /*End sterling:stdLib:mem_domain*/ /*Start Theorem sterling:stdLib:domain_select*/ Theorem sterling-$-stdLib-$-domain_select[A, B] : forall (L : list ($lib__pair A B)) LRest A B D, ($fix__sterling-$-stdLib-$-domain (L) (D)) -> ($fix__sterling-$-stdLib-$-select (($pair_c) (A) (B)) (LRest) (L)) -> exists DRest, ($fix__sterling-$-stdLib-$-select (A) (DRest) (D)) /\ ($fix__sterling-$-stdLib-$-domain (LRest) (DRest)). [Show Proof] /*End sterling:stdLib:domain_select*/ /*Start Theorem sterling:stdLib:domain_unique*/ Theorem sterling-$-stdLib-$-domain_unique[A, B] : forall (L : list ($lib__pair A B)) DA DB, ($fix__sterling-$-stdLib-$-domain (L) (DA)) -> ($fix__sterling-$-stdLib-$-domain (L) (DB)) -> DA = DB. [Show Proof] /*End sterling:stdLib:domain_unique*/ /*Start Theorem sterling:stdLib:values_mem*/ Theorem sterling-$-stdLib-$-values_mem[A, B] : forall L (A : A) (B : B) V, ($fix__sterling-$-stdLib-$-mem (($pair_c) (A) (B)) (L)) -> ($fix__sterling-$-stdLib-$-values (L) (V)) -> $fix__sterling-$-stdLib-$-mem (B) (V). [Show Proof] /*End sterling:stdLib:values_mem*/ /*Start Theorem sterling:stdLib:values_select*/ Theorem sterling-$-stdLib-$-values_select[A, B] : forall (L : list ($lib__pair A B)) LRest A B V, ($fix__sterling-$-stdLib-$-values (L) (V)) -> ($fix__sterling-$-stdLib-$-select (($pair_c) (A) (B)) (LRest) (L)) -> exists VRest, ($fix__sterling-$-stdLib-$-select (B) (VRest) (V)) /\ ($fix__sterling-$-stdLib-$-values (LRest) (VRest)). [Show Proof] /*End sterling:stdLib:values_select*/ /*Start Theorem sterling:stdLib:values_unique*/ Theorem sterling-$-stdLib-$-values_unique[A, B] : forall (L : list ($lib__pair A B)) VA VB, ($fix__sterling-$-stdLib-$-values (L) (VA)) -> ($fix__sterling-$-stdLib-$-values (L) (VB)) -> VA = VB. [Show Proof] /*End sterling:stdLib:values_unique*/ /*Start Theorem sterling:stdLib:zip_unique*/ Theorem sterling-$-stdLib-$-zip_unique[A, B] : forall (L1 : list A) (L2 : list B) LA LB, ($fix__sterling-$-stdLib-$-zip (L1) (L2) (LA)) -> ($fix__sterling-$-stdLib-$-zip (L1) (L2) (LB)) -> LA = LB. [Show Proof] /*End sterling:stdLib:zip_unique*/ /*Start Theorem sterling:stdLib:zip_mem_after*/ Theorem sterling-$-stdLib-$-zip_mem_after[A, B] : forall LA LB (A : A) (B : B) Z, ($fix__sterling-$-stdLib-$-zip (LA) (LB) (Z)) -> ($fix__sterling-$-stdLib-$-mem (($pair_c) (A) (B)) (Z)) -> ($fix__sterling-$-stdLib-$-mem (A) (LA)) /\ ($fix__sterling-$-stdLib-$-mem (B) (LB)). [Show Proof] /*End sterling:stdLib:zip_mem_after*/ /*Start Theorem sterling:stdLib:zip_mem_before1*/ Theorem sterling-$-stdLib-$-zip_mem_before1[A, B] : forall LA (LB : list B) (A : A) Z, ($fix__sterling-$-stdLib-$-zip (LA) (LB) (Z)) -> ($fix__sterling-$-stdLib-$-mem (A) (LA)) -> exists B, $fix__sterling-$-stdLib-$-mem (($pair_c) (A) (B)) (Z). [Show Proof] /*End sterling:stdLib:zip_mem_before1*/ /*Start Theorem sterling:stdLib:zip_mem_before2*/ Theorem sterling-$-stdLib-$-zip_mem_before2[A, B] : forall (LA : list A) LB (B : B) Z, ($fix__sterling-$-stdLib-$-zip (LA) (LB) (Z)) -> ($fix__sterling-$-stdLib-$-mem (B) (LB)) -> exists A, $fix__sterling-$-stdLib-$-mem (($pair_c) (A) (B)) (Z). [Show Proof] /*End sterling:stdLib:zip_mem_before2*/ /*Start Theorem sterling:stdLib:drop_is_integer*/ Theorem sterling-$-stdLib-$-drop_is_integer[A] : forall N (R : list A) (L : list A), ($fix__sterling-$-stdLib-$-drop (N) (L) (R)) -> is_integer (N). [Show Proof] /*End sterling:stdLib:drop_is_integer*/ /*Start Theorem sterling:stdLib:drop_geq_0*/ Theorem sterling-$-stdLib-$-drop_geq_0[A] : forall N (R : list A) (L : list A), ($fix__sterling-$-stdLib-$-drop (N) (L) (R)) -> $greatereq_integer (N) (($posInt) ($zero)). [Show Proof] /*End sterling:stdLib:drop_geq_0*/ /*Start Theorem sterling:stdLib:drop_unique*/ Theorem sterling-$-stdLib-$-drop_unique[A] : forall N (RA : list A) (RB : list A) (L : list A), ($fix__sterling-$-stdLib-$-drop (N) (L) (RA)) -> ($fix__sterling-$-stdLib-$-drop (N) (L) (RB)) -> RA = RB. [Show Proof] /*End sterling:stdLib:drop_unique*/ /*Start Theorem sterling:stdLib:append_drop*/ Theorem sterling-$-stdLib-$-append_drop[A] : forall N (L2 : list A) (L : list A) (L1 : list A), ($append (L1) (L2) (L)) -> (extensibella-$-stdLib-$-length (L1) (N)) -> $fix__sterling-$-stdLib-$-drop (N) (L) (L2). [Show Proof] /*End sterling:stdLib:append_drop*/ /*Start Theorem sterling:stdLib:take_is_integer*/ Theorem sterling-$-stdLib-$-take_is_integer[A] : forall N (F : list A) (L : list A), ($fix__sterling-$-stdLib-$-take (N) (L) (F)) -> is_integer (N). [Show Proof] /*End sterling:stdLib:take_is_integer*/ /*Start Theorem sterling:stdLib:take_geq_0*/ Theorem sterling-$-stdLib-$-take_geq_0[A] : forall N (F : list A) (L : list A), ($fix__sterling-$-stdLib-$-take (N) (L) (F)) -> $greatereq_integer (N) (($posInt) ($zero)). [Show Proof] /*End sterling:stdLib:take_geq_0*/ /*Start Theorem sterling:stdLib:take_unique*/ Theorem sterling-$-stdLib-$-take_unique[A] : forall N (RA : list A) (RB : list A) (L : list A), ($fix__sterling-$-stdLib-$-take (N) (L) (RA)) -> ($fix__sterling-$-stdLib-$-take (N) (L) (RB)) -> RA = RB. [Show Proof] /*End sterling:stdLib:take_unique*/ /*Start Theorem sterling:stdLib:take_length*/ Theorem sterling-$-stdLib-$-take_length[A] : forall N (R : list A) (L : list A), ($fix__sterling-$-stdLib-$-take (N) (L) (R)) -> extensibella-$-stdLib-$-length (R) (N). [Show Proof] /*End sterling:stdLib:take_length*/ /*Start Theorem sterling:stdLib:append_take*/ Theorem sterling-$-stdLib-$-append_take[A] : forall N (L2 : list A) (L : list A) (L1 : list A), ($append (L1) (L2) (L)) -> (extensibella-$-stdLib-$-length (L1) (N)) -> $fix__sterling-$-stdLib-$-take (N) (L) (L1). [Show Proof] /*End sterling:stdLib:append_take*/ /*Start Theorem sterling:stdLib:range_is*/ Theorem sterling-$-stdLib-$-range_is : forall Low High R, (is_integer (Low)) -> ($fix__sterling-$-stdLib-$-range (Low) (High) (R)) -> is_list (is_integer) (R). [Show Proof] /*End sterling:stdLib:range_is*/ /*Start Theorem sterling:stdLib:is_list_int_mem*/ Theorem sterling-$-stdLib-$-is_list_int_mem : forall L (X : $lib__integer), (is_list (is_integer) (L)) -> ($fix__sterling-$-stdLib-$-mem (X) (L)) -> is_integer (X). [Show Proof] /*End sterling:stdLib:is_list_int_mem*/ /*Start Theorem sterling:stdLib:range_low_lesseq*/ Theorem sterling-$-stdLib-$-range_low_lesseq : forall Low High R X, (is_integer (Low)) -> ($fix__sterling-$-stdLib-$-range (Low) (High) (R)) -> ($fix__sterling-$-stdLib-$-mem (X) (R)) -> $lesseq_integer (Low) (X). [Show Proof] /*End sterling:stdLib:range_low_lesseq*/ /*Start Theorem sterling:stdLib:range_high_lesseq*/ Theorem sterling-$-stdLib-$-range_high_lesseq : forall Low High R X, (is_integer (Low)) -> ($fix__sterling-$-stdLib-$-range (Low) (High) (R)) -> ($fix__sterling-$-stdLib-$-mem (X) (R)) -> $lesseq_integer (X) (High). [Show Proof] /*End sterling:stdLib:range_high_lesseq*/ /*Start Theorem sterling:stdLib:in_range*/ Theorem sterling-$-stdLib-$-in_range : forall Low High R X, (is_integer (Low)) -> (is_integer (X)) -> ($fix__sterling-$-stdLib-$-range (Low) (High) (R)) -> ($lesseq_integer (Low) (X)) -> ($lesseq_integer (X) (High)) -> $fix__sterling-$-stdLib-$-mem (X) (R). [Show Proof] /*End sterling:stdLib:in_range*/ /*Start Theorem sterling:stdLib:range_unique*/ Theorem sterling-$-stdLib-$-range_unique : forall Low High R1 R2, ($fix__sterling-$-stdLib-$-range (Low) (High) (R1)) -> ($fix__sterling-$-stdLib-$-range (Low) (High) (R2)) -> R1 = R2. [Show Proof] /*End sterling:stdLib:range_unique*/ /*Start Theorem sterling:stdLib:range_smaller_exists*/ Theorem sterling-$-stdLib-$-range_smaller_exists : forall Low High R Low', (is_integer (Low)) -> (is_integer (Low')) -> ($fix__sterling-$-stdLib-$-range (Low) (High) (R)) -> ($less_integer (Low) (Low')) -> exists R', $fix__sterling-$-stdLib-$-range (Low') (High) (R'). [Show Proof] /*End sterling:stdLib:range_smaller_exists*/ /*Start Theorem sterling:stdLib:range_subset*/ Theorem sterling-$-stdLib-$-range_subset : forall Low Low' High R R', (is_integer (Low)) -> (is_integer (Low')) -> ($fix__sterling-$-stdLib-$-range (Low) (High) (R)) -> ($fix__sterling-$-stdLib-$-range (Low') (High) (R')) -> ($less_integer (Low) (Low')) -> $fix__sterling-$-stdLib-$-subset (R') (R). [Show Proof] /*End sterling:stdLib:range_subset*/ /*Start Theorem sterling:stdLib:range_select_unique*/ Theorem sterling-$-stdLib-$-range_select_unique : forall Low High R X Rest Rest', (is_integer (Low)) -> ($fix__sterling-$-stdLib-$-range (Low) (High) (R)) -> ($fix__sterling-$-stdLib-$-select (X) (Rest) (R)) -> ($fix__sterling-$-stdLib-$-select (X) (Rest') (R)) -> Rest = Rest'. [Show Proof] /*End sterling:stdLib:range_select_unique*/ /*Start Theorem sterling:stdLib:range_exists*/ Theorem sterling-$-stdLib-$-range_exists : forall Low High, (is_integer (Low)) -> (is_integer (High)) -> exists R, $fix__sterling-$-stdLib-$-range (Low) (High) (R). [Show Proof] /*End sterling:stdLib:range_exists*/ /*Start Extensible_Theorem walkthrough:host:typeOf_unique*/ Theorem walkthrough-$-host-$-typeOf_unique : forall Ctx T TyA TyB, ($ext__1__walkthrough-$-host-$-typeOf (Ctx) (T) (TyA)) -> ($ext__1__walkthrough-$-host-$-typeOf (Ctx) (T) (TyB)) -> TyA = TyB. [Show Proof] /*End walkthrough:host:typeOf_unique*/ /*Start Extensible_Theorem walkthrough:host:ty_lookup*/ Theorem walkthrough-$-host-$-ty_lookup : forall Ctx1 Ctx2 T Ty, ($ext__1__walkthrough-$-host-$-typeOf (Ctx1) (T) (Ty)) -> (forall X XTy, ($fix__sterling-$-stdLib-$-lookup (Ctx1) (X) (XTy)) -> $fix__sterling-$-stdLib-$-lookup (Ctx2) (X) (XTy)) -> $ext__1__walkthrough-$-host-$-typeOf (Ctx2) (T) (Ty). [Show Proof] /*End walkthrough:host:ty_lookup*/ /*Start Theorem walkthrough:host:empty_ty_any*/ Theorem walkthrough-$-host-$-empty_ty_any : forall T Ty Ctx, ($ext__1__walkthrough-$-host-$-typeOf (nil) (T) (Ty)) -> $ext__1__walkthrough-$-host-$-typeOf (Ctx) (T) (Ty). [Show Proof] /*End walkthrough:host:empty_ty_any*/ /*Start Extensible_Theorem walkthrough:host:subst_type_preservation*/ Theorem walkthrough-$-host-$-subst_type_preservation : forall T Ctx X XTy Ty R S, ($ext__1__walkthrough-$-host-$-typeOf ((($pair_c) (X) (XTy))::(Ctx)) (T) (Ty)) -> ($ext__2__walkthrough-$-host-$-subst (X) (R) (T) (S)) -> ($ext__1__walkthrough-$-host-$-typeOf (nil) (R) (XTy)) -> $ext__1__walkthrough-$-host-$-typeOf (Ctx) (S) (Ty). [Show Proof] /*End walkthrough:host:subst_type_preservation*/ /*Start Extensible_Theorem walkthrough:host:type_preservation*/ Theorem walkthrough-$-host-$-type_preservation : forall T Ty T', ($ext__1__walkthrough-$-host-$-typeOf (nil) (T) (Ty)) -> ($ext__0__walkthrough-$-host-$-eval (T) (T')) -> $ext__1__walkthrough-$-host-$-typeOf (nil) (T') (Ty). [Show Proof] /*End walkthrough:host:type_preservation*/ /*Start Projection Constraint walkthrough:host:proj_type_same*/ Theorem walkthrough-$-host-$-proj_type_same : forall G T Ty T_T, ($proj__walkthrough-$-host-$-tm (G) (T) (T_T)) -> ($ext__1__walkthrough-$-host-$-typeOf (G) (T) (Ty)) -> $ext__1__walkthrough-$-host-$-typeOf (G) (T_T) (Ty). [Show Proof] /*End walkthrough:host:proj_type_same*/ /*Start Ext_Size for walkthrough:host:eval*/ Theorem walkthrough-$-host-$-ext_size_pos_eval : forall T T' N, ($extSize__walkthrough-$-host-$-eval (T) (T') (N) ) -> $lesseq_integer (($posInt) ($zero)) (N). [Show Proof] Theorem walkthrough-$-host-$-ext_size_is_int_eval : forall T T' N, ($extSize__walkthrough-$-host-$-eval (T) (T') (N) ) -> extensibella-$-stdLib-$-is_integer (N). [Show Proof] Theorem walkthrough-$-host-$-drop_ext_size_eval : forall T T' N, ($extSize__walkthrough-$-host-$-eval (T) (T') (N) ) -> $ext__0__walkthrough-$-host-$-eval (T) (T'). [Show Proof] Theorem walkthrough-$-host-$-add_ext_size_eval : forall T T', ($ext__0__walkthrough-$-host-$-eval (T) (T') ) -> exists N, $extSize__walkthrough-$-host-$-eval (T) (T') (N). [Show Proof] /*End Ext_Size for walkthrough:host:eval*/ /*Start Proj_Rel for walkthrough:host:eval*/ Theorem walkthrough-$-host-$-drop_proj_rel_eval : forall T T', ($projRel__walkthrough-$-host-$-eval (T) (T') ) -> $ext__0__walkthrough-$-host-$-eval (T) (T'). [Show Proof] /*End Proj_Rel for walkthrough:host:eval*/ /*Start Ext_Ind for walkthrough:host:eval*/ Theorem $toProjRel__$ext__0__walkthrough-$-host-$-eval : forall N G T T' Ty, ($extSize__walkthrough-$-host-$-eval (T) (T') (N) ) -> (extensibella-$-stdLib-$-acc (N) ) -> ($ext__1__walkthrough-$-host-$-typeOf (G) (T) (Ty)) -> $projRel__walkthrough-$-host-$-eval (T) (T') . [Show Proof] Theorem walkthrough-$-host-$-add_proj_rel_eval : forall G T T' Ty, ($ext__0__walkthrough-$-host-$-eval (T) (T') ) -> ($ext__1__walkthrough-$-host-$-typeOf (G) (T) (Ty)) -> $projRel__walkthrough-$-host-$-eval (T) (T') . [Show Proof] /*End Ext_Ind for walkthrough:host:eval*/ /*Start Extensible_Theorem walkthrough:big_step:big_step_type_preservation*/ Theorem walkthrough-$-big_step-$-big_step_type_preservation : forall T Ty T', ($ext__1__walkthrough-$-host-$-typeOf (nil) (T) (Ty)) -> ($ext__0__walkthrough-$-big_step-$-big_step (T) (T')) -> $ext__1__walkthrough-$-host-$-typeOf (nil) (T') (Ty). [Show Proof] /*End walkthrough:big_step:big_step_type_preservation*/
In this file, in addition to the language definitions and theorems about standard library relations, of which there are many, we have the Abella versions of the proofs for the theorems introduced by the host language and the big step extension. These are down at the end of the file. Note they are in the same order as in the composed module, an order that maintains the order used by the host language and the order used by the big step extension. Each of the proofs of these theorems is built by taking pieces of the proofs for each module and combining them.
If we look at the proof for type preservation, pulled out here, we see we start the proof by induction and case analysis on the key relation, giving us five cases:
Theorem walkthrough-$-host-$-type_preservation : forall T Ty T', ($ext__1__walkthrough-$-host-$-typeOf (nil) (T) (Ty)) -> ($ext__0__walkthrough-$-host-$-eval (T) (T')) -> $ext__1__walkthrough-$-host-$-typeOf (nil) (T') (Ty). induction on 2. intros Ty Ev. Ev: case Ev (keep). Ty: case Ty. apply IH to Ty Ev1. search. Ty: case Ty. apply IH to Ty1 Ev2. search. Ty: case Ty. Ty: case Ty. apply walkthrough-$-host-$-subst_type_preservation to Ty Ev2 Ty1. search. Ty: case Ty. apply IH to Ty Ev1. search. Ty: case Ty. apply walkthrough-$-host-$-subst_type_preservation to Ty1 Ev2 Ty. search.Compare these to the three cases given by the host language
%E-App-Step1 Ty: case Ty. apply IH to Ty Ev1. search. %E-App-Step2 Ty: case Ty. apply IH to Ty1 Ev2. search. %E-App-Subst Ty: case Ty. Ty: case Ty. apply subst_type_preservation to Ty Ev2 Ty1. search.and the two given by the let extension
%E-Let-Step Ty: case Ty. apply IH to Ty Ev1. search. %E-Let-Subst Ty: case Ty. apply subst_type_preservation to Ty1 Ev2 Ty. search.We see they are the same, modulo the use of full names for the lemmas, because the full proof is built by taking the cases from the proofs from the individual modules and putting them together. The same can be observed for the other extensible theorems from the host language, including the projection constraint and
Ext_Ind proof, both of which
are declared in Abella with Theorem,
the only type of theorem declaration in Abella.
We can see a similar thing with the proof of the big step extension's property, where we have three cases:
Theorem walkthrough-$-big_step-$-big_step_type_preservation : forall T Ty T', ($ext__1__walkthrough-$-host-$-typeOf (nil) (T) (Ty)) -> ($ext__0__walkthrough-$-big_step-$-big_step (T) (T')) -> $ext__1__walkthrough-$-host-$-typeOf (nil) (T') (Ty). induction on 2. intros Ty Big. Big: case Big (keep). search. apply walkthrough-$-host-$-type_preservation to Ty Big1. apply IH to _ Big2. search. apply walkthrough-$-host-$-proj_type_same to Big1 Ty. apply IH to _ Big2. search.Keep in mind the definition of
big_step in the
composed language:
Define $ext__0__walkthrough-$-big_step-$-big_step : ($ty__walkthrough-$-host-$-tm) ->
($ty__walkthrough-$-host-$-tm) -> prop by
$ext__0__walkthrough-$-big_step-$-big_step (T) (T) := $ext__0__walkthrough-$-host-$-value (T);
$ext__0__walkthrough-$-big_step-$-big_step (T) (T2) :=
exists T1, ($ext__0__walkthrough-$-host-$-eval (T) (T1)) /\
($ext__0__walkthrough-$-big_step-$-big_step (T1) (T2));
$ext__0__walkthrough-$-big_step-$-big_step (walkthrough-$-let-$-let (S) (Tm1) (Tm)) (T1) :=
exists T_T,
($proj__walkthrough-$-host-$-tm (nil) (walkthrough-$-let-$-let (S) (Tm1) (Tm)) (T_T)) /\
($ext__0__walkthrough-$-big_step-$-big_step (T_T) (T1)).
We have three clauses, one corresponding to the
Big-End rule, one corresponding to
the Big-Step rule, and one
corresponding to the Big-D rule
instantiated for the let construct from the let
extension. When the big step extension wrote its proof, it knew
the first two rules, but its proof for the third rule was generic,
as it did not know the let constructor:
%Big-End search. %Big-Step apply type_preservation to Ty Big1. apply IH to _ Big2. search. %Big-D apply proj_type_same to Big1 Ty. apply IH to _ Big2. search.Because of the restrictions Extensibella places on proofs, as we saw above when writing the generic proof, this generic proof can be used even when the rule is instantiated for
let,
or any other construct. If our composed language contained more
constructs from other extensions, this proof would be present with
one copy for each, and it would be valid for all.
Note that the lemmas
ext_size_is_int_typeOf and
ext_size_pos_typeOf we used in
the proof of Ext_Ind in the let
extension have been given full, automatically-generated proofs in
the composition, validating our use of them as lemmas by showing
they do hold.
This concludes our walkthrough of modular metatheory in Extensibella. A few places to go from here: