Library CPS_pre

Properties of lifts and substitutions of CPS terms

Author : Zaynah Dargaye Created : 29th April 2009




Require Import List.

Require Import Coqlib.

Require Import Coqlib2.

Require Import CPS.

Require Import CPS_subst.




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

     intuition || auto

end.




Lemma CTsubst_Cnil: 

 forall t tw cn tn cn2, 

 CTsubst_rec nil tw t cn tn = CTsubst_rec nil tw t cn2 tn.




Lemma CTsubst_list_Cnil:

forall t tw cn tn cn2, 

 CTsubst_list_rec nil tw t cn tn = CTsubst_list_rec nil tw t cn2 tn.




Lemma CTsubst_pat_Cnil: 

forall t tw cn tn cn2, 

 CTsubst_pat_rec nil tw t cn tn = CTsubst_pat_rec nil tw t cn2 tn.




Lemma CTsubst_patlist_Cnil: 

 forall t tw cn tn cn2, 

 CTsubst_patlist_rec nil tw t cn tn = CTsubst_patlist_rec nil tw t cn2 tn.




Lemma CTsubst_Tnil: 

 forall t cw cn tn tn2, 

 CTsubst_rec cw nil t cn tn = CTsubst_rec cw nil t cn tn2.




Lemma CTsubst_list_Tnil:

forall t cw cn tn tn2, 

 CTsubst_list_rec cw nil t cn tn = CTsubst_list_rec cw nil t cn tn2.




Lemma CTsubst_pat_Tnil: 

forall t cw cn tn tn2, 

 CTsubst_pat_rec cw nil  t cn tn = CTsubst_pat_rec cw nil t cn tn2.




Lemma CTsubst_patlist_Tnil: 

 forall t cw cn tn tn2, 

 CTsubst_patlist_rec cw nil t cn tn = CTsubst_patlist_rec cw nil t cn tn2.




Lemma CTlift_list_length: 

 forall t n, length (CTlift_list t n) = length t.




Lemma Clift_length: 

 forall l  , length (Clift_list l) = length l.




Lemma Tlift_length: 

 forall l  m, length (Tlift_list l m) = length l.




Fixpoint Cvalid_at_depth (k:nat) (t:cpsterm) {struct t}:Prop:=

 match t with 

 | CVar i =>  i< k

 | TLamb ari t1 => Cvalid_at_depth (S k) t1

 | TMu ari t1 => Cvalid_at_depth (S k) t1

 | TApp t1 t2=> 

       let fix Cvalid_list (k:nat) (tl:list cpsterm) {struct tl} :Prop:= 

       match tl with 

      | nil => True

      | a::m => (Cvalid_at_depth k a)/\(Cvalid_list k m)

       end in

       Cvalid_at_depth k t1/\Cvalid_list k t2

 |TLet t1 t2 =>Cvalid_at_depth k t1/\Cvalid_at_depth k t2

 |TConstr r l => 

     let fix Cvalid_list (k:nat) (tl:list cpsterm) {struct tl} :Prop:= 

       match tl with 

      | nil => True

      | a::m => (Cvalid_at_depth k a)/\(Cvalid_list k m)

       end in Cvalid_list k l

  |TMatch t1 pl => 

       let fix Cvalid_patlist (k:nat) (tl:list cpat) {struct tl} :Prop:= 

       match tl with 

      | nil => True

      | a::m => (Cvalid_pat k a)/\(Cvalid_patlist k m)

       end in Cvalid_at_depth k t1 /\ Cvalid_patlist k pl

  | _ => True

 end 

with Cvalid_pat (k:nat) (p:cpat) {struct p}: Prop:= 

 match p with | TPatc r t => Cvalid_at_depth k t end

 .




Fixpoint Cvalid_list (k:nat) (tl:list cpsterm) {struct tl} :Prop:= 

 match tl with 

 | nil => True

 | a::m => (Cvalid_at_depth k a)/\(Cvalid_list k m)

 end.




Fixpoint Cvalid_patlist (k:nat) (tl:list cpat) {struct tl} :Prop:= 

       match tl with 

      | nil => True

      | a::m => (Cvalid_pat k a)/\(Cvalid_patlist k m)

end.




Definition Cvalidl_at_depth (k:nat)(tl:list cpsterm):Prop:= 

 forall t, In t tl -> Cvalid_at_depth k t.




Lemma Cvl: 

 forall tl k, Cvalid_list k tl -> Cvalidl_at_depth k tl.




Definition Cclosed (t:cpsterm):= Cvalid_at_depth O t.




Definition Cclosed_list (tl: list cpsterm) := Cvalid_list O tl.




Lemma cvalid_up : 

 forall t n m , n < m -> 

  Cvalid_at_depth n t-> Cvalid_at_depth m t.




Lemma lift_Cvalid_at_depth : 

 forall t  k,  Cvalid_at_depth k t ->Clift_rec t  k= t.




Lemma Cclosed_lift: 

 forall t, Cclosed t ->  Clift  t = t.




Lemma Cclosed_list_Clift: 

 forall tl, Cclosed_list tl -> Clift_list tl = tl.




Lemma cvalid_up_list: 

 forall tl n m, n < m-> Cvalid_list  n tl -> Cvalid_list m tl.




Lemma Closed_Tlift: 

forall t m n k, Cvalid_at_depth k t -> Cvalid_at_depth k (Tlift_rec t m n).




Lemma Cclosed_Tlift_list: 

 forall l m, Cclosed_list l -> Cclosed_list (Tlift_list l m).




Lemma Cclosed_list_CT: 

 forall l m, Cclosed_list l -> Cclosed_list (CTlift_list l m).




 Lemma Cvalid_nth: 

 forall l i w k, 

 Cvalid_list k l ->

 nth_error l i = Some w -> Cvalid_at_depth k w.




Lemma CTsubst_Cvalid_at_depth: 

 forall t cn  k1 k2, Cvalid_at_depth k1 t-> 

         CTsubst_rec cn nil t k1 k2 = t.




Lemma CTsubst_Cvalid_depth: 

 forall t cn  k1 k2 l, Cvalid_at_depth k1 t-> 

         CTsubst_rec cn l t k1 k2 = 

         CTsubst_rec nil l t O k2.




Lemma CTsubst_distr_App: 

 forall t1 t2 cw tw cn tn , CTsubst_rec cw tw (TApp t1 t2) cn tn= 

                   TApp (CTsubst_rec cw tw t1 cn tn) (CTsubst_list_rec cw tw t2 cn tn).




Lemma Csubst_distr_unApp: 

 forall t1 t2 cw tw cn tn , CTsubst_rec cw tw (unApp t1 t2) cn tn = 

                     unApp (CTsubst_rec cw tw t1 cn tn) (CTsubst_rec cw tw t2 cn tn).




Lemma Csubst_O : 

 forall w, CTsubst_rec (w::nil) nil (CVar O) O O = w.




Lemma Cvalid_app: 

 forall t1 t2 k,  Cvalid_list k t1 -> Cvalid_list k t2->Cvalid_list  k (t1++t2).




Definition Cclosed_pat (p:cpat) := Cvalid_pat O p.

Definition Cclosed_patlist (pl:list cpat):= Cvalid_patlist O pl.

Lemma Tlift_O: 

 forall t n , Tlift_rec t n O =t.




Lemma Tlift_list_O: 

 forall t n , Tlift_list_rec t n O =t.




Fixpoint Clift_n (t:cpsterm) (n:nat) {struct n}:cpsterm:= 

 match n with 

 | O => t 

 | S n =>  (Clift_n (Clift t) n)

 end.




Lemma Cclosed_CT: 

 forall t, Cclosed t -> CTlift t O = t.




Lemma Cclosed_CT_list: 

 forall lv, Cclosed_list lv->  (CTlift_list lv 0) =lv.




Lemma Cclosed_Clift_n: 

 forall n t, Cclosed t -> Clift_n t n = t.




Lemma CTlift_app: 

forall l1 l2 ari,

 CTlift_list l1 ari ++ CTlift_list l2 ari = CTlift_list (l1 ++ l2) ari.




Lemma Tlift_app: 

forall l1 l2 ari,

 Tlift_list l1 ari ++ Tlift_list l2 ari = Tlift_list (l1 ++ l2) ari.




Lemma inf_nth: 

 forall A l n , n < length l -> exists v:A, nth_error l n = Some v.




Lemma nth_cclosed: 

 forall l, Cclosed_list l -> 

 forall n v, nth_error l n = Some v -> Cclosed v.




Lemma Sn_n_diff: 

 forall n, n <> S n.




Lemma Cclosed_app: 

 forall l1 l2 , Cclosed_list l1 -> Cclosed_list l2 -> Cclosed_list (l1++l2).




Lemma Cclosed_rev: 

 forall l, Cclosed_list l -> Cclosed_list (rev l).




Lemma Csubst_depth: 

forall k m ca, 

 Cclosed ca ->

 Cvalid_at_depth (S m) k ->

 Cvalid_at_depth m (CTsubst_rec (ca::nil) nil k m O).






















Lemma Clift_nth_sm : 

 forall l i v, nth_error l i = Some v -> 

                    nth_error (Clift_list l) i = Some (Clift v).




Lemma Clift_nth_none : 

 forall l i , nth_error l i = None -> 

                    nth_error (Clift_list l) i = None.




Lemma Clift_rec_length: 

 forall l n , length (Clift_list_rec l n ) = length l.




Lemma Clift_rec_nth_sm: 

  forall l i v n , nth_error l i = Some v -> 

  nth_error (Clift_list_rec l n) i = Some (Clift_rec v n).




Lemma Clift_rec_nth_none : 

 forall l i n, nth_error l i = None -> 

                    nth_error (Clift_list_rec l n) i = None.




Lemma CTlift_length: 

 forall l n, length (CTlift_list l n) = length l.




Lemma CTlift_nth_sm : 

  forall l n i v, nth_error l i = Some v -> 

                         nth_error (CTlift_list l n) i = Some (CTlift v n).




Lemma CTlift_nth_none : 

 forall l n i , nth_error l i = None -> 

                      nth_error (CTlift_list l n) i = None.




Lemma nth_inf: 

 forall A l (v:A) i, nth_error l i = Some v -> i < length l.




Lemma Tlift_rec_length: 

 forall l n k , length (Tlift_list_rec l k n ) = length l.




Lemma Tlift_rec_nth_sm: 

  forall l i v n k , nth_error l i = Some v -> 

  nth_error (Tlift_list_rec l n k) i = Some (Tlift_rec v n k).




Lemma Tlift_rec_nth_none : 

 forall l i n k, nth_error l i = None -> 

                    nth_error (Tlift_list_rec l n k) i = None.




Lemma CTlift_list_rec : 

 forall t ari, CTlift_list t ari = Clift_list_rec (Tlift_list_rec t  O ari  ) O.




Lemma Clift_rec_list : 

 forall t, Clift_list t = Clift_list_rec t  O.




Lemma Tlift_rec_list : 

 forall t ari , Tlift_list t ari = Tlift_list_rec t  O ari.




Fixpoint Cllift_rec (t:cpsterm) (ari:nat) (q:nat){struct t}: cpsterm:= 

 match t with 

 | CVar i => if lt_ge_dec i ari then CVar i else CVar (i+q)

 | TVar i => TVar i 

 | TLamb k b => TLamb k (Cllift_rec b (S ari) q) 

 | TMu k b => TMu k (Cllift_rec b (S ari) q) 

 | TApp t1 t2 => 

     let fix Cllift_list_rec (tl:list cpsterm) (n q:nat) {struct tl}: list cpsterm:=

     match tl with 

     | nil => nil 

     | a::m => (Cllift_rec a n q):: (Cllift_list_rec m n q) 

     end in

     TApp (Cllift_rec t1 ari q) (Cllift_list_rec t2 ari q)

| TLet t1 t2 => TLet (Cllift_rec t1 ari q) (Cllift_rec t2 ari q) 

| TConstr k tl => 

      let fix Cllift_list_rec (tl:list cpsterm)  (ari q:nat) {struct tl}:list cpsterm:=

     match tl with 

     | nil => nil 

     | a::m => (Cllift_rec a ari q)::(Cllift_list_rec m ari q)

     end in 

     TConstr k (Cllift_list_rec tl ari q)

 |TMatch t pl => 

      let fix Cllift_patlist_rec (tl:list cpat)  (ari q:nat) {struct tl}:list cpat:=

     match tl with 

     | nil => nil 

     | a::m => (Cllift_pat_rec a  ari q)::(Cllift_patlist_rec m  ari q)

     end in  

     TMatch (Cllift_rec t  ari q) (Cllift_patlist_rec pl  ari q) 

 end

with Cllift_pat_rec (p:cpat) ( ari q:nat ) {struct p}: cpat:= 

 match p with 

 | TPatc k t => TPatc k (Cllift_rec t  ari q)

 end.







Definition Cllift (t:cpsterm) (q:nat):= Cllift_rec t O q.




Fixpoint Cllift_list_rec (tl:list cpsterm) (n q:nat) {struct tl}: list cpsterm:=

match tl with 

 | nil => nil 

 | a::m => (Cllift_rec a n q):: (Cllift_list_rec m n q) 

end.




Fixpoint Cllift_patlist_rec (tl:list cpat)  (ari q:nat) {struct tl}:list cpat:=

     match tl with 

     | nil => nil 

     | a::m => (Cllift_pat_rec a  ari q)::(Cllift_patlist_rec m  ari q)

     end.




Lemma Cllift_length: 

 forall l n m , length (Cllift_list_rec l n m) = length l.




Lemma CTsubst_length: 

 forall l cl tl ic it, length (CTsubst_list_rec cl tl l ic it) = length l.




Lemma CTsubst_nth: 

forall tu n a cw tw ic it,

 nth_error tu n = Some a -> 

nth_error (CTsubst_list_rec cw tw tu ic it) n = 

 Some  (CTsubst_rec cw tw a ic it).




Lemma Cllift_nth: 

 forall tu n a ic it,

 nth_error tu n = Some a -> 

nth_error (Cllift_list_rec tu ic it) n = 

 Some  (Cllift_rec  a ic it).




Lemma Tlift_nth: 

 forall tu n a ic it,

 nth_error tu n = Some a -> 

nth_error (Tlift_list_rec tu ic it) n = 

 Some  (Tlift_rec  a ic it).




Lemma CTsubst_prop1: 

forall a ic it l1 l2,

 CTsubst_rec l1 l2 (Cllift_rec (Tlift_rec a it (length l2) ) ic (length l1)) ic it = 

 a.










Lemma CTsubst_list_prop1: 

forall a ic it l1 l2,

 CTsubst_list_rec l1 l2 (Cllift_list_rec (Tlift_list_rec a it (length l2) ) ic (length l1)) ic it = 

 a.




Lemma Tlift_Clift_rec_comm: 

 forall t n m k, 

 Tlift_rec (Clift_rec t n) m k = 

 Clift_rec (Tlift_rec t m k) n.




Lemma Tlift_Clift_comm: 

 forall t n, 

 Tlift (Clift t) n = Clift (Tlift t n) .




Ltac omegaContradiction := elimtype False; omega.




Lemma Clift_Clift_prop_1 :

  forall t (n n' : nat) ,

  Clift_rec  (Clift_rec t (n + n')) n = Clift_rec  (Clift_rec t n) (1 + (n + n')) .







Lemma CTlift_comm_1: 

forall t2 n0 n,

 (Clift_rec (CTlift t2 n0) (S n))  = (CTlift (Clift_rec t2 n) n0).




Lemma Tlift_comm_eq: 

 forall t s1  k1 k2 , 

 Tlift_rec (Tlift_rec t s1 k1) s1 k2 = 

 Tlift_rec t s1 (k1+k2).




Lemma Tlift_comm_lt: 

 forall t s1 s2 k1 k2, 

 s1 <=s2 -> 

 Tlift_rec (Tlift_rec t s2 k2) s1 k1 = 

 Tlift_rec (Tlift_rec t s1 k1) (s2+k1) k2.




Lemma Tlift_comm_prop: 

 forall t n1 n2 k1, 

 (Tlift_rec (Tlift_rec t n1 k1) (n1 + k1) n2) = 

 (Tlift_rec t n1 (k1+n2)).
















Lemma Tlift_Clift_list_rec_comm: 

 forall a  n m k , 

 Clift_list_rec (Tlift_list_rec a k n) m = Tlift_list_rec (Clift_list_rec a m) k n.




Lemma Clift_Clift_list_prop_1 :

  forall t (n n' : nat) ,

  Clift_list_rec  (Clift_list_rec t (n + n')) n = 

  Clift_list_rec  (Clift_list_rec t n) (1 + (n + n')) .




Lemma Clift_CTsubst_prop1: 

forall cu cw tw  ic it n,

  CTsubst_rec (Clift_list_rec cw n) (Clift_list_rec tw n)

  (Clift_rec cu n) (1+ ic+n) it =

Clift_rec (CTsubst_rec cw tw cu (ic+n) it) n.
















Lemma Tlift_list_comm_eq:

forall (t : list cpsterm) (s1 k1 k2 : nat),

       Tlift_list_rec (Tlift_list_rec t s1 k1) s1 k2 = Tlift_list_rec t s1 (k1 + k2).




Lemma Tlift_list_comm_lt: 

forall (t : list cpsterm) (s1 s2 k1 k2 : nat),

       s1 <= s2 ->

       Tlift_list_rec (Tlift_list_rec t s2 k2) s1 k1 =

       Tlift_list_rec (Tlift_list_rec t s1 k1) (s2 + k1) k2.




Lemma Tlift_CTsubst_prop1: 

forall cu cw tw  ic it  n0 k,

  CTsubst_rec (Tlift_list_rec cw k n0) (Tlift_list_rec tw k n0)

  (Tlift_rec cu k n0) ic (it+n0+k) = 

 Tlift_rec (CTsubst_rec cw tw cu ic (it+k)) k n0.






















Lemma Tlift_list_CTsubst_prop1: 

forall cu cw tw  ic it  n0 k,

  CTsubst_list_rec (Tlift_list_rec cw k n0) (Tlift_list_rec tw k n0)

  (Tlift_list_rec cu k n0) ic (it+n0+k) = 

 Tlift_list_rec (CTsubst_list_rec cw tw cu ic (it+k)) k n0.




Lemma CTlift_CTsubst_prop1: 

forall cu cw tw ari ic it,

  CTsubst_rec (CTlift_list cw ari) (CTlift_list tw ari)

  (CTlift cu ari) (S ic) (it + ari ) =

CTlift (CTsubst_rec cw tw cu ic it) ari.




Lemma CTlift_CTsubst_list_prop1: 

forall cu cw tw ari ic it,

  CTsubst_list_rec (CTlift_list cw ari) (CTlift_list tw ari)

  (CTlift_list cu ari) (S ic) (it + ari ) =

CTlift_list (CTsubst_list_rec cw tw cu ic it) ari.




Lemma Tlift_Cllift_comm: 

 forall t tn cn kt kc, 

 Tlift_rec (Cllift_rec t cn kc) tn kt = 

 Cllift_rec (Tlift_rec t tn kt) cn kc.




Lemma Tlift_Cllift_list_comm: 

 forall t tn cn kt kc, 

 Tlift_list_rec (Cllift_list_rec t cn kc) tn kt = 

 Cllift_list_rec (Tlift_list_rec t tn kt) cn kc.




Lemma Cllift_Clift: 

 forall t n' n m, 

Cllift_rec (Clift_rec t n' ) (1+n+n') m = 

  Clift_rec (Cllift_rec t (n+n') m) n'.




Lemma Cllift_Clift_list: 

 forall t n' n m, 

Cllift_list_rec (Clift_list_rec t n' ) (1+n+n') m = 

  Clift_list_rec (Cllift_list_rec t (n+n') m) n'.




Lemma CTsubst_Csubst: 

forall t ic it jc jt cu tu cw tw,

 CTsubst_rec cw tw (CTsubst_rec cu tu t ic it) (ic+jc) (it+jt) = 

 CTsubst_rec (CTsubst_list_rec cw tw cu   (ic+jc) (it+jt)) 

          (CTsubst_list_rec cw tw tu   (ic+jc) (it+jt))

   (CTsubst_rec (Cllift_list_rec (Tlift_list_rec cw it (length tu)) ic (length cu)) 

      (Cllift_list_rec (Tlift_list_rec tw it (length tu)) ic (length cu))

   t (ic+jc+length cu) (it+jt+length tu)) ic it.














































Lemma CTsubst_comp: 

 forall t cw tw cu tu nc nt, 

 CTsubst_rec cw tw 

      (CTsubst_rec (Cllift_list_rec (Tlift_list_rec cu nt (length tw)) nc (length cw)) 

                                (Cllift_list_rec (Tlift_list_rec tu nt (length tw)) nc (length cw))

          t (nc+(length cw)) (nt+(length tw)) ) nc nt = 

  CTsubst_rec (cw++cu) (tw++tu) t nc nt.

























Lemma CTsubst_comp_list: 

 forall t cw tw cu tu nc nt, 

 CTsubst_list_rec cw tw 

      (CTsubst_list_rec (Cllift_list_rec (Tlift_list_rec cu nt (length tw)) nc (length cw)) 

                                (Cllift_list_rec (Tlift_list_rec tu nt (length tw)) nc (length cw))

          t (nc+(length cw)) (nt+(length tw)) ) nc nt = 

  CTsubst_list_rec (cw++cu) (tw++tu) t nc nt.




Lemma CTsubst_comp_pat: 

forall t cw tw cu tu nc nt, 

 CTsubst_pat_rec cw tw 

      (CTsubst_pat_rec (Cllift_list_rec (Tlift_list_rec cu nt (length tw)) nc (length cw)) 

                                (Cllift_list_rec (Tlift_list_rec tu nt (length tw)) nc (length cw))

          t (nc+(length cw)) (nt+(length tw)) ) nc nt = 

  CTsubst_pat_rec (cw++cu) (tw++tu) t nc nt .




Lemma CTsubst_comp_patlist: 

 forall t cw tw cu tu nc nt, 

 CTsubst_patlist_rec cw tw 

      (CTsubst_patlist_rec (Cllift_list_rec (Tlift_list_rec cu nt (length tw)) nc (length cw)) 

                                (Cllift_list_rec (Tlift_list_rec tu nt (length tw)) nc (length cw))

          t (nc+(length cw)) (nt+(length tw)) ) nc nt = 

  CTsubst_patlist_rec (cw++cu) (tw++tu) t nc nt.




Lemma CTsubst_Cvalid_list: 

 forall tl cn k1 k2,

         Cvalid_list k1 tl ->CTsubst_list_rec cn nil tl k1 k2 =tl.




Lemma Cvalid_Cllift: 

 forall t n m , Cvalid_at_depth n t->Cllift_rec t n m = t.




Lemma Cclosed_Cllift: 

  forall t n m , Cclosed t->Cllift_rec t n m = t.




Lemma Cvalid_Cllift_list: 

 forall t n m , Cvalid_list n t->Cllift_list_rec t n m = t.




Lemma Cvalid_Cllift_pat: 

 forall t n m , Cvalid_pat n t->Cllift_pat_rec t n m = t.




Lemma Cvalid_Cllift_patlist: 

 forall t n m , Cvalid_patlist n t->Cllift_patlist_rec t n m = t.




Lemma Csubst_Tlift_comm: 

forall a va m n k, 

 Tlift_rec (CTsubst_rec (va::nil) nil a m O) n k = 

 CTsubst_rec (Tlift_rec va n k::nil) nil (Tlift_rec a n k) m O.
















Lemma Cllift_1_Clift: 

 forall t n, Cllift_rec t n 1 = Clift_rec t n.




Lemma Cllift_1_Clift_list: 

 forall t n, Cllift_list_rec t n 1 = Clift_list_rec t n.

Lemma Clift_Csubst_prop2: 

 forall t a n n', 

 Clift_rec (CTsubst_rec (a::nil) nil t n O) (n+n') = 

 CTsubst_rec (Clift_rec a (n+n')::nil) nil (Clift_rec t (1+n+n')) n O.