Library Lambda.TPOSR.CtxReduction


Require
 Import
 Lambda.Tactics.

Require
 Import
 Lambda.Utils.




Require
 Import
 Lambda.TPOSR.Terms.

Require
 Import
 Lambda.TPOSR.Reduction.

Require
 Import
 Lambda.TPOSR.Conv.

Require
 Import
 Lambda.TPOSR.LiftSubst.

Require
 Import
 Lambda.TPOSR.Env.

Require
 Import
 Lambda.TPOSR.Types.

Require
 Import
 Lambda.TPOSR.Thinning.

Require
 Import
 Lambda.TPOSR.LeftReflexivity.







Implicit
 Types
 i
 k
 m
 n
 p
 : nat.

Implicit
 Type
 s
 : sort.

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

Implicit
 Types
 e
 f
 g
 : lenv.




Inductive
 red_in_env : lenv -> lenv -> Prop
 :=

  | red_env_hd : ∀ e
 t
 u
 s
, e
 |-- t
 -> u
 : Srt_l s
 -> e
 |-- u
 -> u
 : Srt_l s
 ->

        red_in_env (t
 :: e
) (u
 :: e
)

  | red_env_tl :

      ∀ e
 f
 t
, red_in_env e
 f
 -> 

      tposr_wf (t
 :: e
) ->

      red_in_env (t
 :: e
) (t
 :: f
).




Hint
 Resolve
 red_env_hd red_env_tl: coc
.




Lemma
 red_item :

   ∀ n
 t
 e
,

   item_llift t
 e
 n
 ->

   ∀ f
, red_in_env e
 f
 ->

   item_llift t
 f
 n
 ∨

   ((∀ g
, trunc _
 (S n
) e
 g
 -> trunc _
 (S n
) f
 g
) ∧

   ∃ u
, item_llift u
 f
 n
 ∧ (∃ s
 : sort, tposr_wf f
 -> f
 |-- t
 -> u
 : s
)).




Lemma
 ind_red_env :

  (∀ e
 t
 u
 T
, e
 |-- t
 -> u
 : T
 -> 

  ∀ f
, red_in_env e
 f
 -> f
 |-- t
 -> u
 : T
) ∧

  (∀ e
, tposr_wf e
 -> 

  ∀ f
, red_in_env e
 f
 -> tposr_wf f
) ∧

  (∀ e
 t
 u
 s
, e
 |-- t
 ~= u
 : s
 -> 

  ∀ f
, red_in_env e
 f
 -> f
 |-- t
 ~= u
 : s
) ∧

  (∀ e
 t
 u
 s
, e
 |-- t
 >-> u
 : s
 -> 

  ∀ f
, red_in_env e
 f
 -> f
 |-- t
 >-> u
 : s
).




Lemma
 tposr_red_env : ∀ e
 t
 u
 T
, e
 |-- t
 -> u
 : T
 -> 

  ∀ f
, red_in_env e
 f
 -> f
 |-- t
 -> u
 : T
.




Lemma
 eq_red_env : ∀ e
 u
 v
 s
, e
 |-- u
 ~= v
 : s
 ->

  ∀ f
, red_in_env e
 f
 -> f
 |-- u
 ~= v
 : s
.




Lemma
 coerce_red_env : ∀ e
 T
 U
 s
, e
 |-- T
 >-> U
 : s
 -> 

  ∀ f
, red_in_env e
 f
 -> f
 |-- T
 >-> U
 : s
.




Hint
 Resolve
 tposr_red_env eq_red_env coerce_red_env : ecoc
.