Library Fml_subst
Require Import List.
Require Import Coqlib.
Require Import Coqlib2.
Require Import Fml.
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) || auto
end.
I. Lift and simultaneous substitution
Fixpoint lift_rec (t:term) (n:nat) (ari:nat){struct t}: term:=
match t with
| Var i => if lt_ge_dec i n then Var i else Var (i+ari)
| Mu m b => Mu m (lift_rec b (n+(S (S m))) ari)
|Lamb m b=> Lamb m (lift_rec b (n+(S m)) ari)
| App t1 t2 =>
let fix lift_list_rec (tl:list term) (n:nat) (ari:nat) {struct tl}:list term:=
match tl with
| nil => nil
| a::m => (lift_rec a n ari)::(lift_list_rec m n ari)
end in
App (lift_rec t1 n ari) (lift_list_rec t2 n ari)
|tLet t1 t2=> tLet (lift_rec t1 n ari) (lift_rec t2 (S n) ari)
|Con k tl =>
let fix lift_list_rec (tl:list term) (n:nat) (ari:nat) {struct tl}:list term:=
match tl with
| nil => nil
| a::m => (lift_rec a n ari)::(lift_list_rec m n ari)
end in
Con k (lift_list_rec tl n ari)
|Match t pl =>
let fix lift_patlist_rec (tl:list pat) (n:nat) (ari:nat) {struct tl}:list pat:=
match tl with
| nil => nil
| a::m => (lift_pat_rec a n ari)::(lift_patlist_rec m n ari)
end in
Match (lift_rec t n ari) (lift_patlist_rec pl n ari)
end
with lift_pat_rec (p:pat) (n ari:nat) {struct p}: pat:=
match p with
| Patc k t => Patc k (lift_rec t (n+ k) ari)
end.
Definition lift (t:term) (ari:nat) := lift_rec t O ari.
Fixpoint lift_list_rec (tl:list term) (n:nat) (ari:nat) {struct tl}:list term:=
match tl with
| nil => nil
| a::m => (lift_rec a n ari)::(lift_list_rec m n ari)
end.
Fixpoint lift_list (tl:list term) (ari:nat) {struct tl}:list term:=
match tl with
| nil => nil
| a::m => (lift a ari)::(lift_list m ari)
end.
Fixpoint lift_patlist_rec (tl:list pat) (n:nat) (ari:nat) {struct tl}:list pat:=
match tl with
| nil => nil
| a::m => (lift_pat_rec a n ari)::(lift_patlist_rec m n ari)
end.
Fixpoint subst_rec (tl :list term) (t: term) (d : nat) {struct t}:term:=
match t with
| Var m =>
let u:= (length tl+d)%nat in
match compare_bd_dec m d u with
| INF _ => Var m
| IN _ _ =>
match nth_error tl (m-d) with |Some w => w | None =>Var m end
| SUP _=> Var (m+d-u)
end
| Mu ari b => Mu ari (subst_rec (lift_list tl (S(S ari))) b (d+(S (S ari))) )
|Lamb ari b => Lamb ari (subst_rec (lift_list tl (S ari)) b (d+(S ari)))
| App t1 t2 =>
let fix subst_list_rec
(tl :list term) (l: list term) (d : nat) {struct l}: list term:=
match l with
| nil => nil
| a::m => (subst_rec tl a d )::(subst_list_rec tl m d )
end in
App (subst_rec tl t1 d ) (subst_list_rec tl t2 d )
|tLet t1 t2 => tLet (subst_rec tl t1 d) (subst_rec (lift_list tl 1) t2 (S d))
|Con n l =>
let fix subst_list_rec
(tl :list term) (l: list term) (d : nat) {struct l}: list term:=
match l with
| nil => nil
| a::m => (subst_rec tl a d )::(subst_list_rec tl m d )
end in Con n (subst_list_rec tl l d)
| Match t pl =>
let fix subst_patlist_rec
(tl :list term) (l: list pat) (d : nat) {struct l}: list pat:=
match l with
| nil => nil
| a::m => (subst_pat_rec tl a d )::(subst_patlist_rec tl m d )
end in Match (subst_rec tl t d) (subst_patlist_rec tl pl d)
end
with subst_pat_rec (tl:list term) (p:pat) (d:nat) {struct p}:pat:=
match p with
|Patc n t => Patc n (subst_rec (lift_list tl n) t (d+ n))
end.
Fixpoint subst_list_rec
(tl :list term) (l: list term) (d : nat) {struct l}: list term:=
match l with
| nil => nil
| a::m => (subst_rec tl a d )::(subst_list_rec tl m d )
end.
Fixpoint subst_patlist_rec
(tl :list term) (l: list pat) (d : nat) {struct l}: list pat:=
match l with
| nil => nil
| a::m => (subst_pat_rec tl a d )::(subst_patlist_rec tl m d )
end.
Definition Subst (w:list term) (t:term) :=
match w with | nil => t
| _ => subst_rec w t O end.
Fixpoint Subst_list (tl : list term) (l:list term) {struct l}:list term :=
match l with
| nil => nil
|a::m => Subst tl a ::Subst_list tl m
end.
II. big-step semantics CBV based on substitution
Inductive eval_term:term->term->Prop:=
| emu: forall ari t, eval_term (Mu ari t) (Mu ari t)
| elamb: forall ari t, eval_term (Lamb ari t) (Lamb ari t)
| eapp : forall t1 t2 vb t v ari,
eval_term t1 (Lamb ari t)->
length t2 = (S ari) -> eval_list t2 vb->
eval_term (subst_rec (rev vb) t O) v ->
eval_term (App t1 t2) v
| eappr: forall t1 t2 vb t v ari,
eval_term t1 (Mu ari t)->
length t2 = (S ari) -> eval_list t2 vb->
eval_term (subst_rec ((rev vb)++(Mu ari t)::nil) t O) v ->
eval_term (App t1 t2) v
|elet: forall t1 t2 v1 v2,
eval_term t1 v1 ->
eval_term (subst_rec (v1::nil) t2 O) v2 ->
eval_term (tLet t1 t2) v2
|econst : forall n l vl,
eval_list l vl ->
eval_term (Con n l) (Con n vl)
| ematch: forall t n lv p ca v,
eval_term t (Con n lv) ->
nth_error p n = Some (Patc (length lv) ca) ->
eval_term (subst_rec (rev lv) ca O) v ->
eval_term (Match t p) v
with eval_list:list term->list term->Prop:=
| enil: eval_list nil nil
| econs:forall a va m vm,
eval_term a va ->
eval_list m vm->
eval_list (a::m) (va::vm).
Scheme eval_term_ind6 := Minimality for eval_term Sort Prop
with eval_list_ind6 := Minimality for eval_list Sort Prop.
III. Lift properties
Lemma lift_nth:
forall l i n, nth_error l i = None ->
nth_error (lift_list l n) i = None.
Lemma lift_nth_sm:
forall l i n v, nth_error l i = Some v ->
nth_error (lift_list l n) i = Some (lift v n) .
Lemma lift_list_length:
forall l n, length (lift_list l n ) = length l.
Lemma lift_rec_lift_list:
forall l n , lift_list l n = lift_list_rec l O n.
Lemma lift_list_app:
forall l1 l2 n , lift_list (l1++l2) n =
(lift_list l1 n) ++ (lift_list l2 n).
Ltac LIFT_TAC :=
match goal with
| [ |- context[lt_ge_dec ?a ?b] ] =>
case_eq (lt_ge_dec a b); intros; simpl; auto; LIFT_TAC
| [ |- context[compare_dec ?a ?b] ] =>
case_eq(compare_dec a b); intros; simpl; auto; LIFT_TAC
| [ |- context[match ?x with Some _ => _ | None => _ end] ] =>
case_eq x; intros; simpl; auto; LIFT_TAC
| [ |-context[compare_bd_dec ?a ?b ?c] ] =>
case_eq (compare_bd_dec a b c);intros;simpl;auto;LIFT_TAC
| _ =>
omega || (elimtype False; omega) || (progress f_equal; auto; LIFT_TAC; fail) || auto
end.
Lemma lift_comm_prop:
forall t n1 n2 k1,
(lift_rec (lift_rec t n1 k1) (n1 + k1) n2) =
(lift_rec t n1 (k1+n2)).
Lemma lift_comm_eq:
forall t s1 k1 k2 ,
lift_rec (lift_rec t s1 k1) s1 k2 =
lift_rec t s1 (k1+k2).
Lemma lift_list_comm_eq:
forall t s1 k1 k2 ,
lift_list_rec (lift_list_rec t s1 k1) s1 k2 =
lift_list_rec t s1 (k1+k2).
Lemma lift_comm_lt:
forall t s1 s2 k1 k2,
(s1 <=s2)%nat ->
lift_rec (lift_rec t s2 k2) s1 k1 =
lift_rec (lift_rec t s1 k1) (s2+k1) k2.
Lemma lift_list_rec_comm_lt:
forall t s1 s2 k1 k2,
(s1 <=s2)%nat ->
lift_list_rec (lift_list_rec t s2 k2) s1 k1 =
lift_list_rec (lift_list_rec t s1 k1) (s2+k1) k2.
Lemma lift_list_prop:
forall t k1 k2,
(lift_list (lift_list t k1) k2) =
(lift_list t (k1+k2)).
Lemma lift_comm_prop1:
forall t n1 n2 k1,
(lift_rec (lift_rec t n1 k1) (n1 + k1) n2) =
(lift_rec t n1 (k1+n2)).
Lemma lift_list_comm_prop1:
forall t n1 n2 k1,
(lift_list_rec (lift_list_rec t n1 k1) (n1 + k1) n2) =
(lift_list_rec t n1 (k1+n2)).
Lemma lift_rec_length:
forall l n m, length(lift_list_rec l n m) = length l.
Lemma lift_rec_nth_sm:
forall l n m i t, nth_error l i = Some t ->
nth_error (lift_list_rec l m n) i = Some (lift_rec t m n).
Lemma lift_rec_nth_none:
forall l n m i , nth_error l i = None ->
nth_error (lift_list_rec l m n) i = None.
IV. Properties of theimultaneous substitution
Lemma subst_lift_prop:
forall t m l1 ,
subst_rec l1 (lift_rec t m (length l1)) m = t.
Lemma Subst_comp:
forall t l1 l2 m , subst_rec l1 (subst_rec (lift_list_rec l2 m
(length l1)) t (length l1+m)) m =
subst_rec (l1++l2) t m .
Lemma subst_rec_length:
forall l l1 n, length (subst_list_rec l1 l n) = length l.
Lemma subst_app_spec :
forall t l1 l2 k ,
subst_rec l1 (subst_rec (lift_list_rec l2 k (length l1)) t k) k = (subst_rec (l2++l1) t k).
Lemma subst_nth_sm :
forall u l o i x, nth_error u i = Some x ->
nth_error (subst_list_rec l u o) i = Some (subst_rec l x o).
Lemma lift_subst_prop:
forall b a k n0 n, lift_rec (subst_rec a b (n+k)) k n0 =
subst_rec (lift_list_rec a k n0) (lift_rec b k n0) (n + n0+k) .
Lemma lift_subst_list_prop:
forall b a k n0 n, lift_list_rec (subst_list_rec a b (n+k)) k n0 =
subst_list_rec (lift_list_rec a k n0) (lift_list_rec b k n0) (n + n0+k) .
Lemma the_subst_para :
forall t w u i j ,
subst_rec w (subst_rec u t i) (i+j) =
subst_rec (subst_list_rec w u (i+j)) (subst_rec (lift_list_rec w i (length u)) t (i+j+length u)) i.