Library Lambda.TPOSR.PreCtxCoercion


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
 pre_coerce_in_env : lenv -> lenv -> Prop
 :=

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

        pre_coerce_in_env (t
 :: e
) (u
 :: e
)

  | pre_coerce_env_tl :

      ∀ e
 f
 t
, pre_coerce_in_env e
 f
 -> 

      ∀ s
, f
 |-- t
 -> t
 : Srt_l s
 ->

      pre_coerce_in_env (t
 :: e
) (t
 :: f
).




Hint
 Resolve
 pre_coerce_env_hd pre_coerce_env_tl: coc
.




Lemma
 coerce_item :

   ∀ n
 t
 e
,

   item_llift t
 e
 n
 ->

   ∀ f
, pre_coerce_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, f
 |-- t
 >-> u
 : s
 ∧ f
 |-- u
 -> u
 : s
)).




Lemma
 ind_pre_coerce_env :

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

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

  (∀ e
, tposr_wf e
 -> 

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

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

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

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

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




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

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




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

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




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

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




Hint
 Resolve
 tposr_pre_coerce_env eq_pre_coerce_env coerce_pre_coerce_env : ecoc
.




Inductive
 pre_coerce_in_env_full : lenv -> lenv -> Prop
 :=

  | pre_coerce_env_trans : ∀ e
 f
 g
, pre_coerce_in_env_full e
 f
 -> pre_coerce_in_env_full f
 g
 -> pre_coerce_in_env_full e
 g


  | pre_coerce_env_in_env : ∀ e
 f
, pre_coerce_in_env e
 f
 -> pre_coerce_in_env_full e
 f


  | pre_coerce_env_nil : pre_coerce_in_env_full nil nil.




Hint
 Resolve
 pre_coerce_env_in_env pre_coerce_env_nil : coc
.




Lemma
 pre_coerce_env_sym : ∀ e
 f
, pre_coerce_in_env e
 f
 -> pre_coerce_in_env f
 e
.




Lemma
 pre_coerce_env_full_sym : ∀ e
 f
, pre_coerce_in_env_full e
 f
 -> pre_coerce_in_env_full f
 e
.




Hint
 Resolve
 pre_coerce_env_sym pre_coerce_env_full_sym : coc
.




Lemma
 pre_coerce_env_full :

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

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




Lemma
 pre_coerce_env_full_cons : ∀ G
 D
, pre_coerce_in_env_full G
 D
 -> ∀ T
, tposr_wf (T
 :: G
) ->

  pre_coerce_in_env_full (T
 :: G
) (T
 :: D
).




Corollary
 tposrp_pre_coerce_env_full : 

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

  ∀ f
, pre_coerce_in_env_full e
 f
 -> f
 |-- t
 -+> u
 : T
).




Corollary
 eq_pre_coerce_env_full : 

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

  ∀ f
, pre_coerce_in_env_full e
 f
 -> f
 |-- t
 ~= u
 : s
).




Hint
 Resolve
 pre_coerce_env_full eq_pre_coerce_env_full : ecoc
.




Corollary
 coerce_pre_coerce_env_full : 

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

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