Library Lambda.TPOSR.PreSubstitutionTPOSR


Require
 Import
 Lambda.Tactics.




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.LeftReflexivity.

Require
 Import
 Lambda.TPOSR.Thinning.

Require
 Import
 Lambda.TPOSR.CtxReduction.

Require
 Import
 Lambda.TPOSR.CtxExpansion.

Require
 Import
 Lambda.TPOSR.PreCtxCoercion.

Require
 Import
 Lambda.TPOSR.Substitution.




Require
 Import
 Coq.Arith.Lt.







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.




Lemma
 sub_red_env : ∀ g
 d
 d'
 T
, g
 |-- d
 -> d'
 : T
 -> g
 |-- d'
 -> d'
 : T
 ->

  ∀ n
 e
 f
, sub_in_lenv d
 T
 n
 e
 f
 -> trunc lterm n
 f
 g
 ->

  ∃ f'
, (sub_in_lenv d'
 T
 n
 e
 f'
 ∧ trunc lterm n
 f'
 g
).




Lemma
 wf_coerce : ∀ e
, tposr_wf e
 -> pre_coerce_in_env_full e
 e
.




Lemma
 pre_coerce_env_full_cons_coerce : ∀ G
 D
, pre_coerce_in_env_full G
 D
 -> 

  ∀ T
 U
 s
, G
 |-- T
 >-> U
 : s
 -> G
 |-- T
 -> T
 : s
 -> G
 |-- U
 -> U
 : s
 ->

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




Lemma
 ind_substitution_tposr : 

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

   ∀ g
 d
 d'
 T
, g
 |-- d
 -> d'
 : T
 -> g
 |-- d'
 -> d'
 : T
 ->

   ∀ f
 n
, sub_in_lenv d
 T
 n
 e
 f
 -> trunc _
 n
 f
 g
 -> 

   f
 |-- (lsubst_rec d
 t
 n
) -> (lsubst_rec d'
 u
 n
) : (lsubst_rec d
 U
 n
) ∧

   ∃ f'
, sub_in_lenv d'
 T
 n
 e
 f'
 ∧ trunc _
 n
 f'
 g
 ∧

   tposr_wf f'
 ∧ pre_coerce_in_env_full f
 f'
) ∧

   (∀ e
, tposr_wf e
 ->

   ∀ g
 d
 d'
 T
, g
 |-- d
 -> d'
 : T
 -> g
 |-- d'
 -> d'
 : T
 ->

   ∀ n
 f
, sub_in_lenv d
 T
 n
 e
 f
 -> trunc _
 n
 f
 g
 -> 

   tposr_wf f
 ∧

   ∃ f'
, sub_in_lenv d'
 T
 n
 e
 f'
 ∧ trunc _
 n
 f'
 g
 ∧

   tposr_wf f'
 ∧ pre_coerce_in_env_full f
 f'


   ) ∧

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

   ∀ g
 d
 d'
 T
, g
 |-- d
 -> d'
 : T
 -> g
 |-- d'
 -> d'
 : T
 ->

   ∀ f
 n
, sub_in_lenv d
 T
 n
 e
 f
 -> trunc _
 n
 f
 g
 -> 

   f
 |-- (lsubst_rec d
 t
 n
) ~= (lsubst_rec d'
 u
 n
) : s
 ∧

   f
 |-- (lsubst_rec d'
 t
 n
) ~= (lsubst_rec d
 u
 n
) : s
) ∧

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

   ∀ g
 d
 d'
 T
, g
 |-- d
 -> d'
 : T
 -> g
 |-- d'
 -> d'
 : T
 ->

   ∀ f
 n
, sub_in_lenv d
 T
 n
 e
 f
 -> trunc _
 n
 f
 g
 -> 

   f
 |-- (lsubst_rec d
 t
 n
) >-> (lsubst_rec d'
 u
 n
) : s
 ∧

   f
 |-- (lsubst_rec d'
 t
 n
) >-> (lsubst_rec d
 u
 n
) : s
).




Corollary
 substitution_tposr_tposr_n : ∀ g
 d
 d'
 t
, g
 |-- d
 -> d'
 : t
 -> g
 |-- d'
 -> d'
 : t
 ->

   ∀ e
 u
 v
 U
, e
 |-- u
 -> v
 : U
 ->

   ∀ f
 n
, sub_in_lenv d
 t
 n
 e
 f
 -> trunc _
 n
 f
 g
 -> 

   f
 |-- (lsubst_rec d
 u
 n
) -> (lsubst_rec d'
 v
 n
) : (lsubst_rec d
 U
 n
).




Corollary
 substitution_tposr_tposr_wf_n : ∀ g
 d
 d'
 t
, g
 |-- d
 -> d'
 : t
 -> g
 |-- d'
 -> d'
 : t
 ->

   ∀ e
, tposr_wf e
 -> ∀ f
 n
, sub_in_lenv d
 t
 n
 e
 f
 -> 

   trunc _
 n
 f
 g
 -> tposr_wf f
.




Corollary
 substitution_tposr_eq_n : ∀ g
 d
 d'
 t
, g
 |-- d
 -> d'
 : t
 -> g
 |-- d'
 -> d'
 : t
 ->

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

   ∀ f
 n
, sub_in_lenv d
 t
 n
 e
 f
 -> trunc _
 n
 f
 g
 -> 

   f
 |-- (lsubst_rec d
 u
 n
) ~= (lsubst_rec d'
 v
 n
) : s
.




Corollary
 substitution_tposr_coerce_n : ∀ g
 d
 d'
 t
, g
 |-- d
 -> d'
 : t
 -> g
 |-- d'
 -> d'
 : t
 ->

   ∀ e
 u
 v
 s
, e
 |-- u
 >-> v
 : s
 ->

   ∀ f
 n
, sub_in_lenv d
 t
 n
 e
 f
 -> trunc _
 n
 f
 g
 -> 

   f
 |-- (lsubst_rec d
 u
 n
) >-> (lsubst_rec d'
 v
 n
) : s
.




Corollary
 substitution_tposr_tposr : ∀ e
 t
 u
 v
 U
, (t
 :: e
) |-- u
 -> v
 : U
 ->

  ∀ d
 d'
, e
 |-- d
 -> d'
 : t
 -> e
 |-- d'
 -> d'
 : t
 -> 

  e
 |-- (lsubst d
 u
) -> (lsubst d'
 v
) : (lsubst d
 U
).




Corollary
 substitution_tposr_eq : 

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

   ∀ d
 d'
, e
 |-- d
 -> d'
 : t
 -> e
 |-- d'
 -> d'
 : t
 ->

   e
 |-- (lsubst d
 u
) ~= (lsubst d'
 v
) : s
.




Corollary
 substitution_tposr_coerce : 

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

   ∀ d
 d'
, e
 |-- d
 -> d'
 : t
 -> e
 |-- d'
 -> d'
 : t
 ->

   e
 |-- (lsubst d
 u
) >-> (lsubst d'
 v
) : s
.




Corollary
 substitution_tposr_tposrp_aux : ∀ G
 u
 v
 U
, G
 |-- u
 -+> v
 : U
 -> ∀ t
 e
, G
 = (t
 :: e
) ->

  ∀ d
 d'
, e
 |-- d
 -> d'
 : t
 -> e
 |-- d'
 -> d'
 : t
 ->

  e
 |-- (lsubst d
 u
) -+> (lsubst d'
 v
) : (lsubst d
 U
).




Corollary
 substitution_tposr_tposrp : ∀ t
 e
 u
 v
 U
, t
 :: e
 |-- u
 -+> v
 : U
 -> 

  ∀ d
 d'
, e
 |-- d
 -> d'
 : t
 -> e
 |-- d'
 -> d'
 : t
 ->

 e
 |-- (lsubst d
 u
) -+> (lsubst d'
 v
) : (lsubst d
 U
).




Corollary
 substitution_sorted_n : 

  ∀ g
 d
 d'
 t
, g
 |-- d
 -> d'
 : t
 -> g
 |-- d'
 -> d'
 : t
 ->

   ∀ e
 u
 v
 s
, e
 |-- u
 -> v
 : s
 ->

   ∀ f
 n
, sub_in_lenv d
 t
 n
 e
 f
 -> trunc _
 n
 f
 g
 -> 

   f
 |-- (lsubst_rec d
 u
 n
) -> (lsubst_rec d'
 v
 n
) : Srt_l s
.




Corollary
 substitution_sorted : ∀ e
 t
 u
 v
 s
, (t
 :: e
) |-- u
 -> v
 : Srt_l s
 ->

  ∀ d
 d'
, e
 |-- d
 -> d'
 : t
 -> e
 |-- d'
 -> d'
 : t
 -> e
 |-- (lsubst d
 u
) -> (lsubst d'
 v
) : Srt_l s
.




Hint
 Resolve
 substitution_tposr_tposr substitution_tposr_coerce substitution_tposr_eq substitution_tposr_tposrp : ecoc
.