Library Lambda.TPOSR.Env


Require
 Export
 Lambda.MyList.

Require
 Import
 Lambda.TPOSR.Terms.

Require
 Import
 Lambda.TPOSR.Reduction.

Require
 Import
 Lambda.TPOSR.LiftSubst.




Implicit
 Types
 i
 k
 m
 n
 p
 : nat.

Implicit
 Type
 s
 : sort.

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




Definition
 lenv := list lterm.




Implicit
 Types
 e
 f
 g
 : lenv.




Definition
 item_llift t
 e
 n
 :=

ex2
 (fun
 u
 ⇒ t
 = llift (S n
) u
) (fun
 u
 ⇒ item lterm u
 (e
:list lterm) n
).




Inductive
 ins_in_lenv A
 : nat → lenv → lenv → Prop
 :=

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

    | ins_S :

        ∀ n
 e
 f
 t
,

        ins_in_lenv A
 n
 e
 f
 →

        ins_in_lenv A
 (S n
) (t
 :: e
) (llift_rec 1 t
 n
 :: f
).




  Hint
 Resolve
 ins_O ins_S: coc
.




  Lemma
 ins_item_ge :

   ∀ A
 n
 e
 f
,

   ins_in_lenv 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_lenv A
 n
 e
 f
 →

   ∀ v
 : nat,

   n
 > v
 → ∀ t
, item_llift t
 e
 v
 → item_llift (llift_rec 1 t
 n
) f
 v
.




  Inductive
 sub_in_lenv t
 T
 : nat → lenv → lenv → Prop
 :=

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


    | sub_S :

        ∀ e
 f
 n
 u
,

        sub_in_lenv t
 T
 n
 e
 f
 →

        sub_in_lenv t
 T
 (S n
) (u
 :: e
) (lsubst_rec t
 u
 n
 :: f
).




  Hint
 Resolve
 sub_O sub_S: coc
.




  Lemma
 nth_sub_sup :

   ∀ t
 T
 n
 e
 f
,

   sub_in_lenv 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_lenv t
 T
 n
 e
 f
 → item _
 T
 e
 n
.




  Lemma
 nth_sub_inf :

   ∀ t
 T
 n
 e
 f
,

   sub_in_lenv t
 T
 n
 e
 f
 →

   ∀ v
 : nat,

   n
 > v
 → ∀ u
, item_llift u
 e
 v
 → item_llift (lsubst_rec t
 u
 n
) f
 v
.