Executable Specification

[View trans]

Reasoning

[View cps_typ_pres]

Click on a command or tactic to see a detailed view of its use.

Specification "trans".

Import "typing". [View typing]

% CPS context
Define cctx : olist -> prop by
  cctx nil;
  nabla x, cctx ((pi k\ cps x k (k x)) :: L) := cctx L.

Define vars_of_cctx : olist -> list tm -> prop by
  vars_of_cctx nil nil;
  nabla x, vars_of_cctx ((pi k\ cps x k (k x)):: L) (x :: L') :=
    vars_of_cctx L L'.

Theorem cctx_mem : forall L E,
  cctx L -> member E L -> 
    exists X, E = (pi k\ cps X k (k X)) /\ name X.


% Translation to CPS types
Define cps_ty : ty -> ty -> ty -> prop by
  cps_ty T tnat tnat;
  cps_ty T tunit tunit;
  cps_ty T (prod T1 T2) (prod T1' T2') :=
    cps_ty T T1 T1' /\ cps_ty T T2 T2';
  cps_ty T (arr T1 T2) (arr (prod (arr T2' T) T1') T):=
    cps_ty T T1 T1' /\ cps_ty T T2 T2'.

Define cps_sctx : ty -> olist -> olist -> prop by
  cps_sctx S nil nil;
  nabla x, cps_sctx S (of x T :: L) (of x T' :: L') :=
    cps_ty S T T' /\ cps_sctx S L L'.

Theorem cps_ty_exists : forall S T,
  {is_sty T} -> exists T', cps_ty S T T'.

Theorem cps_ty_pres : forall S T T',
  {is_sty S} -> {is_sty T} -> cps_ty S T T' -> {is_sty T'}.

Theorem cps_ty_det : forall S T T' T'',
  cps_ty S T T' -> cps_ty S T T'' -> T' = T''.
  
Theorem cps_sctx_exists : forall TL S,
  sctx TL -> exists TL', cps_sctx S TL TL'.

Theorem cps_sctx_pres : forall S L L',
   {is_sty S} -> sctx L -> cps_sctx S L L' -> sctx L'.

Theorem cps_sctx_mem_sync: forall S T T' TL TL' M,
  cps_ty S T T' -> cps_sctx S TL TL' -> member (of M T) TL -> member (of M T') TL'.

Theorem cps_sctx_vars_sync: forall S TL TL' Vs,
  cps_sctx S TL TL' -> vars_of_sctx TL Vs -> vars_of_sctx TL' Vs.
 
% Type preservation
Theorem cps_typ_pres : forall TL CL M T K M' T' TL' S, 
  {is_sty T} -> {is_sty S} -> sctx TL -> cctx CL -> 
  {TL |- of M T} -> {CL |- cps M K M'} -> 
  cps_ty S T T' -> cps_sctx S TL TL' ->
    {TL', pi x\ of x T' => of (K x) S |- of M' S}.
induction on 6. intros. case H6. % Case: M = nat N, M' = K (nat N) apply sof_nat_inv to _ H5. case H7. search. % Case: M = pred M1 case H5. case H7. assert {TL', pi x\ of x tnat => of (let (pred x) K) S |- of M' S}. backchain IH. assert {pi x\of x tnat => of (K x) S |- pi x\of x tnat => of (let (pred x) K) S}. cut H11 with H12. search. % Context case apply sctx_mem to _ H11. case H10. case H12. % Case: M = plus M1 M2 case H5. case H7. assert {TL', pi x\ of x tnat => of (M2' x) S |- of M' S}. backchain IH. assert {TL', pi x\ of x tnat => of (let (plus n1 x) K) S |- of (M2' n1) S}. backchain IH with M = M2. assert {pi x\of x tnat => of (K x) S, of n1 tnat |- pi x\of x tnat => of (let (plus n1 x) K) S}. cut H14 with H15. assert {TL', pi x\of x tnat => of (K x) S |- pi x\of x tnat => of (M2' x) S}. cut H13 with H17. search. % Context case apply sctx_mem to _ H12. case H11. case H13. % Case: M = ifz M1 M2 M3 case H5. assert {TL', pi x\of x tnat => of (let (fix f\K) (k\ifz x (M2' k) (M3' k))) S |- of M' S}. backchain IH with M = M1, T = tnat. assert {TL', pi x\of x T' => of (app n1 x) S |- of (M2' n1) S}. backchain IH with M = M2, T = T. assert {TL', pi x\of x T' => of (app n1 x) S |- of (M3' n1) S}. backchain IH with M = M3, T = T. assert {of n1 (arr T' S) |- pi x\ of x T' => of (app n1 x) S}. cut H16 with H18. cut H17 with H18. assert {TL', of n1 (arr T' S), of n2 tnat |- of (ifz n2 (M2' n1) (M3' n1)) S}. assert {pi x\of x T' => of (K x) S |- of (fix f\K) (arr T' S)}. apply cps_ty_pres to _ _ H7. search. assert {TL', pi x\of x T' => of (K x) S |- pi x\ of x tnat => of (let (fix f\K) (k\ifz x (M2' k) (M3' k))) S}. cut H15 with H23. search. % Context case apply sctx_mem to _ H13. case H12. case H14. % Case: M = unit. apply sof_unit_inv to _ H5. case H7. search. % Case: M = pair M1 M2 case H5. case H7. apply sof_is_sty to _ H11. apply sof_is_sty to _ H12. assert {TL', pi x\ of x T1' => of (M2' x) S |- of M' S}. backchain IH with M = M1, T = T1. assert {TL', pi x\ of x T2' => of (let (pair n1 x) K) S |- of (M2' n1) S}. backchain IH with M = M2, T = T2. assert {pi x\of x T' => of (K x) S, of n1 T1' |- pi x\of x T2' => of (let (pair n1 x) K) S}. cut H18 with H19. assert {TL', pi x\of x T' => of (K x) S |- pi x\of x T1' => of (M2' x) S}. cut H17 with H21. search. % Context case apply sctx_mem to _ H12. case H11. case H13. % Case: M = fst M1 case H5. apply sof_is_sty to _ H10. case H11. assert exists T2', cps_ty S T2 T2'. backchain cps_ty_exists. case H14. assert {TL', pi x\ of x (prod T' T2') => of (let (fst x) K) S |- of M' S}. backchain IH with M = M1, T = prod T T2. assert {pi x\of x T' => of (K x) S |- pi x\of x (prod T' T2') => of (let (fst x) K) S}. cut H16 with H17. search. % Context case apply sctx_mem to _ H11. case H10. case H12. % Case: M = snd M1 case H5. apply sof_is_sty to _ H10. case H11. assert exists T1', cps_ty S T1 T1'. backchain cps_ty_exists. case H14. assert {TL', pi x\ of x (prod T1' T') => of (let (snd x) K) S |- of M' S}. backchain IH with M = M1, T = prod T1 T. assert {pi x\of x T' => of (K x) S |- pi x\of x (prod T1' T') => of (let (snd x) K) S}. cut H16 with H17. search. % Context case apply sctx_mem to _ H11. case H10. case H12. % Case: M = let M1 R case H5. apply sof_is_sty to _ H11. assert exists T1', cps_ty S T1 T1'. backchain cps_ty_exists. case H14. assert {TL', of n1 T1', pi x\ of x T' => of (K x) S |- of (R' n1) S}. backchain IH with M = R n1, T = T, TL = of n1 T1 :: TL, CL = (pi k\cps n1 k (k n1)) :: CL. assert {TL', pi x\ of x T1' => of (R' x) S |- of M' S}. backchain IH with M = M1, T = T1. assert {TL', pi x\ of x T' => of (K x) S |- pi x\ of x T1' => of (R' x) S}. cut H17 with H18. search. % Context case apply sctx_mem to _ H12. case H11. case H13. % Case: M = fix R case H5. assert exists T1' T2', T' = (arr (prod (arr T2' S) T1') S). case H7. search. case H12. case H7. case H1. apply cps_ty_pres to _ _ H13. apply cps_ty_pres to _ _ H14. assert {TL', of n2 (arr (prod (arr T2' S) T1') S), of n3 T1', pi x\ of x T2' => of (app n1 x) S |- of (R' n2 n1 n3) S}. backchain IH with TL = of n3 T1 :: of n2 (arr T1 T2) :: TL, TL' = of n3 T1' :: of n2 (arr (prod (arr T2' S) T1') S) :: TL', CL = (pi k\cps n3 k (k n3)) :: (pi k\cps n2 k (k n2)) :: CL, M = R n2 n3, K = y\app n1 y, M' = R' n2 n1 n3, T = T2, T' = T2', S = S. assert {of n1 (arr T2' S) |- pi x\of x T2' => of (app n1 x) S}. cut H19 with H20. assert {TL' |- of (fix (f\p\let (fst p) (k\let (snd p) (x\R' f k x)))) (arr (prod (arr T2' S) T1') S)}. search. % Context case apply sctx_mem to _ H11. case H10. case H12. % Case: M = @ M1 M2. case H5. apply sof_is_sty to _ H12. assert exists T1', cps_ty S T1 T1'. backchain cps_ty_exists. case H14. apply cps_ty_pres to _ _ H7. apply cps_ty_pres to _ _ H15. assert cps_ty S (arr T1 T) (arr (prod (arr T' S) T1') S). assert {TL', pi x\ of x (arr (prod (arr T' S) T1') S) => of (M2' x) S |- of M' S}. backchain IH with TL = TL, CL = CL, M = M1, K = M2', M' = M', T = (arr T1 T), S = S. assert {TL', pi x2\ of x2 T1' => of (let (fix (f\K)) (k\let (pair k x2) (p\app n1 p))) S |- of (M2' n1) S}. backchain IH with TL = TL, CL = CL, T = T1, S = S, M = M2, K = (x2\let (fix (f\K)) (k\let (pair k x2) (p\app n1 p))), M' = M2' n1. assert {(pi x\ of x T' => of (K x) S), of n1 (arr (prod (arr T' S) T1') S) |- pi x2\ of x2 T1' => of (let (fix (f\K)) (k\let (pair k x2) (p\app n1 p))) S}. cut H20 with H21. assert {TL', pi x\of x T' => of (K x) S |- pi x\ of x (arr (prod (arr T' S) T1') S) => of (M2' x) S}. cut H19 with H23. search. % Context case apply sctx_mem to _ H12. case H11. case H13. % Context case apply cctx_mem to _ H10. case H9. apply sctx_var_mem to _ H5 _. apply cps_sctx_mem_sync to H7 H8 H12. search.
Theorem cps_typ_pres_closed : forall S M K M', {is_sty S} -> {of M tnat} -> {cps M K M'} -> {pi x\ (of x tnat => of (K x) S) |- of M' S}. Theorem cps_typ_pres_atom : forall M M', {of M tnat} -> {cps' M M'} -> {of M' tnat}.