Library Lambda.TPOSR.UnlabConv


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

Require
 Import
 Lambda.TPOSR.Validity.

Require
 Import
 Lambda.TPOSR.TypesDepth.

Require
 Import
 Lambda.TPOSR.TypesFunctionality.

Require
 Import
 Lambda.TPOSR.UniquenessOfTypes.

Require
 Import
 Lambda.TPOSR.ChurchRosserDepth.

Require
 Import
 Lambda.TPOSR.ChurchRosser.

Require
 Import
 Lambda.TPOSR.Injectivity.

Require
 Import
 Lambda.TPOSR.SubjectReduction.

Require
 Import
 Lambda.TPOSR.Unlab.

Require
 Import
 Lambda.TPOSR.TPOSR_trans.




Implicit
 Types
 s
 : sort.




Hint
 Unfold
 tposr_term tposr_term_depth : coc
.

Hint
 Unfold
 equiv_sort : coc
.

Hint
 Resolve
 conv_env : coc
.




Lemma
 equiv_sort_strenghten : ∀ G
 s
 s'
, equiv G
 s
 s'
 -> ∀ e
, tposr_wf e
 -> equiv e
 s
 s'
.




Lemma
 tposr_sort_strenghten : ∀ G
 s
 s'
, G
 |-- s
 -> s
 : s'
 -> ∀ e
, tposr_wf e
 -> e
 |-- s
 -> s
 : s'
.




Lemma
 tposr_term_conv_env : ∀ e
 t
 T
, tposr_term e
 t
 T
 ->

  ∀ f
, conv_in_env e
 f
 -> tposr_term f
 t
 T
.




Hint
 Resolve
 tposr_term_conv_env : coc
.




Lemma
 generation_pi1_alt :

  ∀ e
 T
 M
 X
 C
, e
 |-- Pi1_l T
 M
 -> X
 : C
 ->

  exists2
 A
 B
, T
 = Sum_l A
 B
 ∧ equiv e
 C
 A
 ∧

  exists4
 A'
 B'
 s1
 s2
, 

  e
 |-- A
 >-> A'
 : s1
 ∧ A
 :: e
 |-- B
 >-> B'
 : s2
 ∧

  ∃ M'
, e
 |-- M
 -> M'
 : Sum_l A
 B
 ∧

  ((X
 = Pi1_l (Sum_l A'
 B'
) M'
) ∨

  (exists4
 u
 u'
 v
 v'
,

  M
 = Pair_l (Sum_l A'
 B'
) u
 v
 ∧

  ∃ A''
, e
 |-- A'
 -> A''
 : s1
 ∧

  ∃ B''
, A'
 :: e
 |-- B'
 -> B''
 : s2
 ∧

  e
 |-- M
 -> Pair_l (Sum_l A''
 B''
) u'
 v'
 : Sum_l A'
 B'
 ∧

  X
 = u'
)).




Lemma
 generation_pi2_alt :

  ∀ e
 T
 M
 X
 C
, e
 |-- Pi2_l T
 M
 -> X
 : C
 ->

  exists2
 A
 B
, T
 = Sum_l A
 B
 ∧ equiv e
 C
 (lsubst (Pi1_l T
 M
) B
) ∧

  exists4
 A'
 B'
 s1
 s2
, 

  e
 |-- A
 >-> A'
 : s1
 ∧ A
 :: e
 |-- B
 >-> B'
 : s2
 ∧

  ∃ M'
, e
 |-- M
 -> M'
 : Sum_l A
 B
 ∧

  ((X
 = Pi2_l (Sum_l A'
 B'
) M'
) ∨

  (exists4
 u
 u'
 v
 v'
,

  M
 = Pair_l (Sum_l A'
 B'
) u
 v
 ∧

  ∃ A''
, e
 |-- A'
 -> A''
 : s1
 ∧

  ∃ B''
, A'
 :: e
 |-- B'
 -> B''
 : s2
 ∧

  e
 |-- M
 -> Pair_l (Sum_l A''
 B''
) u'
 v'
 : Sum_l A'
 B'
 ∧

  X
 = v'
)).




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

  ∀ U
 V
 s'
, Srt_l s
 :: e
 |-- U
 >-> V
 : s'
 -> e
 |-- lsubst u
 U
 >-> lsubst v
 V
 : s'
.




Lemma
 generation_sump : ∀ e
 t
 u
 T
, e
 |-- t
 -+> u
 : T
 -> 

  ∀ U
 V
, t
 = Sum_l U
 V
 ->

  exists2
 U'
 V'
,

  ∃ s1
 : sort,

  ∃ s2
 : sort, u
 = Sum_l U'
 V'
 ∧ e
 |-- U
 -+> U'
 : s1
 ∧ U
 :: e
 |-- V
 -+> V'
 : s2
.




Lemma
 generation_tposrp_sum : ∀ e
 t
 u
 T
, e
 |-- t
 -+> u
 : T
 -> 

  ∀ U
 V
, t
 = Sum_l U
 V
 -> ∀ U'
 V'
, u
 = Sum_l U'
 V'
 ->

  ∃ s1
 : sort,

  ∃ s2
 : sort, e
 |-- U
 -+> U'
 : s1
 ∧ U
 :: e
 |-- V
 -+> V'
 : s2
.




Lemma
 tposr_unlab_conv : ∀ M
 G
 N
 A
 B
, tposr_term G
 M
 A
 -> tposr_term G
 N
 B
 ->

  (|M|) = (|N|) ->

  ∃ P
, 

  (G
 |-- M
 -+> P
 : A
 ∧

  G
 |-- M
 -+> P
 : B
 ∧

  G
 |-- N
 -+> P
 : A
 ∧

  G
 |-- N
 -+> P
 : B
).




Corollary
 unlab_conv_sorted : ∀ G
 A
 B
 s
 t
, tposr_term G
 A
 (Srt_l s
) ->

  tposr_term G
 B
 (Srt_l t
) -> ( | A
 | ) = ( | B
 | ) -> s
 = t
 ∧ G
 |-- A
 ~= B
 : s
.




Inductive
 conv_in_env_full : lenv -> lenv -> Prop
 :=

  | conv_env_trans : ∀ e
 f
 g
, conv_in_env_full e
 f
 -> conv_in_env_full f
 g
 -> conv_in_env_full e
 g


  | conv_env_in_env : ∀ e
 f
, conv_in_env e
 f
 -> conv_in_env_full e
 f


  | conv_env_nil : conv_in_env_full nil nil.




Hint
 Resolve
 conv_env_in_env conv_env_nil : coc
.




Lemma
 conv_env_full_sym : ∀ e
 f
, conv_in_env_full e
 f
 -> conv_in_env_full f
 e
.




Lemma
 conv_env_full :

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

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




Lemma
 conv_env_full_cons : ∀ G
 D
, conv_in_env_full G
 D
 -> ∀ T
, tposr_wf (T
 :: G
) ->

  conv_in_env_full (T
 :: G
) (T
 :: D
).




Corollary
 tposrp_conv_env_full : 

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

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




Corollary
 eq_conv_env_full : 

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

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




Hint
 Resolve
 conv_env_full eq_conv_env_full : ecoc
.




Corollary
 coerce_conv_env_full : 

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

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




Lemma
 unlab_conv_ctx_conv : ∀ G
 D
, tposr_wf G
 -> tposr_wf D
 -> 

  (unlab_ctx D
) = (unlab_ctx G
) -> conv_in_env_full G
 D
.




Corollary
 unlab_conv_ctx : ∀ D
, tposr_wf D
 -> ∀ G
 M
 N
 A
, G
 |-- M
 -> N
 : A
 -> 

 (unlab_ctx D
) = (unlab_ctx G
) -> D
 |-- M
 -> N
 : A
.




Corollary
 eq_unlab_conv_ctx : ∀ D
, tposr_wf D
 -> ∀ G
 M
 N
 s
, G
 |-- M
 ~= N
 : s
 -> 

 (unlab_ctx D
) = (unlab_ctx G
) -> D
 |-- M
 ~= N
 : s
.




Corollary
 coerce_unlab_conv_ctx : ∀ D
, tposr_wf D
 -> ∀ G
 M
 N
 s
, G
 |-- M
 >-> N
 : s
 -> 

 (unlab_ctx D
) = (unlab_ctx G
) -> D
 |-- M
 >-> N
 : s
.




Require
 Import
 Lambda.Reduction.

Require
 Import
 Lambda.Conv.




Lemma
 conv_eq : ∀ t
 u
, conv (|t|) (|u|) ->

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