Require Export TaitCore.
Require Export nc.

Set Implicit Arguments.

Module NormalizationProofNc (R:Requirements).

Import R.

Notation App' := (nc2 App).
Notation app' := (nc2 (@app _)).

Lemma app'_ass : forall (l1 l2 l3: context!) ,
 app' (app' l1 l2) l3 = app' l1 (app' l2 l3).
Proof.
intros; unfold nc2.
case l1; case l2; case l3; intros.
rewrite app_ass; auto.
Qed.

Definition SN (rhos:context!) (rho:type) (r:term!) :=
  forall k (sigmas:context!) ,
    (letnc taus' := app' rhos sigmas in letnc r':= r in F taus' rho r' k) ->
  { s:term | letnc taus' := app' rhos sigmas in letnc r':= r in N taus' rho r' s }.

Definition SA (rhos:context!) (rho:type) (r:term!) :=
  forall k (sigmas:context!) ,
    (letnc taus' := app' rhos sigmas in letnc r':= r in F taus' rho r' k) ->
  { s:term | letnc taus' := app' rhos sigmas in letnc r':= r in A taus' rho r' s }.

Open Scope type_scope.

Fixpoint SC (rhos:context!) (rho:type) (r:term!) {struct rho} : Type :=
  (letnc rhos' := rhos in letnc r' := r in TypJ rhos' r' rho) **
  match rho with
  | Iota => SN rhos Iota r
  | rho-->sigma =>
    forall s sigmas, SC (app' rhos sigmas) rho s ->
      SC (app' rhos sigmas) sigma (App' r s)
  end.

Lemma SN_ext_ctx : forall rho rhos sigmas r,
 (letnc rhos' := rhos in letnc r' := r in TypJ rhos' r' rho) ->
 SN rhos rho r -> SN (app' rhos sigmas) rho r.

Lemma SC_TypJ :
 forall rhos rho r, SC rhos rho r ->
 (letnc rhos' := rhos in letnc r' := r in TypJ rhos' r' rho).

Lemma SC_ext_ctx : forall rho rhos sigmas r,
 SC rhos rho r -> SC (app' rhos sigmas) rho r.
Proof.
destruct rho; simpl; intuition.
nc; auto.
nc; auto.
rewrite app'_ass; rewrite app'_ass in X; auto.
Qed.

Lemma one :
 forall rho rhos r,
 (letnc rhos' := rhos in letnc r' := r in TypJ rhos' r' rho) ->
 (SC rhos rho r -> SN rhos rho r)*(SA rhos rho r -> SC rhos rho r).

Definition head (rs:list term) :=
 match rs with
  | nil => [0]
  | r::_ => r
 end.

Definition tail (rs:list term) :=
 match rs with
  | nil => nil
  | _::rs => rs
 end.

Notation head' := (nc1 head).
Notation tail' := (nc1 tail).
Notation "'nth'' n" := (nc2 (nth n)) (at level 10).

Fixpoint SCs (sigmas:context!) (rhos: context) (rs: (list term)!) {struct rhos} : Type :=
 match rhos with
 | nil => letnc rs' := rs in rs' = nil
 | rho::rhos =>
   (letnc rs' := rs in rs' <> nil) **
   (SC sigmas rho (head' rs))*(SCs sigmas rhos (tail' rs))
end.

Lemma SCs_length : forall sigmas rhos rs, SCs sigmas rhos rs ->
  letnc rs' := rs in length rhos = length rs'.

Lemma SCs_nth : forall sigmas rhos rho rs r n, n < length rhos ->
  SCs sigmas rhos rs ->
  SC sigmas (nth n rhos rho) (nth' n rs r).
Proof.
induction rhos.
intros.
elimtype False.
inversion H0.
intros.
simpl in X.
destruct X.
destruct h.
destruct n.
simpl.
assert (nth' 0 rs r = head' rs).
nc; destruct l; try tauto.
rewrite H1; auto.
assert (nth' (S n) rs r = nth' n (tail' rs) r).
nc; destruct l; tauto.
rewrite H1.
simpl; apply IHrhos; intuition.
Defined.

Lemma SCs_ext_ctx : forall sigmas sigmas0 rhos rs,
 SCs sigmas rhos rs -> SCs (app' sigmas sigmas0) rhos rs.
Proof.
induction rhos; simpl; intuition; apply SC_ext_ctx; auto.
Qed.

Notation "'sub'' r" := (nc1 (sub r)) (at level 10).
Notation support' := (nc1 support).

Lemma three : forall r rs rhos sigmas rho,
  SCs sigmas rhos (support' rs) -> TypJ rhos r rho ->
  SC sigmas rho (sub' r rs).
Proof.
induction r.
intros.
destruct H0.
simpl in H1.
subst rho.
set (r:=let (rs'):=rs in nc [n-length rs'+shift rs']).
replace (sub' n rs) with (nth' n (support' rs) r).
apply SCs_nth; auto.
inversion_clear H0; auto.
nc; auto.

intros.
set (sigma := typ rhos r2).
assert (H1: TypJ rhos r1 (sigma-->rho)). eauto.
assert (H2: TypJ rhos r2 (typ rhos r2)). eauto.
assert (IH1:= IHr1 rs rhos sigmas (sigma --> rho) X H1).
assert (IH2:= IHr2 rs rhos sigmas (typ rhos r2) X H2).
simpl in IH1.
destruct IH1 as [_ B].
assert (sigmas = app' sigmas (nc nil)).
nc; rewrite <- app_nil_end; auto.
rewrite H3; replace (sub' (r1;r2) rs) with (App' (sub' r1 rs) (sub' r2 rs)).
apply (B (sub' r2 rs) (nc nil)); simpl_list; auto.
rewrite <- H3; auto.
nc; auto.

rename t into rho.
intros.
destruct H0.
subst rho0.
set (freeze:= sub' (\ rho, r) rs).
assert (letnc sigmas':=sigmas in letnc rs':=rs in
  (TypJ sigmas' (sub (\ rho, r) rs') (rho --> typ (rho::rhos) r))).
nc.
 apply TypJ_sub2 with rhos; auto.
 rewrite <- (SCs_length (nc c) rhos X); auto with arith.
 intros.
 lapply (@SCs_nth (nc c) rhos d' (support' (nc rs')) (nc d) n); auto.
 intros.
eapply SC_TypJ; eauto.
simpl; split; intros.
rename rhos' into sigmas'.
nc; auto.
destruct (@one rho (app' sigmas sigmas0) s); auto.
nc; eauto.
set (rs0 := let (rs'):=rs in let (s'):=s in nc ((s'::rs')#rs'.(shift))).
apply two with (sub' r rs0).
nc; eauto.
apply IHr with (rhos:=rho::rhos).
simpl; intuition.
subst.
nc.
simpl in *; discriminate.
replace (head' (support' rs0)) with s; auto.
nc; auto.
apply SCs_ext_ctx; auto.
replace (tail' (support' rs0)) with (support' rs); auto.
nc; auto.
inversion_clear H0; split; auto.
nc; auto.
apply Ax6; auto.
Qed.

Lemma SCs_seq : forall rhos (sigmas:context!) k,
 (letnc sigmas':=sigmas in length sigmas' = k) ->
  SCs (app' sigmas (nc rhos)) rhos (nc (map Var (seq k (length rhos)))).

Lemma normalizeTheorem :
 forall rhos rho r, TypJ rhos r rho -> { s:term | N rhos rho r s }.
Proof.
intros.
destruct (@one rho (nc rhos) (nc r)); auto.
nc; auto.
assert (SC (nc rhos) rho (nc r)).
rewrite <- (sub_id r (length rhos)).
replace (nc (sub r (id (length rhos)))) with (sub' r (nc (id (length rhos)))).
apply three with rhos; auto.
unfold id; simpl.
generalize (@SCs_seq rhos (nc nil) 0); simpl_list; simpl; auto.
intro H1; apply H1.
nc; eauto.
nc; auto.
destruct (s X (length rhos) (nc nil)); intros.
nc; simp; auto.
exists x.
nc; rewrite <- app_nil_end in n; auto.
Defined.

End NormalizationProofNc.