Library Cpsopt_pre1
Require Import List.
Require Import Coqlib.
Require Import Coqlib2.
Require Import Fml.
Require Import CPS.
Require Import CPS_subst.
Require Import CPS_pre.
Require Import f2cps.
Require Import f2cps_help.
Require Import Cpsopt.
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.
I. Beta v equivalence
Inductive cbvequiv: cpsterm->cpsterm ->Prop:=
| btv : forall n , cbvequiv (TVar n) (TVar n)
| bcv : forall n, cbvequiv (CVar n) (CVar n)
| bcl : forall t a n, cbvequiv t a -> cbvequiv (TLamb n t) (TLamb n a)
| bmu: forall t a n , cbvequiv t a->cbvequiv (TMu n t) (TMu n a)
|bapp_beta: forall t v va a,
cbvequiv v va -> is_catom va =true->
cbvequiv t a ->
cbvequiv (unApp (TLamb 0 t) v) (CTsubst_rec (va::nil) nil a O O)
|bapp: forall t1 t2 t3 t4,
cbvequiv t1 t3 -> cbvequiv_list t2 t4->
cbvequiv (TApp t1 t2) (TApp t3 t4)
|btlet: forall t1 t2 t3 t4,
cbvequiv t1 t3->cbvequiv t2 t4->
cbvequiv (TLet t1 t2) (TLet t3 t4)
|bconst: forall m l1 l2,
cbvequiv_list l1 l2->
cbvequiv (TConstr m l1) (TConstr m l2)
|bmatch: forall t1 t2 pl1 pl2,
cbvequiv t1 t2->
cbvequiv_plist pl1 pl2->
cbvequiv (TMatch t1 pl1) (TMatch t2 pl2)
with
cbvequiv_list: list cpsterm->list cpsterm->Prop:=
| bnil : cbvequiv_list nil nil
| bcons: forall t1 m1 tl ml, cbvequiv t1 m1 -> cbvequiv_list tl ml ->
cbvequiv_list (t1::tl) (m1::ml)
with cbvequiv_pat:cpat->cpat->Prop:=
|bpat: forall n t1 t2 ,
cbvequiv t1 t2->
cbvequiv_pat (TPatc n t1) (TPatc n t2)
with cbvequiv_plist:list cpat->list cpat->Prop:=
|bpnil: cbvequiv_plist nil nil
|bpcons: forall hd1 hd2 tl1 tl2,
cbvequiv_pat hd1 hd2->
cbvequiv_plist tl1 tl2->
cbvequiv_plist (hd1::tl1) (hd2::tl2).
Scheme cbvequiv_ind6 := Minimality for cbvequiv Sort Prop
with cbvequiv_list_ind6 := Minimality for cbvequiv_list Sort Prop
with cbvequiv_pat_ind6:= Minimality for cbvequiv_pat Sort Prop
with cbvequiv_plist_ind6 := Minimality for cbvequiv_plist Sort Prop.
II beta v equivalence properties
Lemma cbvequiv_refl:
forall t , cbvequiv t t.
Lemma is_atom_cbvequiv:
forall t1 t2, cbvequiv t1 t2 -> is_catom t1 =true->
is_catom t2 =true.
Lemma isatom_cbvequiv_list:
forall t1 t2, cbvequiv_list t1 t2->is_catom_list t1=true-> is_catom_list t2=true.
Lemma cbv_atom_other:
forall t1 c1 ,
is_catom t1 =true-> cbvequiv t1 c1 -> cps_case_of t1 = other ->
cps_case_of c1 = other.
Lemma cbvequiv_length:
forall l l' , cbvequiv_list l l' -> length l' = length l.
Lemma cbvequiv_nth:
forall l l' , cbvequiv_list l l' ->
forall i v, nth_error l i = Some v ->
exists v', nth_error l' i = Some v' /\ cbvequiv v v'.
Lemma cbvequiv_nth_none:
forall l l', cbvequiv_list l l' ->
forall i, nth_error l i = None ->nth_error l' i = None.
Lemma cbvequiv_app:
forall l1 m1 , cbvequiv_list l1 m1 ->
forall l2 m2, cbvequiv_list l2 m2 ->
cbvequiv_list (l1++l2) (m1++m2).
Lemma cbvequiv_rev:
forall l l', cbvequiv_list l l' -> cbvequiv_list (rev l) (rev l').
Lemma cbvequiv_Clift_rec:
forall k1 k2 n,
cbvequiv k1 k2 ->
cbvequiv (Clift_rec k1 n) (Clift_rec k2 n).
Lemma cbvequiv_Clift:
forall k1 k2 ,
cbvequiv k1 k2 ->
cbvequiv (Clift k1 ) (Clift k2 ).
Lemma cbvequiv_Tlift_rec:
forall t1 t2 n k, cbvequiv t1 t2 -> cbvequiv (Tlift_rec t1 n k) (Tlift_rec t2 n k).
Lemma cbvequiv_Tlift:
forall t1 t2 k, cbvequiv t1 t2 -> cbvequiv (Tlift t1 k) (Tlift t2 k).
Lemma cbvequiv_CTlift:
forall t t' n, cbvequiv t t' -> cbvequiv (CTlift t n) (CTlift t' n).
Lemma cbvequiv_Clift_list:
forall tl tl', cbvequiv_list tl tl' ->
cbvequiv_list (Clift_list tl) (Clift_list tl').
Lemma cbvequiv_Tlift_list:
forall tl tl', cbvequiv_list tl tl' ->
forall n , cbvequiv_list (Tlift_list tl n) (Tlift_list tl' n).
Lemma cbvequiv_CTlift_list:
forall tl tl', cbvequiv_list tl tl' ->
forall n , cbvequiv_list (CTlift_list tl n) (CTlift_list tl' n).
Lemma cbvequiv_plist_nth:
forall p p1,
cbvequiv_plist p p1->
forall n m ca, nth_error p n = Some (TPatc m ca)->
exists ca', nth_error p1 n = Some (TPatc m ca') /\ cbvequiv ca ca'.
Lemma inter1:
forall va w cv ,
is_catom va =true ->
ceval_term va w-> cbvequiv cv w->
cbvequiv cv va.
III. beta v equivalence preserves by substitution
Lemma CTsubst_cbvequiv:
forall t a ca cb ta tb cn tn,
cbvequiv t a->
is_catom_list ca = true->is_catom_list ta = true->
is_cval_list ca = true->is_cval_list ta = true->
cbvequiv_list ca cb ->
cbvequiv_list ta tb->
cbvequiv (CTsubst_rec ca ta t cn tn) (CTsubst_rec cb tb a cn tn).
III Preservation of beta v equivalence by evaluation
Definition cbvequiv_prop (t:cpsterm) (v:cpsterm):Prop:=
forall t2, cbvequiv t t2->
exists w, ceval_term t2 w /\ cbvequiv v w.
Definition cbvequiv_list_prop (t: list cpsterm) (v:list cpsterm):Prop:=
forall t2, cbvequiv_list t t2->
exists w, ceval_list t2 w /\ cbvequiv_list v w.
Lemma cbv_lamb_prop:
forall (ari : nat) (t : cpsterm),
cbvequiv_prop (TLamb ari t) (TLamb ari t).
Lemma cbv_mu_prop:
forall (ari : nat) (t : cpsterm),
cbvequiv_prop (TMu ari t) (TMu ari t).
Lemma cbv_app1_prop:
forall (t1 c : cpsterm) (t2 : list cpsterm) (cv : cpsterm)
(vb : list cpsterm) (t v : cpsterm) (ari : nat),
ceval_term t1 (TLamb ari t) ->
cbvequiv_prop t1 (TLamb ari t) ->
length t2 = ari ->
ceval_term c cv ->
cbvequiv_prop c cv ->
ceval_list t2 vb ->
cbvequiv_list_prop t2 vb ->
ceval_term (CTsubst_rec (cv :: nil) (rev vb) t 0 0) v ->
cbvequiv_prop (CTsubst_rec (cv :: nil) (rev vb) t 0 0) v ->
cbvequiv_prop (TApp t1 (c :: t2)) v.
Lemma cbv_app2_prop:
forall (t1 c cv t v : cpsterm) (t2 vb : list cpsterm) (ari : nat),
ceval_term t1 (TMu ari t) ->
cbvequiv_prop t1 (TMu ari t) ->
length t2 = ari ->
ceval_term c cv ->
cbvequiv_prop c cv ->
ceval_list t2 vb ->
cbvequiv_list_prop t2 vb ->
ceval_term
(CTsubst_rec (cv :: nil) (rev vb ++ TMu ari t :: nil) t 0 0) v ->
cbvequiv_prop
(CTsubst_rec (cv :: nil) (rev vb ++ TMu ari t :: nil) t 0 0) v ->
cbvequiv_prop (TApp t1 (c :: t2)) v.
Lemma cbv_tlet_prop:
forall t1 t2 v1 v2 : cpsterm,
ceval_term t1 v1 ->
cbvequiv_prop t1 v1 ->
ceval_term (CTsubst_rec nil (v1 :: nil) t2 0 0) v2 ->
cbvequiv_prop (CTsubst_rec nil (v1 :: nil) t2 0 0) v2 ->
cbvequiv_prop (TLet t1 t2) v2.
Lemma cbv_constr_prop:
forall (n : nat) (l vl : list cpsterm),
ceval_list l vl ->
cbvequiv_list_prop l vl -> cbvequiv_prop (TConstr n l) (TConstr n vl).
Lemma cbv_match_prop:
forall (t : cpsterm) (n : nat) (lv : list cpsterm) (p : list cpat)
(ca v : cpsterm),
ceval_term t (TConstr n lv) ->
cbvequiv_prop t (TConstr n lv) ->
nth_error p n = Some (TPatc (length lv) ca) ->
ceval_term (CTsubst_rec nil (rev lv) ca 0 0) v ->
cbvequiv_prop (CTsubst_rec nil (rev lv) ca 0 0) v ->
cbvequiv_prop (TMatch t p) v.
Lemma cbvequiv_nil_prop:
cbvequiv_list_prop nil nil .
Lemma cbvequiv_cons_prop:
forall (a va : cpsterm) (m vm : list cpsterm),
ceval_term a va ->
cbvequiv_prop a va ->
ceval_list m vm ->
cbvequiv_list_prop m vm -> cbvequiv_list_prop (a :: m) (va :: vm).
Theorem cbvequiv_eval_prop:
forall c c0 : cpsterm, ceval_term c c0 -> cbvequiv_prop c c0.
Theorem cbvequiv_eval:
forall t v, ceval_term t v ->
forall t2, cbvequiv t t2->
exists w, ceval_term t2 w /\ cbvequiv v w.
Theorem cbvequiv_list_eval:
forall t v, ceval_list t v ->
forall t2, cbvequiv_list t t2->
exists w, ceval_list t2 w /\ cbvequiv_list v w.
IV beta-v-equivalence preserves by smart App
Lemma TApp_App_beta_cbvequiv:
forall t1 c1 t2 c2,
is_catom t1 =true->
cbvequiv t2 c2 -> cbvequiv t1 c1 ->
cbvequiv (unApp t1 t2) (App_beta c1 c2).