Library EnvECC

Require Export Omega.
Require Export MyList.
Require Export TermECC.

  Definition env := list term.

  Definition item_lift t e n :=
    exists2 u, t = lift (S n) u & item u (e:env) n.


  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/a>)`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.