Library f2cps_pre

Properties of the smart constructors of the naive CPS conversion

Author : Zaynah Dargaye

Created : 29th April 2009




Require Import List.

Require Import Coqlib.

Require Import Coqlib2.

Require Import Fml.

Require Import Fml_subst.

Require Import CPS.

Require Import CPS_subst.

Require Import CPS_pre.

Require Import f2cps.

Require Import f2cps_help.




 Ltac DO_IT :=

match goal with

| [ |- context[lt_ge_dec ?a ?b] ] => 

      case_eq (lt_ge_dec a b); intros; simpl; auto; DO_IT

| [ |- context[compare_dec ?a ?b] ] =>

     case_eq(compare_dec a b); intros; simpl; auto; DO_IT

| [ |- context[match ?x with Some _ => _ | None => _ end] ] =>

     case_eq x; intros; simpl; auto; DO_IT

| [ |-context[compare_bd_dec ?a ?b ?c] ] =>

     case_eq (compare_bd_dec a b c);intros;simpl;auto;DO_IT

| _ =>

     omega || (elimtype False; omega) || (progress f_equal; auto; DO_IT; fail) ||  

     (progress intuition;DO_IT;fail) || intuition || auto

end.




Fixpoint ctrad_plist (pl:list pat) :list cpat:= 

     match pl with 

     | nil => nil | a::m => ctrad_pat a::ctrad_plist m end.




Lemma Cvalid_mklist: 

 forall n , Cvalid_list  (S n) (mklist n).




Lemma CTsubst_list_rec_mklist: 

 forall n tl cl m m1, n <= m->

   CTsubst_list_rec cl tl (mklist n) m m1=  (mklist n).




Lemma Tlift_mklist: 

 forall k n m, 

Tlift_list_rec (mklist k) n m = mklist k.




Lemma Tsubst_rec_mklist: 

 forall k t n m, 

CTsubst_list_rec nil t (mklist k) n m = mklist k.




Lemma mklist_length: 

 forall m, length (mklist m) =m .




Lemma Clist_mklist_app_inv: 

forall l1 l  n,   

 Cclosed_list l -> Cclosed_list l1 ->

CTsubst_list_rec (l++l1) nil (mklist (length l)) n O= 

 CTsubst_list_rec l nil (mklist (length l)) n O .




Lemma Cvalid_at_depth_mkargs2 : 

 forall tl   body m, 

       Cclosed_list tl -> length tl <= m ->

       Cvalid_at_depth  (S m) body -> 

       Cvalid_at_depth  (S m - length tl) (mkargs2  tl body) .




Fixpoint Clift_n (t:cpsterm) (n:nat){struct n}:cpsterm:=

 match n with | O => t | S m => Clift_n (Clift t) m end.




Lemma Cclosed_Clift_n: 

 forall n t  , Cclosed t -> Clift_n t n = t.




Lemma Csubst_mkarg2: 

 forall tl tbody n t1,  

  Cclosed_list tl -> 

  CTsubst_rec (t1::nil) nil (mkargs2 tl tbody) n O = 

  mkargs2 tl (CTsubst_rec  ((Clift_n t1 (length tl))::nil) nil tbody (length tl +n) O).




Lemma Cvalid_Appn_body: 

 forall n , Cvalid_at_depth   (S (S n)) (Appn_body n).




Lemma Cvalid_Appn : 

 forall tl tf ,

   Cclosed tf -> Cclosed_list tl ->

   Cclosed  (Appn tf tl (Appn_body (length tl))).




Lemma mkargs2_subst:

forall tl lv k m,

  Cclosed_list lv ->  

  (CTsubst_rec  nil lv

        (mkargs2 tl (Appn_body k)) 0 m) = 

   (mkargs2 (CTsubst_list_rec nil lv  tl 0 m) (Appn_body k)).




Lemma mklist_Clubst: 

forall vb, 

 Cclosed_list vb->

 CTsubst_list_rec (rev vb) nil (mklist (length  vb)) 0 0= vb.




Lemma CTsubst_Appn: 

 forall vb' t1 t2, 

 Cclosed t1 -> Cclosed t2 ->

 Cclosed_list vb' ->

 (CTsubst_rec (rev (t1::t2::vb')) nil (Appn_body (length vb')) 0 O) = 

 TApp t2 (t1::vb').




Lemma ctrad_list_length: 

 forall tl, length (ctrad_list tl) = length tl.




Lemma Cclosed_ctrad_ctrad_at: 

 forall t, Cclosed (ctrad t)/\Cclosed (ctrad_atom t).













Lemma Cclosed_ctrad: 

 forall t, Cclosed (ctrad t).




Lemma Cclosed_ctrad_atom: 

forall t, Cclosed (ctrad_atom t).




Lemma Cclosed_list_ctrad_list: 

 forall tl, Cclosed_list (ctrad_list tl).




Lemma Cclosed_list_ctrad_atom_list: 

forall tl, Cclosed_list (ctrad_atom_list tl).




Lemma Cvalid_pat2_ctrad: 

 forall p, Cvalid_pat (S (S O)) (ctrad_pat p).




Lemma Cvalid_patlist2_ctrad: 

 forall pl, Cvalid_patlist (S (S O)) (ctrad_plist pl).




Lemma Tlift_mkargs2_app: 

forall tl n m k, 

 length tl <= k -> 

(Tlift_rec (mkargs2 (ctrad_list tl) (Appn_body k)) n m ) = 

    (mkargs2 (Tlift_list_rec (ctrad_list tl) n m) (Appn_body k)).




Lemma Tlift_mkargs2_Constr: 

forall tl n m k op, 

 length tl <= k -> 

(Tlift_rec (mkargs2 (ctrad_list tl) (Constr_body op k)) n m ) = 

    (mkargs2 (Tlift_list_rec (ctrad_list tl) n m) (Constr_body op k)).




Lemma is_atom_Tlift: 

forall l n0 m, 

  is_atom l =is_atom (lift_rec l n0 m).




Lemma is_atom_list_Tlift: 

forall l n0 m, 

  is_atom_list l =is_atom_list (lift_list_rec l n0 m).




Lemma Tlift_ctrad_atom: 

 forall t  ,(forall n m , Tlift_rec (ctrad t) n m = ctrad (lift_rec t n m))/\

  (forall n m, Tlift_rec (ctrad_atom t) n m = ctrad_atom (lift_rec t n m))    .










Lemma Tlift_ctrad: 

 forall t   n m , Tlift_rec (ctrad t) n m = ctrad (lift_rec t n m).




Lemma Tlift_ctrad_at: 

 forall t   n m , Tlift_rec (ctrad_atom t) n m = ctrad_atom (lift_rec t n m).




Lemma Tlift_ctrad_list: 

 forall t   n m , Tlift_list_rec (ctrad_list t) n m = ctrad_list (lift_list_rec t n m).




Lemma Tlift_ctrad_atom_list: 

 forall t   n m , Tlift_list_rec (ctrad_atom_list t) n m = ctrad_atom_list (lift_list_rec t n m).




Lemma Tlift2_ctrad_list: 

 forall t  m , Tlift_list (ctrad_list t) m = ctrad_list (lift_list t m).




Lemma Tlift2_ctrad_atom_list: 

 forall t m , Tlift_list(ctrad_atom_list t) m = ctrad_atom_list (lift_list t m).




Lemma Constr_body_Ts: 

 forall n op m lv, CTsubst_rec nil lv (Constr_body op n) O m = (Constr_body op n).
















Lemma mkargs2_subst_constr:

forall tl lv  m op n,

  Cclosed_list lv ->  

  (CTsubst_rec  nil lv

        (mkargs2 tl (Constr_body op n )) O m) = 

   (mkargs2 (CTsubst_list_rec nil lv  tl O m) (Constr_body op n )).




Lemma Csubst_depth_pat: 

  forall k m ca, Cclosed ca ->Cvalid_pat (S m) k -> 

 Cvalid_pat m (CTsubst_pat_rec (ca::nil) nil k m O).




Lemma Csubst_depth_patlist: 

 forall k m ca, Cclosed ca ->Cvalid_patlist (S m) k -> 

 Cvalid_patlist m (CTsubst_patlist_rec (ca::nil) nil k m O).




Lemma Csubst_Cvalid_pat: 

 forall  t n k, Cvalid_pat k t-> CTsubst_pat_rec n nil t k O=t.




Lemma Csubst_Cvalid_patlist: 

forall tl n k, Cvalid_patlist k tl -> CTsubst_patlist_rec n nil tl k O=tl.




 Lemma Csubst_pat_nth_sm: 

 forall p n ca r cm cj tm tj, nth_error p n = Some (TPatc r ca) -> 

            nth_error (CTsubst_patlist_rec cj tj p cm tm) n =

            Some (CTsubst_pat_rec cj tj (TPatc r ca) cm tm).




Lemma ctrad_patlist_nth: 

 forall p n r c, nth_error p n = Some (Patc r c) -> 

                         nth_error (ctrad_plist p) n = Some (ctrad_pat (Patc r c)).




Lemma Csubst_patlist_spec: 

forall p t,

 Cclosed t-> 

 Cvalid_patlist 0 (CTsubst_patlist_rec (t::nil) nil (ctrad_plist p) 1 O).




Lemma Subst_Tsubst: 

 forall t,(forall l  m  , is_atom_list l = true ->  

 ctrad (subst_rec  l t m) = CTsubst_rec nil (ctrad_atom_list l) (ctrad t) 0 m) /\

  forall l  m ,is_atom_list l = true ->  is_atom t=true ->

 ctrad_atom (subst_rec  l t m) = CTsubst_rec nil (ctrad_atom_list l) (ctrad_atom t) 0 m .











































Lemma isatom_Clift_n: 

 forall n t, is_catom t= true ->is_catom (Clift_n t n) =true.