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.