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.
induction on 2. intros. case H2.
  case H1. search.
  case H1. backchain IH.

% 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'.
induction on 1. intros. case H1.
  search.
  search.
  apply IH to H2 with S = S. apply IH to H3 with S = S. search.
  apply IH to H2 with S = S. apply IH to H3 with S = S. search.
Theorem cps_ty_pres : forall S T T',
  {is_sty S} -> {is_sty T} -> cps_ty S T T' -> {is_sty T'}.
induction on 3. intros. case H3.
  search.
  search.
  case H2. apply IH to _ _ H4. apply IH to _ _ H5. search.
  case H2. apply IH to _ _ H4. apply IH to _ _ H5. search.
Theorem cps_ty_det : forall S T T' T'',
  cps_ty S T T' -> cps_ty S T T'' -> T' = T''.
induction on 1. intros. case H1.
  case H2. search.
  case H2. search.
  case H2. apply IH to H3 H5. apply IH to H4 H6. search.
  case H2. apply IH to H3 H5. apply IH to H4 H6. search.
  
Theorem cps_sctx_exists : forall TL S,
  sctx TL -> exists TL', cps_sctx S TL TL'.
induction on 1. intros. case H1.
  search.
  apply cps_ty_exists to H3 with S = S. 
    apply IH to H2 with S = S. search.
Theorem cps_sctx_pres : forall S L L',
   {is_sty S} -> sctx L -> cps_sctx S L L' -> sctx L'.
induction on 3. intros. case H3.
  search.
  case H2. apply cps_ty_pres to _ _ H4.
    apply IH to _ _ H5. search.
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'.
induction on 3. intros. case H3.
  case H2. apply cps_ty_det to H1 H4. search.
  case H2. apply IH to H1 H6 H4. search.
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.
induction on 1. intros. case H1.
  search.
  case H2. unfold. backchain IH.
 
% 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}.
intros.
  apply cps_typ_pres to _ H1 _ _ H2 H3 _ _. search.
Theorem cps_typ_pres_atom : forall M M',
  {of M tnat} -> {cps' M M'} -> {of M' tnat}.
intros. case H2.
  apply cps_typ_pres_closed to _ H1 H3.
  assert {pi x\of x tnat => of x tnat}.
  cut H4 with H5. search.