Require Import sc_term. 
Require Import sc_red.
Require Import sc_context. 
Require Import Peano_dec.
Require Import Compare_dec.
Require Import Lt.
Require Import Omega.
Require Import List.
Require Import sc_typ sc_sr.
Require Import sc_typ_alt sc_sr_alt.
Require Import sc_glue.


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


Definition proviso A := forall s, A = !s -> exists t, Ax s t.

(*Inductive wf_ti : Env -> Prop :=
 | wf_ti_nil : nil ⊣ti
 | wf_ti_cons : forall Γ A s, Γ ⊢ A : !s -> A::Γ ⊣ti
where "Γ ⊣ti" := (wf_ti Γ) : SC_ti_scope*)
Inductive typ_ti : Env -> Term -> Term -> Prop :=
 | typ_ti_sort : forall Γ s1 s2, Ax s1 s2 -> Γ ⊢ !s1 : !s2
 | typ_ti_pi : forall Γ s1 s2 s3 A B Ta Tb, Rel s1 s2 s3 ->
    Γ ⊢ A : Ta -> Ta ▹▹ !s1 -> A::Γ ⊢ B : Tb -> Tb ▹▹ !s2 -> Γ ⊢ Π(A),B : !s3
 | typ_ti_la : forall Γ A A' B B' M Tm s, Γ ⊢ Π(A'),B' : !s -> A'::Γ ⊢ M : Tm ->
  Tm ▹▹ B -> A' ▹▹ A -> B' ▹▹ B -> Γ ⊢ λ[A'],M : Π(A),B
 | typ_ti_var : forall Γ v A B l, Γ;A ⊢ l : B ->  A ↓ v  ⊂ Γ -> 
   Γ ⊢ v ## l : B
 | typ_ti_app (*cut3*): forall Γ M A B l, proviso A -> Γ ⊢ M : A -> Γ ; A ⊢ l : B ->
    Γ ⊢ M · l : B
where "Γ ⊢ t : T" := (typ_ti Γ t T) : SC_ti_scope
with typ_ti_list : Env -> Term -> Term_List -> Term -> Prop :=
 | typ_ti_list_ax : forall Γ A, Γ ; A ⊢ [[]] : A
 | typ_ti_list_pi : forall Γ A B M Tm l C, Γ ⊢ M : Tm -> Tm ▹▹ A -> 
   Γ ;B[ ← M]  ⊢ l : C -> Γ ; Π(A),B ⊢ M ::: l : C
 | typ_ti_list_exp : forall Γ A l C B , Γ ; A ⊢ l : B -> C ▹▹ A ->
    Γ; C ⊢ l : B
where "Γ ; A ⊢ l : T" := (typ_ti_list Γ A l T) : SC_ti_scope.

Hint Constructors typ_ti typ_ti_list.

Scheme typ_ti_ind' := Induction for typ_ti Sort Prop
      with typ_ti_list_ind' := Induction for typ_ti_list Sort Prop.

Combined Scheme typ_ti_induc from typ_ti_ind', typ_ti_list_ind'.

Open Scope SC_ti_scope.

Lemma soundness : (forall Γ M T, Γ ⊢ M : T -> (Γ ⊣)%SC -> (Γ ⊢ M : T)%SC) /\
 (forall Γ A l B, Γ ; A ⊢ l : B -> forall s, (Γ ⊢ A : !s)%SC -> (Γ; A ⊢ l : B)%SC).
apply typ_ti_induc; intros; simpl in *.
eauto.
(**)
econstructor. apply r. eapply TypRed_gen. apply  H. trivial. trivial.
eapply TypRed_gen. apply H0. econstructor. eapply TypRed_gen. apply H. trivial. 
apply r0. trivial.
(**)
econstructor. econstructor. apply H. trivial. eapply TypRed_gen.
apply sc_typ.Gen1b in H. destruct H as (s1 & s2 & s3 & h); decompose [and] h; clear h.
eapply sc_typ.typ_conv. apply H0. econstructor. apply H2. apply H4. eauto. trivial. intuition.
eapply sc_sr.SubRed_gen. apply H. trivial. intuition. intuition.
(**)
destruct (sc_typ.wf_item_lift Γ A v H0 i) as (s & ?). econstructor. eapply H. apply H1.
trivial.
(**)
econstructor. apply H. trivial. apply sc_typ.wf_typ in H. destruct H as ( ? & s & ?).
destruct H2. unfold proviso in p. destruct (p s H2) as (s' & ?).
eapply H0. rewrite H2. constructor. apply H3. trivial. eapply H0. apply H2. trivial.
(** list **)
econstructor. apply H.
(**)
econstructor. apply H1. eapply TypRed_gen. apply H. apply sc_typ.wf_typ in H1 as ( ? & _ ); trivial. trivial.
apply sc_typ.Gen1b in H1 as (s1 & s2 & s3 & h); decompose [and] h; clear h.
apply H0 with s2. change !s2 with !s2[← M]. eapply sc_typ.substitution. apply H4. eapply TypRed_gen.
apply H. apply sc_typ.wf_typ in H2 as (? & _ ); trivial. apply r. intuition.
apply sc_typ.wf_typ in H4 as ( ? & _ ); trivial.
(**)
eapply sc_typ.typ_list_conv_l. eapply H. eapply sc_sr.SubRed_gen. apply H0. trivial. apply H0. 
intuition.
Qed.



Lemma completeness_ep : (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 Γ -> True).
apply typ_induc_ep; intros; simpl in *; eauto.

assert (proviso A). unfold proviso; intros.
apply StoupCorrect_ep in t0. destruct t0.
subst. inversion H2; subst; clear H2. exists x; trivial.
eauto.
Qed.



Lemma completeness : (forall Γ M T, (Γ ⊢ M : T)%SC -> exists T', Γ ⊢ M : T' /\ T ▹▹ T') /\
 (forall Γ A l B, (Γ ; A ⊢ l : B)%SC -> exists B', Γ; A ⊢ l : B' /\ B ▹▹ B') /\
 (forall Γ , (Γ ⊣)%SC -> True).
split. intros.
apply Left2Right in H. apply postpone in H. destruct H as ( T' & ? & ?).
apply completeness_ep in H. exists T'; intuition.

split. intros.
apply Left2Right in H. apply postpone in H. destruct H as ( B'' & B' & s & h); decompose [and] h; clear h.
apply completeness_ep in H3. exists B'; intuition.

intros; trivial.
Qed.