Library f2cps_help
Helpfull properties of atoms and the naive CPS conversion
Author : Zaynah DargayeCreated: 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.