Library Env
Require Export Omega.
Require Export MyList.
Require Export Term.
Definition env := list term.
Definition item_lift t e n :=
exists2 u, t = lift (S n) u & item u (e:env) n.
Lemma item_lift_fun : forall x y e n,
item_lift x e n ->
item_lift y e n ->
x=y.
Inductive ins_in_env (A : term) : nat -> env -> env -> Prop :=
| ins_O : forall e, ins_in_env A 0 e (A :: e)
| ins_S :
forall n e f t,
ins_in_env A n e f ->
ins_in_env A (S n) (t :: e) (lift_rec 1 t n :: f).
Hint Resolve ins_O ins_S: coc.
Lemma ins_item_ge :
forall A n e f,
ins_in_env A n e f -> forall v t, n <= v -> item t e v -> item t f (S v).
Lemma ins_item_lift_ge :
forall A n e f,
ins_in_env A n e f -> forall v t, n <= v ->
item_lift t e v -> item_lift (lift_rec 1 t n) f (S v).
Lemma ins_item_lt :
forall A n e f,
ins_in_env A n e f ->
forall v t, n > v -> item t e v -> item (lift_rec 1 t (n-S v)) f v.
Lemma ins_item_lift_lt :
forall A n e f,
ins_in_env A n e f ->
forall v t, n > v -> item_lift t e v -> item_lift (lift_rec 1 t n) f v.
Inductive sub_in_env (t T : term) : nat -> env -> env -> Prop :=
| sub_O : forall e : env, sub_in_env t T 0 (T :: e) e
| sub_S :
forall e f n u,
sub_in_env t T n e f ->
sub_in_env t T (S n) (u :: e) (subst_rec t u n :: f).
Hint Resolve sub_O sub_S: coc.
Lemma nth_sub_sup :
forall t T n e f,
sub_in_env t T n e f -> forall v u, n <= v -> item u e (S v) -> item u f v.
Lemma nth_sub_eq : forall t T n e f, sub_in_env t T n e f -> item T e n.
Lemma sub_item_lift_sup :
forall t T n e f,
sub_in_env t T n e f -> forall v u, n < v ->
item_lift u e v -> item_lift (subst_rec t u n) f (pred v).
Lemma sub_item_lift_eq : forall t T n e f x,
sub_in_env t T n e f -> item_lift x e n -> subst_rec t x n = lift n T.
Lemma nth_sub_inf :
forall t T n e f,
sub_in_env t T n e f ->
forall v u, n > v -> item_lift u e v -> item_lift (subst_rec t u n) f v.
Section Reduction.
Variable R : term -> term -> Prop.
Variable R_lift :
forall x y n k, R x y -> R (lift_rec n x k) (lift_rec n y k).
Inductive red1_in_env : env -> env -> Prop :=
| red1_env_hd : forall e t u, R t u -> red1_in_env (t :: e) (u :: e)
| red1_env_tl :
forall e f t, red1_in_env e f -> red1_in_env (t :: e) (t :: f).
Hint Constructors red1_in_env: coc.
Lemma red_item :
forall n t e f,
item_lift t e n ->
red1_in_env e f ->
item_lift t f n \/
(forall g, trunc (S n) e g -> trunc (S n) f g) /\
(exists2 u, R t u & item_lift u f n).
End Reduction.
Hint Constructors ins_in_env: coc.
Hint Constructors sub_in_env: coc.
Hint Constructors red1_in_env: coc.
Require Export MyList.
Require Export Term.
Definition env := list term.
Definition item_lift t e n :=
exists2 u, t = lift (S n) u & item u (e:env) n.
Lemma item_lift_fun : forall x y e n,
item_lift x e n ->
item_lift y e n ->
x=y.
Inductive ins_in_env (A : term) : nat -> env -> env -> Prop :=
| ins_O : forall e, ins_in_env A 0 e (A :: e)
| ins_S :
forall n e f t,
ins_in_env A n e f ->
ins_in_env A (S n) (t :: e) (lift_rec 1 t n :: f).
Hint Resolve ins_O ins_S: coc.
Lemma ins_item_ge :
forall A n e f,
ins_in_env A n e f -> forall v t, n <= v -> item t e v -> item t f (S v).
Lemma ins_item_lift_ge :
forall A n e f,
ins_in_env A n e f -> forall v t, n <= v ->
item_lift t e v -> item_lift (lift_rec 1 t n) f (S v).
Lemma ins_item_lt :
forall A n e f,
ins_in_env A n e f ->
forall v t, n > v -> item t e v -> item (lift_rec 1 t (n-S v)) f v.
Lemma ins_item_lift_lt :
forall A n e f,
ins_in_env A n e f ->
forall v t, n > v -> item_lift t e v -> item_lift (lift_rec 1 t n) f v.
Inductive sub_in_env (t T : term) : nat -> env -> env -> Prop :=
| sub_O : forall e : env, sub_in_env t T 0 (T :: e) e
| sub_S :
forall e f n u,
sub_in_env t T n e f ->
sub_in_env t T (S n) (u :: e) (subst_rec t u n :: f).
Hint Resolve sub_O sub_S: coc.
Lemma nth_sub_sup :
forall t T n e f,
sub_in_env t T n e f -> forall v u, n <= v -> item u e (S v) -> item u f v.
Lemma nth_sub_eq : forall t T n e f, sub_in_env t T n e f -> item T e n.
Lemma sub_item_lift_sup :
forall t T n e f,
sub_in_env t T n e f -> forall v u, n < v ->
item_lift u e v -> item_lift (subst_rec t u n) f (pred v).
Lemma sub_item_lift_eq : forall t T n e f x,
sub_in_env t T n e f -> item_lift x e n -> subst_rec t x n = lift n T.
Lemma nth_sub_inf :
forall t T n e f,
sub_in_env t T n e f ->
forall v u, n > v -> item_lift u e v -> item_lift (subst_rec t u n) f v.
Section Reduction.
Variable R : term -> term -> Prop.
Variable R_lift :
forall x y n k, R x y -> R (lift_rec n x k) (lift_rec n y k).
Inductive red1_in_env : env -> env -> Prop :=
| red1_env_hd : forall e t u, R t u -> red1_in_env (t :: e) (u :: e)
| red1_env_tl :
forall e f t, red1_in_env e f -> red1_in_env (t :: e) (t :: f).
Hint Constructors red1_in_env: coc.
Lemma red_item :
forall n t e f,
item_lift t e n ->
red1_in_env e f ->
item_lift t f n \/
(forall g, trunc (S n) e g -> trunc (S n) f g) /\
(exists2 u, R t u & item_lift u f n).
End Reduction.
Hint Constructors ins_in_env: coc.
Hint Constructors sub_in_env: coc.
Hint Constructors red1_in_env: coc.