Require Import PTS.
Require Import PTS_beta.
Require Import PTS_env.
Require Import PTS_correctness.
Require Import List.

(* How to deal with Beta reduction in the context *)
Inductive Beta_env : Env -> Env -> Prop :=
 | Beta_env_hd : forall A B e, A → B -> Beta_env (A::e) (B::e)
 | Beta_env_cons : forall A e f, Beta_env e f -> Beta_env (A::e) (A::f)
.

Inductive Betas_env : Env -> Env -> Prop :=
 | Betas_env_refl : forall e, Betas_env e e
 | Betas_env_Beta : forall e f, Beta_env e f -> Betas_env e f
 | Betas_env_trans : forall e f g, Betas_env e f -> Betas_env f g -> Betas_env e g.

Notation " a →e b " := (Beta_env a b) (at level 20).
Notation " a →→e b " := (Betas_env a b) (at level 20).

(* simples facts on env / beta *)
Lemma Betas_env_nil_ : forall e g,e →→e g -> (e = nil -> g = nil).
intros e g H.
induction H; intros.
trivial.
subst.
inversion H.
intuition.
Qed.

Lemma Betas_env_nil : forall g, nil →→e g -> g = nil.
intros.
apply (Betas_env_nil_ nil g H); intuition.
Qed.

Lemma Betas_env_nil2_ : forall e g , e →→e g -> (g = nil -> e = nil).
intros e g H; induction H; intros.
trivial.
subst; inversion H.
intuition.
Qed.

Lemma Betas_env_nil2 : forall e, e →→e nil -> e = nil.
intros ; apply (Betas_env_nil2_ e nil) ; trivial.
Qed.

Lemma Betas_env_inv_ : forall E F, E →→e F -> 
 (forall a b g f,E = a::g -> F = b::f  -> a→→b /\ g→→e f).
intros E F H; induction H; intros.
rewrite H0 in H.
injection H; intros; subst.
split; constructor.
inversion H; subst.
injection H3; injection H4; intros; subst.
rewrite H5; split; constructor; trivial.
injection H3; injection H4; intros; subst.
rewrite H6; split; constructor; trivial.
destruct f.
rewrite (Betas_env_nil g H0) in *; discriminate.
subst.
destruct (IHBetas_env2 t b f f0); intuition; 
destruct (IHBetas_env1 a t g0 f); intuition.
apply Betas_trans with (y:=t); trivial.
apply Betas_env_trans with  (f:=f); trivial.
Qed.

Lemma Betas_env_inv :forall a b g f, (a::g)  →→e  (b::f) -> a →→ b /\ g→→e f.
intros.
apply Betas_env_inv_ with (a::g) (b::f) ; trivial.
Qed.

Lemma Betas_env_hd : forall A C f, A→→C -> (A::f) →→e (C::f).
intros.
induction H.
constructor.
constructor; apply Beta_env_hd; trivial.
apply Betas_env_trans with (f:=y::f); intuition.
Qed.

Lemma Betas_env_cons : forall A g f , g →→e f -> (A::g) →→e (A::f).
intros.
induction H.
constructor.
constructor; apply Beta_env_cons; trivial.
apply Betas_env_trans with (f:=A::f); trivial.
Qed.

Lemma Betas_env_comp : forall A B g f, A→→B -> g→→e f -> (A::g) →→e (B::f).
intros.
apply Betas_env_trans with (f:= A::f).
apply Betas_env_cons; trivial.
apply Betas_env_hd; trivial.
Qed.

(* Important one 
we have to proof subject reduction and context reduction at the same time
*)
Lemma Beta_sound :  
  forall Γ x A, Γ ⊢ x : A->
  (forall y, x→ y ->  Γ ⊢y : A) /\ (forall Γ', Γ →e Γ' -> Γ' ⊢ x : A).
intros; induction H; split; intros.
(*1*)
inversion H0. inversion H0.
(*2*)
inversion H0. inversion H0; subst.
destruct IHCorrectness.
apply Cnv with (B ↑ 1) s; intuition.
apply Betac_lift; apply Betac_sym; constructor; constructor; trivial.
apply cVar with s; intuition.
destruct (wf_app Γ A !s H B s (H1 B H4)) as [S [T K]].
change !s with !s↑ 1.
apply thinning with S T; intuition.
(*==*)
apply cVar with s; trivial.
intuition.
(*3*)
inversion H1. 
(*==*)
inversion H1; subst;
destruct IHCorrectness2; 
apply cWkv with s ; intuition.
(*4*)
inversion H1. 
(*==*)
inversion H1; subst;
destruct IHCorrectness2;
apply cWks with s; intuition.
(*5*)
destruct IHCorrectness1 ; destruct IHCorrectness2.
inversion H2; subst.
apply cPi with s t; intuition.
apply cPi with s t; intuition.
apply H6; apply Beta_env_hd; intuition.
(*==*)
apply cPi with s t; intuition.
apply H6; apply Beta_env_cons; intuition.
(*6*)
destruct IHCorrectness1; destruct IHCorrectness2; destruct IHCorrectness3.
inversion H3; subst.
apply cLa with s t u; intuition.
apply Cnv with (Pi B0 B) u; intuition.
apply cLa with s t u; intuition.
apply H7; apply Beta_env_hd; intuition.
apply H9; apply Beta_env_hd; intuition.
apply cPi with s t; intuition.
(*==*)
apply cLa with s t u; intuition.
apply H7; apply Beta_env_cons; intuition.
apply H9 ; apply Beta_env_cons; intuition.
(*7*) (* delicate case, we gives lots of detail with assert *)
(* Proof from Barendregt 92 *)
destruct IHCorrectness1; destruct IHCorrectness2.
(*
 Γ ⊢ a : Π(B), A -> Γ ⊢ Π(B), A : !s  ( Π(B), A is welltyped Γ)
*)
assert (exists s, Γ ⊢ Π(B), A : !s).
   apply TypeCorrect in H; destruct H.  destruct H; discriminate. trivial.
   destruct H6 as [u Hu].
(* 
  Γ ⊢ Π(B), A : !s  ->  Γ ⊢ B : !s1      B::Γ ⊢ A: s2    Rel s1 s2 s
  Π(B), A  is well formed so we can type his domain / co domain
*)
assert (exists s1 , exists s2, Rel s1 s2 u /\ Γ ⊢ B : !s1 /\ B::Γ ⊢ A : !s2).
   apply Geniii in Hu. destruct Hu as [s1 [s2 [s3 [h1 [h2 [h3 h4]]]]]].
   apply conv_sort in h1. rewrite h1 in *.  exists s1; exists s2; intuition.
   destruct H6 as [s1 [s2 [h1 [h2 h3]]]].
(* 
   Γ ⊢ b : B     B::Γ ⊢ A : !t    -> Γ ⊢ A[ ← b] : !t
*)
assert (Γ ⊢ A[ ← b] : !s2).
   change !s2 with !s2[←b].
   apply substitution with Γ B (B::Γ) B !s1; intuition.
   apply sub_O.
inversion H1; subst.
(* case (λ(x:A0) . b0) b  →  b[b0] *)
(*
  Γ ⊢ λ[A0], b0 : Π (B),A ->  A0 == B     and A0::Γ ⊢ b0 : D  with D == A
*)
apply Geniv in H. destruct H as [s1' [s2' [s3' [ D [ h1' [h2' [ h3' [h4' h5']]]]]]]].
apply Betac_Pi_inv in h1'. destruct h1'.
(* since A == D, convert the type *)
apply Cnv with (D [ ← b]) s2; intuition.
apply Betac_subst2; apply Betac_sym; trivial.
(* apply the substitution lemma with everthing we have now *)
apply substitution with Γ A0 (A0::Γ) B !s1; intuition.
(* convert since A0 == B *)
apply Cnv with B s1'; intuition.
apply sub_O.
(* case a b →  a' b  or a b  → a b'  with  a → a' or  b → b' *)
apply cApp with B ; intuition.
apply Cnv with (A [← y0]) s2.
apply Betac_subst; apply Betac_sym; constructor; constructor; intuition.
apply cApp with B; intuition.
change !s2 with !s2[←b].
apply substitution with Γ B (B::Γ) b B; intuition.
apply sub_O.
(*==*)
apply cApp with B; intuition.
(*8*)
apply Cnv with A s; intuition.
(*==*)
apply Cnv with A s; intuition.
Qed.

Lemma SubjectRed : forall Γ x T, Γ ⊢ x : T-> 
  forall y , x →→ y -> Γ ⊢ y : T.
intros. induction H0.
trivial.
destruct (Beta_sound Γ  x T H).
intuition.
intuition.
Qed.

(* Type reduction *)
Lemma Beta_typ_sound : forall Γ x T, Γ ⊢ x : T -> 
 forall T', T →→ T' -> Γ ⊢ x : T'.
intros.
assert ((exists s, T = !s )\/ exists s,  Γ ⊢ T : !s ) by ( apply TypeCorrect in H; intuition).
destruct H1 as [[s Hs]|[s Hs]].
rewrite Hs in *. apply Betas_S in H0. rewrite H0; trivial.
apply Cnv with T s; intuition.
apply SubjectRed with T; intuition.
Qed.

(* Env reduction soundness *)
Lemma Beta_env_sound : forall Γ x T, Γ ⊢ x : T -> 
 forall Γ' , Γ  →→e Γ' -> Γ' ⊢ x : T.
intros.
induction H0.
trivial.
destruct (Beta_sound e x T H).
intuition.
intuition.
Qed.

(* compilation of all this *)
Lemma Subject_Reduction :  forall Γ x A, Γ ⊢ x : A ->
  forall Γ' y B, x→→ y -> Γ →→e Γ' -> A→→ B -> Γ' ⊢ y : B.
intros.
apply Beta_typ_sound with A; intuition.
apply Beta_env_sound with Γ; intuition.
apply SubjectRed with x; intuition.
Qed.