Require Import sc_term. 
Require Import sc_red.
Require Import sc_context. 
Require Import sc_typ.
Require Import sc_sr.
Require Import sc_typ_alt.
Require Import sc_sr_alt.
Require Import List.

Open Scope SC_scope_alt.

Lemma Left2Right : (forall Γ M T,  (Γ ⊢ M : T)%SC -> Γ ⊢ M : T) /\
   (forall Γ A l B ,  (Γ; A ⊢ l : B)%SC -> Γ; A ⊢ l : B) /\
   ( forall  Γ , (Γ ⊣)%SC -> Γ ⊣).
apply typ_induc; intros.
(**)
eauto.
(**)
eauto.
(**)
apply Gen1b in H. destruct H as (s1 & s2 & s3 & h); decompose [and] h ; clear h.
apply RBx_RT_sort in H5. injection H5; intros; subst; clear H5.
apply typ_la with B s1 s2 s; intuition.
(**)
eauto.
(**)
destruct (StoupCorrect Γ  A l B H0) as (s & ?).
apply typ_app with A ; trivial.
(**)
apply RBx_RST_confl in r. destruct r as (C & ? & ?).
apply typ_conv_1 with C s; trivial. apply typ_conv_2 with A; trivial.
(** list **)
eauto.
(**)
eauto.
(**)
apply RBx_RST_confl in r. destruct r as ( D & ? & ?).
apply typ_list_conv_r_1 with D s; trivial. apply typ_list_conv_r_2 with A; trivial.
(**)
apply RBx_RST_confl in r. destruct r as ( D & ? & ?).
apply typ_list_conv_l_1 with D s; trivial. apply typ_list_conv_l_2 with A; trivial.
(**)
trivial.
(**)
eauto.
Qed.

Lemma Right2Left : (forall Γ M T,  Γ ⊢ M : T -> (Γ ⊢ M : T)%SC) /\
   (forall Γ A l B ,  Γ; A ⊢ l : B -> (Γ; A ⊢ l : B)%SC) /\
   ( forall  Γ , Γ ⊣ -> (Γ ⊣)%SC).
apply typ_induc_alt; intros.
(**)
eauto.
(**)
eauto.
(**)
apply sc_typ.typ_conv with (Π (A'), B) s3.
apply sc_typ.typ_la with s3.
apply sc_typ.typ_pi with s1 s2. trivial. trivial. 
apply sc_sr.SubRed_gen with B'; trivial.
trivial.
apply sc_typ.typ_pi with s1 s2. trivial. apply sc_sr.SubRed_gen with A'; trivial.
apply sc_sr.SubRed_gen with B'; trivial. 
eapply sc_sr.SubRed_gen2. apply H0. intuition. eauto.
(**)
eauto.
(**)
apply sc_typ.typ_app with A. trivial. trivial.
(**)
apply sc_typ.typ_conv with A s. trivial. 
apply sc_sr.SubRed_gen with B'; trivial. eauto.
(** list **)
apply sc_typ.typ_list_ax with s. apply sc_sr.SubRed_gen with A'; trivial.
(**)
apply sc_typ.typ_list_pi with s. apply sc_sr.SubRed_gen with T; trivial. trivial. trivial.
(**)
apply sc_typ.typ_list_conv_l with A s. trivial. apply sc_sr.SubRed_gen with B'; trivial. eauto.
(**)
apply sc_typ.typ_list_conv_r with C s. trivial. apply sc_sr.SubRed_gen with B'; trivial. eauto.
(** wf **)
trivial.
(**)
eauto.
Qed.


Inductive wf_ep : Env -> Prop :=
 | wf_ep_nil : wf_ep nil 
 | wf_ep_cons : forall Γ A s, typ_ep Γ A (!s) -> wf_ep (A::Γ)
with typ_ep : Env -> Term -> Term -> Prop :=
 | typ_ep_sort : forall Γ s1 s2, Ax s1 s2 -> wf_ep Γ -> typ_ep Γ (!s1) (!s2)
 | typ_ep_pi : forall Γ s1 s2 s3 A B, Rel s1 s2 s3 ->
    typ_ep Γ A (!s1) -> typ_ep (A::Γ) B (!s2) -> typ_ep Γ (Π(A),B) (!s3)
 | typ_ep_la : forall Γ A A' B B' M s1 s2 s3, Rel s1 s2 s3 -> typ_ep Γ A' (!s1) -> A' ▹▹ A ->
   typ_ep (A'::Γ) B' (!s2) -> B' ▹▹ B -> typ_ep (A'::Γ) M B -> typ_ep Γ (λ[A'],M) (Π(A),B)
 | typ_ep_var : forall Γ v A B l, typ_list_ep Γ A l B ->  A ↓ v  ⊂ Γ -> 
   typ_ep Γ (v ## l) B
 | typ_ep_app (*cut3*): forall Γ M A B l, typ_ep Γ M A -> typ_list_ep Γ A l B ->
    typ_ep Γ (M · l)  B
with typ_list_ep : Env -> Term -> Term_List -> Term -> Prop :=
 | typ_list_ep_ax : forall Γ A' A s, typ_ep Γ A' (!s) -> A' ▹▹ A -> typ_list_ep Γ A ([[]])  A
 | typ_list_ep_pi : forall Γ A B T s M l C, typ_ep Γ T (!s) -> T ▹▹ (Π(A),B ) -> typ_ep Γ M A -> 
   typ_list_ep Γ  (B[ ← M])  l C -> typ_list_ep Γ (Π(A),B)  (M ::: l)  C
 | typ_list_ep_conv_l : forall Γ A l C' C B s , typ_list_ep Γ A l B -> typ_ep Γ C' (!s) -> 
  C' ▹▹ C -> C ▹▹ A -> typ_list_ep Γ C l  B .

Hint Constructors wf_ep typ_ep typ_list_ep.

Scheme typ_ind_ep := Induction for typ_ep Sort Prop
      with typ_list_ind_ep := Induction for typ_list_ep Sort Prop
      with wf_ind_ep := Induction for wf_ep Sort Prop.

Combined Scheme typ_induc_ep from typ_ind_ep, typ_list_ind_ep, wf_ind_ep.

Lemma sens1 : (forall Γ M T, typ_ep Γ M T -> Γ ⊢ M : T ) /\
  (forall Γ A l B, typ_list_ep Γ A l B -> Γ; A ⊢ l : B) /\
  (forall Γ, wf_ep Γ  -> Γ ⊣).
apply typ_induc_ep; intros; eauto.
Qed.



Lemma TypRed : (forall Γ M T, typ_ep Γ M T -> forall T', T ▹▹ T' -> typ_ep Γ M T') /\
             (forall Γ A l B, typ_list_ep Γ A l B -> forall B', B ▹▹ B' -> typ_list_ep Γ A l B') /\
             (forall Γ, wf_ep Γ -> True).
apply typ_induc_ep; intros.
(**)
apply RBx_RT_sort in H0; subst. eauto.
(**)
apply RBx_RT_sort in H1; subst. eauto.
(**)
apply RBx_RT_to_Pi in H2 as (K & L & -> & ?& ?).
eauto.
(**)
apply typ_ep_var with A; intuition.
(**)
apply typ_ep_app with A; intuition.
(**)
econstructor. apply typ_list_ep_ax with A' s; trivial. eauto.
apply t. trivial. trivial.
(**)
econstructor. apply t. trivial. trivial. intuition.
(**)
eauto.
(**)
trivial. trivial.
Qed.

Lemma StoupRed : forall Γ A l B, typ_list_ep Γ A l B -> forall A', A ▹▹ A' -> exists B',  typ_list_ep Γ A' l B' /\ B ▹▹ B' .
induction 1; intros.
exists A'0; eauto.
(**)
apply RBx_RT_to_Pi in H3 as (K & L & -> & ? & ?).
destruct (IHtyp_list_ep (L[ ← M])) as ( B' & ? &?). eauto.
exists B'; split; trivial.
econstructor. apply H. eauto. eapply TypRed. apply H1. trivial. trivial.
(**)
destruct (RBx_diamond C A A' H2 H3) as (Z & ?& ?).
destruct (IHtyp_list_ep Z H4) as (B' & ? & ?).
exists B'; eauto.
Qed.



Lemma postpone : (forall Γ M T, Γ ⊢ M : T -> exists T', 
  typ_ep Γ M T' /\  T ▹▹ T') /\
 (forall Γ A l B, Γ ; A ⊢ l : B -> exists B'', exists B',  exists s, 
  typ_ep Γ B'' (!s) /\ B'' ▹▹ B /\  B ▹▹ B' /\ typ_list_ep Γ A l B') /\
 (forall Γ, Γ ⊣ -> wf_ep Γ).
apply typ_induc_alt; intros.
(**)
exists !s2; intuition.
(**)
destruct H as (T'1 &  ? & ?).
destruct H0 as (T'2 & ? & ?).
apply RBx_RT_sort in H2. subst. apply RBx_RT_sort in H1; subst.
exists !s3;  eauto.
(**)
destruct H as (T'1 & ? & ?).
destruct H0 as (T'2 &  ? & ?).
destruct H1 as (T'3 & ? & ?).
apply RBx_RT_sort in H2; subst. apply RBx_RT_sort in H3; subst.
exists ( Π (A), T'3); eauto.
(**)
destruct H as (B'' & B' & s & h). decompose [and] h; clear h.
exists B'; eauto.
(**)
destruct H0 as (B'' & B' & sB & h). decompose [and] h; clear h.
destruct H as (K'  & ? & ?).
destruct (StoupRed Γ A l B' H4 K' H3) as (Z & ? & ?).
exists Z; eauto.
(**)
destruct H0 as ( ? & ? & ?).
apply RBx_RT_sort in H1; subst.
destruct H as (TM & ?& ?).
exists TM; eauto.
(** list **)
destruct H as (? & ? & ?).
apply RBx_RT_sort in H0; subst.
exists A'; exists A; exists s; eauto.
(**)
destruct H1 as (B'' & B' &  s' & h). decompose [and] h; clear h.
destruct H as (?  & ?& ?). apply RBx_RT_sort in H4; subst.
destruct H0 as (TM  & ?& ?).
exists B''; exists B'; exists s'; split; trivial;
split; trivial. split; trivial.
apply typ_list_ep_conv_l with (Π(TM),B) T s; trivial.
econstructor.  apply H. eauto. trivial. trivial. eauto.
(**)
destruct H as (K'' & K' &  s' & h). decompose [and] h; clear h.
destruct H0 as (? & ?& ? ). apply RBx_RT_sort in H3; subst.
exists K''; exists K'; exists s'; intuition. eauto.
(**)
destruct H as (K'' & K' &  s' & h). decompose [and] h; clear h.
destruct H0 as (? &  ?& ?). apply RBx_RT_sort in H3; subst.
exists B'; exists K'; exists s; intuition. eauto.
(** env **)
trivial.
(**)
destruct H as (? & ? & ?). apply RBx_RT_sort in H0; subst.
eauto.
Qed.

Lemma TypeCorrect_ep : (forall Γ M T, typ_ep Γ M T -> (exists s, T = !s )\/(exists s, typ_ep Γ T !s)) /\
          (forall Γ A l B , typ_list_ep Γ A l B -> (exists s, B = !s )\/(exists s, typ_ep Γ B !s)) /\
          (forall Γ, wf_ep Γ -> True).
apply typ_induc_ep;intros.
(**)
left;exists s2; trivial.
(**)
left; exists s3; trivial.
(**)
right.
assert ( Γ  ⊢ (Π (A), B) : !s3).
apply SubRed_gen with (Π (A'), B').
apply sens1 in t; apply sens1 in t0. eauto. eauto.
apply postpone in H2. destruct H2 as (? & ? & ?). apply RBx_RT_sort in H3; subst.
exists s3; trivial.
(**)
trivial.
(**)
trivial.
(**)
apply sens1 in t. destruct postpone as ( ? & _).
destruct (H0 Γ A !s) as ( ? & ?& ?).
apply SubRed_gen with A'; trivial. apply RBx_RT_sort in H2; subst.
right; exists s; trivial.
(**)
trivial.
(**)
trivial.
(**)
trivial.
(**)
trivial.
Qed.

Lemma SR_ep : forall Γ M T, typ_ep Γ M T -> forall M', M ▹ M' -> exists T', typ_ep Γ M' T' /\ T ▹▹ T' .
intros.
apply sens1 in H.
apply SubRed in H. destruct H.
destruct postpone.
apply H2. apply H. trivial.
Qed.


Lemma SR_ep_gen : forall Γ M T, typ_ep Γ M T -> forall M', M ▹▹ M' -> exists T', typ_ep Γ M' T' /\ T ▹▹ T' .
intros. revert Γ T H. induction H0; intros. exists T; intuition.
destruct (SR_ep Γ s T H1 t H) as (T' & ? & ?).
destruct (IHRBx_RT Γ T' H2) as (T'' & ? & ?).
exists T''; eauto.
Qed.

Lemma StoupCorrect_ep : forall Γ A l B , typ_list_ep Γ A l B -> exists s, typ_ep Γ A !s.
induction 1; intros.
destruct postpone as ( ? & _).
destruct (H1 Γ A !s) as (? & ? &?). apply SubRed_gen with A'; trivial. apply sens1; trivial.
apply RBx_RT_sort in H3; subst.
exists s; trivial.
(**)
destruct (SR_ep_gen Γ T !s H (Π(A),B) H0) as ( w &? & ?).
apply RBx_RT_sort in H4; subst. exists s; trivial.
(**)
destruct (SR_ep_gen Γ C' !s H0 C H1) as (w& ? & ?). apply RBx_RT_sort in H4; subst.
exists s; trivial.
Qed.

Lemma postpone_plus : forall Γ A l B, Γ ; A ⊢ l : B -> exists B', B ▹▹ B' /\ typ_list_ep Γ A l B'.
intros.
apply postpone in H.
destruct H as (B'' & B' & s & h); decompose [and] h; clear h.
exists B'; intuition.
Qed.