Require Import sc_term. 
Require Import sc_red.
Require Import sc_context. 
Require Import sc_typ.
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.

Hint Constructors Beta_env.

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




Theorem SubRed_in_ctxt : (forall Γ M F, Γ ⊢ M : F -> forall Γ',  Γ' ⊣ -> Γ ▹e Γ'-> Γ' ⊢ M : F) /\
 (forall Γ C l D , Γ ; C ⊢ l : D -> forall Γ',  Γ' ⊣ -> Γ ▹e Γ'-> Γ'; C  ⊢ l : D) /\
 (forall Γ , Γ ⊣ -> True).
apply typ_induc; simpl; intros; trivial.
(**)
eauto.
(**)
econstructor; eauto.
(**)
econstructor; eauto. apply H0.
destruct (Gen1b Γ' A B !s)as (s1 &s2 & s3 & h); intuition. apply wf_cons with s1; trivial. intuition.
(**)
destruct (Beta_env_item_lift Γ Γ' H1 A v i).
apply typ_var with A. apply H ; trivial. trivial.
destruct H2 as (AA & ? & ?). 
apply typ_var with AA.
assert (exists s, Γ' ⊢ AA: !s).
apply wf_item_lift with v. eapply wf_typ_list. apply H. trivial. trivial. trivial.
destruct H4 as (sA & ?).  eapply typ_list_conv_l.  apply H ; trivial. apply H4. eauto. trivial.
(**)
eauto.
(**)
eauto.
(* list *)
eauto.
(**) eauto.
(**) eauto.
(**) eauto.
Qed.

Theorem SubRed : (forall Γ M F, Γ ⊢ M : F -> forall M', M ▹ M'-> Γ ⊢ M' : F ) /\
                 (forall Γ H l F, Γ ; H ⊢ l : F -> forall l',l ▹' l' ->  Γ ; H ⊢ l' : F) /\ 
                 (forall Γ, Γ ⊣ -> True).
destruct SubRed_in_ctxt as (S1 & S2 & _).
apply typ_induc; try split; intros.
(**)
inversion H0.
(**)
inversion H1; subst; clear H1.
eauto. econstructor. apply r. intuition. eauto.
(**)
inversion H1; subst; clear H1.
eauto. econstructor. econstructor.
apply H. eauto. eapply S1. apply t0.
destruct (Gen1b Γ B0 B !s)as (s1 &s2 & s3 & h); intuition. apply wf_cons with s1; trivial. intuition.
apply t. eauto.
(**)
inversion H0; subst; clear H0. eauto.
(**)
inversion H1; subst; clear H1.
 apply Gen1c in t. destruct t as (B0 & ? & ? & ?).
 apply Gen2b in t0. destruct t0 as (A1 & B1 & h); decompose [and] h; clear h.
 assert (exists s, Γ ⊢ A0: !s).
 apply wf_typ in H3. destruct H3. apply wf_inv in H3. intuition. destruct H7 as (sA & ?).
 assert (exists s, A0::Γ ⊢ B0: !s).
 inversion H1; subst; clear H1. apply Gen1b in H13. destruct H13 as (s1 & s2 & s3 & h); decompose [and] h; clear h.
 exists s2; trivial. destruct H9 as (sB & ?). 
 destruct (RBx_RST_to_Pi A0 B0 A1 B1). eauto.
 apply typ_app with (B0[ ← v]). apply cut4 with (A0::Γ) Γ A0; trivial.
 apply typ_conv with A1 sA; trivial. intuition. eauto.
 apply typ_list_conv_l with (B1 [ ← v]) sB; trivial.
 change !sB with !sB[ ← v]. apply cut4 with (A0::Γ) Γ A0; trivial.
 apply typ_conv with A1 sA; trivial. intuition. eauto. 
 apply RBx_RST_subst. intuition.
  
 assert (exists s, Γ ⊢ B : !s). apply TypeCorrect_list in t0. trivial.  destruct H1 as (sB & ?).
 apply Gen2a in t0.
 apply typ_conv with A sB; trivial. intuition.

 apply Gen1e in t. inversion t; subst; clear t.
 apply typ_var with A0; trivial. apply cut1 with A; 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.
(**)
eauto.
(* list *)
inversion H0.
(**)
inversion H2; subst; clear H2. econstructor. apply t. eauto. 
assert (exists s, A::Γ ⊢ B : !s). apply Gen1b in t. destruct t as (s1 & s2 &s3 & h); decompose [and] h; exists s2; trivial.
destruct H2 as (sB & ?).
apply typ_list_conv_l with( B [ ← M]) sB; trivial. 
change !sB with !sB[ ← t']. eapply substitution. apply H2. apply H0. trivial. constructor.
eapply wf_typ. apply H2.  apply RBx_RST_subst2. eauto.
econstructor. apply t. trivial. apply H1. trivial.
(**)
eauto.
(**)
eauto.
Qed.


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

Theorem TypRed_gen : forall Γ M F, Γ ⊢ M : F -> forall F', F ▹▹ F'-> Γ ⊢ M : F'.
intros.
destruct (TypeCorrect Γ M F H). destruct H1; subst.
apply RBx_RT_sort in H0; subst; trivial.
apply typ_conv with F x; eauto.
apply SubRed_gen with F; trivial.
Qed.


Theorem CtxtRed : forall Γ, Γ ⊣  -> forall Γ',  Γ ▹e  Γ'  -> Γ' ⊣ .
induction  Γ ; intros.
(**)
inversion H0.
(**)
inversion H; subst; clear H.
inversion H0; subst; clear H0.
apply wf_cons with s. apply SubRed with a; trivial.
destruct SubRed_in_ctxt.
apply wf_cons with s. eapply H. apply H2.
apply IHΓ. eapply wf_typ. apply H2. trivial. trivial.
Qed.

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



Theorem CtxtRed_gen : forall Γ, Γ ⊣  -> forall Γ',  Γ ▹▹e  Γ'  -> Γ' ⊣ .
intros. induction H0.
apply CtxtRed in H0; trivial.
trivial.
intuition.
Qed.

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