-----------------------------------------------------------------------------------------
Expressions of EMF*_ST:
f ::=
| x | \x. f | f1 f2 | (f1,f2) | ...
| pret f | pbind f1 x.f2 | run f
| stret f1 | stbind f1 x.f2 | get f | put f | lift f
We additionally assume the existence of a base type called (state).
Remark: In order to improve readability, we abbreviate Pure.return f as pret f. Similarly, we
also use shorthand notation for Pure.bind, ST.return, ST.get, ST.put and ST.lift. As a small
simplification, we assume that all the constants are used in EMF*_ST in their fully applied forms.
-----------------------------------------------------------------------------------------
Evaluation contexts of EMF*_ST:
We let the evaluation contexts F be the reflect/reify-free evaluation contexts of EMF*.
-----------------------------------------------------------------------------------------
Operational semantics of EMF*_ST:
The operational semantics of EMF*_ST is given by a small-step call-by-value reduction relation between
configurations (S,f), where (|- S : Tot state) and f is an EMF*_ST expression.
We also have a notion of values v in EMF*_ST, which coincides with the definition of values for EMF*.
v ::=
| \x. f
| (v1,v2)
| inl v
| inr v
| ... (all other fully applied constants with all arguments being values)
The reduction rules are given by:
(S,f) ~> (S',f')
---------------------- [Context]
(S,F[f]) ~> (S',F[f'])
-------------------------- [Beta]
(S,(\x. f)v) ~> (S,f[v/x])
------------------------- [Proj-L]
(S,fst (v1,v2)) ~> (S,v1)
------------------------- [Proj-L]
(S,snd (v1,v2)) ~> (S,v2)
---------------------------------------------- [Case-L]
(S,case (inl v as y) x.f1 x.f2) ~> (S,f1[v/x])
---------------------------------------------- [Case-R]
(S,case (inr v as y) x.f1 x.f2) ~> (S,f2[v/x])
------------------------- [Run-PureRet]
(S,run (pret v)) ~> (S,v)
------------------------------------ [PureBind]
(S,pbind (pret v) x.f) ~> (S,f[v/x])
-------------------------------------- [STBind]
(S,stbind (stret v) x.f) ~> (S,f[v/x])
------------------------ [STGet]
(S,get v) ~> (S,stret S)
------------------------- [STPut]
(S,put v) ~> (v,stret ())
-------------------------------- [STLift]
(S,lift (pret v)) ~> (S,stret v)
-----------------------------------------------------------------------------------------
Contexts:
K S ::=
| (F : Tot) //a Tot context
| (F : Pure) //a Pure context
| (F : ST) //an inert ST context
| reify (F : ST) S //an active ST context
| pbind (K' S) xn.((\x. reify f) (fst xn) (snd xn)) //an active ST context
where the F are evaluation contexts which when filled by a suitably typed term produce
a Tot, Pure or ST term, respectively
-----------------------------------------------------------------------------------------
Context sorts:
sorts = Tot | Pure | Active | Inert
sort_of (K S) \in sorts
sort_of (F : Tot) = Tot
sort_of (F : Pure) = Pure
sort_of (reify (F : ST) S) = Active
sort_of (pbind (K S) xn.((\x.reify f) (fst xn) (snd xn))) = Active when sort_of (K S) = Active
sort_of (F : ST) = Inert
Remark: In the paper, these sorts are attached directly to the contexts K S.
Definition: A context K S is said to be well-sorted iff (sort_of K S) is defined.
From here onwards, we assume that all contexts we are working with are well-sorted.
-----------------------------------------------------------------------------------------
The translation [.] from contexts K S to evaluation contexts F of EMF*_ST:
[(F : C)] = F
[reify F S] = F
[pbind (K S) xn.((\x. reify f1) (fst xn) (snd xn))] = stbind [K S] x.f1
-----------------------------------------------------------------------------------------
The simulation relation:
R (K S f)
\defeq
1. sort_of K S = Inert
\/ 2. exists K' S' f'.
(S, [K S] f) ~>+ (S', [K' S'] f')
/\ (K S f) ~>+ (K' S' f')
/\ sort_of K' S' <> Inert
/\ sort_of K S = sort_of K' S'
/\ ((sort_of K S = Tot \/ sort_of K S = Pure) ==> S = S')
\/ 3. exists v S'.
sort_of K S = Active
/\ (S,[K S] f) ~>* (S',stret v)
/\ (K S f) ~>+ pret (v,S')
\/ 4. exists v.
sort_of K S = Pure
/\ K S f = [K S] f = pret v
\/ 5. exists v.
sort_of K S = Tot
/\ K S f = [K S] f = v
Remark: The reader should note that the presentation of these five cases here differs
slightly from the the presentation given in the simulation theorem in the paper. The
two presentations are however equivalent. We use the presentation given here in the
proof of the theorem below.
-----------------------------------------------------------------------------------------
Theorem: forall K S f C . |- K S f : C ==> R (K S f)
Proof: By well-founded induction on with the order
K1 S1 f1 < K2 S2 f2 iff 1. K1 S1 f1 is a proper subterm of K2 S2 f2
\/ 2. K1 S1 = reify (F1 : ST) S1
/\ K2 S2 = reify (F2 : ST) S2
/\ S1 = S2
/\ F1 f1 is a proper subterm of F2 f2
Case (K S = (F : Tot)):
By definition of [.], we have that ([K S] f = F f).
As (F : Tot) and (|- F f : C), we must have (C = Tot t) for some t.
We proceed by case analysis on the structure of F f,
ruling out impossible cases by using the typing information (|- F f : Tot t).
Case (F f = \x. f1):
By definition, (\x. f1) is a value in EMF*.
By definition of [.], we have ([(F : Tot)] f = F f = \x. f1)
and
((F : Tot) f = F f = \x. f1)
Therefore, we have proved case 5 of R (K S f).
Case (F f = f1 f2):
The proof of this case is analogous to that for the application case below when (K S = reify (F : ST) S).
The main difference compared to the referred case below is that here we do not use the [Context] rule to push
the reduction sequence given by the IHs under reify. In short, we first use IH with ((o : Tot) f1) and then,
depending on which case the IH returns, we either can prove case 2 of R (K S f) immediately, or further use
the IH with ((o : Tot) : f2). In the case when both f1 and f2 end up being values, we observe that because
f1 is a value at function type (which we know by inverting the typing of the application), then f1 must be
a lambda abstraction (as we assumed that all constants are fully applied for the purposes of this note).
As a result, we can prove case 2 of R (K S f) by making a beta-step in both semantics.
Case (F f = (f1,f2)):
By inverting the typing of (|- (f1,f2) : Tot t), we get that (|- f1 : Tot t1) and (|- f2 : Tot t2) for some t1 and t2.
We proceed by using the IH with (|- (o : Tot) f1 : Tot t1),
which we can do because (((o : Tot) f1) < (F : Tot) f) by case 1 of the wf order.
Case when IH returns case 1:
Case when IH returns case 2:
In this case, the IH tells us that we get to use ((S, f1) ~>+ (S,[K1 S] f1')) and (f1 ~>+ K1 S f1').
In addition, the IH also tells us that (sort_of (o : Tot) = sort_of(K1 S) = Tot).
By using the [Context] rule in both semantics, we get that ((S, (f1,f2)) ~>+ (S, ([K1 S] f1',f2)))
and
((f1,f2) ~>+ (K1 S f1',f2))
By the virtue of the definition of contexts K S, we must have K1 S = (F' : Tot) for some F',
because the IH told us that (sort_of K1 S = Tot).
But then, we have ([K1 S] f1' = [(F' : Tot)] f1' = F' f1')
and
(K1 S f1' = F' f1').
Therefore, we can pick S' = S
K' S' = (o : Tot)
f' = (F' f1',f2)
With this choice of (K' S'), we have ( sort_of (K S)
= sort_of (F : Tot)
= Tot
= sort_of (o : Tot)
= sort_of (K' S'))
As a result, we have proved case 2 of R (K S f).
Case when IH returns case 3:
We prove this case by deriving false from (sort_of (o : Tot) = Active) and (sort_of (o : Tot) = Tot).
Case when IH returns case 4:
We prove this case by deriving false from (sort_of (o : Tot) = Pure) and (sort_of (o : Tot) = Tot).
Case when IH returns case 5:
In this case, the IH tells us that f1 is a value.
We proceed by using the IH with (|- (o : Tot) f2 : Tot t2),
which we can do because (((o : Tot) f2) < (F : Tot) f) by case 1 of the wf order.
Case when IH returns case 1:
We prove this case by deriving false from (sort_of (o : Tot) = Inert) and (sort_of (o : Tot) = Tot).
Case when IH returns case 2:
Analogous to the case 2 for use of the IH with ((o : Tot) f1).
Case when IH returns case 3:
We prove this case by deriving false from (sort_of (o : Tot) = Active) and (sort_of (o : Tot) = Tot).
Case when IH returns case 4:
We prove this case by deriving false from (sort_of (o : Tot) = Pure) and (sort_of (o : Tot) = Tot).
Case when IH returns case 5:
In this case, the IH tells us that f2 is a value.
As we already knew that f1 was a value, the pair (f1,f2) is also a value.
By definition of [.], we know that ([(F : Tot)] f = F f = (f1,f2))
and
((F : Tot) f = F f = (f1,f2))
As a result, we have proved case 5 of R (K S f).
Cases (F f = fst f1) and (F f = snd f2):
Both follow similar pattern to the pairing case above: we first invert the typing of the
projections; we then use the IH with the empty Tot context and the argument to the projections;
if the IH returns case 2, we use [Context] rule to push the given derivation sequences under the
projections; if the IH returns case 5, we get that the arguments of the projections are values;
as the only value that types at the product type is a pair of values, we can take a beta-step in
both of the semantics, and prove case 2 of R (K S f).
Cases (F f = inl f1) and (F f = inr f2):
Following the same proof strategy as the above case for projections.
Cases for all other constants:
Cases for all other constants also follow the strategy outlined in the case for projections.
If the constant takes more than one argument, we invert typing and use the IH on each of the
arguments from left-to-right. At the very end, all the arguments will be values and, therefore,
the whole term is a value, allowing us to immediately prove case 5 of R (K S f).
Case (F f = case (f1 as y) x.f2 x.f3):
As with application, proved analogously to the case below where (K S = reify (F' : ST) S; F' = case (f1 as y) x.f2 x.f3).
Again, the main difference is that here we do not use the [Context] rule to push the derivation sequences under reify.
Case (F f = run f1):
By inverting the typing of (|- run f1 : Tot t), we get that (|- f1 : Pure t1 wp1) for some f1 and wp1.
We proceed by using the IH with (|- (o : Pure) f1 : Pure t1 wp1),
which we can do because (((o : Pure) f1) < (F : Tot) f) by case 1 of the wf order.
Case when IH returns case 1:
We prove this case by deriving false from (sort_of (o : Pure) = Inert) and (sort_of (o : Pure) = Pure).
Case when IH returns case 2:
In this case, IH tells us that we get to use ((S, f1) ~>+ (S,[K1 S] f1')) and (f1 ~>+ K1 S f1').
In addition, the IH also tells us that (sort_of (o : Pure) = sort_of(K1 S) = Pure).
By using the [Context] rule in both semantics, we get that ((S, run f1) ~>+ (S, run ([K1 S] f1')))
and
(run f1 ~>+ run (K1 S f1'))
As the IH told us that (sort_of K1 S = Pure), then by the virtue of the definition of contexts K S,
we must have (K1 S = (F' : Pure)) for some F'
But then, we have ([K1 S] f1' = [(F' : Pure)] f1' = F' f1')
and
(K1 S f1' = F' f1').
Therefore, we can pick S' = S
K' S' = (o : Tot)
f' = run (F' f1')
With this choice of (K' S'), we have ( sort_of (K S)
= sort_of (F : Tot)
= Tot
= sort_of (o : Tot)
= sort_of (K' S'))
As a result, we have proved case 2 of R (K S f).
Case when IH returns case 3:
We prove this case by deriving false from (sort_of (o : Pure) = Active) and (sort_of (o : Pure) = Pure).
Case when IH returns case 4:
In this case, the IH tells us that ((o : Pure) f1 = f1 = pret v) for some v.
In the semantics of EMF*_ST, we have ( (S, [(F : Tot)] f)
= (S, F f)
= (S, run f1)
= (S, run (pret v))
~> (S, v))
In the semantics of EMF*, we have ( (F : Tot) f
= F f
= run f1
= run (pret v)
~> v)
Therefore, we can pick S' = S
K' S' = (o : Tot)
f' = v
With this choice of (K' S'), we have ( sort_of (K S)
= sort_of (F : Tot)
= Tot
= sort_of (o : Tot)
= sort_of (K' S'))
As a result, we have proved case 2 of R (K S f).
Case when IH returns case 5:
We prove this case by deriving false from (sort_of (o : Pure) = Tot) and (sort_of (o : Pure) = Pure).
Case (K S = (F : Pure)):
By definition of [.], we have that ([K S] f = F f).
As (F : Pure) and (|- F f : C), we must have (C = Pure t wp) for some t and wp.
We proceed by case analysis on the structure of F f,
ruling out impossible cases by using the typing information (|- F f : Pure t wp).
Case (F f = f1 f2):
Similarly to the above application case when (K S = (F : Tot), this case is again
proved using the same pattern as in the application case below when (K S = reify (F : ST) S).
We refer the reader to the above application case when (K S = (F : Tot) for a
description of how the proof proceeds.
Case (F f = case (f1 as y) x.f2 x.f3):
The proof of this case is analogous to the (case) case below when (K S = reify (F : ST) S).
As with the application case, the main difference with the referred (case) case is that here
we do not (need to) use the [Context] rule to push the reduction sequences under reify.
Case (F f = pret f1):
By inverting the typing of (|-pret f1 : Pure t wp), we get that (|- f1 : Tot t1) for some t1.
We proceed by using the IH with (|- (o : Tot) f1 : Tot t1),
which we can do because (((o : Tot) f1) < (F : Pure) f) by case 1 of the wf order.
Case when IH returns case 1:
We prove this case by deriving false from (sort_of (o : Tot) = Inert) and (sort_of (o : Tot) = Tot).
Case when IH returns case 2:
In this case, IH tells us that we get to use ((S, f1) ~>+ (S,[K1 S] f1')) and (f1 ~>+ K1 S f1').
In addition, the IH also tells us that (sort_of (o : Tot) = sort_of(K1 S) = Tot).
By using the [Context] rule in both semantics, we get that ((S, pret f1) ~>+ (S, pret ([K1 S] f1')))
and
(pret f1 ~>+ pret (K1 S f1'))
By the virtue of the definition of contexts K S, we must have K1 S = (F' : Tot) for some F',
because the IH told us that (sort_of K1 S = Tot).
But then, we have ([K1 S] f1' = [(F' : Tot)] f1' = F' f1')
and
(K1 S f1' = F' f1').
Therefore, we can pick S' = S
K' S' = (o : Pure)
f' = pret (F' f1')
With this choice of (K' S'), we have ( sort_of (K S)
= sort_of (F : Pure)
= Pure
= sort_of (o : Pure)
= sort_of (K' S'))
As a result, we have proved case 2 of R (K S f).
Case when IH returns case 3:
We prove this case by deriving false from (sort_of (o : Tot) = Active) and (sort_of (o : Tot) = Tot).
Case when IH returns case 4:
We prove this case by deriving false from (sort_of (o : Tot) = Pure) and (sort_of (o : Tot) = Tot).
Case when IH returns case 5:
In this case, the IH tells us that f1 is a value.
Therefore, we can pick v = f1.
As a result, we have proved case 4 of R (K S f).
Case (F f = pbind f1 x.f2):
By inverting the typing of (|- pbind f1 x.f2 : Pure t wp), we get that (|- f1 : Pure t1 wp1) for some t1 and wp1.
We proceed by using the IH with (|- (o : Pure) f1 : Pure t1 wp1),
which we can do because (((o : Pure) f1) < (F : Pure) f) by case 1 of the wf order.
Case when IH returns case 1:
We prove this case by deriving false from (sort_of (o : Pure) = Inert) and (sort_of (o : Pure) = Pure).
Case when IH returns case 2:
In this case, IH tells us that we get to use ((S, f1) ~>+ (S,[K1 S] f1')) and (f1 ~>+ K1 S f1').
In addition, the IH also tells us that (sort_of (o : Pure) = sort_of(K1 S) = Pure).
By using the [Context] rule in both semantics, we get that ((S, pbind f1 x.f2) ~>+ (S, pbind ([K1 S] f1') x.f2))
and
(pbind f1 x.f2 ~>+ pbind (K1 S f1') x.f2)
As the IH told us that (sort_of K1 S = Pure), then by the virtue of the definition of contexts K S,
we must have K1 S = (F' : Pure) for some F'
But then, we have ([K1 S] f1' = [(F' : Pure)] f1' = F' f1')
and
(K1 S f1' = F' f1').
Therefore, we can pick S' = S
K' S' = (o : Pure)
f' = pbind (F' f1') x.f2
With this choice of (K' S'), we have ( sort_of (K S)
= sort_of (F : Pure)
= Pure
= sort_of (o : Pure)
= sort_of (K' S'))
As a result, we have proved case 2 of R (K S f).
Case when IH returns case 3:
We prove this case by deriving false from (sort_of (o : Pure) = Active) and (sort_of (o : Pure) = Pure).
Case when IH returns case 4:
In this case, the IH tells us that (f1 = pret v1) for some v1.
In the semantics of EMF*_ST, we have ( (S, [(F : Pure)] f)
= (S, F f)
= (S, pbind f1 x.f2)
= (S, pbind (pret v1) x.f2)
~> (S, f2[v1/x]))
In the semantics of EMF*, we have ( (F : Pure) f
= F f
= pbind f1 x.f2
= pbind (pret v) x.f2
~> f2[v/x])
Therefore, we can pick S' = S
K S' = (o : Pure)
f' = f2[v/x]
With this choice of (K' S'), we have ( sort_of (K S)
= sort_of (F : Pure)
= Pure
= sort_of (o : Pure) = sort_of (K' S'))
As a result, we have proved case 2 of R (K S f).
Case when IH returns case 5:
We prove this case by deriving false from (sort_of (o : Pure) = Tot) and (sort_of (o : Pure) = Pure).
Case (K S = (F : ST)):
In this case, (type_of K S = Inert).
As a result, we have trivially proved case 1 of R (K S f).
Case (K S = reify (F : ST) S):
By definition of hole filling, we have (K S f = reify (F f) S).
By definition of [.], we have ([reify (F : ST) S] f = F f).
As (K S f = reify (F f) S) and (|- K S f : C), we must have that (C = Pure t1 wp1) for some t1 and wp1.
By inverting the typing of (|- reify (F f) S : Pure t1 wp1), we have that (|- F f : ST t2 wp2) for some t2 and wp2.
We proceed by case analysis on the structure of F f,
ruling out impossible cases by using the typing information (|- F f : Pure t2 wp2).
Case (F f = f1 f2):
By inverting the typing of (|- f1 f2 : ST t2 wp2),
we get that (|- f1 : Tot (x:t3 -> ST t4 wp4)) and (|- f2 : Tot t3) for some x, t3, t4, wp4.
We proceed by using the IH with (|- (o : Tot) f1 : Tot (x:t3 -> ST t4 wp4)),
which we can do because (((o : Tot) f1) < (reify (F : ST) S f)) by case 1 of the wf order.
Case when IH returns case 1:
We prove this case by deriving false from (sort_of (o : Tot) = Inert) and (sort_of (o : Tot) = Tot).
Case when IH returns case 2:
In this case, IH tells us that we get to use ((S, f1) ~>+ (S,[K1 S] f1')) and (f1 ~>+ K1 S f1').
In addition, the IH also tells us that (sort_of (o : Tot) = sort_of(K1 S) = Tot).
By using the [Context] rule in both semantics, we get that ((S, f1 f2) ~>+ (S, ([K1 S] f1') f2))
and
(reify (f1 f2) S ~>+ reify ((K1 S f1') f2) S)
By the virtue of the definition of contexts K S, we must have K1 S = (F' : Tot) for some F',
because the IH told us that (sort_of K1 S = Tot).
But then, we have ([K1 S] f1' = [(F' : Tot)] f1' = F' f1')
and
(K1 S f1' = F' f1').
Therefore, we can pick S' = S
K' S' = reify (o : ST) S
f' = (F' f1') f2
With this choice of (K' S'), we have ( sort_of (K S)
= sort_of (reify (F : ST) S)
= Active
= sort_of (reify (o : ST) S)
= sort_of (K' S'))
As a result, we have proved case 2 of R (K S f).
Case when IH returns case 3:
We prove this case by deriving false from the assumption that (stret v) has Tot type.
Case when IH returns case 4:
We prove this case by deriving false from the assumption that (pret v) has Tot type.
Case when IH returns case 5:
In this case, the IH tells us that f1 is a value.
We proceed by using the IH with (|- (o : Tot) f2 : Tot t3),
which we can de because ((o : Tot) f2 < (reify (o : ST) S (f1 f2))).
Case when IH returns case 1:
We prove this case by deriving false from (sort_of (o : Tot) = Inert) and (sort_of (o : Tot) = Tot).
Case when IH returns case 2:
In this case, Ih tells us that we get to use ((S,f2) ~>+ (S, [K1 S] f2')) and (f2 ~>+ K1 S f2').
In addition, the IH also tells us that (sort_of (o : Tot) = sort_of(K1 S) = Tot).
By using the [Context] rule in both semantics, we get that ((S, f1 f2) ~>+ (S, f1 ([K1 S] f2')))
and
(reify (f1 f2) S ~>+ reify (f1 (K1 S f2')) S).
By the virtue of the definition of contexts K S, we must have K1 S = (F' : Tot) for some F',
because the IH told us that (sort_of K1 S = Tot).
But then, we have ([K1 S] f2' = [(F' : Tot)] f2' = F' f2')
and
(K1 S f2' = F' f2').
Therefore, we can pick S' = S
K' S' = reify (o : ST) S
f' = f1 (F' f2')
With this choice of (K' S'), we have ( sort_of (K S)
= sort_of (reify (F : ST) S)
= Active
= sort_of (reify (o : ST) S)
= sort_of (K' S'))
As a result, we have proved case 2 of R (K S f).
Case when IH returns case 3:
We prove this case by deriving false from the assumption that (stret v) has Tot type.
Case when IH returns case 4:
We prove this case by deriving false from the assumption that (pret v) has Tot type.
Case when IH returns case 5:
In this case, the IH tells us that f2 is a value.
Recalling that f1 was also a value and (|- f1 : Tot (x:t3 -> ST t4 wp4)),
then f1 must be of the form (\x. f3) for some f3.
As a result, we can take a beta-step in both semantics: ((S, (\x. f3) f2) ~> (S, f3[f2/x]))
and
((\x. f3) f2 ~> f3[f2/x]).
By using the [Context] rule in the semantics of EMF*, we get that (reify ((\x. f3) f2) S ~> reify (f3[f2/x]) S).
Therefore, we can pick S' = S
K' S' = reify (o : ST) S
f' = f3[f2/x]
With this choice of (K' S'), we have ( sort_of (K S)
= sort_of (reify (F : ST) S)
= Active
= sort_of (reify (o : ST) S)
= sort_of (K' S'))
As a result, we have proved case 2 of R (K S f).
Case (F f = case (f1 as y) x.f2 x.f3):
By inverting the typing of (|- case (f1 as y) x.f2 x.f3 : ST t2 wp2),
we get that (|- f1 : Tot (sum t3 t4)), (x : t3 |- f2 : ST t5 wp5) and (x : t4 |- f3 : ST t6 wp6)
for some t3 t4 t5 wp5 t6 wp6.
We proceed by using the IH with (|- (o : Tot) f1 : Tot (sum t3 t4)),
which we can do because (((o : Tot) f1) < (reify (F : ST) S f)) by case 1 of the wf order.
Case when IH returns case 1:
We prove this case by deriving false from (sort_of (o : Tot) = Inert) and (sort_of (o : Tot) = Tot).
Case when IH returns case 2:
In this case, IH tells us that we get to use ((S, f1) ~>+ (S,[K1 S] f1')) and (f1 ~>+ K1 S f1').
The rest of this case is analogous to the first use of IH when (F f = f1 f2) above,
using the [Context] rule in both semantics to push the above reductions under case and reify.
Case when IH returns case 3:
We prove this case by deriving false from the assumption that (stret v) has Tot type.
Case when IH returns case 4:
We prove this case by deriving false from the assumption that (pret v) has Tot type.
Case when IH returns case 5:
In this case, the IH tells us that f1 is a value.
As f1 is a value and (|- f1 : Tot (sum t3 t4)),
then f1 must be either of the form (inl v1) for some v1 or (inl v2) for some v2.
The case when (f1 = inl v1):
In both semantics we can take a beta-step: ((S, case (inl v1 as y) x.f2 x.f3) ~> (S, f2[v1/x]))
and
(case (inl v1 as y) x.f2 x.f3 ~> f2[v1/x])
By using the [Context] rule in the semantics of EMF*, we get that ( reify (case (inl v1 as y) x.f2 x.f3) S
~> reify (f2[v1/x]) S)
By the definition of [.] and hole filling,
we know that ([reify (o : ST) S] (f2[v1/x]) = f2[v1/x]).
Therefore, we can pick S' = S
K S' = reify (o : ST)
f' = f2[v1/x]
With this choice of (K' S'), we have ( sort_of (K S)
= sort_of (reify (F : ST) S)
= Active
= sort_of (reify (o : ST) S)
= sort_of (K' S'))
As a result, we have proved case 2 of R (K S f).
The case when (f1 = inr v2):
Analogously to the above case when (f1 = inl v1).
Case (F f = stret f1):
By inverting the typing of (|- stret f1 : ST t2 wp2),
we get that (|- f1 : Tot t3) for some t3.
We proceed by using the IH with (|- (o : Tot) f1 : Tot t3),
which we can do because (((o : Tot) f1) < (reify (F : ST) S f)) by case 1 of the wf-order.
Case when IH returns case 1:
We prove this case by deriving false from (sort_of (o : Tot) = Inert) and (sort_of (o : Tot) = Tot).
Case when IH returns case 2:
In this case, IH tells us that we get to use ((S, f1) ~>+ (S,[K1 S] f1')) and (f1 ~>+ K1 S f1').
In addition, the IH also tells us that (sort_of (o : Tot) = sort_of(K1 S) = Tot).
By using the [Context] rule in both semantics, we get that ((S, stret f1) ~>+ (S, stret ([K1 S] f1')))
and
(reify (stret f1) S ~>+ reify (stret (K1 S f1')) S).
By the virtue of the definition of contexts K S, we must have K1 S = (F' : Tot) for some F',
because the IH told us that (sort_of K1 S = Tot).
But then, we have ([K1 S] f1' = [(F' : Tot)] f1' = F' f1')
and
(K1 S f1' = F' f1').
Therefore, we can pick S' = S
K' S' = reify (o : ST) S
f' = stret (F' f1')
With this choice of (K' S'), we have ( sort_of (K S)
= sort_of (reify (F : ST) S)
= Active
= sort_of (reify (o : ST) S)
= sort_of (K' S'))
As a result, we have proved case 2 of R (K S f).
Case when IH returns case 3:
In this case, the IH tells us that ( (S,[reify (o : ST) S] f1)
= (S,f1)
~>* (S'',stret v))
Therefore, in the semantics of EMF*_ST we have ( (S,stbind f1 x.f2)
~>* (S'',stbind (stret v) x.f2)
~> (S'',f2[v/x])
= (S'',[reify (o : ST) S''] (f2[v/x]))).
The IH also tells us that (reify f1 S ~>+ pret (v,S'')).
Therefore, in the semantics of EMF*, we have ( reify (F : ST) S f
= reify (F f) S
= reify (stbind f1 x.f2) S
~>+ pbind (reify f1 S) xn.((\x. reify f2) (fst xn) (snd xn))
~>+ pbind (pret (v,S'')) xn.((\x. reify f2) (fst xn) (snd xn))
~>+ reify (f2[v/x]) S''
= reify (o : ST) S'' (f2[v/x]))
Therefore, we can pick S' = S''
K' S' = reify (o : ST) S''
f' = f2[v/x]
With this choice of (K' S'), we have ( sort_of (K S)
= sort_of (reify (F : ST) S)
= Active
= sort_of (reify (o : ST) S'')
= sort_of (K' S'))
As a result, we have proved case 2 of R (K S f).
Case when IH returns case 4:
We prove this case by deriving false from the assumption that (pret v = reify f1 S).
Case when IH returns case 5:
We prove this case by deriving false from the assumption that (reify f1 S) is a value.
Case (F f = get f1):
By inverting the typing of (|- get f1 : ST t2 wp2), we get that (|- f1 : Tot unit).
We proceed by using the IH with (|- (o : Tot) f1 : Tot unit),
which we can do because (((o : Tot) f1) < (reify (F : ST) S f)) by case 1 of the wf order.
Case when IH returns case 1:
We prove this case by deriving false from (sort_of (o : Tot) = Inert) and (sort_of (o : Tot) = Tot).
Case when IH returns case 2:
In this case, IH tells us that we get to use ((S, f1) ~>+ (S,[K1 S] f1')) and (f1 ~>+ K1 S f1').
In addition, the IH also tells us that (sort_of (o : Tot) = sort_of(K1 S) = Tot).
By using the [Context] rule in both semantics, we get that ((S, get f1) ~>+ (S, get ([K1 S] f1')))
and
(get f1 ~>+ get (K1 S f1'))
By the virtue of the definition of contexts K S, we must have K1 S = (F' : Tot) for some F',
because the IH told us that (sort_of K1 S = Tot).
But then, we have ([K1 S] f1' = [(F' : Tot)] f1' = F' f1')
and
(K1 S f1' = F' f1').
Therefore, we can pick S' = S
K' S' = reify (o : ST) S
f' = get (F' f1')
With this choice of (K' S'), we have ( sort_of (K S)
= sort_of (reify (F : ST) S)
= Active
= sort_of (reify (o : ST) S)
= sort_of (K' S'))
As a result, we have proved case 2 of R (K S f).
Case when IH returns case 3:
We prove this case by deriving false from (sort_of (o : Tot) = Active) and (sort_of (o : Tot) = Tot).
Case when IH returns case 4:
We prove this case by deriving false from (sort_of (o : Tot) = Pure) and (sort_of (o : Tot) = Tot).
Case when IH returns case 5:
In this case, the IH tells us that f1 is a value.
As f1 is a value, we must have (f1 = v1) for some v1.
In the semantics of EMF*_ST, we have ( (S, F f)
= (S, get f1)
= (S, get v1)
~> (S, stret S))
In the semantics of EMF*, we have ( reify (F : ST) S f
= reify (F f) S
= reify (get f1) S
= reify (get v1) S
~> (\h. pret (h,h)) S)
~> pret (S,S))
Therefore, we can pick v = S
S' = S
As a result, we have proved case 3 of R (K S f).
Case (F f = put f1):
By inverting the typing of (|- put f1 : ST t2 wp2), we get that (|- f1 : Tot state).
We proceed by using the IH with (|- (o : Tot) f1 : Tot state),
which we can do because (((o : Tot) f1) < (reify (F : ST) S f)) by case 1 of the wf order.
Case when IH returns case 1:
We prove this case by deriving false from (sort_of (o : Tot) = Inert) and (sort_of (o : Tot) = Tot).
Case when IH returns case 2:
In this case, IH tells us that we get to use ((S, f1) ~>+ (S,[K1 S] f1')) and (f1 ~>+ K1 S f1').
In addition, the IH also tells us that (sort_of (o : Tot) = sort_of(K1 S) = Tot).
By using the [Context] rule in both semantics, we get that ((S, put f1) ~>+ (S, put ([K1 S] f1')))
and
(put f1 ~>+ put (K1 S f1'))
By the virtue of the definition of contexts K S, we must have K1 S = (F' : Tot) for some F',
because the IH told us that (sort_of K1 S = Tot).
But then, we have ([K1 S] f1' = [(F' : Tot)] f1' = F' f1')
and
(K1 S f1' = F' f1').
Therefore, we can pick S' = S
K' S' = reify (o : ST) S
f' = put (F' f1')
With this choice of (K' S'), we have ( sort_of (K S)
= sort_of (reify (F : ST) S)
= Active
= sort_of (reify (o : ST) S)
= sort_of (K' S'))
As a result, we have proved case 2 of R (K S f).
Case when IH returns case 3:
We prove this case by deriving false from (sort_of (o : Tot) = Active) and (sort_of (o : Tot) = Tot).
Case when IH returns case 4:
We prove this case by deriving false from (sort_of (o : Tot) = Pure) and (sort_of (o : Tot) = Tot).
Case when IH returns case 5:
In this case, the IH tells us that f1 is a value.
As f1 is a value, we must have (f1 = v1) for some v1.
In the semantics of EMF*_ST, we have ( (S, F f)
= (S, put f1)
= (S, put v1)
~> (v1, stret ()))
In the semantics of EMF*, we have ( reify (F : ST) S f
= reify (F f) S
= reify (put f1) S
= reify (put v1) S
~> (\h. pret ((),v1)) S)
~> pret ((),v1))
Therefore, we can pick v = ()
S' = v1
As a result, we have proved case 3 of R (K S f).
Case (F f = lift f1):
By inverting the typing of (|- lift f1 : ST t2 wp2), we get that (|- f1 : Pure t3 wp3) for some t3 and wp3.
We proceed by using the IH with (|- (o : Pure) f1 : Pure t3 wp3),
which we can do because (((o : Pure) f1) < (reify (F : ST) S f)) by case 1 of the wf order.
Case when IH returns case 1:
We prove this case by deriving false from (sort_of (o : Pure) = Inert) and (sort_of (o : Pure) = Pure).
Case when IH returns case 2:
In this case, IH tells us that we get to use ((S, f1) ~>+ (S,[K1 S] f1')) and (f1 ~>+ K1 S f1').
In addition, the IH also tells us that (sort_of (o : Pure) = sort_of(K1 S) = Pure).
By using the [Context] rule in both semantics, we get that ((S, lift f1) ~>+ (S, lift ([K1 S] f1')))
and
(lift f1 ~>+ lift (K1 S f1'))
As the IH also tells us that (sort_of K1 S = Pure), then by the virtue of
the definition of contexts K S, we must have K1 S = (F' : Pure) for some F'
But then, we have ([K1 S] f1' = [(F' : Pure)] f1' = F' f1')
and
(K1 S f1' = F' f1').
Therefore, we can pick S' = S
K' S' = reify (o : ST) S
f' = lift (F' f1')
With this choice of (K' S'), we have ( sort_of (K S)
= sort_of (reify (F : ST) S)
= Active
= sort_of (reify (o : ST) S)
= sort_of (K' S'))
As a result, we have proved case 2 of R (K S f).
Case when IH returns case 3:
We prove this case by deriving false from (sort_of (o : Pure) = Active) and (sort_of (o : Pure) = Pure).
Case when IH returns case 4:
In this case, the IH tells us that (f1 = pret v1).
In the semantics of EMF*_ST, we have ( (S, [reify (F : ST) S] f)
= (S, F f)
= (S, lift (pret f1))
= (S, lift (pret v1))
~> (S, stret v1))
In the semantics of EMF*, we have ( reify (F : ST) S f
= reify (F f) S
= reify (lift (pret f1)) S
= reify (lift (pret v1)) S
~> (\h. pret (v1,h)) S
~> pret (v1,S))
Therefore, we can pick v = v1
S' = S
As a result, we have proved case 3 of R (K S f).
Case when IH returns case 5:
We prove this case by deriving false from (sort_of (o : Pure) = Tot) and (sort_of (o : Pure) = Pure).
Case (K S = pbind (K1 S) xn.((\x. reify f1) (fst xn) (snd xn))):
Under our global assumption that all contexts we are working with are well-sorted,
we have that (sort_of (pbind (K1 S) xn.((\x. reify f1) (fst xn) (snd xn))) = Active) and (sort_of K1 S = Active).
By definition of hole filling, we have (K S f = pbind (K1 S f) xn.((\x. reify f1) (fst xn) (snd xn))).
By definition of [.], we have ([pbind (K1 S) xn.((\x. reify f1) (fst xn) (snd xn))] f = stbind ([K1 S] f) x.f1).
According to the definition of the typing relation, we must have that (C = Pure t1 wp1 for some t1 and wp1).
By inverting the typing of (|- pbind (K1 S f) xn.((\x. reify f1) (fst xn) (snd xn)) : Pure t1 wp1),
we have that (|- K1 S f : Pure t2 wp2) for some t2 and wp2.
We proceed by using the IH with (|- K1 S f : Pure t3 wp3),
which we can do because ((K1 S f) < (pbind (K1 S) xn.((\x. reify f1) (fst xn) (snd xn)) f)) by case 1 of the wf order.
Case when IH returns case 1:
We prove this case by deriving false from (sort_of (K1 S) = Inert) and (sort_of (K1 S) = Active).
Case when IH returns case 2:
In this case, IH tells us that we get to use ((S, [K1 S] f) ~>+ (S,[K2 S] f2)) and (K1 S f ~>+ K2 S f2).
In addition, the IH also tells us that (sort_of (o : Tot) = sort_of(K1 S) = Tot).
In the semantics of EMF*_ST, we have ( (S, [pbind (K1 S) xn.((\x. reify f1) (fst xn) (snd xn))] f)
= (S, stbind ([K1 S] f) x.f1)
~>+ (S, stbind ([K2 S] f2) x.f1)
= (S, [pbind (K2 S) xn.((\x. reify f1) (fst xn) (snd xn))] f2))
In the semantics of EMF*, we have ( pbind (K1 S) xn.((\x. reify f1) (fst xn) (snd xn)) f
= pbind (K1 S f) xn.((\x. reify f1) (fst xn) (snd xn))
~>+ pbind (K2 S f2) xn.((\x. reify f1) (fst xn) (snd xn))
= pbind (K2 S) xn.((\x. reify f1) (fst xn) (snd xn)) f2)
Therefore, we can pick S' = S
K' S' = pbind (K2 S) xn.((\x. reify f1) (fst xn) (snd xn))
f' = f2
With this choice of (K' S'), we have ( sort_of (K S)
= sort_of (reify (F : ST) S)
= Active
= sort_of (pbind (K2 S) xn.((\x. reify f1) (fst xn) (snd xn)))
= sort_of (K' S'))
As a result, we have proved case 2 of R (K S f).
Case when IH returns case 3:
In this case, the IH tells us that ( (S, [pbind (K1 S) xn.((\x. reify f1) (fst xn) (snd xn))] f)
= (S, stbind ([K1 S] f) x.f1)
~>* (S'', stret v))
Therefore, in the semantics of EMF*_ST we have ( (S,stbind f1 x.f2)
~>* (S'',stbind (stret v) x.f2)
~> (S'',f1[v/x])
= (S'',[reify (o : ST) S''] (f1[v/x])))
The IH also tells us that (K1 S f ~>+ pret (v,S'')).
Therefore, in the semantics of EMF*, we have ( pbind (K1 S) xn.((\x. reify f1) (fst xn) (snd xn)) f
= pbind (K1 S f) xn.((\x. reify f1) (fst xn) (snd xn))
~>+ pbind (pret (v,S'')) xn.((\x. reify f1) (fst xn) (snd xn))
~>+ reify (f1[v/x]) S''
= reify (o : ST) S'' (f1[v/x]))
Therefore, we can pick S' = S''
K' S' = reify (o : ST) S''
f' = f1[v/x]
With this choice of (K' S'), we have ( sort_of (K S)
= sort_of (reify (F : ST) S)
= Active
= sort_of (reify (o : ST) S'')
= sort_of (K' S'))
As a result, we have proved case 2 of R (K S f).
Case when IH returns case 4:
We prove this case by deriving false from (sort_of (K1 S) = Pure) and (sort_of (K1 S) = Active).
Case when IH returns case 5:
We prove this case by deriving false from (sort_of (K1 S) = Tot) and (sort_of (K1 S) = Active).
qed.