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

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.