Library Lambda.Env


Require
 Import
 Lambda.Terms.

Require
 Import
 Lambda.Reduction.

Require
 Import
 Lambda.LiftSubst.

Require
 Export
 Lambda.MyList.




Implicit
 Types
 i
 k
 m
 n
 p
 : nat.

Implicit
 Type
 s
 : sort.

Implicit
 Types
 A
 B
 M
 N
 T
 t
 u
 v
 : term.




Definition
 env := list term.




Implicit
 Types
 e
 f
 g
 : env.




Definition
 item_lift t
 e
 n
 :=

  ex2 (fun
 u
 ⇒ t
 = lift (S n
) u
) (fun
 u
 ⇒ item term u
 (e
:list term) n
).




Inductive
 ins_in_env A
 : nat → env → env → Prop
 :=

| ins_O : ∀ e
, ins_in_env A
 0 e
 (A
 :: e
)

| ins_S :

  ∀ 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 :

  ∀ A
 n
 e
 f
,

    ins_in_env A
 n
 e
 f
 →

    ∀ v
 : nat, n
 ≤ v
 → ∀ t
, item _
 t
 e
 v
 → item _
 t
 f
 (S v
).




  Lemma
 ins_item_lt :

   ∀ A
 n
 e
 f
,

   ins_in_env A
 n
 e
 f
 →

   ∀ v
 : nat,

   n
 > v
 → ∀ t
, item_lift t
 e
 v
 → item_lift (lift_rec 1 t
 n
) f
 v
.




Inductive
 sub_in_env t
 T
 : nat → env → env → Prop
 :=

| sub_O : ∀ e
, sub_in_env t
 T
 0 (T
 :: e
) e


| sub_S :

  ∀ 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 :

  ∀ t
 T
 n
 e
 f
,

    sub_in_env t
 T
 n
 e
 f
 →

    ∀ v
 : nat, n
 ≤ v
 → ∀ u
, item _
 u
 e
 (S v
) → item _
 u
 f
 v
.




  Lemma
 nth_sub_eq : ∀ t
 T
 n
 e
 f
, sub_in_env t
 T
 n
 e
 f
 → item _
 T
 e
 n
.




  Lemma
 nth_sub_inf :

   ∀ t
 T
 n
 e
 f
,

   sub_in_env t
 T
 n
 e
 f
 →

   ∀ v
 : nat,

   n
 > v
 → ∀ u
, item_lift u
 e
 v
 → item_lift (subst_rec t
 u
 n
) f
 v
.