Require Import base ars data.fintype f.types f.fsyntax f.fsemantics.

Definition active {m n} (s : tm m n) : bool :=
  match s with
  | lam _ | tlam _ => true
  | _ => false
  end.

Definition tpred := forall m n, tm m n -> Prop.

Definition M (P : tpred) : tpred :=
  fun m1 n1 s => forall m2 n2 (f : ren m1 m2) (g : ren n1 n2), P m2 n2 (rename f g s).

Inductive R (P : tpred) m n (s : tm m n) : Prop :=
| RI :
    (active s -> M P s) ->
    (forall t, step s t -> R P t) ->
    R P s.

Definition D : model tpred tpred :=
  {| Var := id
   ; Arr := fun (U V : tpred) (m n : nat) (s : tm m n) =>
     if s isn't lam b then False else
       forall (u : tm m n), R U u -> R V (inst (@tvar m) (u .: @var m n) b)
   ; All := fun F m n v =>
     if v isn't tlam b then False else
       forall P A, R (F P) (inst (A .: @tvar m) (@var m n) b)
  |}.

Notation V A ρ := (eval D ρ A).
Notation K A ρ := (M (V A ρ)).
Notation E A ρ := (R (V A ρ)).

Lemma R_sn {m n} (P : tpred) (s : tm m n) :
  R P s -> sn step s.
Proof. elim; by eauto using @sn. Qed.

Lemma R_step {m n} (P : tpred) (s t : tm m n) :
  step s t -> R P s -> R P t.
Proof. move=> st [_]. by apply. Qed.

Lemma R_var {m n} (P : tpred) (i : fin n) :
  R P (var m i).
Proof. apply: RI. by []. move=> t st. by inv st. Qed.

Lemma R_rename m1 m2 n1 n2 (f : ren m1 m2) (g : ren n1 n2) (P : tpred) (s : tm m1 n1) :
  R P s -> R P (rename f g s).
Proof.
  elim=> /={s}s ns _ ih. constructor.
  - move=> hns m3 n3 f' g'. rewrite ren_comp. apply: ns. by destruct s.
  - move=> t. rewrite ren_inst => /step_weak[s' st <-{t}].
    rewrite -ren_inst. exact: ih.
Qed.

Lemma K_var c m1 n1 (i : fin c) (ρ : fin c -> tpred) (s : tm m1 n1) :
  K (tvar i) ρ s = forall m2 n2 (f : ren m1 m2) (g : ren n1 n2), ρ i m2 n2 (rename f g s).
Proof. by []. Qed.

Lemma K_arr c m1 n1 (A B : ty c) (ρ : fin c -> tpred) (b : tm m1 n1.+1) :
  K (arr A B) ρ (lam b) =
  forall m2 n2 (f : ren m1 m2) (g : ren n1 n2) (u : tm m2 n2),
    E A ρ u -> E B ρ (inst (f >> @tvar m2) (u .: g >> @var m2 n2) b).
Proof.
  rewrite/M/=; fext=> m2 n2 f g u hu. rewrite ren_inst_comp. by fsimpl.
Qed.

Lemma K_all c m1 n (A : ty c.+1) (ρ : fin c -> tpred) (b : tm m1.+1 n) :
  K (all A) ρ (tlam b) =
  forall m2 (f : ren m1 m2) P B,
    E A (P .: ρ) (inst (B .: f >> @tvar m2) (@var m2 n) b).
Proof.
  rewrite/M/=. apply: pext=> H.
  - move=> m2 f P B. move: (H m2 n f id P B). rewrite ren_inst_comp. by fsimpl.
  - move=> m2 n2 f g P B.
    move: (H m2 f P B). rewrite ren_inst_comp. unfold up; fsimpl=>/=.
    move=> HH. move: (R_rename id g HH). rewrite inst_ren_comp.
    fsimpl. rewrite ty_ren_id. exact.
Qed.

Lemma V_weaken c m n (A : ty c) (ρ : fin c -> tpred) (P : tpred) (s : tm m n) :
  V (tyrename shift A) (P .: ρ) m n s = V A ρ m n s.
Proof. by rewrite eval_weaken. Qed.

Lemma K_weaken c m n (A : ty c) (ρ : fin c -> tpred) (P : tpred) (s : tm m n) :
  K (tyrename shift A) (P .: ρ) s = K A ρ s.
Proof. fext=>*; by rewrite V_weaken. Qed.

Lemma E_weaken c m n (A : ty c) (ρ : fin c -> tpred) (P : tpred) (s : tm m n) :
  E (tyrename shift A) (P .: ρ) s = E A ρ s.
Proof. f_equal. fext=> *; by rewrite V_weaken. Qed.

Lemma V_beta c m n (A : ty c.+1) (B : ty c) (ρ : fin c -> tpred) (s : tm m n) :
  V (tyinst (B .: @tvar c) A) ρ m n s = V A (V B ρ .: ρ) m n s.
Proof. by rewrite eval_beta. Qed.

Lemma E_beta c m n (A : ty c.+1) (B : ty c) (ρ : fin c -> tpred) (s : tm m n) :
  E (tyinst (B .: @tvar c) A) ρ s = E A (V B ρ .: ρ) s.
Proof. by rewrite eval_beta. Qed.

Definition C {c n} (Γ : fin n -> ty c) (ρ : fin c -> tpred) : forall {m k}, subst m n k -> Prop :=
  fun m k f => forall i, E (Γ i) ρ (f i).

Lemma C_scons c m n k A (Γ : fin n -> ty c) (ρ : fin c -> tpred) (f : subst m n k) (s : tm m k) :
  E A ρ s -> C Γ ρ f -> C (A .: Γ) ρ (s .: f).
Proof. move=> ls cf; hnf=>/=; by case. Qed.

Lemma C_rename c m1 m2 n1 n2 n3 (Γ : fin n1 -> ty c) (ρ : fin c -> tpred) (f : subst m1 n1 n2) (g : ren m1 m2) (h : ren n2 n3) :
  C Γ ρ f -> C Γ ρ (f >> rename g h).
Proof.
  move=> cf i /=. apply: R_rename. exact: cf.
Qed.

Lemma C_up c m n k (A : ty c) (Γ : fin n -> ty c) (ρ : fin c -> tpred) (f : subst m n k) :
  C Γ ρ f -> C (A .: Γ) ρ (upi f).
Proof.
  move=> cf. apply: C_scons. exact: R_var. exact: C_rename.
Qed.

Lemma E2_ind {c1 c2 m1 m2 n1 n2} (A : ty c1) (B : ty c2) (ρ1 : fin c1 -> tpred) (ρ2 : fin c2 -> tpred)
      (P : tm m1 n1 -> tm m2 n2 -> Prop) :
  (forall (s : tm m1 n1) (t : tm m2 n2),
      E A ρ1 s ->
      E B ρ2 t ->
      (forall s', step s s' -> P s' t) ->
      (forall t', step t t' -> P s t') ->
      P s t) ->
  forall (s : tm m1 n1) (t : tm m2 n2),
    E A ρ1 s -> E B ρ2 t -> P s t.
Proof.
  move=> h s t ls. elim: ls t => {s} s ns ls ihs t.
  elim=> {t} t nt lt iht. apply: h. constructor. exact: ns. exact: ls.
  constructor. exact: nt. exact: lt.
  move=> u /ihs. apply. constructor. exact: nt. exact: lt.
  move=> u. exact: iht.
Qed.

Lemma E_app c m n A B (s t : tm m n) (ρ : fin c -> tpred) :
  E (arr A B) ρ s -> E A ρ t -> E B ρ (app s t).
Proof.
  move: s t. apply: E2_ind => s t ns nt ihs iht. constructor. by [].
  move=> u st. inv st.
  - case: ns. rewrite K_arr => /(_ erefl)/=H _.
    exact: (H m n id id t nt).
  - exact: ihs.
  - exact: iht.
Qed.

Lemma E_lam c m1 n1 (A B : ty c) (ρ : fin c -> tpred) (s : tm m1 n1.+1) :
  sn step s ->
  (forall m2 n2 (f : ren m1 m2) (g : ren n1 n2) (a : tm m2 n2),
      E A ρ a -> E B ρ (inst (f >> @tvar _) (a .: g >> @var _ _) s)) ->
  E (arr A B) ρ (lam s).
Proof.
  elim=>{s} s _ ih h. constructor.
  - move=> _. rewrite K_arr. exact: h.
  - move=> t st. inv st. apply: ih. exact: H0. move=> m2 n2 f g a la.
    apply: R_step (h _ _ f g _ la). exact: step_inst.
Qed.

Lemma E_tapp c m n (A : ty c.+1) (B : ty c) (ρ : fin c -> tpred) (s : tm m n) (C : ty m) :
  E (all A) ρ s -> E (tyinst (B .: @tvar _) A) ρ (tapp s C).
Proof.
  elim=> {s} s h1 ih h2. rewrite E_beta. constructor => [//|t st]. inv st.
  specialize (h1 erefl). rewrite K_all in h1. exact: h1.
Qed.

Lemma E_tlam c m1 n (A : ty c.+1) (ρ : fin c -> tpred) (s : tm m1.+1 n) :
  sn step s ->
  (forall m2 (f : ren m1 m2) P B, E A (P .: ρ) (inst (B .: f >> @tvar _) (@var _ _) s)) ->
  E (all A) ρ (tlam s).
Proof.
  elim=> {s} s _ ih h. constructor.
  - rewrite K_all => _. exact: h.
  - move=> t st. inv st. apply: ih => [//|m2 f P B]. move: (h m2 f P B).
    apply: R_step. exact: step_inst.
Qed.

Theorem fundamental m1 n1 Γ A (s : tm m1 n1) :
  has_type Γ s A ->
  forall m2 n2 (σ : tysubst m1 m2) (f : subst m2 n1 n2) (ρ : fin m1 -> tpred),
    C Γ ρ f -> E A ρ (inst σ f s).
Proof.
  elim=> {m1 n1 Γ s A} [m1 n1 Γ i|m1 n1 Γ s t A B _ ihA _ ihB|m1 n1 Γ s A B _ ih|m1 n1 Γ s A B _ ih|m1 n1 Γ s A _ ih] m2 n2 σ τ ρ ct.
  - exact: ct.
  - cbn. apply: E_app. exact: ihA. exact: ihB.
  - cbn. apply: E_lam. apply: R_sn. apply: ih. exact: C_up.
    move=> m3 n3 f g a la.
    have->: inst (f >> tvar (n:=m3)) (a .: g >> var m3 (n:=n3)) (inst σ (upi τ) s)
          = inst (σ >> tyrename f) (a .: τ >> rename f g) s.
    { rewrite inst_comp. unfold upi; fsimpl=> /=. f_equal.
      fext=> t /=. by rewrite ty_ren_inst.
      fext=> /=; case=> //=i. rewrite ren_inst. fsimpl=>/=.
      rewrite inst_comp. by rewrite ren_inst. }
    apply: ih. apply: C_scons. exact: la. exact: C_rename.
  - cbn. apply: E_tapp. exact: ih.
  - cbn. apply: E_tlam.
    + case/(_ _)/Wrap: (ih _ _ (tup σ) (τ >> rename shift id) ((fun _ _ _ => False) .: ρ)).
      move=> i /=. rewrite E_weaken. apply: R_rename. exact: ct.
      exact: R_sn.
    + move=> m3 f P B. rewrite inst_comp. apply: ih.
      move=> i /=. rewrite ren_inst_comp. fsimpl. rewrite E_weaken.
      rewrite -ren_inst. apply: R_rename. exact: ct.
Qed.

Theorem strong_normalization m n Γ A (s : tm m n) : has_type Γ s A -> sn step s.
Proof.
  move=> tp. move: (@fundamental m n Γ A s tp m n (@tvar m) (@var m n) (fun _ _ _ _ => False)). case/(_ _)/Wrap.
  - move=> i. exact: R_var.
  - rewrite inst_ids. exact: R_sn.
Qed.