Require Import sc_term. 
Require Import sc_red.
Require Import sc_context. 
Require Import sc_typ_alt.
Require Import List.


Reserved Notation "Γ ▹e Γ' " (at level 80, no associativity).

Inductive Beta_env : Env -> Env -> Prop :=
 | Beta_env_hd : forall A B Γ, A ▹ B -> A::Γ ▹e B::Γ
 | Beta_env_cons : forall A Γ Γ', Γ ▹e Γ' -> A::Γ ▹e A::Γ'
where "Γ ▹e Γ'" := (Beta_env Γ Γ') : SC_scope.


Reserved Notation "Γ ▹▹e Γ' " (at level 80, no associativity).

Inductive Betas_env : Env -> Env -> Prop :=
 | Betas_env_intro : forall Γ Γ', Γ ▹e Γ' -> Γ ▹▹e Γ'
 | Betas_env_refl : forall Γ, Γ ▹▹e Γ
 | Betas_env_trans : forall Γ Γ' Γ'', Γ ▹▹e Γ' -> Γ' ▹▹e Γ'' -> Γ ▹▹e Γ''
where "Γ ▹▹e Γ'" := (Betas_env Γ Γ') : SC_scope.

Hint Constructors Beta_env Betas_env.

Lemma Betas_foo: forall A B , A ▹▹ B -> forall Γ, A::Γ  ▹▹e B::Γ.
induction 1; intros.
trivial.
apply Betas_env_trans with  (t::Γ); intuition.
Qed.

Lemma Betas_env_trans2 : forall Γ Γ',  Γ ▹▹e Γ'-> forall A B,  A ▹▹ B -> A :: Γ ▹▹e B:: Γ'.
assert (forall Γ Γ',  Γ ▹▹e Γ'-> forall A ,   A :: Γ ▹▹e A:: Γ').
induction 1; intros; eauto.
intros.
eapply  Betas_env_trans. apply H. apply H0. apply Betas_foo. trivial.
Qed.

Lemma Betas_env_nil : forall Γ, nil ▹▹e Γ -> Γ = nil.
intros.
remember (@nil Term) as N. revert HeqN.
induction H; intros.
subst. inversion H.
trivial.
replace Γ' with Γ in *.
intuition. intuition.
Qed.

Lemma Betas_env_cons : forall A Γ Γ', A::Γ ▹▹e Γ' -> exists B, exists Γ'', 
  Γ' = B::Γ'' /\ A ▹▹ B /\ Γ ▹▹e Γ''.
intros. remember (A::Γ) as G. revert HeqG. revert Γ. revert A.
induction H; intros; subst.
inversion H; subst; clear H.
exists B; exists Γ0; intuition.
exists A; exists Γ'0; intuition.
exists A; exists Γ0; intuition.
destruct (IHBetas_env1 A Γ0 (refl_equal (A::Γ0))) as (A' & ΓA & ? & ? & ?); subst.
destruct (IHBetas_env2 A' ΓA (refl_equal (A'::ΓA))) as (A'' & ΓB & ?& ? & ?); subst.
exists A''; exists ΓB; eauto.
Qed.


Hint Resolve Betas_env_trans2.



Lemma Beta_env_item_lift : forall Γ Γ' , Γ ▹e Γ'-> forall A v,  A ↓ v ⊂ Γ  ->
  (A ↓ v ⊂ Γ') \/ (exists B, A ▹ B /\ B ↓ v ⊂ Γ').
induction 1; intros.
destruct H0 as (AA & ? & ?). inversion H1; subst; clear H1.
right. exists (B↑ 1 ); split; intuition. exists B; intuition.
left. exists AA; intuition.
(**)
destruct H0 as (AA & ? &?). inversion H1; subst; clear H1.
left.  exists A;intuition.
destruct (IHBeta_env (AA↑(S n)) n). exists AA; intuition.
left. destruct H0 as ( B & ? & ?).
apply inv_lift in H0. exists AA; intuition.
constructor. rewrite H0; trivial.
destruct H0 as ( B & ? & ?).
right. exists (B↑ 1 ); split.
change (S (S n)) with (1+ (S n)). rewrite <- lift_lift. intuition.
destruct H1 as (BB & ? & ?).
exists BB; split. rewrite H1. rewrite lift_lift. trivial.
constructor; trivial.
Qed.

Lemma Betas_env_item_lift : forall Γ Γ' , Γ ▹▹e Γ'-> forall A v,  A ↓ v ⊂ Γ  ->
  (A ↓ v ⊂ Γ') \/ (exists B, A ▹▹ B /\ B ↓ v ⊂ Γ').
induction 1; intros.
destruct (Beta_env_item_lift Γ Γ' H A v H0). left; trivial.
destruct H1 as (B & ? & ?).
right; exists B; intuition.

left; trivial.
destruct (IHBetas_env1 A v H1).
destruct (IHBetas_env2 A v H2).
left; trivial. destruct H3 as (B & ? & ?). right; exists B; intuition.
destruct H2 as (B & ? & ?).
destruct (IHBetas_env2 B v H3).
right; exists B; intuition.
destruct H4 as (B' & ? & ?).
right; exists B'; eauto.
Qed.

Lemma Beta_env_item_lift_up : forall Γ Γ' , Γ' ▹e Γ-> forall A v,  A ↓ v ⊂ Γ  ->
  (A ↓ v ⊂ Γ') \/ (exists B, B ▹ A /\ B ↓ v ⊂ Γ').
induction 1; intros.
destruct H0 as (AA & ? & ?). inversion H1; subst; clear H1.
right. exists (A↑ 1 ); split; intuition. exists A; intuition.
left. exists AA; intuition.
(**)
destruct H0 as (AA & ? &?). inversion H1; subst; clear H1.
left.  exists A;intuition.
destruct (IHBeta_env (AA↑(S n)) n). exists AA; intuition.
left. destruct H0 as ( B & ? & ?).
apply inv_lift in H0. exists AA; intuition.
constructor. rewrite H0; trivial.
destruct H0 as ( B & ? & ?).
right. exists (B↑ 1 ); split.
change (S (S n)) with (1+ (S n)). rewrite <- lift_lift. intuition.
destruct H1 as (BB & ? & ?).
exists BB; split. rewrite H1. rewrite lift_lift. trivial.
constructor; trivial.
Qed.

Lemma Betas_env_item_lift_up : forall Γ Γ' , Γ' ▹▹e Γ-> forall A v,  A ↓ v ⊂ Γ  ->
  (A ↓ v ⊂ Γ') \/ (exists B, B ▹▹ A /\ B ↓ v ⊂ Γ').
induction 1; intros.
destruct (Beta_env_item_lift_up Γ' Γ H A v H0). left; trivial.
destruct H1 as (B & ? & ?).
right; exists B; intuition.

left; trivial.
destruct (IHBetas_env2 A v H1).
destruct (IHBetas_env1 A v H2).
left; trivial. destruct H3 as (B & ? & ?). right; exists B; intuition.
destruct H2 as (B & ? & ?).
destruct (IHBetas_env1 B v H3).
right; exists B; intuition.
destruct H4 as (B' & ? & ?).
right; exists B'; eauto.
Qed.

Theorem TypRed : (forall Γ M F, Γ ⊢ M : F -> forall F', F ▹▹ F' -> Γ ⊢ M : F' ) /\
                 (forall Γ H l F, Γ ; H ⊢ l : F -> forall H'  F' , H ▹▹ H' -> F ▹▹ F' ->  Γ ; H' ⊢ l : F') /\
                 (forall Γ, Γ ⊣ -> True).
apply typ_induc_alt; simpl; intros.
(**)
apply RBx_RT_sort in H0;  subst. eauto.
(**)
apply RBx_RT_sort in H1;  subst. eauto.
(**)
apply RBx_RT_to_Pi in H2. destruct H2 as (C & D & ? & ? & ?). subst.
econstructor. apply r. apply H. trivial. eauto.
eapply H0. eauto. eauto.
eapply H1. trivial.
(**)
econstructor. eapply H. apply RBx_RT_refl. trivial. trivial.
(**)
econstructor. apply t. apply H0. trivial. trivial.
(**)
destruct (RBx_diamond B A F' r0 H1) as (D & ?& ?).
apply typ_conv with D B' s.
apply H. trivial. trivial. eauto. trivial.
(** list **)
destruct (RBx_diamond A H' F' H0 H1) as (D & ? & ?).
apply typ_list_conv_l with D A' s.
apply typ_list_conv_r with D A' s. 
econstructor. apply H. trivial. eauto.
apply H. trivial. eauto.  trivial.
apply H. trivial. eauto. trivial.
(**)
apply RBx_RT_to_Pi in H2. destruct H2 as (C' & D' & ? & ?& ?); subst.
econstructor.  apply H. trivial. eauto.
apply H0. trivial. apply H1. eauto. trivial.
(**)
destruct (RBx_diamond B A H' r0 H1) as ( D & ? & ?).
apply typ_list_conv_l with D B' s. apply H. trivial. trivial. trivial. eauto. trivial.
(**)
destruct (RBx_diamond B C F' r0 H2) as ( D & ? & ?).
apply typ_list_conv_r with D B' s. apply H. trivial. trivial. trivial.
eauto. trivial.
(**)
trivial.
(**)
trivial.
Qed.

Lemma cut4' : (forall Γ t T , Γ  ⊢ t  : T  -> forall Δ P A', Δ  ⊢ P : A' -> 
 forall A A'' s Γ' n , Δ  ⊢ A'' : !s -> A'' ▹▹  A ->  A'' ▹▹ A' -> sub_in_env Δ P A n Γ Γ' -> 
  Γ ⊣  -> Γ' ⊢ t [ n ←P ]  : T [ n ←P ]) .
intros.
destruct TypRed as (? & _).
eapply cut4. apply H.
destruct (RBx_diamond A'' A A' H2 H3) as (B & ?& ?).
apply typ_conv with B A'' s.  apply H6 with A'. apply H0.
trivial. trivial. apply H2. trivial. trivial. apply wf_typ with t T; trivial.
Qed.
Lemma cut2' : (forall Γ C l B , Γ ; C ⊢ l  :B  -> forall Δ P A', Δ  ⊢ P : A' -> 
 forall A A'' s Γ' n , Δ  ⊢ A'' : !s -> A'' ▹▹  A ->  A'' ▹▹ A' -> sub_in_env Δ P A n Γ Γ' -> 
  Γ ⊣  -> Γ' ; C[ n ←P ] ⊢ l [[ n ←P ]]  : B [ n ←P ]).
intros.
destruct TypRed as (? & _ & _).
eapply cut2. apply H.
destruct (RBx_diamond A'' A A' H2 H3) as ( D & ? & ?).
apply typ_conv with D A'' s. apply H6 with A'. apply H0. trivial.
trivial. apply H2. trivial. trivial. trivial.
Qed.

Lemma cut_wf' : (forall Γ , Γ ⊣  -> forall Δ P A', Δ  ⊢ P : A' -> 
 forall A A'' s Γ' n , Δ  ⊢ A'' : !s -> A'' ▹▹  A ->  A'' ▹▹ A' -> sub_in_env Δ P A n Γ Γ' -> 
  Γ' ⊣ ).
intros.
induction H4. apply wf_typ with P A'; trivial.
inversion H; subst; clear H.
apply wf_cons with s0. change !s0 with (!s0 [n ← P]). 
eapply cut4'. apply H6. apply H0. apply H1. apply H2. trivial. trivial. 
apply wf_typ with B !s0; trivial.
Qed.



Lemma cut1 :forall l' Γ  C A , Γ ; C ⊢ l' : A -> forall l B, Γ ;A ⊢l : B -> Γ ; C ⊢ l'@l : B.
induction l'; simpl;intros.
apply Gen2a in H. destruct H as (D & A' & C' & sA & sC & h); decompose [and] h;clear h.
destruct TypRed as ( _ & ? & _).
apply typ_list_conv_l with D C' sC; trivial.
apply H5 with A B. trivial. trivial. trivial.

apply Gen2b in H . destruct H  as (A' & B' & T' & sT & h); decompose [and] h; clear h.
inversion H4; subst; clear H4. 
apply typ_list_conv_l with (Π (A'), B') T' sT; trivial.
apply typ_list_pi with T' sT; trivial. eauto. apply IHl' with A; trivial.
Qed.

Theorem SubRed : (forall Γ M F, Γ ⊢ M : F -> 
                      (forall M', M ▹ M'-> Γ ⊢ M' : F ) /\ (forall Γ', Γ ▹e Γ'-> Γ' ⊢ M : F)) /\
                 (forall Γ H l F, Γ ; H ⊢ l : F -> 
                      (forall l',l ▹' l' ->  Γ ; H ⊢ l' : F) /\ (forall Γ',  Γ ▹e Γ'-> Γ'; H  ⊢ l : F)) /\
                 (forall Γ, Γ ⊣ -> forall Γ', Γ ▹e Γ' -> Γ' ⊣).
apply typ_induc_alt; try split; intros.
(**)
inversion H0.

eauto.
(**)
destruct H; destruct H0.
inversion H1; subst; clear H1.
eauto. econstructor. apply r. intuition. eauto.

destruct H; destruct H0.
eauto.
(**)
destruct H; destruct H0; destruct H1.
inversion H2; subst; clear H2.
eauto.
destruct (RBx_diamond A' B0 A) as (D & ? & ?); intuition.
apply typ_conv with (Π (D), B) (Π (A'), B') s3.
apply typ_la with B' s1 s2 s3; intuition. eauto. eauto. eauto.

destruct H; destruct H0; destruct H1.
econstructor. apply r. eauto. trivial. eauto. trivial. eauto.
(**)
destruct H.
inversion H0; subst; clear H0.
eauto.

destruct H.
destruct (Beta_env_item_lift Γ Γ' H0 A v i).
apply typ_var with A; intuition. destruct H2 as ( Z & ?& ?).
apply typ_var with Z.
assert (exists s, Γ' ⊢ Z: !s).
apply wf_item_lift with v. eapply wf_typ_list. apply H1. trivial. trivial.
destruct H4 as (sZ & ?). destruct TypRed as ( _ & ? & _).
apply H5 with A B. apply H1. trivial. intuition. trivial. trivial.
(**)
destruct H; destruct H0.
inversion H1; subst; clear H1.
(* case : BETA  *)
apply Gen2b in t0 as (Av & Bv & Tv & sv & h); decompose [and] h; clear h.
apply Gen1c in t as (Au & Bu & Bu'' & sA & sB & h); decompose [and] h; clear h.
inversion H7; subst; clear H7.
inversion H6; subst; clear H6.
destruct (RBx_diamond A (Π (Au), Bu) (Π (Av), Bv)) as (P   & ? & ?); trivial.
apply RBx_RT_to_Pi in H6 as (RA & Z' & ? & ?& ?).
apply RBx_RT_to_Pi in H7 as (Z2 & Z2' & ? & ?& ?).
rewrite H7 in H6. injection H6; intros; subst; clear H6.
destruct TypRed as (TR_term & TR_ty & _).
apply typ_app  with (Bu [ ← v]) ; trivial.
apply cut4 with (A0::Γ)  Γ A0. trivial.
apply typ_conv with RA A0 sA; trivial.
apply TR_term with Av; trivial.  eauto. constructor.
apply wf_typ with u Bu ; trivial.

apply typ_list_conv_l with (Z' [ ← v]) (Bu'' [ ← v]) sB.
apply TR_ty with (Bv[ ← v]) B; trivial.  eauto.
change (!sB) with (!sB [ ← v]).
apply cut4 with (A0::Γ)  Γ A0. trivial.
apply typ_conv with RA A0 sA; trivial.
apply TR_term with Av; trivial.  eauto. constructor.
apply wf_typ with u Bu ; trivial. eauto.
eauto.

(* BETA EMPTY LIST, OK *)
apply Gen2a in t0 as (D & PB & PA & sB & sA & h); decompose [and] h; clear h.
destruct TypRed as (? & _).
apply typ_conv with D PB sB. apply H8 with A. trivial. trivial. trivial. trivial. eauto.

apply Gen1e in t. inversion t; subst; clear t.
apply typ_var with A0; trivial.
destruct TypRed as (_ & ? & _). 
apply cut1 with A. trivial. trivial.
intros; intro; discriminate. intros; intro; discriminate. intros; intro; discriminate.

apply Gen1e in t. inversion t; subst; clear t.
apply typ_app with A0 ; trivial.
apply cut1 with A;trivial.
intros; intro; discriminate. intros; intro; discriminate. intros; intro; discriminate.

eauto.

eauto.

destruct H; destruct H0.
eauto.
(** fin app case \o/ **)
destruct H;destruct H0; eauto.

destruct H;destruct H0; eauto.
(** list **)
inversion H0.

destruct H; eauto.
(**)
destruct H; destruct H0; destruct H1.
inversion H2; subst; clear H2.
eauto.

apply typ_list_pi with T s; intuition.
destruct TypRed as (_ & ? & _).
apply H2 with (B [ ← M]) C; trivial. eauto.

eauto.

destruct H; destruct H0; destruct H1.
eauto.
(**)
destruct H; destruct H0.
eauto.

destruct H; destruct H0.
eauto.
(**)
destruct H; destruct H0.
eauto.

destruct H; destruct H0.
eauto.

(** wf **)
inversion H.
(**)
destruct H.
inversion H0; subst; clear H0.
eauto.
eauto.
Qed.

Theorem SubRed_gen : forall Γ M F, Γ ⊢ M : F -> forall M', M ▹▹ M'-> Γ ⊢ M' : F.
intros. induction H0.
trivial.
destruct SubRed.
apply IHRBx_RT.
apply H2 in H.  destruct H. apply H. trivial.  
Qed.


Theorem SubRed_gen2 : forall Γ M F, Γ ⊢ M : F ->  forall Γ', Γ ▹▹e Γ'-> Γ' ⊢ M : F.
intros. induction H0.
destruct SubRed. eapply H1. apply H. trivial.
trivial.
intuition.
Qed.

Theorem SubRed_List_gen : forall Γ H l F, Γ ; H ⊢ l : F -> forall l',l ▹▹' l' ->  Γ ; H ⊢ l' : F.
intros. induction H1.
trivial.
destruct SubRed.
apply IHRBx_RT_List. 
apply H4 in H0. destruct H0. apply H0. trivial.
Qed.

Theorem SubRed_List_gen2 :  forall Γ H l F, Γ ; H ⊢ l : F -> forall Γ',  Γ ▹▹e Γ'-> Γ'; H  ⊢ l : F.
intros. induction H1.
destruct SubRed. eapply H3. apply H0. trivial.
trivial.
intuition.
Qed.
        
Theorem Ctxt_gen : forall Γ, Γ ⊣ -> forall Γ', Γ ▹▹e Γ' -> Γ' ⊣.
intros. induction H0.
destruct SubRed as (_ & _ & ?). eapply  H1. apply H. trivial.
trivial.
intuition.
Qed.


Lemma TypeCorrect : forall Γ t T , Γ ⊢ t : T -> exists s, (T = !s \/ Γ ⊢ T : !s)
 with TypeCorrect_list : forall Γ A l T, Γ ; A ⊢ l : T -> exists s, Γ ⊢ T : !s.
destruct 1.
(**)
exists s2;left;  trivial.
(**)
exists s3; left; trivial.
(**)
exists s3; right.
econstructor. apply H. apply SubRed_gen with A'; trivial.
eapply SubRed_gen2. eapply SubRed_gen. apply H2. trivial. intuition.
(**)
apply TypeCorrect_list in H. destruct H. exists x; right; trivial.
(**)
apply TypeCorrect_list in H0 . destruct H0. exists x; right; trivial.
(**)
exists s; right. eapply SubRed_gen. apply H0. trivial.
(** list **)
destruct 1.
(**)
exists s. eapply SubRed_gen. apply H. trivial.
(**)
eapply TypeCorrect_list. apply H2.
(**)
eapply TypeCorrect_list. apply H.
(**)
exists s. eapply SubRed_gen. apply H0. trivial.
Qed.


Lemma StoupCorrect : forall Γ A l T, Γ ; A ⊢ l : T -> exists s, Γ ⊢ A : !s.
induction 1.
exists s. eapply SubRed_gen. apply H. trivial.
exists s.  eapply SubRed_gen. apply H. trivial.
exists s.  eapply SubRed_gen. apply H0. trivial.
trivial.
Qed.

Lemma typ_conv_1 : forall Γ M A B s, Γ ⊢ M : A -> Γ ⊢ B : !s -> B ▹▹ A -> Γ ⊢ M : B.
intros. eapply typ_conv. apply H. apply H0. trivial. trivial.
Qed.

Lemma typ_conv_2 : forall Γ M A B , Γ ⊢ M : A -> A ▹▹ B -> Γ ⊢ M : B.
intros. eapply TypRed. apply H. trivial.
Qed.

Lemma typ_list_conv_l_1 : forall Γ A l C B s , Γ ; A ⊢ l : C -> Γ ⊢ B : !s -> 
   B ▹▹ A  -> Γ; B ⊢ l : C.
intros. eapply  typ_list_conv_l. apply H. apply H0. trivial. trivial.
Qed.

Lemma typ_list_conv_l_2 : forall Γ A l C B  , Γ ; A ⊢ l : C -> 
   A ▹▹ B  -> Γ; B ⊢ l : C.
intros. eapply TypRed. apply H. trivial. trivial.
Qed.

Lemma typ_list_conv_r_1 : forall Γ A l C B  s , Γ ; A ⊢ l : C -> Γ ⊢ B : !s -> 
  B ▹▹ C  -> Γ; A ⊢ l : B.
intros. eapply typ_list_conv_r. apply H. apply H0. trivial. trivial.
Qed.

Lemma typ_list_conv_r_2 : forall Γ A l C B  , Γ ; A ⊢ l : C -> C ▹▹ B  -> 
 Γ; A ⊢ l : B.
intros. eapply TypRed. apply H. trivial. trivial.
Qed.