Library Lambda.TPOSR.TypesDepth
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.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.
Reserved Notation "G |-- u -> v : T [ n ]" (at level 70, u, v, T, n at next level).
Require Import Lambda.TPOSR.MaxLemmas.
Inductive tposrd_wf : lenv -> Prop :=
| wfd_nil : tposrd_wf nil
| wfd_cons : ∀ G A A' s n, G |-- A -> A' : Srt_l s [n] -> tposrd_wf (A :: G)
with tposrd : lenv -> lterm -> lterm -> lterm -> nat -> Prop :=
| tposrd_var : ∀ e, tposrd_wf e ->
∀ n T, item_llift T e n -> e |-- (Ref_l n) -> (Ref_l n) : T [0]
| tposrd_set : ∀ e, tposrd_wf e -> e |-- (Srt_l set) -> (Srt_l set) : Srt_l kind [0]
| tposrd_prop : ∀ e, tposrd_wf e -> e |-- (Srt_l prop) -> (Srt_l prop) : Srt_l kind [0]
| tposrd_prod : ∀ e A A' s1 n, e |-- A -> A' : Srt_l s1 [n] ->
∀ B B' s2 m, (A :: e) |-- B -> B' : Srt_l s2 [m] ->
e |-- Prod_l A B -> Prod_l A' B' : Srt_l s2 [S (max n m)]
| tposrd_abs : ∀ e A A' s1 n, e |-- A -> A' : Srt_l s1 [n] ->
∀ B B' s2 m, (A :: e) |-- B -> B' : Srt_l s2 [m] ->
∀ M M' p, (A :: e) |-- M -> M' : B [p] ->
e |-- Abs_l A M -> Abs_l A' M' : (Prod_l A B) [S (max3 n m p)]
| tposrd_app : ∀ e A A' s1 n, e |-- A -> A' : Srt_l s1 [n] ->
∀ B B' s2, (A :: e) |-- B >-> B' : s2 ->
∀ M M' p, e |-- M -> M' : (Prod_l A B) [p] ->
∀ N N' q, e |-- N -> N' : A [q] ->
e |-- App_l B M N -> App_l B' M' N' : lsubst N B [S (max3 n p q)]
| tposrd_beta : ∀ e A A' s1 n, e |-- A -> A' : Srt_l s1 [n] ->
∀ B B' s2 m, (A :: e) |-- B -> B' : Srt_l s2 [m] ->
∀ M M' p, (A :: e) |-- M -> M' : B [p] ->
∀ N N' q, e |-- N -> N' : A [q] ->
e |-- App_l B (Abs_l A M) N -> lsubst N' M' : lsubst N B [S (max4 n m p q)]
| tposrd_conv : ∀ e M N A n, e |-- M -> N : A [n] ->
∀ B s, e |-- A >-> B : s ->
e |-- M -> N : B [S n]
| tposrd_subset : ∀ e A A' n, e |-- A -> A' : Srt_l set [n] ->
∀ B B' m, (A :: e) |-- B -> B' : Srt_l prop [m] ->
e |-- Subset_l A B -> Subset_l A' B' : Srt_l set [S (max n m)]
| tposrd_sum : ∀ e A A' s1 n, e |-- A -> A' : Srt_l s1 [n] ->
∀ B B' s2 m, (A :: e) |-- B -> B' : Srt_l s2 [m] ->
∀ s3, sum_sort s1 s2 s3 ->
e |-- Sum_l A B -> Sum_l A' B' : Srt_l s3 [S (max n m)]
| tposrd_pair : ∀ e A A' s1 n, e |-- A -> A' : Srt_l s1 [n] ->
∀ B B' s2 m, (A :: e) |-- B -> B' : Srt_l s2 [m] ->
∀ s3, sum_sort s1 s2 s3 ->
∀ u u' p, e |-- u -> u' : A [p] ->
∀ v v' q, e |-- v -> v' : lsubst u B [q] ->
e |-- Pair_l (Sum_l A B) u v -> Pair_l (Sum_l A' B') u' v' : Sum_l A B [S (max4 n m p q)]
| tposrd_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' p, e |-- t -> t' : Sum_l A B [p] ->
e |-- Pi1_l (Sum_l A B) t -> Pi1_l (Sum_l A' B') t' : A [S p]
| tposrd_pi1_red : ∀ e A A' s1 n, e |-- A -> A' : Srt_l s1 [n] ->
∀ B B' s2 m, (A :: e) |-- B -> B' : Srt_l s2 [m] ->
∀ s3, sum_sort s1 s2 s3 ->
∀ u u' v v' p, e |-- Pair_l (Sum_l A B) u v -> Pair_l (Sum_l A' B') u' v' : Sum_l A B [p] ->
∀ A'', e |-- A'' >-> A : s1 ->
∀ B'', A'' :: e |-- B'' >-> B : s2 ->
e |-- Pi1_l (Sum_l A'' B'') (Pair_l (Sum_l A B) u v) -> u' : A'' [S (max3 n m p)]
| tposrd_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' p, e |-- t -> t' : Sum_l A B [p] ->
e |-- Pi2_l (Sum_l A B) t -> Pi2_l (Sum_l A' B') t' : lsubst (Pi1_l (Sum_l A B) t) B [S p]
| tposrd_pi2_red : ∀ e A A' s1 n, e |-- A -> A' : Srt_l s1 [n] ->
∀ B B' s2 m, (A :: e) |-- B -> B' : Srt_l s2 [m] ->
∀ s3, sum_sort s1 s2 s3 ->
∀ u u' v v' p,
e |-- Pair_l (Sum_l A B) u v -> Pair_l (Sum_l A' B') u' v' : Sum_l A B [p] ->
∀ A'', e |-- A'' >-> A : s1 ->
∀ B'', A'' :: e |-- B'' >-> B : s2 ->
e |-- Pi2_l (Sum_l A'' B'') (Pair_l (Sum_l A B) u v) -> v' : lsubst (Pi1_l (Sum_l A'' B'') (Pair_l (Sum_l A B) u v)) B''
[S (max3 n m p)]
where "G |-- T -> U : s [ n ]" := (tposrd G T U s n).
Hint Resolve wfd_nil tposrd_set tposrd_prop tposrd_subset : coc.
Hint Resolve tposrd_prod tposrd_abs tposrd_app tposrd_sum : coc.
Scheme ind_tposr := Induction for tposrd Sort Prop.
Scheme tposrd_wf_mutind := Induction for tposrd Sort Prop
with wf_tposrd_mutind := Induction for tposrd_wf Sort Prop.
Require Import Lambda.TPOSR.Types.
Lemma tposr_tposrd :
(∀ e t u T, tposr e t u T ->
∃ n, e |-- t -> u : T [n]) ∧
(∀ e, tposr_wf e -> tposrd_wf e).
Corollary tposr_tposrd_type : ∀ e t u T, tposr e t u T ->
∃ n, e |-- t -> u : T [n].
Corollary tposr_tposrd_wf : ∀ e, tposr_wf e -> tposrd_wf e.
Definition tod := tposr_tposrd_type.
Coercion tposr_to_tposrd_wf := fun e ⇒ fun d : tposr_wf e ⇒
tposr_tposrd_wf d.
Hint Resolve tposr_tposrd_type tposr_tposrd_wf : coc.
Require Import Lambda.TPOSR.LeftReflexivity.
Require Import Lambda.TPOSR.RightReflexivity.
Lemma tposrd_tposr :
(∀ e t u T n, tposrd e t u T n ->
tposr e t u T) ∧
(∀ e, tposrd_wf e -> tposr_wf e).
Corollary tposrd_tposr_type : ∀ e t u T n, e |-- t -> u : T [n] ->
e |-- t -> u : T.
Definition fromd := tposrd_tposr_type.
Hint Resolve tposrd_tposr_type : ecoc.
Corollary tposrd_tposr_wf : ∀ e, tposrd_wf e -> tposr_wf e.
Hint Resolve tposrd_tposr_wf : coc.
Lemma tposr_to_tposrd : ∀ (P : Prop) e t u T n, e |-- t -> u : T [n] ->
(e |-- t -> u : T -> P) -> P.
Definition tposr_term_depth G M A :=
∃ M', ∃ n, G |-- M -> M' : A [n].
Lemma tposrd_tposr_term_depth : ∀ G t u T n, G |-- t -> u : T [n] ->
tposr_term_depth G t T.
Hint Resolve tposrd_tposr_term_depth : ecoc.
Lemma tposr_term_tod : ∀ G M A, tposr_term G M A -> tposr_term_depth G M A.
Hint Resolve tposr_term_tod : coc.
Lemma tposr_term_fromd : ∀ G M A, tposr_term_depth G M A -> tposr_term G M A.
Hint Resolve tposr_term_fromd : coc.