Library Cpsopt_pre

The transitive and reflexive closure of the beta v equivalence of CPS terms

Author : Zaynah Dargaye

Created : 29th April 2009





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

Require Import f2cps_proof.

Require Import f2cps_help.

Require Import Cpsopt.

Require Import Cpsopt_pre1.




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 the closure of the beta v equivalence


Inductive  cbveq: cpsterm->cpsterm->Prop:= 

 | cbv_refl: forall t, cbveq t t 

 | cbv_simpl : forall t1 t2, cbvequiv t1 t2 -> cbveq t1 t2

 | cbv_trans : forall t1 t2 t3, 

        cbveq t1 t2-> cbveq t2 t3 -> cbveq t1 t3.




Inductive cbveq_list: list cpsterm->list cpsterm->Prop:= 

 | cbvl_refl : forall l, cbveq_list l l

 | cbvl_simpl: forall l1 l2, cbvequiv_list l1 l2 -> cbveq_list l1 l2

 | cbvl_trans: forall l1 l2 l3, cbveq_list l1 l2->cbveq_list l2 l3-> 

                                                   cbveq_list l1 l3.




Inductive cbveq_pat: cpat->cpat->Prop:= 

  |cbvp_refl: forall t, cbveq_pat t t 

 | cbvp_simpl : forall t1 t2, cbvequiv_pat t1 t2 -> cbveq_pat t1 t2

 | cbvp_trans : forall t1 t2 t3, 

        cbveq_pat t1 t2-> cbveq_pat t2 t3 -> cbveq_pat t1 t3.




Inductive cbveq_plist: list cpat->list cpat->Prop:= 

 | cbvpl_refl : forall l, cbveq_plist l l

 | cbvpl_simpl: forall l1 l2, cbvequiv_plist l1 l2 -> cbveq_plist l1 l2

 | cbvpl_trans: forall l1 l2 l3, cbveq_plist l1 l2->cbveq_plist l2 l3-> 

                                                   cbveq_plist l1 l3.




Lemma cbvequiv_list_refl : 

 forall l, cbvequiv_list l l .




Lemma cbv_cons_refl: 

 forall tl ml, cbveq_list tl ml -> forall t, cbveq_list (t::tl) (t::ml).




Lemma cbv_cons_simpl: 

 forall tl ml, cbveq_list tl ml ->

  forall t1 m1, cbvequiv t1 m1 -> 

  cbveq_list (t1::tl) (m1::ml).




Lemma cbv_cons_1: 

 forall t1 t2, cbveq t1 t2 -> 

 forall l, cbveq_list (t1::l) (t2::l).




Lemma cbvl_cons: 

 forall t1 t2, cbveq t1 t2-> 

 forall l1 l2, cbveq_list l1 l2 -> 

 cbveq_list (t1::l1) (t2::l2).




Lemma cbv_App_left: 

 forall t1 m1 , cbveq t1 m1 -> 

 forall t2, cbveq (TApp t1 t2) (TApp m1 t2).




Lemma cbv_App_right: 

 forall t2 m2, cbveq_list t2 m2 -> 

 forall m1, cbveq (TApp m1 t2) (TApp m1 m2).




Lemma cbv_App: 

 forall t1 t2 m1 m2, 

 cbveq t1 m1 -> cbveq_list t2 m2-> 

 cbveq (TApp t1 t2) (TApp m1 m2).




Lemma cbv_App_beta: 

 forall t1 t2,

 is_catom t1=true ->is_catom t2 =true ->  

 cbveq (unApp t1 t2) (App_beta t1 t2).




Lemma isatom_cbv: 

 forall t1 t2, cbveq t1 t2->is_catom t1 =true ->is_catom t2 =true.




Lemma TApp_App_beta_cbv: 

 forall t1 m1 t2 m2, 

  is_catom t1=true ->is_catom t2 =true ->  

  cbveq t1 m1 -> cbveq t2 m2 -> 

  cbveq (unApp t1 t2) (App_beta m1 m2).




Lemma cbv_CLamb: 

 forall a a' , cbveq a a' -> cbveq (TLamb 0 a) (TLamb 0 a').




Lemma cbv_TLamb: 

 forall a a', cbveq a a' -> forall ari , cbveq (TLamb (S ari) a) (TLamb (S ari ) a').




Lemma cbv_TMu : 

 forall a a', cbveq a a' -> forall ari , cbveq (TMu ari a) (TMu ari a').




Lemma cbv_Clift : 

 forall t1 t2 , cbveq t1 t2 ->  

  forall n , cbveq (Clift_rec t1 n) (Clift_rec t2 n).




Lemma cbv_Clift_n: 

 forall n t1 t2, cbveq t1 t2 -> 

  cbveq (Clift_n t1 n) (Clift_n t2 n).




 Lemma cbv_Tlift : 

 forall t1 t2 , cbveq t1 t2 ->  

  forall n m, cbveq (Tlift_rec t1 n m) (Tlift_rec t2 n m).




Lemma cbveq_eval: 

 forall t1 t2, cbveq t1 t2 -> 

 forall v1, ceval_term t1 v1 -> 

 exists v2 , ceval_term t2 v2 /\ cbveq v1 v2.




Lemma cbveq_spec: 

 forall k l k2,

 is_catom k =true -> 

 cbveq (CTsubst_rec (k::nil) nil l O O ) k2 -> 

 cbveq (unApp (TLamb 0 l) k) k2.




Lemma cbv_Appn_k:

forall m a b, 

 is_catom a =true ->  

  cbveq a b -> cbveq (CTsubst_rec (a::nil) nil (Appn_body m) (S m) O)

              (Appn_bodyk b m).




Lemma cbv_TLet: 

 forall t1 t2, cbveq t1 t2 -> 

 forall t, cbveq (TLet t t1) (TLet t t2).




Lemma  Clift_n_Clift: 

 forall m k, Clift_n (Clift k) m = Clift_n k (m+1).




Lemma cbv_Constr: 

 forall k1 k2, cbveq_list k1 k2 -> forall n , cbveq (TConstr n k1) (TConstr n k2).




Lemma cbvequiv_pat_refl : 

 forall p , cbvequiv_pat p p.




Lemma cbvequiv_plist_refl: 

 forall pl, cbvequiv_plist pl pl.




Lemma cbv_Match_1: 

 forall t1 m1, cbveq t1 m1-> 

 forall pl, cbveq (TMatch t1 pl) (TMatch m1 pl).




Lemma cbv_Match: 

 forall pl1 pl2, cbveq_plist pl1 pl2-> 

 forall t1 m1, cbveq t1 m1->cbveq (TMatch t1 pl1) (TMatch m1 pl2).




 Lemma cbv_TPat:

  forall t1 m1, cbveq t1 m1-> 

  forall m , cbveq_pat (TPatc m t1) (TPatc m m1).




Lemma cbv_pcons_1: 

 forall t1 t2, cbveq_pat t1 t2 -> 

 forall pl, cbveq_plist (t1::pl) (t2::pl).




Lemma cbv_pcons: 

 forall pl1 pl2, cbveq_plist pl1 pl2-> 

 forall t1 t2, cbveq_pat t1 t2 -> 

 cbveq_plist (t1::pl1) (t2::pl2).