Library Lambda.TPOSR.TPOSR_trans


Require
 Import
 Lambda.Utils.

Require
 Import
 Lambda.Tactics.

Require
 Import
 Lambda.MyList.




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

Require
 Import
 Lambda.TPOSR.Thinning.

Require
 Import
 Lambda.TPOSR.LeftReflexivity.

Require
 Import
 Lambda.TPOSR.Substitution.

Require
 Import
 Lambda.TPOSR.SubstitutionTPOSR.

Require
 Import
 Lambda.TPOSR.CtxConversion.

Require
 Import
 Lambda.TPOSR.RightReflexivity.

Require
 Import
 Lambda.TPOSR.CtxCoercion.

Require
 Import
 Lambda.TPOSR.Equiv.

Require
 Import
 Lambda.TPOSR.Generation.

Require
 Import
 Lambda.TPOSR.Validity.

Require
 Import
 Lambda.TPOSR.TypesDepth.

Require
 Import
 Lambda.TPOSR.TypesFunctionality.

Require
 Import
 Lambda.TPOSR.UniquenessOfTypes.

Require
 Import
 Lambda.TPOSR.ChurchRosser.

Require
 Import
 Lambda.TPOSR.SubjectReduction.







Implicit
 Types
 i
 k
 m
 n
 p
 : nat.

Implicit
 Type
 s
 : sort.

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




Lemma
 substitution_tposrp_tposr : ∀ e
 d
 d'
 t
, e
 |-- d
 -+> d'
 : t
 ->

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

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




Lemma
 substitution_tposrp_coerce : ∀ e
 d
 d'
 t
, e
 |-- d
 -+> d'
 : t
 ->

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

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




Require
 Import
 Lambda.TPOSR.Substitution.




Lemma
 tposrp_abs_aux :  ∀ e
 A
 A'
 Ts1
, e
 |-- A
 -+> A'
 : Ts1
 ->

  ∀ s1
, Ts1
 = Srt_l s1
 ->

  ∀ B
 M
 M'
, (A
 :: e
) |-- M
 -> M'
 : B
 -> 

  ∀ B'
 s2
, (A
 :: e
) |-- B
 -> B'
 : Srt_l s2
 -> 

  e
 |-- Abs_l A
 M
 -+> Abs_l A'
 M'
 : (Prod_l A
 B
).




Lemma
 tposrp_abs_aux2 :

  ∀ G
 B
 M
 M'
, G
 |-- M
 -+> M'
 : B
 -> 

  ∀ e
 A
 A'
 s1
, e
 |-- A
 -> A'
 : s1
 ->

  G
 = (A
 :: e
) ->

  ∀ B'
 s2
, (A
 :: e
) |-- B
 -> B'
 : Srt_l s2
 -> 

  e
 |-- Abs_l A
 M
 -+> Abs_l A'
 M'
 : (Prod_l A
 B
).




Hint
 Resolve
 conv_env tposrp_conv_env : ecoc
.




Lemma
 tposrp_abs :  ∀ e
 A
 A'
 s1
, e
 |-- A
 -+> A'
 : Srt_l s1
 ->

  ∀ B
 M
 M'
, (A
 :: e
) |-- M
 -+> M'
 : B
 -> 

  ∀ B'
 s2
, (A
 :: e
) |-- B
 -+> B'
 : Srt_l s2
 -> 

  e
 |-- Abs_l A
 M
 -+> Abs_l A'
 M'
 : (Prod_l A
 B
).




Ltac
 conv_in_env
 X
 Y
 e
 s
 :=

  assert
(conv_in_env (X
 :: e
) (Y
 :: e
)) by
 (apply
 conv_env_hd with
 s
 ; auto
 with
 coc
).




Ltac
 coerce_in_env
 X
 Y
 e
 s
 :=

  assert
(coerce_in_env (X
 :: e
) (Y
 :: e
)) by
 (apply
 coerce_env_hd with
 s
 ; auto
 with
 coc
 ecoc
).




Lemma
 tposrp_prod_aux : ∀ e
 A
 A'
 Ts1
, e
 |-- A
 -+> A'
 : Ts1
 ->

  ∀ s1
, Ts1
 = Srt_l s1
 ->

  ∀ B
 B'
 s2
, (A
 :: e
) |-- B
 -> B'
 : Srt_l s2
 ->

  e
 |-- Prod_l A
 B
 -+> Prod_l A'
 B'
 : Srt_l s2
.




Lemma
 tposrp_prod : ∀ e
 A
 A'
 s1
, e
 |-- A
 -+> A'
 : Srt_l s1
 ->

  ∀ B
 B'
 s2
, (A
 :: e
) |-- B
 -+> B'
 : Srt_l s2
 ->

  e
 |-- Prod_l A
 B
 -+> Prod_l A'
 B'
 : Srt_l s2
.




Ltac
 induction_ws
 := induction_with_subterm
.

Ltac
 induction_ws2
 := induction_with_subterms
.




Lemma
 tposrp_app_aux : 

  ∀ e
 A
 A'
 s1
, e
 |-- A
 -+> A'
 : Srt_l s1
 ->

  ∀ B
 B'
 s2
, (A
 :: e
) |-- B
 >-> B'
 : s2
 ->

  ∀ M
 M'
, e
 |-- M
 -> M'
 : (Prod_l A
 B
) -> 

  ∀ N
 N'
, e
 |-- N
 -> N'
 : A
 ->

  e
 |-- App_l B
 M
 N
 -+> App_l B'
 M'
 N'
 : lsubst N
 B
.




Lemma
 tposrp_app_aux2 :

  ∀ e
 M
 M'
 A
 B
, e
 |-- M
 -+> M'
 : (Prod_l A
 B
) -> 

  ∀ B'
 s2
, (A
 :: e
) |-- B
 >-> B'
 : s2
 ->

  ∀ A'
 s1
, e
 |-- A
 -> A'
 : Srt_l s1
 ->

  ∀ N
 N'
, e
 |-- N
 -> N'
 : A
 ->

  e
 |-- App_l B
 M
 N
 -+> App_l B'
 M'
 N'
 : lsubst N
 B
.




Lemma
 tposrp_app_aux3 :

  ∀ e
 N
 N'
 A
, e
 |-- N
 -+> N'
 : A
 ->

  ∀ M
 M'
 B
, e
 |-- M
 -> M'
 : (Prod_l A
 B
) -> 

  ∀ B'
 s2
, (A
 :: e
) |-- B
 >-> B'
 : s2
 ->

  ∀ A'
 s1
, e
 |-- A
 -> A'
 : Srt_l s1
 ->

  e
 |-- App_l B
 M
 N
 -+> App_l B'
 M'
 N'
 : lsubst N
 B
.




Lemma
 tposrp_app : ∀ e
 A
 A'
 s1
, e
 |-- A
 -+> A'
 : Srt_l s1
 ->

  ∀ B
 B'
 s2
, (A
 :: e
) |-- B
 >-> B'
 : s2
 ->

  ∀ M
 M'
, e
 |-- M
 -+> M'
 : (Prod_l A
 B
) -> 

  ∀ N
 N'
, e
 |-- N
 -+> N'
 : A
 ->

  e
 |-- App_l B
 M
 N
 -+> App_l B'
 M'
 N'
 : lsubst N
 B
.




Lemma
 tposrp_subset_aux : ∀ e
 A
 A'
, e
 |-- A
 -+> A'
 : Srt_l set ->

  ∀ B
 B'
, (A
 :: e
) |-- B
 -> B'
 : Srt_l prop ->

  e
 |-- Subset_l A
 B
 -+> Subset_l A'
 B'
 : Srt_l set.




Lemma
 tposrp_subset : ∀ e
 A
 A'
, e
 |-- A
 -+> A'
 : Srt_l set ->

  ∀ B
 B'
, (A
 :: e
) |-- B
 -+> B'
 : Srt_l prop ->

  e
 |-- Subset_l A
 B
 -+> Subset_l A'
 B'
 : Srt_l set.




Lemma
 tposrp_sigma_aux : ∀ e
 A
 A'
 s1
, e
 |-- A
 -+> A'
 : Srt_l s1
 ->

  ∀ B
 B'
 s2
, (A
 :: e
) |-- B
 -> B'
 : Srt_l s2
 ->

  ∀ s3
, sum_sort s1
 s2
 s3
 ->

  e
 |-- Sum_l A
 B
 -+> Sum_l A'
 B'
 : Srt_l s3
.




Lemma
 tposrp_sigma : ∀ e
 A
 A'
 s1
, e
 |-- A
 -+> A'
 : Srt_l s1
 ->

  ∀ B
 B'
 s2
, (A
 :: e
) |-- B
 -+> B'
 : Srt_l s2
 ->

  ∀ s3
, sum_sort s1
 s2
 s3
 ->

  e
 |-- Sum_l A
 B
 -+> Sum_l A'
 B'
 : Srt_l s3
.




Lemma
 tposrp_pair_aux1 : ∀ e
 A
 A'
 s1
, e
 |-- A
 -+> A'
 : Srt_l s1
 ->

  ∀ B
 B'
 s2
, (A
 :: e
) |-- B
 -> B'
 : Srt_l s2
 ->

  ∀ s3
, sum_sort s1
 s2
 s3
 ->

  ∀ u
 u'
, e
 |-- u
 -> u'
 : A
 ->

  ∀ v
 v'
, e
 |-- v
 -> v'
 : lsubst u
 B
 ->

  e
 |-- Pair_l (Sum_l A
 B
) u
 v
 -+> Pair_l (Sum_l A'
 B'
) u'
 v'
 : Sum_l A
 B
.




Lemma
 tposrp_pair_aux2 :

  ∀ e
 A
 B
 B'
 s2
, (A
 :: e
) |-- B
 -+> B'
 : Srt_l s2
 ->

  ∀ A'
 s1
, e
 |-- A
 -> A'
 : Srt_l s1
 ->

  ∀ s3
, sum_sort s1
 s2
 s3
 ->

  ∀ u
 u'
, e
 |-- u
 -> u'
 : A
 ->

  ∀ v
 v'
, e
 |-- v
 -> v'
 : lsubst u
 B
 ->

  e
 |-- Pair_l (Sum_l A
 B
) u
 v
 -+> Pair_l (Sum_l A'
 B'
) u'
 v'
 : Sum_l A
 B
.




Lemma
 tposrp_pair_aux3 :

  ∀ e
 u
 u'
 A
, e
 |-- u
 -+> u'
 : A
 ->

  ∀ A'
 s1
, e
 |-- A
 -> A'
 : Srt_l s1
 ->

  ∀ B
 B'
 s2
, (A
 :: e
) |-- B
 -> B'
 : Srt_l s2
 ->

  ∀ s3
, sum_sort s1
 s2
 s3
 ->

  ∀ v
 v'
, e
 |-- v
 -> v'
 : lsubst u
 B
 ->

  e
 |-- Pair_l (Sum_l A
 B
) u
 v
 -+> Pair_l (Sum_l A'
 B'
) u'
 v'
 : Sum_l A
 B
.




Lemma
 tposrp_pair_aux4 :

  ∀ e
 u
 v
 v'
 B
, e
 |-- v
 -+> v'
 : lsubst u
 B
 ->

  ∀ A
 A'
 s1
, e
 |-- A
 -> A'
 : Srt_l s1
 ->

  ∀ B'
 s2
, (A
 :: e
) |-- B
 -> B'
 : Srt_l s2
 ->

  ∀ s3
, sum_sort s1
 s2
 s3
 ->

  ∀ u'
, e
 |-- u
 -> u'
 : A
 ->

  e
 |-- Pair_l (Sum_l A
 B
) u
 v
 -+> Pair_l (Sum_l A'
 B'
) u'
 v'
 : Sum_l A
 B
.




Lemma
 tposrp_pair : ∀ e
 A
 A'
 s1
, e
 |-- A
 -+> A'
 : Srt_l s1
 ->

  ∀ B
 B'
 s2
, (A
 :: e
) |-- B
 -+> B'
 : Srt_l s2
 ->

  ∀ s3
, sum_sort s1
 s2
 s3
 ->

  ∀ u
 u'
, e
 |-- u
 -+> u'
 : A
 ->

  ∀ v
 v'
, e
 |-- v
 -+> v'
 : lsubst u
 B
 ->

  e
 |-- Pair_l (Sum_l A
 B
) u
 v
 -+> Pair_l (Sum_l A'
 B'
) u'
 v'
 : Sum_l A
 B
.




Lemma
 tposrp_pi1_aux :

  ∀ e
 t
 t'
 A
 B
 , e
 |-- t
 -+> t'
 : Sum_l A
 B
 ->

  ∀ A'
 s1
, e
 |-- A
 >-> A'
 : s1
 ->

  ∀ B'
 s2
, (A
 :: e
) |-- B
 >-> B'
 : s2
 ->

  ∀ s3
, sum_sort s1
 s2
 s3
 ->

  e
 |-- Pi1_l (Sum_l A
 B
) t
 -+> Pi1_l (Sum_l A'
 B'
) t'
 : A
.




Lemma
 tposrp_pi1 :

  ∀ e
 A
 A'
 s1
, e
 |-- A
 >-> A'
 : s1
 ->

  ∀ B
 B'
 s2
, (A
 :: e
) |-- B
 >-> B'
 : s2
 ->

  ∀ s3
, sum_sort s1
 s2
 s3
 ->

  ∀ t
 t'
, e
 |-- t
 -+> t'
 : Sum_l A
 B
 ->

  e
 |-- Pi1_l (Sum_l A
 B
) t
 -+> Pi1_l (Sum_l A'
 B'
) t'
 : A
.




Lemma
 tposrp_pi2_aux : ∀ e
 t
 t'
 A
 B
, e
 |-- t
 -+> t'
 : Sum_l A
 B
 ->

  ∀ A'
 s1
, e
 |-- A
 >-> A'
 : s1
 ->

  ∀ B'
 s2
, (A
 :: e
) |-- B
 >-> B'
 : s2
 ->

  ∀ s3
, sum_sort s1
 s2
 s3
 ->

  e
 |-- Pi2_l (Sum_l A
 B
) t
 -+> Pi2_l (Sum_l A'
 B'
) t'
 : lsubst (Pi1_l (Sum_l A
 B
) t
) B
.




Lemma
 tposrp_pi2 : ∀ e
 A
 A'
 s1
, e
 |-- A
 >-> A'
 : s1
 ->

  ∀ B
 B'
 s2
, (A
 :: e
) |-- B
 >-> B'
 : s2
 ->

  ∀ s3
, sum_sort s1
 s2
 s3
 ->

  ∀ t
 t'
, e
 |-- t
 -+> t'
 : Sum_l A
 B
 ->

  e
 |-- Pi2_l (Sum_l A
 B
) t
 -+> Pi2_l (Sum_l A'
 B'
) t'
 : lsubst (Pi1_l (Sum_l A
 B
) t
) B
.