Library Lambda.TPOSR.Generation


Require
 Import
 Lambda.Utils.

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

Require
 Import
 Lambda.TPOSR.SubstitutionTPOSR.

Require
 Import
 Lambda.TPOSR.CtxConversion.

Require
 Import
 Lambda.TPOSR.CtxCoercion.

Require
 Import
 Lambda.TPOSR.RightReflexivity.

Require
 Import
 Lambda.TPOSR.Basic.

Require
 Import
 Lambda.TPOSR.UnicityOfSorting.

Require
 Import
 Lambda.TPOSR.Equiv.

Require
 Import
 Lambda.TPOSR.TypesDepth.







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
 generation_sort :  ∀ e
 s
 u
 T
, e
 |-- Srt_l s
 -> u
 : T
 -> 

  u
 = Srt_l s
 ∧ T
 = Srt_l kind.




Lemma
 inv_lift_ref : ∀ t
 n
, llift 1 t
 = Ref_l n
 -> ∃ n'
, t
 = Ref_l n'
 ∧ S n'
 = n
.




Lemma
 generation_var : ∀ e
 n
 X
 A
, e
 |-- Ref_l n
 -> X
 : A
 -> 

  X
 = Ref_l n
 ∧

  ∃ B
, item_llift B
 e
 n
 ∧ 

  ∃ s
, e
 |-- A
 >-> B
 : s
.




Lemma
 equiv_sym_sort : ∀ e
, tposr_wf e
 -> ∀ s
, equiv e
 s
 s
.




Lemma
 generation_prod_depth : ∀ e
 U
 V
 X
 A
 n
, e
 |-- Prod_l U
 V
 -> X
 : A
 [n
] -> 

  exists3
 U'
 s1
 m
, exists3
 V'
 s2
 p
, 

  e
 |-- U
 -> U'
 : Srt_l s1
 [m
] ∧ m
 < n
 ∧

  U
 :: e
 |-- V
 -> V'
 : Srt_l s2
 [p
] ∧ p
 < n
 ∧

  X
 = Prod_l U'
 V'
 ∧ equiv e
 A
 (Srt_l s2
).




Lemma
 generation_prod : ∀ e
 U
 V
 X
 A
, e
 |-- Prod_l U
 V
 -> X
 : A
 -> 

  exists2
 U'
 s1
, exists2
 V'
 s2
, 

  e
 |-- U
 -> U'
 : Srt_l s1
 ∧

  U
 :: e
 |-- V
 -> V'
 : Srt_l s2
 ∧

  X
 = Prod_l U'
 V'
 ∧ equiv e
 A
 (Srt_l s2
).




Lemma
 generation_sum_depth : ∀ e
 U
 V
 X
 A
 m
, e
 |-- Sum_l U
 V
 -> X
 : A
 [m
] -> 

  exists3
 U'
 s1
 n
, 

  exists3
 V'
 s2
 p
, ∃ s3
,

  e
 |-- U
 -> U'
 : Srt_l s1
 [n
] ∧ n
 < m
 ∧

  U
 :: e
 |-- V
 -> V'
 : Srt_l s2
 [p
] ∧ p
 < m
 ∧

  sum_sort s1
 s2
 s3
 ∧

  X
 = Sum_l U'
 V'
 ∧ equiv e
 A
 (Srt_l s3
).




Lemma
 generation_sum : ∀ e
 U
 V
 X
 A
, e
 |-- Sum_l U
 V
 -> X
 : A
 -> 

  exists2
 U'
 s1
, 

  exists2
 V'
 s2
, ∃ s3
,

  e
 |-- U
 -> U'
 : Srt_l s1
 ∧

  U
 :: e
 |-- V
 -> V'
 : Srt_l s2
 ∧

  sum_sort s1
 s2
 s3
 ∧

  X
 = Sum_l U'
 V'
 ∧ equiv e
 A
 (Srt_l s3
).




Lemma
 generation_lambda_depth : ∀ e
 T
 M
 X
 A
 m
, e
 |-- Abs_l T
 M
 -> X
 : A
 [m
] -> 

  exists3
 T'
 s1
 n
, exists3
 M'
 s2
 p
, exists3
 C
 C'
 q
,

  e
 |-- T
 -> T'
 : Srt_l s1
 [n
] ∧ n
 < m
 ∧

  T
 :: e
 |-- M
 -> M'
 : C
 [p
] ∧ p
 < m
 ∧

  T
 :: e
 |-- C
 -> C'
 : Srt_l s2
 [q
] ∧ q
 < m
 ∧

  X
 = Abs_l T'
 M'
 ∧ equiv_sort e
 A
  (Prod_l T
 C
) s2
.




Lemma
 generation_lambda : ∀ e
 T
 M
 X
 A
, e
 |-- Abs_l T
 M
 -> X
 : A
-> 

  exists2
 T'
 s1
, 

  exists2
 M'
 s2
,

  exists2
 C
 C'
,

  e
 |-- T
 -> T'
 : Srt_l s1
 ∧

  T
 :: e
 |-- M
 -> M'
 : C
 ∧

  T
 :: e
 |-- C
 -> C'
 : Srt_l s2
 ∧

  X
 = Abs_l T'
 M'
 ∧ equiv_sort e
 A
  (Prod_l T
 C
) s2
.




Lemma
 generation_app_depth : ∀ e
 V
 W
 X
 Y
 Z
 m
, e
 |-- App_l V
 W
 X
 -> Y
 : Z
 [m
] -> 

  exists4
 U
 U'
 s1
 n
,

  exists2
 V'
 s2
,

  exists2
 X'
 q
,

  e
 |-- U
 -> U'
 : Srt_l s1
 [n
] ∧ n
 < m
 ∧

  U
 :: e
 |-- V
 >-> V'
 : s2
 ∧

  e
 |-- X
 -> X'
 : U
 [q
] ∧ q
 < m
 ∧

  equiv_sort e
 Z
 (lsubst X
 V
) s2
 ∧

  ((exists2
 W'
 r
, e
 |-- W
 -> W'
 : Prod_l U
 V
 [r
] ∧ r
 < m
 ∧

  Y
 = App_l V'
 W'
 X'
) ∨

  (exists3
 T
 T'
 r
, 

  W
 = Abs_l U
 T
 ∧

  U
 :: e
 |-- T
 -> T'
 : V
 [r
] ∧ r
 < m
 ∧

  Y
 = lsubst X'
 T'
)).




Lemma
 generation_app : ∀ e
 V
 W
 X
 Y
 Z
, e
 |-- App_l V
 W
 X
 -> Y
 : Z
 -> 

  exists3
 U
 U'
 s1
,

  exists2
 V'
 s2
,

  ∃ X'
,

  e
 |-- U
 -> U'
 : Srt_l s1
 ∧

  U
 :: e
 |-- V
 >-> V'
 : s2
 ∧

  e
 |-- X
 -> X'
 : U
 ∧

  equiv_sort e
 Z
 (lsubst X
 V
) s2
 ∧

  ((∃ W'
, e
 |-- W
 -> W'
 : Prod_l U
 V
 ∧

  Y
 = App_l V'
 W'
 X'
) ∨

  (exists2
 T
 T'
, 

  W
 = Abs_l U
 T
 ∧

  U
 :: e
 |-- T
 -> T'
 : V
 ∧ Y
 = lsubst X'
 T'
)).




Lemma
 generation_app2 : ∀ e
 V
 W
 X
 Y
 Z
, e
 |-- App_l V
 W
 X
 -> Y
 : Z
 -> 

  exists3
 U
 U'
 s1
,

  exists2
 V'
 s2
,

  exists2
 X'
 W'
,

  e
 |-- U
 -> U'
 : Srt_l s1
 ∧

  U
 :: e
 |-- V
 >-> V'
 : s2
 ∧

  e
 |-- W
 -> W'
 : Prod_l U
 V
 	∧

  e
 |-- X
 -> X'
 : U
 ∧

  equiv_sort e
 Z
 (lsubst X
 V
) s2
 ∧

  ((Y
 = App_l V'
 W'
 X'
) ∨

  (exists2
 T
 T'
, 

  W
 = Abs_l U
 T
 ∧

  U
 :: e
 |-- T
 -> T'
 : V
 ∧ Y
 = lsubst X'
 T'
)).




Lemma
 generation_pair_depth : ∀ e
 T
 M
 N
 X
 C
 m
, e
 |-- Pair_l T
 M
 N
 -> X
 : C
 [m
] ->

  exists4
 A
 A'
 s1
 n
,

  exists4
 B
 B'
 s2
 p
,

  ∃ s3
,

  T
 = Sum_l A
 B
 ∧

  e
 |-- A
 -> A'
 : Srt_l s1
 [n
] ∧ n
 < m
 ∧

  A
 :: e
 |-- B
 -> B'
 : Srt_l s2
 [p
] ∧ p
 < m
 ∧

  sum_sort s1
 s2
 s3
 ∧

  exists2
 M'
 q
, e
 |-- M
 -> M'
 : A
 [q
] ∧ q
 < m
 ∧

  exists2
 N'
 r
, e
 |-- N
 -> N'
 : lsubst M
 B
 [r
] ∧ r
 < m
 ∧

  X
 = Pair_l (Sum_l A'
 B'
) M'
 N'
 ∧ equiv_sort e
 C
 (Sum_l A
 B
) s3
.




Lemma
 generation_pair : ∀ e
 T
 M
 N
 X
 C
, e
 |-- Pair_l T
 M
 N
 -> X
 : C
 ->

  exists3
 A
 A'
 s1
,

  exists3
 B
 B'
 s2
,

  ∃ s3
,

  T
 = Sum_l A
 B
 ∧

  e
 |-- A
 -> A'
 : Srt_l s1
 ∧

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

  sum_sort s1
 s2
 s3
 ∧

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

  ∃ N'
, e
 |-- N
 -> N'
 : lsubst M
 B
 ∧

  X
 = Pair_l (Sum_l A'
 B'
) M'
 N'
 ∧ equiv_sort e
 C
 (Sum_l A
 B
) s3
.




Require
 Import
 Lambda.TPOSR.MaxLemmas.




Lemma
 generation_pi1_depth : ∀ e
 T
 M
 X
 C
 m
, e
 |-- Pi1_l T
 M
 -> X
 : C
 [m
] ->

  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
 ∧

  ((exists2
 M'
 n
, e
 |-- M
 -> M'
 : Sum_l A
 B
 [n
] ∧

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

  (exists4
 u
 u'
 v
 v'
,

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

  exists2
 A''
 n
, e
 |-- A'
 -> A''
 : s1
 [n
] ∧ n
 < m
 ∧

  exists2
 B''
 p
, A'
 :: e
 |-- B'
 -> B''
 : s2
 [p
] ∧ p
 < m
 ∧

  ∃ q
, e
 |-- M
 -> Pair_l (Sum_l A''
 B''
) u'
 v'
 : Sum_l A'
 B'
 [q
] ∧ q
 < m
 ∧

  X
 = u'
)).




Lemma
 generation_pi1 :

  ∀ 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_depth : ∀ e
 T
 M
 X
 C
 m
, e
 |-- Pi2_l T
 M
 -> X
 : C
 [m
] ->

  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
 ∧

  ((exists2
 M'
 n
, e
 |-- M
 -> M'
 : Sum_l A
 B
 [n
] ∧

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

  (exists4
 u
 u'
 v
 v'
,

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

  exists2
 A''
 n
, e
 |-- A'
 -> A''
 : s1
 [n
] ∧ n
 < m
 ∧

  exists2
 B''
 p
, A'
 :: e
 |-- B'
 -> B''
 : s2
 [p
] ∧ p
 < m
 ∧

  ∃ q
, e
 |-- M
 -> Pair_l (Sum_l A''
 B''
) u'
 v'
 : Sum_l A'
 B'
 [q
] ∧ q
 < m
 ∧

  X
 = v'
)).




Lemma
 generation_pi2 :

  ∀ 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
 generation_subset_depth : ∀ e
 U
 V
 X
 A
 m
, e
 |-- Subset_l U
 V
 -> X
 : A
 [m
] -> 

  exists2
 U'
 n
, 

  exists2
 V'
 p
, 

  e
 |-- U
 -> U'
 : Srt_l set [n
] ∧ n
 < m
 ∧

  U
 :: e
 |-- V
 -> V'
 : Srt_l prop [p
] ∧ p
 < m
 ∧

  X
 = Subset_l U'
 V'
 ∧ equiv_sort e
 A
 (Srt_l set) kind.




Lemma
 generation_subset : ∀ e
 U
 V
 X
 A
, e
 |-- Subset_l U
 V
 -> X
 : A
 -> 

  exists2
 U'
 V'
, 

  e
 |-- U
 -> U'
 : Srt_l set ∧

  U
 :: e
 |-- V
 -> V'
 : Srt_l prop ∧

  X
 = Subset_l U'
 V'
 ∧ equiv_sort e
 A
 (Srt_l set) kind.