Executable Specification

[View trans]

Reasoning

[View ch_typ_pres]

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 cnil (hbase x))) :: L) := ch_ctx L.

Define vars_of_ch_ctx : olist -> tm'_list -> prop by
  vars_of_ch_ctx nil cnil;
  vars_of_ch_ctx ((ch X (htm cnil (hbase X))) :: L) (ccons 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 cnil (hbase X))) /\ name' X.

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 cnil (hbase M))) CL -> exists T, member (of' M T) L.


% Lemmas for auxiliary predicates
Theorem cappend_str : forall L M1 M2 M3,
  ch_ctx L -> {L |- cappend M1 M2 M3} -> {cappend M1 M2 M3}.

Theorem hconstr_str : forall L M R M',
  ch_ctx L -> {L |- hconstr M R M'} -> {hconstr M R M'}.

Theorem hcombine_str : forall L M1 M2 R M',
  ch_ctx L -> {L |- hcombine M1 M2 R M'} -> {hcombine M1 M2 R M'}.

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'}.

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'}.

Theorem crev_str : forall L L1 L2 L3,
  ch_ctx L -> {L |- crev L1 L2 L3} -> {crev L1 L2 L3}.

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}.

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'}.

Theorem abstract_str : forall L R R' F,
  ch_ctx L -> {L |- abstract R R' F} -> {abstract R R' F}.

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'}.

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} -> 
  {cappend FE1 FE2 FE} -> {L |- of'' (htm FE M) T}.

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} -> {cappend FE1 FE2 FE12} -> {cappend FE12 FE3 FE} ->
    {L |- of'' (htm FE M) T}.
    

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} -> {cappend FE1 FE2 FE} -> 
    {L |- of'' (htm FE M) T}.

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}.

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}.


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.

Theorem ctx2'_move_head : forall L E L1 L2,
  ctx2' L (E :: L1) L2 -> 
    exists L', ctx2' L' L1 (E :: L2) /\ subset L' L.

Theorem ctx2'_is_ctx : forall L L1 L2,
  ctx2' L L1 L2 -> ctx' L.

Theorem ctx2'_is_ctx2 : forall L L1 L2,
  ctx2' L L1 L2 -> ctx' L2.

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}.

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 -> {crev Vs1 Vs2 Vs} -> 
  {tm'_list_to_tuple Vs FA} -> {L |- of' FA TE}.
  
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)}.

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)}.
    

% 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 (ccons (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.