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