Library f2cps_help

Helpfull properties of atoms and 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.




Fixpoint ctrad_atom_list (tl:list term) {struct tl}:list cpsterm:=

      match tl with | nil => nil 

    | a::m=>ctrad_atom a :: ctrad_atom_list m end  .

I. Properties of continuation detection


Lemma case_clamb: 

 forall t c, cps_case_of t = clamb c -> t = TLamb 0 c.




Lemma Clift_case_of: 

forall t n , cps_case_of t = other -> cps_case_of (Clift_rec t n) = other.

II. Atoms properties


Lemma is_atom_nth: 

 forall l , is_atom_list l = true -> 

 forall i x, nth_error l i = Some x -> is_atom x = true.




Lemma is_atom_subst: 

 forall t l0 m, 

 is_atom_list l0 = true-> 

 is_atom t = is_atom (subst_rec l0 t m).




Lemma is_atom_subst_list:

forall l l0 m,  

 is_atom_list l0 = true->

 is_atom_list l= is_atom_list (subst_list_rec l0 l m).




Lemma is_atom_eval: 

 forall t v, eval_term t v -> 

 is_atom t = true-> t =v.




Lemma is_atom_eval_list: 

 forall tl vl, eval_list tl vl-> is_atom_list tl=true  -> tl = vl.




Lemma isatom_Tlift_rec: 

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




Lemma isatom_Tlift_list_rec: 

 forall t n k , is_catom_list t = true -> is_catom_list (Tlift_list_rec t n k) = true.




Lemma isatom_Tlift : 

 forall t k , is_catom t =true-> is_catom (Tlift t k) = true.




Lemma isatom_Tlift_list: 

  forall t, is_catom_list t = true -> forall k , is_catom_list (Tlift_list t k) = true.




Lemma isatom_Clift_rec: 

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




Lemma isatom_Clift_list_rec: 

 forall t n, is_catom_list t =true-> is_catom_list (Clift_list_rec t n) = true.




Lemma isatom_Clift: 

 forall t, is_catom t =true-> is_catom (Clift t) = true.




Lemma isatom_Clift_list: 

 forall t, is_catom_list t =true-> is_catom_list (Clift_list t) =true.




Lemma isatom_nth : 

 forall t, is_catom_list t =true->

    forall i v, nth_error t i = Some v ->is_catom v=true.




Lemma isatom_CTlift: 

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




Lemma isatom_CTlift_list: 

 forall t n, is_catom_list t =true-> is_catom_list (CTlift_list t n) = true.




Lemma isatom_app: 

 forall l1 , is_catom_list l1 =true-> 

 forall l2, is_catom_list l2 =true-> is_catom_list (l1++l2) = true.




Lemma isatom_rev: 

 forall l1, is_catom_list l1 =true -> is_catom_list (rev l1) = true.




Lemma is_catom_CTsubst: 

forall va w2 wl nc nt,

 is_catom_list w2 = true -> 

 is_catom_list wl = true ->

 is_catom va = true -> 

 is_catom (CTsubst_rec w2 wl va nc nt) = true.




Lemma ctrad_catom: 

  forall t,  is_catom (ctrad_atom t) = true.




Lemma ctrad_catom_list: 

  forall t, is_catom_list (ctrad_atom_list t) = true.




Lemma ctrad_ctrad_atom: 

 forall t , is_atom t = true -> 

 ctrad t = TLamb 0 (unApp (CVar 0) (ctrad_atom t)).




Fixpoint is_cval (t:cpsterm){struct t}:bool:= 

 match t with 

 | TLamb _ _ =>true

 | TMu _ _ =>true

 | TConstr _ l => let fix is_cval_list (l:list cpsterm) {struct l}:bool:= 

                                match l with 

                                | nil=>true

                                |a::m=> 

                                  if (  is_cval a) then is_cval_list m else false end 

                                in is_cval_list l 

 | _ => false  

 end .




Fixpoint  is_cval_list (l:list cpsterm) {struct l}:bool:= 

match l with 

| nil=>true

|a::m=> 

if (  is_cval a) then is_cval_list m else false end .




Lemma isatom_ceval: 

 forall t2 vb, 

   is_catom t2=true -> ceval_term t2 vb -> 

  is_cval t2= true /\vb=t2.




Lemma isatom_ceval_list: 

 forall t2 vb, 

   is_catom_list t2=true -> ceval_list t2 vb -> 

  is_cval_list t2= true /\vb=t2.




Lemma ceval_is_cval_atom: 

 forall t v, ceval_term t v -> is_cval v = true/\ is_catom v=true.




Lemma is_cval_isatom: 

 forall v , is_cval v = true -> is_catom v=true.




Lemma is_cval_Clift: 

 forall t, is_cval t = true -> 

 is_cval (Clift t) = true.




Lemma is_cval_Tlift: 

  forall t k, is_cval t = true -> 

 is_cval (Tlift t k) = true.







Lemma iscval_Clift_list : 

 forall v , is_cval_list v = true -> is_cval_list (Clift_list v) = true.




Lemma iscval_Tlift_list : 

 forall v n, is_cval_list v = true -> is_cval_list (Tlift_list v n) = true.




Lemma iscval_CTlift: 

 forall t n , is_cval t = true -> is_cval (CTlift t n) = true.




Lemma is_cval_CTlift_list: 

 forall t n ,  is_cval_list t = true -> is_cval_list (CTlift_list t n) = true.




Lemma is_cval_app: 

 forall l1 l2, is_cval_list l1 = true -> is_cval_list l2 = true -> 

 is_cval_list (l1++l2) = true.




Lemma is_cval_rev: 

 forall l, is_cval_list l = true -> is_cval_list (rev l) = true.




Lemma isatom_eval_list: 

 forall t v, ceval_list t v -> is_catom_list v = true /\is_cval_list v = true.




Theorem eval_atom_ceval:

forall (t t0 : term), eval_term t t0 ->  

 ceval_term (ctrad_atom t0) (ctrad_atom t0).




Lemma eval_atom_ceval_list: 

 forall l1 vl, eval_list l1 vl-> 

 ceval_list (ctrad_atom_list vl) (ctrad_atom_list vl).




Lemma ctrad_atom_app: 

 forall l1 l2, ctrad_atom_list (l1++l2) = 

 ctrad_atom_list l1++ctrad_atom_list l2.




Lemma ctrad_atom_rev: 

 forall l, rev (ctrad_atom_list l) = ctrad_atom_list (rev l).




Lemma is_atom_app: 

 forall l1 l2, is_atom_list l1= true ->is_atom_list l2= true-> 

                    is_atom_list (l1++l2) = true.




Lemma is_atom_rev: 

 forall l, is_atom_list l = true-> is_atom_list (rev l) = true.




Lemma is_atom_val: 

 forall t v, eval_term t v->is_atom v = true.




Lemma is_atom_val_list: 

 forall t v, eval_list t v -> is_atom_list v = true.




Lemma isatom_eval: 

 forall t v, eval_term t v -> 

    eval_term v v.




Lemma eval_length: 

 forall l1 lv, eval_list l1 lv -> length lv = length l1.




Lemma match_val_nth: 

  forall l i v , nth_error l i = Some v -> 

  nth_error (ctrad_atom_list l) i = Some (ctrad_atom v).




Lemma match_val_nth_none:  

 forall l i , nth_error l i = None -> nth_error (ctrad_atom_list l) i = None.




Lemma ctrad_atom_length: 

 forall l, length (ctrad_atom_list l) = length l.




Lemma is_atom_lift_rec: 

 forall t, is_atom t = true -> forall n k, is_atom (lift_rec t n k) = true.




Lemma is_atom_lift_list_rec: 

 forall t, is_atom_list t = true -> 

   forall n k, is_atom_list (lift_list_rec t n k) = true.




Lemma is_atom_lift: 

 forall t k, is_atom t= true -> is_atom (lift t k) = true.




Lemma is_atom_lift_list: 

  forall t k, is_atom_list t= true -> is_atom_list (lift_list t k) = true.