Require Import base ord ars data.fintype ccomega.sorts
        ccomega.syntax ccomega.reduction ccomega.churchrosser
        ccomega.subtyping ccomega.typing ccomega.contextmorphism.

(* Finite contexts *)

Definition cempty {n} : ctx n :=
  fun _ _ => False.

Inductive is_finite : forall {n}, ctx n -> Prop :=
| is_finite_empty n : @is_finite n cempty
| is_finite_ext n (A : tm n) (Gamma : ctx n) :
    is_finite Gamma -> is_finite (ext Gamma A).

Lemma is_finite_var {n} (Gamma : ctx n) :
  is_finite Gamma ->
  forall s A, Gamma s A -> exists i, s = var i.
Proof.
  elim=> {n Gamma}//n A Gamma _ ih s B [{s B}|{s B}s B tp]. by exists bound.
  case: (ih s B tp) => i -> /=. by exists (shift i).
Qed.

Lemma is_finite_prod {n} (Gamma : ctx n) A B C :
  is_finite Gamma -> ~Gamma (prod A B) C.
Proof.
  by move=> /is_finite_var H/H[].
Qed.

Lemma is_finite_lam {n} (Gamma : ctx n) s A :
  is_finite Gamma -> ~Gamma (lam s) A.
Proof.
  by move=> /is_finite_var H/H[].
Qed.

(* Inversion Lemmas *)

Lemma ty_prod_invX n (Gamma : ctx n) A B u :
  is_finite Gamma ->
  [ Gamma |- prod A B :- u ] ->
    [ Gamma |- A ] /\ [ ext Gamma A |- B ].
Proof.
  move e:(prod A B) => s tc tp. elim: tp A B e tc => //{n Gamma s u}.
  - move=> n Gamma s A tp A' B' eqn tc; subst. exfalso. exact: is_finite_prod tc tp.
  - move=> n Gamma A B u v tp1 _ tp2 _ A' B' [e1 e2] tc; subst. split; eexists; by eauto.
Qed.

Lemma ty_prod_inv n (Gamma : ctx n) A B :
  is_finite Gamma ->
  [ Gamma |- prod A B ] ->
    [ Gamma |- A ] /\ [ ext Gamma A |- B ].
Proof. move=> tc [u h]. exact: ty_prod_invX h. Qed.

Lemma ty_lam_invX n (Gamma : ctx n) s A B C :
  is_finite Gamma ->
  [ Gamma |- lam s :- C ] ->
  (C <: prod A B /\ [ ext Gamma A |- B ]) \/ prod A B = C ->
  [ ext Gamma A |- s :- B ].
Proof.
  move e:(lam s) => t tc tp. elim: tp A B s e tc => // {n Gamma t C}.
  - move=> n Gamma s A tp A' B' t eqn tc. subst. exfalso. exact: is_finite_lam tc tp.
  - move=> n Gamma A B s u tp1 _ tp2 _ A' B' s' [->] tc [|[->->//]].
    move=> [/sub_prod_inv[con sub] [m tp3]]. apply: ty_sub sub tp3 _.
    apply: ty_ctx_conv tp2 _ tp1. exact: conv_sym.
  - move=> n Gamma u A B s sub1 tp1 ih1 tp2 ih2 A' B' t eqn1 tc [[sub2 [m tp3]]|eqn2];
      subst; apply: ih2 => //; left; split => //.
    + exact: sub_trans sub1 sub2. by exists m.
    + move: tc => /ty_prod_inv H. case: (H A' B') => //. by exists u.
Qed.

Lemma ty_lam_inv n (Gamma : ctx n) s A B :
  is_finite Gamma ->
  [ Gamma |- lam s :- prod A B ] -> [ ext Gamma A |- s :- B ].
Proof. move=> tc tp. apply: ty_lam_invX tp _ => //. by right. Qed.

(* Main Result *)

Lemma is_type_weakening n (Gamma : ctx n) A B :
  [ Gamma |- B ] -> [ ext Gamma A |- rename shift B ].
Proof.
  move=> [u tp]. exists u. apply: eweakening => //; last first. exact: tp. by [].
Qed.

Lemma context_ok_ext n (Gamma : ctx n) A :
  context_ok Gamma -> [Gamma |- A] -> context_ok (ext Gamma A).
Proof.
  move=> h1 h2 s B [{s B}|{s B}s B /h1 h3]; exact: is_type_weakening.
Qed.

Lemma propagation n (Gamma : ctx n) s A :
  is_finite Gamma -> context_ok Gamma ->
  [ Gamma |- s :- A ] -> [ Gamma |- A ].
Proof.
  move=> tc1 tc2 tp. elim: tp tc1 tc2 => {n Gamma s A} /=
    [n Gamma s A e tc1 tc2||n Gamma A B _ t _ ih tp _ tc1 tc2|n Gamma A B s u v h1 h2 h3 h4 tc|
    |n Gamma u A B s _ tp _ _ _ _ tc] //.
  - exact: tc2 e.
  - move: (ih tc1 tc2) => [u {ih} H]. case: (ty_prod_inv tc1 (ex_intro _ _ H)) => _ [v ih].
    exists v. exact: (@ty_cut _ _ _ _ _ _ ih tp).
  - apply: ty_prod_wf. by exists u. apply: h3. exact: is_finite_ext. apply: context_ok_ext => //. by exists u.
  - by exists u.
Qed.

Lemma subject_reduction n (Gamma : ctx n) s A :
  [ Gamma |- s :- A ] ->
  is_finite Gamma -> context_ok Gamma ->
    forall t, step s t -> [ Gamma |- t :- A ].
Proof.
  elim => {n Gamma s A}.
  - move=> n Gamma s A e tc1 tc2 t st. case: (is_finite_var tc1 e) => i E; subst. by inv st.
  - move=> n Gamma u tc1 tc2 t st. by inv st.
  - move=> n Gamma A B s t tp1 ih1 tp2 ih2 tc1 tc2 u st. inv st.
    + apply ty_lam_inv in tp1 => //. exact: ty_cut tp1 tp2.
    + apply: ty_app tp2. exact: ih1.
    + move: (tp1) => /propagation. move/(_ tc1 tc2) => /ty_prod_inv[]// _ [u tp3].
      eapply ty_sub; last first. eapply ty_app. eassumption. exact: ih2.
      move: (ty_cut tp3 tp2) => /= h. apply h. apply: conv_sub.
      apply: conv_beta. exact: conv1i.
  - move=> n Gamma A B s u tp1 ih1 tp2 ih2 tc1 tc2 t st. inv st.
    apply: ty_lam (tp1) _. apply: ih2 => //. exact: is_finite_ext. apply: context_ok_ext => //. by exists u.
  - move=> n Gamma A B u v tp1 ih1 tp2 ih2 tc1 tc2 t st. inv st.
    + apply: ty_prod. exact: ih1. eapply (ty_ctx_conv tp2).
      exact: conv1i. eassumption.
    + apply: ty_prod => //. apply: ih2 => //. exact: is_finite_ext. apply: context_ok_ext => //. by exists u.
  - move=> n Gamma s A B u tp1 ih1 con tp2 ih2 tc1 tc2 t st.
    apply: ty_sub tp1 ih1 _. exact: ih2.
Qed.