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