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

Specification "trans".

Import "typing". [View typing]

%% Contexts for code hoisting
Define ch_ctx : olist -> prop by
  ch_ctx nil;
  nabla x, ch_ctx ((ch x (htm nil (hbase x))) :: L) := ch_ctx L.

Define vars_of_ch_ctx : olist -> list tm' -> prop by
  vars_of_ch_ctx nil nil;
  vars_of_ch_ctx ((ch X (htm nil (hbase X))) :: L) (X :: L') :=
    vars_of_ch_ctx L L'.

Theorem ch_ctx_mem : forall L E,
  ch_ctx L -> member E L -> exists X, 
    E = (ch X (htm nil (hbase X))) /\ name X.
induction on 2. intros. case H2.
  case H1. search.
  case H1. apply IH to _ H3. search.
Theorem ch_ctx_ctx'_sync : forall L Vs CL M,
  vars_of_ch_ctx CL Vs -> vars_of_ctx' L Vs -> 
  member (ch M (htm nil (hbase M))) CL -> exists T, member (of' M T) L.
induction on 3. intros. case H3.
  case H1. case H2. search.
  case H1. case H2. apply IH to _ _ H4. search.

% Lemmas for auxiliary predicates
Theorem cappend_str[A] : forall L (M1:list A) M2 M3,
  ch_ctx L -> {L |- appd M1 M2 M3} -> {appd M1 M2 M3}.
induction on 2. intros. case H2.
  search. 
  apply IH to _ H3. search.
  apply ch_ctx_mem to _ H4. case H3.
Theorem hconstr_str : forall L M R M',
  ch_ctx L -> {L |- hconstr M R M'} -> {hconstr M R M'}.
induction on 2. intros. case H2.
  search. 
  apply IH to _ H3. search.
  apply ch_ctx_mem to _ H4. case H3.
Theorem hcombine_str : forall L M1 M2 R M',
  ch_ctx L -> {L |- hcombine M1 M2 R M'} -> {hcombine M1 M2 R M'}.
induction on 2. intros. case H2.
  search. 
  apply IH to _ H3. search.
  apply IH to _ H3. search.
  apply ch_ctx_mem to _ H4. case H3.
Theorem hcombine3_str : forall L M1 M2 M3 R M',
  ch_ctx L -> {L |- hcombine3 M1 M2 M3 R M'} -> {hcombine3 M1 M2 M3 R M'}.
induction on 2. intros. case H2.
  search.
  apply IH to _ H3. search.
  apply IH to _ H3. search.
  apply IH to _ H3. search.
  apply ch_ctx_mem to _ H4. case H3.
Theorem hcombine_abs_str : forall L M R R' M',
  ch_ctx L -> {L |- hcombine_abs M R R' M'} -> {hcombine_abs M R R' M'}.
induction on 2. intros. case H2.
  search. 
  apply IH to _ H3. search.
  apply IH to _ H3. search.
  apply ch_ctx_mem to _ H4. case H3.
Theorem crev_str[A] : forall L (L1:list A) L2 L3,
  ch_ctx L -> {L |- rev L1 L2 L3} -> {rev L1 L2 L3}.
induction on 2. intros. case H2.
  search.
  apply IH to _ H3. search.
  apply ch_ctx_mem to _ H4. case H3.
Theorem tm'_list_to_tuple_str : forall L L' T,
  ch_ctx L -> {L |- tm'_list_to_tuple L' T} -> {tm'_list_to_tuple L' T}.
induction on 2. intros. case H2.
  search.
  apply IH to _ H3. search.
  apply ch_ctx_mem to _ H4. case H3.
Theorem hoist_abs_str : forall L R f l FA R' F',
  ch_ctx L -> {L |- hoist_abs R f l FA R' F'} -> {hoist_abs R f l FA R' F'}.
induction on 2. intros. case H2.
  apply crev_str to _ H3. apply tm'_list_to_tuple_str to _ H4. search.
  apply IH to _ H3. search.
  apply ch_ctx_mem to _ H4. case H3.
Theorem abstract_str : forall L R R' F,
  ch_ctx L -> {L |- abstract R R' F} -> {abstract R R' F}.
intros. case H2.
  apply hoist_abs_str to _ H3. search.
  apply ch_ctx_mem to _ H4. case H3.
Theorem hconstr_typ_pres : forall L FE M M' T T' R, nabla x,
  ctx' L -> {L |- of'' (htm FE M) T} -> {of' x T |- of' (R x) T'} ->
   {hconstr M R M'} -> {L |- of'' (htm FE M') T'}.
induction on 4. intros. case H4.
  case H2.
    inst H3 with n1 = M1. cut H6 with H5. search.
    apply ctx'_mem to _ H6. case H5.
  case H2.
    apply of'_is_cty to _ H6. 
      assert {of' n2 T |- of' (R n2) T'}. 
        apply IH to _ H7 H9 H5 with x = n2.
      search.
    apply ctx'_mem to _ H7. case H6.
Theorem hcombine_typ_pres : forall L FE1 FE2 FE M1 M2 M T1 T2 T R, nabla x y,
  ctx' L -> {L |- of'' (htm FE1 M1) T1} -> {L |- of'' (htm FE2 M2) T2} -> 
  {of' x T1, of' y T2 |- of' (R x y) T} -> {hcombine M1 M2 R M} -> 
  {appd FE1 FE2 FE} -> {L |- of'' (htm FE M) T}.
induction on 5. intros. case H5.
  case H2. case H3. case H6.
    inst H4 with n1 = M4, n2 = M3.
    cut H9 with H7. cut H10 with H8. search.
    % Context cases
    apply ctx'_focus_inv to _ _ H8. apply ctx'_focus_inv to _ _ H7.
  case H2. case H6.
    assert {L, of' n1 T3 |- of'' (htm FE2 M2) T2}. 
    assert {of' n2 T1, of' n3 T2 |- of' (R n2 n3) T}.
    apply of'_is_cty to _ H8. apply IH to _ H9 H11 H12 H7 _. search.
    % Context case
    apply ctx'_focus_inv to _ _ H8.   
  case H2(keep). case H3. case H6.
    assert {L, of' n1 T3 |- of'' (htm nil (hbase M3)) T1}.
    assert {of' n2 T1, of' n3 T2 |- of' (R n2 n3) T}.
    apply of'_is_cty to _ H9. apply IH to _ H11 H10 H12 H7 _. search.
    % Context case
    apply ctx'_focus_inv to _ _ H9. apply ctx'_focus_inv to _ _ H8.
Theorem hcombine3_typ_pres : forall L FE1 FE2 FE3 FE12 FE M1 M2 M3 M T1 T2 T3 T R, 
  nabla x y z, ctx' L -> {L |- of'' (htm FE1 M1) T1} -> {L |- of'' (htm FE2 M2) T2} -> 
  {L |- of'' (htm FE3 M3) T3} -> {of' x T1, of' y T2, of' z T3 |- of' (R x y z) T} ->
  {hcombine3 M1 M2 M3 R M} -> {appd FE1 FE2 FE12} -> {appd FE12 FE3 FE} ->
    {L |- of'' (htm FE M) T}.
induction on 6. intros. case H6.
  case H2. case H3. case H4.
    case H7. case H8. inst H5 with n1 = M6, n2 = M5, n3 = M4.
    cut H12 with H9. cut H13 with H10. cut H14 with H11. search.
    % Context cases
    apply ctx'_focus_inv to _ _ H11.
    apply ctx'_focus_inv to _ _ H10.
    apply ctx'_focus_inv to _ _ H9.
  case H2. case H7. case H8.
    assert {L, of' n1 T4 |- of'' (htm FE2 M2) T2}.
    assert {L, of' n1 T4 |- of'' (htm FE3 M3) T3}.
    apply of'_is_cty to _ H10.
    apply IH to _ H11 H14 H15 _ H9 _ _. search.
    % Context case
    apply ctx'_focus_inv to _ _ H10.
  case H2. case H3. case H7. case H8.
    assert {L, of' n1 T4 |- of'' (htm FE3 M3) T3}.
    assert {L, of' n1 T4 |- of'' (htm nil (hbase M5)) T1}.
    apply of'_is_cty to _ H11.
    apply IH to _ H15 H12 H14 _ H9 _ _. search.
    % Context cases    
    apply ctx'_focus_inv to _ _ H11.
    apply ctx'_focus_inv to _ _ H10.
  case H2. case H3. case H4.
    case H7. case H8.
    assert {L, of' n1 T4 |- of'' (htm nil (hbase M5)) T1}.
    assert {L, of' n1 T4 |- of'' (htm nil (hbase M4)) T2}.
    apply of'_is_cty to _ H12.
    apply IH to _ H14 H15 H13 _ H9 _ _. search.
    % Context cases
    apply ctx'_focus_inv to _ _ H12.
    apply ctx'_focus_inv to _ _ H11.
    apply ctx'_focus_inv to _ _ H10.
    

Theorem hcombine_abs_let_typ_pres : forall L FE1 FE2 FE M1 R M T1 T, nabla x,
  ctx' L -> {L |- of'' (htm FE1 M1) T1} -> {L, of' x T1 |- of'' (htm FE2 (R x)) T} -> 
  {hcombine_abs M1 R (x\y\let' x y) M} -> {appd FE1 FE2 FE} -> 
    {L |- of'' (htm FE M) T}.
induction on 4. intros. case H4.
  apply of''_is_cty to _ H2. case H2. case H3. case H5.
    search.
    % Context cases
    apply ctx'_focus_inv to _ _ H8. apply ctx'_focus_inv to _ _ H7.
  case H2. case H5.
    assert {L, of' n1 T2, of' n2 T1 |- of'' (htm FE2 (R n2)) T}.
    apply of'_is_cty to _ H7. apply IH to _ H8 H10 H6 H9. search.
    % Context case
    apply ctx'_focus_inv to _ _ H7.   
  apply of''_is_cty to _ H2. case H2(keep). case H3. case H5.
    assert {L, of' n2 T2 |- of'' (htm nil (hbase M2)) T1}.
    assert {L, of' n2 T2, of' n1 T1 |- of'' (htm FE4 (R1 n1 n2)) T}.
    apply of'_is_cty to _ H8. apply of'_is_cty to _ H9. 
    inst H6 with n1 = n2. apply IH to _ H11 H12 H15 _.
    apply of'_str to _ _ H9. search.
    % Context case
    apply ctx'_focus_inv to _ _ H9. apply ctx'_focus_inv to _ _ H8.
Theorem hoist_abs_fun_typ : forall L T1 T2 TE R R' G E FA F, nabla x,
  ctx' L -> {is_cty T1} -> {L, of' x T1 |- of''_body TE (R x) T2} -> 
  {hoist_abs R G E FA R' F} -> 
    {L, of' E TE, of' x T1 |- of' (F x) T2}.
induction on 4. intros. case H4.
  case H3. 
    search.
    apply ctx'_focus_inv to _ _ H7.
  case H3.      
    assert {L, of' n2 T3, of' n1 T1 |- of''_body TE1 (R1 n1 n2) T2}.
      inst H5 with n1 = n2. apply is_cty_str to _ H7.
      apply IH to _ _ H8 H9.
      assert {of' E (prod T3 TE1) |- of' (snd' E) TE1}.
      cut H11 with H12. search.
    apply ctx'_focus_inv to _ _ H6.
Theorem abstract_fun_typ : forall L T1 T2 TE R R' F, nabla x,
  ctx' L -> {is_cty T1} -> {L, of' x T1 |- of''_body TE (R x) T2} -> 
  {abstract R R' F} ->
    nabla l, {L, of' l TE, of' x T1 |- of' (F l x) T2}.
intros. case H4.
  inst H5 with n1 = n2, n2 = n3.
  apply hoist_abs_fun_typ to _ _ H3 H6. search.

Define ctx'_env_typ_split : olist -> ty -> ty -> prop by
  ctx'_env_typ_split nil TE TE;
  ctx'_env_typ_split (of' X T :: L') TE' TE :=
    ctx'_env_typ_split L' (prod T TE') TE.

% ctx2' L L1 L2 holds iff (L = L1,L2)
Define ctx2' : olist -> olist -> olist -> prop by
  ctx2' L L nil := ctx' L;
  nabla x, ctx2' (of' x T :: L) L1 (of' x T :: L2) :=
    ctx2' L L1 L2 /\ {is_cty T}.

Theorem ctx2'_nil1 : forall L L2,
  ctx2' L nil L2 -> L = L2.
induction on 1. intros. case H1.
  search.
  apply IH to H2. search.
Theorem ctx2'_move_head : forall L E L1 L2,
  ctx2' L (E :: L1) L2 -> 
    exists L', ctx2' L' L1 (E :: L2) /\ subset L' L.
induction on 1. intros. case H1.
  case H2.
    exists (of' n1 T :: L3). split.
      search.
      backchain subset_refl. unfold. backchain ctx'_islist.
  apply IH to H2. case H4.
    exists (of' n2 T1 :: of' n1 T :: L4). split.
      search. 
      unfold.
        case H5. search.
        unfold. search. case H5. backchain subset_add.
Theorem ctx2'_is_ctx : forall L L1 L2,
  ctx2' L L1 L2 -> ctx' L.
induction on 1. intros. case H1.
  search.
  apply IH to H2. search.
Theorem ctx2'_is_ctx2 : forall L L1 L2,
  ctx2' L L1 L2 -> ctx' L2.
induction on 1. intros. case H1.
  search.
  apply IH to H2. search.
Define ctx'_prod : olist -> ty -> prop by
  ctx'_prod nil tunit;
  ctx'_prod (of' X T :: L) (prod T TE) := 
    ctx'_prod L TE.

Theorem type_of_tuple : forall L TE Vs FA,
  ctx'_prod L TE -> vars_of_ctx' L Vs -> {tm'_list_to_tuple Vs FA} ->
    {L |- of' FA TE}.
induction on 1. intros. case H1.
  case H2. case H3. search.
  case H2. case H3. apply IH to H4 H5 H6. search.
Theorem type_of_env_tuple : forall L L1 L2 Vs TE TE' Vs1 Vs2 FA,
  ctx2' L L1 L2 -> vars_of_ctx' L1 Vs1 -> vars_of_ctx' L2 Vs2 -> 
  ctx'_prod L2 TE' -> ctx'_env_typ_split L1 TE' TE -> {rev Vs1 Vs2 Vs} -> 
  {tm'_list_to_tuple Vs FA} -> {L |- of' FA TE}.
induction on 5. intros. case H5.
  case H2. case H6. apply ctx2'_nil1 to H1. backchain type_of_tuple.
  case H2. case H6. 
    apply ctx2'_move_head to H1.
    apply IH to H11 _ _ _ H8 H10 H7.
    monotone H13 with L.
      intros. apply subset_mem_trans to H12 H14. search.
    search.
  
Theorem hoist_abs_body_typ : forall L L1 L2 T1 T2 TE TE' R R' G E Vs F, nabla x,
  ctx2' L L1 L2 -> {is_cty T1} -> vars_of_ctx' L2 Vs ->
  ctx'_env_typ_split L2 TE' TE ->
  {L, of' x T1 |- of''_body TE' (R x) T2} -> {hoist_abs R G E Vs R' F} ->
    {L2, of' G (arr' TE (arr' T1 T2)) |- of''_body TE' R' (arr' T1 T2)}.
induction on 6. intros. case H6.
  case H5.
    apply ctx2'_is_ctx2 to H1. 
      apply type_of_env_tuple to _ H3 _ _ H4 H7 H8 with L = L2.
      search.
    apply ctx2'_is_ctx to H1. apply ctx'_focus_inv to _ _ H9.
  case H5.
    assert {L, of' n1 T3, of' n2 T1 |- of''_body TE1 (R1 n2 n1) T2}.
      apply ctx2'_is_ctx to H1. apply is_cty_str to _ H9.
      assert ctx2' (of' n1 T3 :: L) L1 (of' n1 T3 :: L2).
      apply IH to H13 _ _ _ H10 H7.
      search.
    apply ctx2'_is_ctx to H1. apply ctx'_focus_inv to _ _ H8.
Theorem abstract_body_typ : forall L T1 T2 TE R R' F, nabla x,
  ctx' L -> {is_cty T1} ->
  {L, of' x T1 |- of''_body TE (R x) T2} -> {abstract R R' F} ->
    nabla g, {of' g (arr' TE (arr' T1 T2)) |- of''_body TE (R' g) (arr' T1 T2)}.
intros. case H4.
  assert {hoist_abs R n2 n3 nil (R' n2) (x\F n3 x)}.
  apply hoist_abs_body_typ to _ _ _ _ H3 H6 with TE' = TE.
  search.
    

% Type preservation lemma
Theorem ch_typ_pres: forall L CL Vs M M' T,
  ctx' L -> ch_ctx CL -> vars_of_ctx' L Vs -> 
  vars_of_ch_ctx CL Vs -> {L |- of' M T} -> {CL |- ch M M'} ->
    {L |- of'' M' T}.
induction on 6. intros. case H6.
  % Case: M = (nat' N)
  case H5.
    search.

    %Context case
    apply ctx'_focus_inv to _ _ H7. case H9.

  % Case: M = (pred' M1)
  case H5.
    apply IH to _ _ _ _ H9 H7. apply hconstr_str to _ H8.
    apply hconstr_typ_pres to _ H10 _ H11. search.
  
    %Context case
    apply ctx'_focus_inv to _ _ H9. case H11.

  % Case: M = (plus' M1 M2)
  case H5.
    apply IH to _ _ _ _ H11 H7. apply IH to _ _ _ _ H12 H8.
    apply hcombine_str to _ H10. apply cappend_str to _ H9.
    apply hcombine_typ_pres to _ H13 H14 _ H15 H16. search.

    %Context case
    apply ctx'_focus_inv to _ _ H11. case H13.

  % Case: M = (ifz' M1 M2 M3)
  case H5.
    apply IH to _ _ _ _ H13 H7. apply IH to _ _ _ _ H14 H8.
    apply IH to _ _ _ _ H15 H9. apply hcombine3_str to _ H12.
    apply cappend_str to _ H10. apply cappend_str to _ H11.
    apply hcombine3_typ_pres to _ H16 H17 H18 _ H19 H20 H21. 
    search.
    
    %Context case
    apply ctx'_focus_inv to _ _ H13. case H15.

  % Case: M = unit'
  case H5.
    search.
  
    %Context case
    apply ctx'_focus_inv to _ _ H7. case H9.

  % Case: M = (pair' M1 M2)
  case H5.
    apply IH to _ _ _ _ H11 H7. apply IH to _ _ _ _ H12 H8.
    apply hcombine_str to _ H10. apply cappend_str to _ H9.
    apply hcombine_typ_pres to _ H13 H14 _ H15 H16. search.

    %Context case
    apply ctx'_focus_inv to _ _ H11. case H13.

  % Case: M = (let' M1 R)
  case H5.
    apply IH to _ _ _ _ H11 H7. apply of'_is_cty to _ H11. 
    apply IH to _ _ _ _ H12 H8.
    apply hcombine_abs_str to _ H10. apply cappend_str to _ H9.
    apply hcombine_abs_let_typ_pres to _ H13 H15 H16 H17. search.

    %Context case
    apply ctx'_focus_inv to _ _ H11. case H13.

  % Case: M = (fst' M1)
  case H5.
    apply IH to _ _ _ _ H9 H7. apply hconstr_str to _ H8.
    apply hconstr_typ_pres to _ H10 _ H11. search.
  
    %Context case
    apply ctx'_focus_inv to _ _ H9. case H11.

  % Case: M = (snd' M1)
  case H5.
    apply IH to _ _ _ _ H9 H7. apply hconstr_str to _ H8.
    apply hconstr_typ_pres to _ H10 _ H11. search.
  
    %Context case
    apply ctx'_focus_inv to _ _ H9. case H11.

  % Case: M = (app' M1 M2)
  case H5.
    apply IH to _ _ _ _ H11 H7. apply IH to _ _ _ _ H12 H8.
    apply hcombine_str to _ H10. apply cappend_str to _ H9.
    apply hcombine_typ_pres to _ H13 H14 _ H15 H16. search.

    %Context case
    apply ctx'_focus_inv to _ _ H11. case H13.

  % Case: M = (abs' R)
  case H5.
    apply is_cty_str to _ H10. apply IH to _ _ _ _ H9 H7.
    apply abstract_str to _ H8. 
    apply of''_to_alter_ver to _ H12. apply of''_env_str to _ _ H14.
    apply abstract_fun_typ to _ _ H15 H13.
    apply abstract_body_typ to _ _ H15 H13.
    apply of''_env_is_cty to _ H16. apply of'_is_cty to _ H9.
    assert {L |- of''_body (prod (arr' TE (arr' T1 T2)) TE) (habs R'') (arr' T1 T2)}.
    assert {L |- of''_env ((abs' (l\abs' (x\F l x))) :: FE)
                   (prod (arr' TE (arr' T1 T2)) TE)}.
    apply of''_from_alter_ver to _ H22 H21. search.
    
    %Context case
    apply ctx'_focus_inv to _ _ H9. case H11.

  % Case: M = (clos' M1 M2)
  case H5.
    apply IH to _ _ _ _ H11 H7. apply IH to _ _ _ _ H12 H8.
    apply hcombine_str to _ H10. apply cappend_str to _ H9.
    apply hcombine_typ_pres to _ H13 H14 _ H15 H16. search.

    %Context case
    apply ctx'_focus_inv to _ _ H11. case H13.

  % Case: M = (open' M1 (f\e\app' f (pair' M1 (pair' M2 e))))
  case H5.
    apply IH to _ _ _ _ H11 H7. apply IH to _ _ _ _ H12 H8.
    apply hcombine_str to _ H10. apply cappend_str to _ H9.
    apply hcombine_typ_pres to _ H13 H14 _ H15 H16. search.

    %Context case
    apply ctx'_focus_inv to _ _ H11. case H13.
  
  % Case: M = x
  apply ch_ctx_mem to _ H8. case H7. 
    apply ch_ctx_ctx'_sync to H4 H3 H8. case H9.
    case H5. apply ctx'_mem to _ H12. case H11.
    apply ctx'_mem_sync to _ H10 H12. search.
    

Theorem ch_typ_pres_closed : forall M M' T,
  {of' M T} -> {ch M M'} -> {of'' M' T}.
intros. apply ch_typ_pres to _ _ _ _ H1 H2. search.