Library Lambda.TPOSR.Substitution


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

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

   ∀ g
 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
)) ∧

   (∀ e
, tposr_wf e
 ->

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

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

   tposr_wf f
) ∧

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

   ∀ g
 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
) ∧

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

   ∀ g
 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
).




Corollary
 substitution_tposr_n : ∀ g
 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_wf_n : ∀ g
 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_eq_n : ∀ g
 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_coerce_n : ∀ g
 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 : ∀ e
 t
 u
 v
 U
, (t
 :: e
) |-- u
 -> v
 : U
 ->

  ∀ d
, e
 |-- d
 -> d
 : t
 -> e
 |-- (lsubst d
 u
) -> (lsubst d
 v
) : (lsubst d
 U
).




Corollary
 substitution_eq : 

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

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

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




Corollary
 substitution_coerce : 

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

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

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




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

  ∀ d
, e
 |-- d
 -> d
 : t
 -> e
 |-- (lsubst d
 u
) -+> (lsubst d
 v
) : (lsubst d
 U
).




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

  ∀ d
, e
 |-- d
 -> d
 : t
 -> e
 |-- (lsubst d
 u
) -+> (lsubst d
 v
) : (lsubst d
 U
).




Corollary
 substitution_sorted_n : 

  ∀ g
 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
, e
 |-- d
 -> d
 : t
 -> e
 |-- (lsubst d
 u
) -> (lsubst d
 v
) : Srt_l s
.




Hint
 Resolve
 substitution substitution_coerce substitution_eq substitution_tposrp : ecoc
.