Require Import dn_term.
Require Import dn_red.
Require Import dn_context.
Require Import List.
Require Import Peano_dec.
Require Import Compare_dec.
Require Import Lt.
Require Import Omega.
Require Import dn_typ.
Require Import dn_sr.

(* Axiom and Relation part of our PTS are kept unknown, it is not usefull for now *)
Definition Ax := dn_typ.Ax.
Definition Rel := dn_typ.Rel.

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

Inductive wf : Env -> Prop :=
 | wf_nil : nil ⊣
 | wf_cons : forall Γ A s, Γ ⊢ A : !s ->  A::Γ ⊣
where "Γ ⊣" := (wf Γ) : DN_scope_alt
with typ : Env -> Term -> Term -> Prop :=
 | cSort : forall Γ s t, Ax s t -> Γ ⊣ -> Γ  ⊢ !s : !t
 | cVar : forall  Γ A v,  Γ ⊣ ->  A ↓ v  ⊂ Γ ->  Γ ⊢ #v : A 
 | cPi : forall Γ A B s t u, 
     Rel s t u -> Γ ⊢ A : !s -> A::Γ ⊢ B : !t -> Γ ⊢  Π(A), B : !u 
 | cLa : forall Γ A b B B' s t u, Rel s t u ->
   Γ ⊢ A : !s -> A::Γ ⊢ B' : !t -> A::Γ ⊢ b : B -> B' →→ B -> Γ ⊢ λ[A], b: Π(A), B
 | cApp : forall Γ a b A B , Γ ⊢ a : Π(A), B -> Γ ⊢ b :  A -> Γ ⊢ a·b : B[←b]
 | Cnv : forall Γ a A B ,
      Γ ⊢ a : A -> A →→ B -> Γ ⊢ a : B
where "Γ ⊢ t : T" := (typ Γ t T) : DN_scope_alt.

Hint Constructors wf typ.

Scheme typ_ind' := Induction for typ Sort Prop
      with wf_ind' := Induction for wf Sort Prop.

Combined Scheme typ_induc from typ_ind', wf_ind'.

Open Scope DN_scope_alt.

Lemma wf_typ : forall Γ t T, Γ ⊢ t : T -> Γ ⊣.
induction 1; eauto.
Qed.

Hint Resolve wf_typ.

(* Weakening / Thining Lemma *)
(* if we insert something in the context , we have to lift our judgment *)
Theorem weakening: (forall Δ t T, Δ ⊢ t : T -> forall Γ d s n Δ', ins_in_env Γ d n Δ Δ' ->   Γ ⊢ d :!s -> 
                 Δ' ⊢ t ↑ 1 # n : T ↑ 1 # n ) /\
(forall Γ, Γ ⊣ -> forall Δ Γ' n A , ins_in_env Δ A n Γ Γ' -> forall s, Δ ⊢ A : !s -> Γ' ⊣).
apply typ_induc; simpl in *; intros.
(*1*)
eauto.
(*2*)
destruct (le_gt_dec n v).
eapply cVar.  eapply H. apply H0. apply H1. destruct i as (AA & ?& ?). 
exists AA; split. rewrite H2. change (S (S v)) with (1+ S v).
rewrite liftP3; intuition. eapply ins_item_ge. apply H0. trivial. trivial.
eapply cVar . eapply H. apply H0.  apply H1. eapply ins_item_lift_lt. apply H0. trivial. trivial.
(*3*)
econstructor. apply r. eauto. eauto.
(*4*)
econstructor. apply r. eauto. eauto. eauto. eauto.
(*5*)
change n with (0+n). rewrite substP1. simpl.
eapply cApp. eapply H; eauto. eauto.
(*6*)
apply Cnv with (A↑ 1 # n) ; intuition. eauto.
(** wf **)
inversion H; subst; clear H.
apply wf_cons with  s; trivial.
(**)
inversion  H0; subst; clear H0.
apply wf_cons with s0; trivial. 
apply wf_cons with s; trivial.
eapply H.  apply H6. apply H1.
Qed.


Theorem thinning :
   forall Γ t T A s,  
      Γ ⊢ t : T ->  Γ ⊢ A : !s ->
   A::Γ ⊢ t ↑ 1 : T ↑ 1.
intros.
destruct weakening.
eapply H1. apply H. constructor. apply H0.
Qed.

Theorem thinning_n : forall n Δ Δ',
   trunc n Δ Δ' ->
   forall t T , Δ' ⊢ t : T  -> Δ ⊣ ->
               Δ ⊢ t ↑ n : T ↑ n.
intro n; induction n; intros.
inversion H; subst; clear H.
rewrite 2! lift0; trivial.
inversion H; subst; clear H.
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 H1; subst; clear H1.
apply thinning with s; trivial.
eapply IHn. apply H3. trivial. eauto.
Qed.

Definition typ_subst := 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 wf_subst := 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.


Theorem substitution : typ_subst /\ wf_subst.
apply typ_induc; simpl; intros.
(*1*)
eauto.
(*2*)
destruct (lt_eq_lt_dec v n). destruct s.
eapply cVar . eapply H. apply H0. apply H1. eapply nth_sub_item_inf. apply H1. intuition. trivial.
destruct i as (AA & ?& ?).
subst. rewrite substP3; intuition. 
rewrite <- (nth_sub_eq H1 H4).
eapply thinning_n.
eapply sub_trunc. apply H1. trivial. eauto.
eapply cVar.  eapply H. apply H0. apply H1.
destruct i as (AA & ? &?). subst.  rewrite substP3; intuition.
exists AA; split. replace (S (v-1)) with v by intuition. trivial.
eapply nth_sub_sup. apply H1. intuition.
rewrite <- pred_of_minus.
rewrite <- (S_pred v n l). trivial.
(*4*)
econstructor. apply r. eauto. eapply H0. apply H1. constructor; apply H2. eauto.
(*5*)
econstructor. apply r. eauto. eapply H0. apply H2. constructor; apply H3. eauto.
eauto. eauto.
(*6*)
rewrite subst_travers.
eapply cApp.
replace (n+1) with (S n) by intuition. eapply H. apply H1. trivial. trivial.
eauto.
(*7*)
econstructor. eapply H. apply H0. trivial. trivial. eauto.
(** wf **)
inversion H0.
(**)
inversion H1; subst; clear H1. eauto.
econstructor. eapply H. apply H0. trivial. eauto. 
Qed.


Lemma dn_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. eauto. 
Qed.

Lemma dn_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 (Γ' & ?).
destruct (dn_wf_item Γ u n H1 Γ' H H0) as (t &  ?).
exists t. change !t with (!t ↑(S n)).
eapply thinning_n. apply H0. trivial. trivial.
Qed.

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.


Reserved Notation "Γ ⊢' t : T" (at level 80, t, 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 b B B' s t u, Rel s t u -> Γ ⊢ A : !s -> A::Γ ⊢ B' : !t -> A::Γ ⊢ b : B ->
  B' →→ B -> Γ ⊢' λ[A], b: Π(A), B
 | typ'_var : forall  Γ A v, Γ ⊣ -> A ↓ v  ⊂ Γ ->  Γ ⊢' #v : A 
 | typ'_app : forall Γ a b A B , Γ ⊢ a : Π(A), B -> Γ ⊢ b :  A -> Γ ⊢' a·b : B[←b]
where "Γ ⊢' t : T" := (typ' Γ t T) : DN_scope_alt.

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


Hint Constructors typ' .
Hint Resolve typ'_typ.

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 s; exists t; exists u; intuition. econstructor. apply H. trivial. trivial.
destruct IHtyp as (s1 & s2 & s3 & h). trivial. decompose [and] h; clear h.
exists s1; exists s2; exists s3; intuition.
rewrite H6 in H0.
apply Betas_S in H0; subst. trivial.
Qed.


Lemma Gen1c: forall  Γ A b T, Γ ⊢ λ[ A ], b : T -> exists A',  exists B, exists B', exists B'', exists sA, exists sB, 
  Γ ⊢' λ[A],b : Π ( A ), B /\  T = Π ( A' ), B' /\ A →→ A' /\  B'' →→ B /\ 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 A; exists B; exists B; exists B';  exists s; exists t; intuition. eauto.
destruct IHtyp as (A' & B0 & B0' & B0'' & sA & sB &h); intuition. subst.
apply Betas_Pi_inv in H0 as (K & L & -> & ? & ?).
exists K; exists B0; exists L; exists B0''; exists sA; exists sB; intuition.
eauto. eauto.
Qed.


Lemma Betas_env_item_lift : forall Γ Γ' , Γ →→e Γ'-> forall A v,  A ↓ v ⊂ Γ  -> 
  exists B, A →→ B /\ B ↓ v ⊂ Γ'.
induction 1; intros.
exists A; intuition.

destruct (Beta_env_item_lift e f H A v H0) .
exists A; intuition. destruct H1 as (B & ? & ?); exists B; intuition.

destruct (IHBetas_env1 A v H1) as (B & ? & ?).
destruct (IHBetas_env2 B v H3) as (C & ?& ?).
exists C; split; trivial. eauto.
Qed.

Definition typ_subst2 := forall Γ t T , Γ  ⊢ t  : T  -> forall Δ P A, Δ  ⊢ P : A -> 
 forall Γ' A' n , sub_in_env Δ P A' n Γ Γ' ->  A' →→ A -> 
    Γ ⊣  -> exists T', Γ' ⊢ t [ n ←P ]  : T' [ n ←P ] /\ T →→ T'.
Definition wf_subst2 := forall Γ ,  Γ ⊣ -> forall Δ P A A' n Γ' , Δ ⊢ P : A -> 
  sub_in_env  Δ P A' n Γ Γ' -> A'  →→ A ->   Γ' ⊣ .

Theorem substitution2 : typ_subst2 /\ wf_subst2.
apply typ_induc; simpl; intros.
(*1*)
exists !t; simpl; eauto.
(*2*)
destruct (lt_eq_lt_dec v n). destruct s.
exists A; split; trivial.
eapply cVar . eapply H. apply H0. apply H1.  trivial. eapply nth_sub_item_inf. apply H1. intuition. trivial.
exists (A0↑(S n)).
destruct i as (AA & ?& ?).
subst. rewrite substP3; intuition. 
eapply thinning_n.
eapply sub_trunc. apply H1. trivial. eauto.
rewrite <- (nth_sub_eq H1 H5). intuition.
exists A; split; trivial. eapply cVar.  eapply H. apply H0. apply H1. trivial.
destruct i as (AA & ? &?). subst.  rewrite substP3; intuition.
exists AA; split. replace (S (v-1)) with v by intuition. trivial.
eapply nth_sub_sup. apply H1. intuition.
rewrite <- pred_of_minus.
rewrite <- (S_pred v n l). trivial.
(*4*)
exists !u; split; trivial.
edestruct H as ( ? & ?& ?). apply H1. apply H2. trivial. trivial. apply Betas_S in H6; subst.
edestruct H0 as ( ? & ?& ?). apply H1. constructor; apply H2. trivial. eauto.  apply Betas_S in H7; subst.
simpl in *. econstructor. apply r. trivial. trivial.
(*5*)
edestruct H as ( ? & ?& ?). apply H2. apply H3. trivial. trivial. apply Betas_S in H7; subst.
edestruct H0 as ( ? & ?& ?). apply H2. constructor; apply H3. trivial. eauto.  apply Betas_S in H8; subst.
edestruct H1 as ( ? & ?& ?). apply H2. constructor; apply H3. trivial. eauto.
exists (Π (A), x); split; intuition.
simpl in *. econstructor. apply r. trivial. apply H7. trivial. eauto.
(*6*)
edestruct H as (? & ? & ?). apply H1. apply H2. trivial. trivial. 
edestruct H0 as (? & ? & ?). apply H1. apply H2. trivial. trivial.
apply Betas_Pi_inv in H6 as (K & L & -> & ?& ?).
simpl in *. exists (L[   ← b]); intuition.
rewrite subst_travers.
destruct (Betas_diamond A K x0) as (Z & ?& ?); trivial.
apply cApp with (Z[n ← P]) ; trivial.
replace (n+1) with (S n) by intuition. eapply Cnv. apply H5. eauto.
eapply Cnv. apply H7. eauto.
(*7*)
edestruct H as (AA & ?& ?). apply H0. apply H1. trivial. trivial.
destruct (Betas_diamond A B AA b H5) as (Z & ? &?).
exists Z; intuition. eapply Cnv. apply H4. eauto.
(** wf **)
inversion H0.
(**)
inversion H1; subst; clear H1. eauto.
edestruct H as (? & ?& ?). apply H0. apply H7. trivial.
eauto. apply Betas_S in H3; subst.
econstructor. eapply H1.
Qed.

Lemma Ctxt_red :forall Γ M T , Γ ⊢ M : T -> forall  Γ', Γ'⊣ -> Γ →e Γ' ->
  exists T',  Γ' ⊢ M : T' /\ T →→ T'.
induction 1; intros.
exists !t; eauto.
(**)
destruct (Beta_env_item_lift Γ Γ' H2 A v H0).
exists A; split; eauto.
destruct H3 as (B & ? & ?).
exists B; split; eauto.
(**)
destruct (IHtyp1 Γ' H2 H3) as (S & ? & ?). apply Betas_S in H5; subst.
destruct (IHtyp2 (A::Γ')) as (T & ? & ?). eauto. eauto. apply Betas_S in H6; subst.
exists !u; split; eauto.
(**)
destruct (IHtyp1 Γ' H4 H5) as (S & ? & ?). apply Betas_S in H7; subst.
destruct (IHtyp2 (A::Γ')) as (T & ? & ?). eauto. eauto. apply Betas_S in H8; subst.
destruct (IHtyp3 (A::Γ')) as (B'' & ?& ?). eauto. eauto.
exists ( Π (A), B''); split; intuition.
econstructor. apply H. trivial. apply H7. trivial. eauto.
(**)
destruct (IHtyp1 Γ' H1 H2) as (? & ?& ?). apply Betas_Pi_inv in H4 as  (K & L & -> & ? & ?).
destruct (IHtyp2 Γ' H1 H2) as (P & ?& ?).
destruct (Betas_diamond A K P ) as (B'' & ? & ?); trivial.
exists (L[ ← b]); split. apply cApp with B''; trivial.
eapply Cnv. apply H3.  eauto. eapply Cnv. apply H6. trivial. eauto.
(**)
destruct (IHtyp Γ' H1 H2) as ( A' & ? & ?).
destruct (Betas_diamond A B A' H0 H4) as (A'' & ? & ?).
exists A''; split. eapply Cnv. apply H3. trivial. trivial.
Qed.

Lemma SR_exp : forall Γ  M T,  Γ ⊢ M : T ->
   forall N, M → N -> exists T',  Γ ⊢ N : T' /\ T →→ T'.
induction 1; intros.
(**)
inversion H1.
(**)
inversion H1.
(**)
inversion H2; subst; clear H2.
destruct (IHtyp2 y H6) as (TT & ? & ?). apply Betas_S in H3; subst.
exists !u; split; eauto.
destruct (IHtyp1 B0 H6) as (SS & ? & ?). apply Betas_S in H3; subst.
exists !u; split; trivial.
econstructor. apply H. trivial.
destruct (Ctxt_red (A::Γ) B !t H1 (B0::Γ)) as (TT & ?& ?). eauto. eauto.
apply Betas_S in H4; subst. trivial.
(**)
inversion H4; subst; clear H4.
destruct (IHtyp3 y H8) as (BB & ? & ?).
exists (Π (A),BB); split; intuition.
econstructor. apply H. trivial. apply H1. trivial. eauto.
destruct (IHtyp1 B0 H8) as (S & ? & ?). apply Betas_S in H5; subst.
destruct (Ctxt_red (A::Γ) B' !t H1 (B0::Γ)) as ( TT & ? & ?). eauto. eauto.
apply Betas_S in H6; subst.
destruct (Ctxt_red (A::Γ) b B H2 (B0::Γ)) as ( BB & ? & ?). eauto. eauto.
exists ( Π (B0), BB ); split; trivial. econstructor. apply H.
trivial. apply H5. trivial. eauto. eauto.
(**)
inversion H1; subst; clear H1.
apply Gen1c in H as ( K & L & L' &  L'' & sK & sL & h); decompose [and] h; clear h.
injection H2; intros; subst; clear H2.
inversion H; subst; clear H.
destruct substitution2 as (? & _). unfold typ_subst2 in H.
edestruct H as (Z & ? & ?). apply H13. apply H0. constructor. eauto. eauto.
destruct (Betas_diamond L L' Z) as (ZZ & ?& ?); trivial.
exists (ZZ [ ← b]); split;intuition.
eapply Cnv. apply H2. intuition.


destruct (IHtyp1 y H5) as (P & ? & ?). apply Betas_Pi_inv in H2 as (B' & K' & -> & ?& ?).
exists ( K'[ ← b]); intuition.
apply cApp with B' ; trivial. eauto.

destruct (IHtyp2 y H5) as (K' & ? & ?).
exists (B[ ← y]); intuition. apply cApp with K'; trivial. eauto.
(**)
destruct (IHtyp N H1) as ( AA & ? & ?).
destruct (Betas_diamond A B AA H0 H3) as (C & ? & ?).
exists C; intuition. eauto.
Qed.


Lemma sens1 : (forall Γ M T, Γ ⊢ M : T -> (Γ ⊢ M : T)%DN ) /\
  (forall Γ,  Γ ⊣ -> (Γ ⊣)%DN ).
apply typ_induc; intros.
eauto.
(**)
eauto.
(**)
econstructor; eauto.
(**)
econstructor. 
econstructor. apply r. trivial. eapply SubjectRed. apply H0. trivial.
trivial.
(**)
eauto.
(**)
destruct (TypeCorrect Γ a A H) . destruct H0 as (s & ->).
apply Betas_S in b; subst. trivial.
destruct H0 as ( s & ?).
apply dn_typ.Cnv with A s; trivial. 
intuition. apply SubjectRed with A; trivial.
(**)
trivial.
(**)
eauto.
Qed.


Lemma postpone : (forall Γ M T, (Γ ⊢ M : T)%DN -> exists T', 
  Γ ⊢  M :  T' /\  T →→ T') /\
 (forall Γ, (Γ ⊣)%DN -> Γ ⊣).
apply dn_typ.typ_induc; intros.
(**)
exists !t; eauto.
(**)
exists A; eauto.
(**)
destruct H as (? & ? &?). apply Betas_S in H1; subst.
destruct H0 as (? & ? &?). apply Betas_S in H1; subst.
exists !u; eauto.
(**)
destruct H as (? & ? &?). apply Betas_S in H1; subst.
destruct H0 as (? & ? &?).
exists (Π (A),x); intuition.
apply Gen1b in H as (s1 & s2 & s3 & h); decompose [and] h; clear h.
injection H6; intros; subst; clear H6.
econstructor. apply H. trivial. apply H4. trivial. trivial.
(**)
destruct H as (? & ?& ? ). apply Betas_Pi_inv in H1 as (K & L & -> & ? & ?).
destruct H0 as (Z & ? &?).
destruct (Betas_diamond B Z K H3 H1) as (ZZ & ? &?). 
exists (L[← b]); intuition. apply cApp with ZZ. eauto. eauto.
(**)
destruct H as (A' & ? &?). destruct H0 as ( ? & ? & ?). apply Betas_S in H2; subst.
apply Betac_confl in b as (ZZ & ? & ?).
destruct (Betas_diamond A A' ZZ) as (ZZZ & ? &?). eauto. trivial.
exists ZZZ; eauto.
(**)
trivial.
(**)
destruct H as ( ? & ?& ?).
apply Betas_S in H0; subst.
eauto.
Qed.