The general strategy is to define a type-preserving translation from
emf* to CiC, showing the translation to be a simulation
--------------------------------------------------------------------------------
We take this to be a definition of a fragment of CiC
P, Q ::= x
| Type_i
| | | False
| I | | True
| \x:P. Q | P Q | Pi x:P. Q
| (P, Q) | fst P | snd P | prod
| Inl P | Inr P | case (P as y) \x.P \x.Q returns P' | sum
G ::= . | G, x1:P
With the standard typing and reduction rules
G ok
---------------
G |- x : G(x)
G ok
---------------
G |- x : G(x)
---------------------------
G |- Type_i : Type_{i+1}
-------------------
G |- False : Type0
-------------------
G |- True : Type0
-------------------
G |- I : True
....
G |- e : sum Q1 Q2
G, y:sum Q1 Q2 |- Q : Type_i
G, x:Q1 |- P1 : Q [Inl x/y]
G, x:Q2 |- P2 : Q [Inr x/y]
--------------------------------------------------- [C-Case]
G |- case (P as y) \x.P1 \x.P2 returns Q : Q[P/y]
--------------------------------------------------------------------------------
Fact (CiC is SN): G |- M : N ==> M is strongly normalizing.
--------------------------------------------------------------------------------
Translation of emf* to CiC
_______________
| |
| trans_S T = P |
|_______________|
With respect to a fixed signature S, and emf* term T is
translated to a CiC term P
Since the signature S is invariant, we leave it implicit below.
The translation is very uniform:
0. Erase refinement types
1. Erase the WPs from computation types
2. Erase reify and reflect
3. Inline the definitions of return, bind, lift, and the actions
Following the syntax of emf* reproduced here:
wp, t, e ::= x | a -- where x and a are both variables
| Type_i
| T
| x:t{t'}
| x:t -> C
| fun (x:t) -> e
| e1 e2
| case (e as y) x.e1 y.e2 returns t -- dependent sum elimination
| run e -- "reify" for pure terms
| reify e
| reflect e
| M.return t e -- written explicitly
| M.bind t1 t2 wp1 e1 wp2 x.e2
| M.lift_M' t wp e
| M.a ts -- fully applied actions
trans x = x
trans a = a
trans Type_i = Type_i
trans unit = True
trans false = False
trans prod = prod
trans sum = sum
...
translation of all remaining constants are just the identity
trans (x:t{t'}) = trans t //just erase the refinement
trans (x:t -> C) = Pi x:trans t. transC C
transC (Tot t) = trans t
transC (Pure t wp) = trans t //just erase the WPs
transC (F t wp) = trans (S.unfold (F t wp))
where S.unfold (F t wp) is the representation of (F t wp)
trans (fun (x:t) -> e) = \x:trans t. trans e
trans (case (e as y) x.e1 x.e2 returns t)
= case (trans e as y) x.trans e1
x.trans e2
returns (trans t)
trans (run e) = trans e
trans (reify e) = trans e
trans (reflect e) = trans e
trans (Pure.return _ e) = trans e
trans (Pure.bind t1 t2 _ _ e \x.e2) = (\x:trans t1. trans e2) (trans e)
trans (M.bind t1 t2 wp1 wp2 e1 e2)
= (trans (S.unfold (M.bind)))
(trans t1)
(trans t2)
(trans wp1)
(trans wp2)
(trans e1)
(transe e2)
trans (M.return t e)
= (trans (S.unfold (M.return)))
(trans t)
(trans e)
trans (M.lift_M' t wp e)
= (trans (S.unfold (M.lift_M')))
(trans t)
(trans wp)
(trans e)
trans (M.a ts)
= (trans (S.unfold M.a))
(trans ts)
--------------------------------------------------------------------------------
Lemma 1 (Translation preserves types):
S; G |- e : C
==> trans_S G |- trans_S e : transC_s C
Proof: Easy induction on the structure of the emf* typing derivation.
We illustrate a couple of the main cases:
Case (T-Reify):
S; G |- reify e : Tot (S.unfold (F t wp))
From the premise, we have:
S; G |- e : F t wp
From the IH: we have
trans_S G |- trans_S e : trans_S (F t wp)
where trans_S (F t wp) = trans_S (S.unfold (F t wp))
which is exactly what is needed for the conclusion,
since trans_S (reify e) = trans_S e
Case (T-Reflect): Just the dual of T-Reify.
Case (T-Return):
S; G |- M.return t e : M t _
with
S; G |- t : Tot Type0
S; G |- e : Tot t
From the IH: we have, in translated contexts
trans_S t : Type_i
trans_S e : trans_s t
We need to show that
(S.unfold M.return) (trans_S t) (trans_S e) : trans_S (M t _)
But, from well-formedness of S;G, we have
(S.unfold M.return) : a:Type0 -> x:a -> Tot (S.unfold (M a _))
From which the proof is nearly immediate.
Case (T-Bind): Like T-Return, but with many more arguments.
--------------------------------------------------------------------------------
Lemma 1.1 (Substitution commutes with translation)
forall e v. trans (e[v/x]) = trans e [trans v / x]
Proof: Easy induction on e, noting that in most cases, translation is
just homomorphic.
--------------------------------------------------------------------------------
Lemma 2 (Translation is a forward simulation):
There exists a well-founded relation >> on emf* terms such that
forall e, e'.
e ~> e'
==> (trans e' = trans e /\ e >> e') //no steps in CiC, but decreases according to >>
\/ (trans e -> trans e') //CiC steps
Proof:
Pick e1 >> e2 to be:
(one case for each Reify-* rule)
1. reify (reflect v) >> v (Reify-Reflect)
2. run (Pure.return v) >> v (Reify-PureRet)
3. reify (M.return t e) (Reify-Ret)
>> (S.unfold M.return) t e
4. run (Pure.bind t1 t2 _ _ c v) (Reify-PureBind)
>> run (v (run c))
5. reify (M.bind t1 t2 wp1 wp2 c1 \x.c2) (Reify-Bind)
>> (S.unfold M.bind)
(reify t1)
(reify t2)
(reify wp1)
(reify wp2)
(reify c1)
(\x. reify c2)
... one such case for each Reify-* rule
n. e1 >> e2 ==> E[e1] >> E[e2], for any evaluation context E.
>> is trivially well-founded: in fact, using a well-founded
relation here is overkill, since the relation is extremely
simple, just relating pairs of points, without any chains to
consider.
The proof is by induction on the transition relation e ~> e'
Case (Beta): e1 = (fun (x:t) -> e1')
e2 = v
e' = e1'[v/x]
trans e1 = \x:trans t. trans e1'
trans e2 = trans v
trans e' = trans(e1'[v/x])
= trans(e1')[trans v / x] by Lemma 1.1
case (Proj-L, Proj-R): Easy
case (Case-L, Case-R): Easy, using Lemma 1.1
case (Reify-Reflect):
e = reify (reflect v)
e' = v
trans e = trans v
trans e' = trans v'
Conclude using the LHS of the disjunction and case 3 of >>.
case (Reify-PureRet, Reify-PureBind, ...)
All these cases are similar to Reify-Reflect
Case (Context):
Broadly, using
1. the induction hypothesis
2. the closure of >> by emf* evaluation contexts
3. showing that every emf* evaluation context is matched by a CiC redex
--------------------------------------------------------------------------------
Theorem: S; G |- e : C ==> e is normalizing
Proof:
From Lemma 1: trans_S G |- trans_S e : trans_S C
From Fact (CiC is SN): trans_S e has no infinite reduction sequence.
For contradiction, suppose e has an infinite reduction sequence.
But, from Lemma 2, every reduction sequence in emf* can be broken
into a sequence of finite-length fragments, where each such fragment
is matched by a single step of reduction in CiC.
Since there are no infinite reduction sequences in CiC, e cannot have
an infinite reduction.