Require Import sc_term. 
Require Import sc_red.
Require Import sc_context. 
(*Require Import sc_typ.*)
Require Import Peano_dec.
Require Import Compare_dec.
Require Import Lt.
Require Import Omega.
Require Import List.

Reserved Notation "Γ ⊢ t : T" (at level 80, t, T at level 30, no associativity) .
Reserved Notation "Γ ; A ⊢ l : T" (at level 80, A, l, T at level 30, no associativity) .
Reserved Notation "Γ ⊣ " (at level 80, no associativity).

(* we use sc_typ.Ax & sc_typ.Rel *)
Require Import sc_typ.

Definition Ax := sc_typ.Ax.
Definition Rel := sc_typ.Rel.

Inductive wf : Env -> Prop :=
 | wf_nil : nil ⊣
 | wf_cons : forall Γ A s, Γ ⊢ A : !s ->  A::Γ ⊣ 
where "Γ ⊣" := (wf Γ) : SC_scope_alt 
with typ : Env -> Term -> Term -> Prop :=
 | typ_sort : forall Γ s1 s2, Ax s1 s2 -> Γ ⊣ -> Γ ⊢ !s1 : !s2
 | typ_pi : forall Γ s1 s2 s3 A B, Rel s1 s2 s3 -> Γ ⊢ A : !s1 -> A::Γ ⊢ B : !s2 -> 
   Γ ⊢ Π(A),B : !s3
 | typ_la : forall Γ A A' B B' M s1 s2 s3, Rel s1 s2 s3 -> Γ ⊢ A' : !s1 -> A' ▹▹ A -> 
   A'::Γ ⊢ B' : !s2 -> B' ▹▹ B -> A'::Γ ⊢ M : B -> Γ ⊢ λ[A'],M : Π(A),B
 | typ_var : forall Γ v A B l , Γ;A ⊢ l : B ->  A ↓ v  ⊂ Γ ->  Γ ⊢ v ## l : B
 | typ_app (*cut3*): forall Γ M A B l  ,Γ ⊢ M : A -> Γ ; A ⊢ l : B -> Γ ⊢ M · l : B 
 | typ_conv : forall Γ M A B B' s, Γ ⊢ M : A -> Γ ⊢ B' : !s -> B' ▹▹ B ->  B ▹▹ A ->
  Γ ⊢ M : B
where "Γ ⊢ t : T" := (typ Γ t T) : SC_scope_alt
with typ_list : Env -> Term -> Term_List -> Term -> Prop :=
 | typ_list_ax : forall Γ A A' s , Γ ⊢ A' :!s -> A' ▹▹ A -> Γ ; A ⊢ [[]] : A
 | typ_list_pi : forall Γ A B T s M l C , Γ ⊢ T : !s -> T ▹▹ Π(A),B -> Γ ⊢ M : A -> 
   Γ ;B[ ← M]  ⊢ l : C -> Γ ; Π(A),B ⊢ M ::: l : C

 | typ_list_conv_l : forall Γ A l C B B' s , Γ ; A ⊢ l : C -> Γ ⊢ B' : !s -> B' ▹▹ B -> B ▹▹ A  ->
    Γ; B ⊢ l : C
 | typ_list_conv_r : forall Γ A l C B B' s , Γ ; A ⊢ l : C -> Γ ⊢ B' : !s -> B' ▹▹ B -> B ▹▹ C  ->
    Γ; A ⊢ l : B

where "Γ ; A ⊢ l : T" := (typ_list Γ A l T) : SC_scope_alt.


Delimit Scope SC_alt_scope with SCa. 

Open Scope SC_scope_alt.

Hint Constructors wf typ typ_list.

Scheme typ_ind_alt' := Induction for typ Sort Prop
      with typ_list_ind_alt' := Induction for typ_list Sort Prop
      with wf_ind_alt' := Induction for wf Sort Prop.

Combined Scheme typ_induc_alt from typ_ind_alt', typ_list_ind_alt', wf_ind_alt'.

Lemma wf_typ : forall Γ t T, Γ ⊢ t : T -> Γ ⊣ 
 with wf_typ_list :  forall Γ A t T, Γ; A ⊢ t : T -> Γ ⊣ .
destruct 1; trivial.
eapply wf_typ. apply H0.
eapply wf_typ. apply H0.
eapply wf_typ_list. apply H.
eapply wf_typ; apply H.
eapply wf_typ. apply H.
(** list **)
destruct 1; trivial.
eapply wf_typ. apply H.
eapply wf_typ. apply H.
eapply wf_typ. apply H0.
eapply wf_typ; apply H0.
Qed.



Definition wf_weak := forall Γ, Γ ⊣ -> forall Δ Γ' n A, ins_in_env Δ A n Γ Γ' -> forall s, Δ ⊢ A : !s -> Γ' ⊣.
Definition typ_weak := forall Δ t T, Δ ⊢ t : T -> forall d Γ  n Δ' s,  ins_in_env Γ d n Δ Δ' ->
                 Γ ⊢ d :!s -> Δ' ⊢ t ↑ 1 # n : T ↑ 1 # n.
Definition typ_list_weak := forall Δ A l T, Δ ; A ⊢ l : T -> forall d Γ  n Δ' s,  ins_in_env Γ d n Δ Δ' ->
                 Γ ⊢ d :!s -> Δ' ; A  ↑ 1 # n ⊢ l ↑↑ 1 # n : T ↑ 1 # n.

Lemma weakening : typ_weak /\ typ_list_weak /\ wf_weak.
apply typ_induc_alt;simpl; intros.
(* typ *)
econstructor; eauto.
(**)
apply typ_pi with s1 s2; trivial.
  eauto.  change !s3 with (!s3  ↑ 1 # n); eauto. 
(**)
apply typ_la with  (B' ↑ 1 # (S n))  s1 s2 s3; eauto.
(**)
destruct (le_gt_dec n v). apply typ_var with (A↑ 1 # n).
 eapply H. apply H0. apply H1.
 destruct i as (z & ? & ?). exists z; split.
 rewrite H2; apply liftP3; intuition. eapply ins_item_ge. apply H0. trivial. trivial.
 apply typ_var with (A↑ 1 # n) . eauto. 
 eapply ins_item_lift_lt. apply H0. trivial. trivial.
(**)
apply typ_app  with (A↑ 1 # n)  ; eauto.
(**)
econstructor. eapply H. apply H1. apply H2. eapply H0. apply H1. apply H2. eauto. eauto.
(** list **)
apply typ_list_ax with (A' ↑ 1 # n) s ; eauto.
(**)
apply typ_list_pi with (T↑ 1 # n) s. eauto. eauto. eauto.
destruct substP1 as (? & _). change n with (0+n). rewrite <- H4. simpl. eauto.
(**)
eapply typ_list_conv_l. eapply H. apply H1. apply H2. eapply H0. apply H1. apply H2.
eauto. eauto.
(**)
eapply typ_list_conv_r. eapply H. apply H1. apply H2. eapply H0. apply H1. apply H2.
eauto. eauto.
(* wf *)
inversion H; subst; clear H. apply wf_cons with  s; trivial.
(**)
inversion H0; subst; clear H0.
eauto.
apply wf_cons with s. eapply H. apply H6. apply H1.
Qed.

Theorem thinning :
   forall Γ t T A s,
      Γ ⊢ A : !s ->
      Γ ⊢ t : T ->
   A::Γ ⊢ t ↑ 1 : T ↑ 1.
intros.
destruct weakening as (? & _).
eapply H1.
apply H0. apply ins_O. apply H.
Qed.

Theorem thinning_n : forall n Δ Δ',   Δ ⊣ -> trunc n Δ Δ' ->
   forall t T , Δ' ⊢ t : T  ->  Δ ⊢ t ↑ n : T ↑ n.
induction n; intros.
inversion H0; subst; clear H0.
destruct lift0 as ( ? & _). rewrite 2! H0; trivial.
inversion H0; subst; clear H0.
change (S n) with (1+n).
replace (t ↑ (1+n)) with ((t ↑ n )↑ 1) by (apply lift_lift).
replace (T ↑ (1+n)) with ((T ↑ n) ↑ 1) by (apply lift_lift).
inversion H; subst; clear H.
eapply thinning ; trivial. apply H2.
eapply IHn. eapply wf_typ. apply H2. apply H3. trivial.
Qed.

Definition ccut4 := forall Γ t T , Γ  ⊢ t  : T  -> forall Δ P A, Δ  ⊢ P : A -> 
 forall Γ' n, sub_in_env Δ P A n Γ Γ' -> Γ ⊣  -> Γ' ⊢ t [ n ←P ]  : T [ n ←P ].
Definition ccut2 := forall Γ B l C, Γ ; B  ⊢ l  : C  -> forall Δ P A, Δ  ⊢ P : A -> 
 forall Γ' n , sub_in_env Δ P A n Γ Γ' -> Γ ⊣  -> Γ'; B[ n ←P]  ⊢ l [[ n ←P ]]  : C [ n ←P ].
Definition ccut_wf := forall Γ ,  Γ ⊣ -> forall Δ P A n Γ' , Δ ⊢ P : A -> 
  sub_in_env  Δ P A n Γ Γ' ->     Γ' ⊣ .

Lemma sub_trunc : forall Γ0 a A n Γ Δ, sub_in_env Γ0 a A n Γ Δ -> trunc n Δ Γ0.
induction 1.
apply trunc_O.
apply trunc_S. trivial.
Qed.


Lemma wf_item : forall Γ A n, A ↓ n ∈ Γ ->
   forall  Γ', Γ ⊣ ->  trunc (S n) Γ Γ' -> exists s, Γ' ⊢ A : !s.
induction 1; intros.
inversion H0; subst; clear H0.
inversion H5; subst; clear H5.
inversion H; subst.
exists s; trivial.
inversion H1; subst; clear H1.
inversion H0; subst.
apply IHitem; trivial. eapply wf_typ. apply H2.
Qed.

Lemma wf_item_lift : forall Γ t n ,Γ ⊣  -> t ↓ n ⊂ Γ ->
  exists s,  Γ ⊢ t  : !s.
intros.
destruct H0 as (u & ? & ?).
subst.
assert (exists Γ' , trunc (S n) Γ Γ') by (apply item_trunc with u; trivial).
destruct H0 as (Γ' & ?).
eapply wf_item in H1.
destruct H1.
apply (@thinning_n (S n) Γ Γ' H) in H1.
exists x. simpl in H1. trivial.
trivial.
trivial.
trivial.
Qed.

Lemma trunc_sub : forall Δ P A n Γ Γ', sub_in_env Δ P A n Γ Γ' -> trunc (S n) Γ Δ.
induction 1. constructor. constructor.
constructor. trivial.
Qed.


Lemma substitution : ccut4 /\ ccut2 /\ ccut_wf.
apply typ_induc_alt; simpl; intros.
(* typ *)
apply typ_sort ;eauto.
(**)
apply typ_pi with s1 s2; eauto.
(**)
apply typ_la with  (B'[S n ← P]) s1 s2 s3; eauto.
(**)
destruct (lt_eq_lt_dec v n). destruct s.
apply typ_var with (A[n ← P])  . eauto. eapply nth_sub_item_inf. apply H1. intuition. trivial.
destruct i as (z & ?& ?).
destruct (wf_item Γ z v H4 Δ H2). subst.
eapply trunc_sub. apply H1.
apply typ_app with (A[n ← P]).
subst. destruct substP3 as (? &_ ). rewrite H3; intuition.
rewrite <- (nth_sub_eq H1 H4).
eapply thinning_n.
eapply wf_typ_list.  eapply H. apply H0. apply H1. trivial.
eapply sub_trunc. apply H1. trivial. 
eauto. 
apply typ_var with A[n ← P] . eauto.
destruct i as ( z & ? &?). rewrite H3. destruct substP3 as (  ? & _). rewrite H5; intuition.
exists z; intuition.
rewrite <- pred_of_minus.
rewrite <- (S_pred v n l0). reflexivity.
eapply nth_sub_sup. apply H1. intuition.
rewrite <- pred_of_minus.
rewrite <- (S_pred v n l0). trivial.
(**)
apply typ_app with A[n ← P] . eauto. eauto.
(**)
econstructor. eapply H. apply H1. trivial. trivial. eapply H0. apply H1. apply H2.
trivial. eauto. eauto.
(* list *)
apply typ_list_ax with (A' [n ← P]) s ; eauto.
(**)
apply typ_list_pi with  (T[n ← P]) s; eauto.
destruct (subst_travers) as ( ? & _). replace (S n) with (n+1) by intuition.
rewrite <- H5. eauto.
(**)
eapply typ_list_conv_l. eapply H. apply H1. trivial. trivial. eapply H0. apply H1.
apply H2. trivial. eauto. eauto.
(**)
eapply typ_list_conv_r. eapply H. apply H1. trivial. trivial. eapply H0. apply H1.
apply H2. trivial. eauto. eauto.
(* wf *)
inversion H0.
(**)
inversion H1; subst; clear H1. 
eapply wf_typ. apply H0.
apply wf_cons with s. eapply H. apply H0. trivial. eapply wf_typ. apply t.
Qed.



Lemma cut4 : forall Γ t T , Γ  ⊢ t  : T  -> forall Δ P A, Δ  ⊢ P : A -> 
 forall Γ' n , sub_in_env Δ P A n Γ Γ' -> Γ ⊣  -> Γ' ⊢ t [ n ←P ]  : T [ n ←P ].
destruct substitution as (H & _); exact H.
Qed.

Lemma cut2 : forall Γ B l C, Γ ; B  ⊢ l  : C  -> forall Δ P A, Δ  ⊢ P : A -> 
 forall Γ' n , sub_in_env Δ P A n Γ Γ' -> Γ ⊣  -> Γ'; B[ n ←P]  ⊢ l [[ n ←P ]]  : C [ n ←P ].
destruct substitution as ( _ & H & _); exact H.
Qed.

Lemma cut_wf : forall Γ ,  Γ ⊣ -> forall Δ P A n Γ' , Δ ⊢ P : A -> 
  sub_in_env  Δ P A n Γ Γ' ->     Γ' ⊣ .
destruct substitution as ( _ & _ & ?); exact H.
Qed.




(* same judgment but last rule is not conv rule *)
Reserved Notation "Γ ⊢' t : T" (at level 80, t, T at level 30, no associativity) .
Reserved Notation "Γ ; A ⊢' l : T" (at level 80, A, l, T at level 30, no associativity) .

Inductive typ' : Env -> Term -> Term -> Prop :=
 | typ'_sort : forall Γ s1 s2, Ax s1 s2 -> Γ ⊣  -> Γ ⊢' !s1 : !s2
 | typ'_pi : forall Γ s1 s2 s3 A B, Rel s1 s2 s3 ->
    Γ ⊢ A : !s1 -> A::Γ ⊢ B : !s2 -> Γ ⊢' Π(A),B : !s3
 | typ'_la : forall Γ A A' B B' M s1 s2 s3, Rel s1 s2 s3 -> 
   Γ ⊢ A':!s1 -> A' ▹▹ A -> A'::Γ ⊢ B' : !s2 -> B' ▹▹ B -> A'::Γ ⊢ M : B ->
    Γ ⊢' λ[A'],M : Π(A),B
 | typ'_var : forall Γ v A  B l, Γ;A ⊢ l : B ->  A ↓ v  ⊂ Γ -> Γ ⊢' v ## l : B
 | typ'_app (*cut3*): forall Γ M A B l , Γ ⊢ M : A -> Γ ; A ⊢ l : B -> Γ ⊢' M · l : B
where "Γ ⊢' t : T" := (typ' Γ t T) : SC_scope_alt.


Inductive typ'_list : Env -> Term -> Term_List -> Term -> Prop :=
 | typ'_list_ax : forall Γ A A' s, Γ ⊢ A' :!s -> A' ▹▹ A -> Γ ; A ⊢' [[]] : A
 | typ'_list_pi : forall Γ A B s T M l C, Γ ⊢ T : !s -> T ▹▹ Π(A),B -> Γ ⊢ M : A -> 
   Γ ;B[ ← M]  ⊢ l : C -> Γ ; Π(A),B ⊢' M ::: l : C
where "Γ ; A ⊢' l : T" := (typ'_list Γ A l T): SC_scope_alt.

Lemma typ'_typ : forall Γ t T, Γ ⊢' t : T -> Γ ⊢ t : T.
induction 1; intros; simpl in *; eauto.
Qed.

Lemma typ'_list_typ_list : forall Γ C l A, Γ ; C ⊢' l : A -> Γ; C ⊢ l : A.
induction 1; intros; simpl in *; eauto.
Qed.

Hint Constructors typ' typ'_list.
Hint Resolve typ'_typ typ'_list_typ_list.

Lemma Gen1b: forall  Γ A B T, Γ ⊢ Π ( A ), B : T -> exists s1, exists s2, exists s3, Rel s1 s2 s3 /\
 Γ ⊢' Π ( A ), B : !s3 /\ Γ ⊢ A : !s1 /\ A::Γ ⊢ B : !s2 /\ T  ▹▹  !s3.
intros.
remember ( Π ( A ), B) as P; induction H; subst; try discriminate.
injection HeqP; intros; subst; clear HeqP IHtyp1 IHtyp2.
exists s1; exists s2; exists s3; intuition. econstructor. apply H. trivial. trivial.
destruct IHtyp1 as (s1 & s2 & s3 & h). trivial. decompose [and] h; clear h.
exists s1; exists s2; exists s3; intuition.
eauto.
Qed.


Lemma Gen1c: forall  Γ A b T, Γ ⊢ λ[ A ], b : T -> exists A',  exists B, exists B'', exists sA, exists sB, 
  Γ ⊢' λ[A],b : Π ( A' ), B /\ T  ▹▹  Π ( A' ), B /\ A ▹▹ A' /\ B'' ▹▹ B /\ Γ ⊢ A : !sA /\ A::Γ ⊢ B'' : !sB.
intros. remember ( λ[ A ], b) as L;  induction H; subst; try discriminate.
injection HeqL; intros; subst; clear HeqL. clear IHtyp1 IHtyp2 IHtyp3.
exists A0; exists B; exists B'; exists s1; exists s2; intuition. eauto.
destruct IHtyp1 as (A' & B0' & B0'' & sA & sB &h); intuition.
clear IHtyp2.
exists A'; exists B0'; exists B0''; exists sA; exists sB; intuition.
eauto.
Qed.


Lemma Gen1a : forall  Γ s T,  Γ ⊢ !s : T -> exists t,  Γ ⊢' !s : !t /\ T  ▹▹  !t.
intros.
remember !s as S; induction H; subst; try discriminate.
injection HeqS; intros; subst; clear HeqS. exists s2; intuition.
destruct IHtyp1; intuition.
exists x; eauto.
Qed.

Lemma Gen2a: forall Γ C A , Γ; C ⊢ [[]] : A -> exists D, exists A', exists C', exists sa, exists sc,
   Γ ⊢ A' : !sa /\ Γ ⊢ C' : !sc /\ A' ▹▹ A /\ C' ▹▹ C /\ A ▹▹ D /\ C ▹▹ D.
intros.
remember [[]] as L; induction H; subst; try discriminate.
exists A; exists A'; exists A'; exists s; exists s; intuition.

destruct (IHtyp_list (refl_equal [[]])) as (D & C' & A' & sC & sA & h); decompose [and] h; clear h.
exists D; exists C';exists B'; exists sC; exists s; intuition. eauto.
destruct (IHtyp_list (refl_equal [[]])) as (D & C' & A' & sC & sA & h); decompose [and] h; clear h.
exists D; exists B'; exists A'; exists s; exists sA; intuition. eauto.
Qed.


Lemma Gen2b: forall Γ C D M l , Γ; D ⊢ M :::l : C -> exists A, exists B, exists T, exists s, 
    T ▹▹ D /\ D ▹▹ Π(A),B  /\ Γ ⊢ T : !s /\ Γ; Π(A),B ⊢' M :::l : C.
intros.
remember (M:::l) as L; induction H; subst; try discriminate.
injection HeqL; intros; subst; clear HeqL. 
 clear IHtyp_list. exists A; exists B; exists T; exists s; intuition; eauto.

 destruct (IHtyp_list (refl_equal (M:::l))) as (A1 & B1 & T1 & s1  & ? ); clear IHtyp_list.
 exists A1; exists B1; exists B'; exists s; intuition; eauto.

 destruct (IHtyp_list (refl_equal (M:::l))) as (A1 & B1 & T1 & s1 & h); clear IHtyp_list.
 decompose [and] h; clear h.
 exists A1; exists B1; exists T1; exists s1; intuition.
inversion H7; subst; clear H7. eauto.
Qed.



(* seems useless since we inlined subst, same as above for var & app *)
Lemma Gen1e: forall M Γ T, Γ ⊢ M : T -> 
   (forall s, M <> !s) -> (forall A B, M <> Π(A),B) ->
   (forall A b, M <> λ[A],b) -> Γ ⊢' M : T.
induction 1; intros.
 elim(H1 s1); trivial.
 elim (H3 A B); trivial.
 elim (H7 A' M); trivial.
 eauto.
 eauto.
 assert (Γ ⊢' M : A). apply IHtyp1; trivial.
 inversion H6; subst; clear H6.
  elim (H3 s1); trivial.
  elim (H4 A0 B0); trivial.
  elim (H5 A' M0); trivial.
  eauto.
  eauto. 
Qed. 


Lemma sub_in_env_item : forall Δ P A n Γ Γ', sub_in_env Δ P A n Γ Γ' -> A ↓ n ∈ Γ.
induction 1; eauto.
Qed.