From Companion Require Import prelim companion companion_mu.
Require Export autosubst.

Inductive term :=
| Var (x : var)
| App (s t : term)
| Lam (s : {bind term}).

Inductive type :=
| TVar (x : var)
| TFun (A B : type)
| TAll (A : {bind type}).

Instance Ids_term : Ids term. derive. Defined.
Instance Rename_term : Rename term. derive. Defined.
Instance Subst_term : Subst term. derive. Defined.
Instance SubstLemmas_term : SubstLemmas term. derive. Qed.

Instance Ids_type : Ids type. derive. Defined.
Instance Rename_type : Rename type. derive. Defined.
Instance Subst_type : Subst type. derive. Defined.
Instance SubstLemmas_type : SubstLemmas type. derive. Qed.

Inductive step : Rel term :=
| step_beta s t : step (App (Lam s) t) s.[t/]
| step_appl s1 s2 t : step s1 s2 -> step (App s1 t) (App s2 t)
| step_appr s t1 t2 : step t1 t2 -> step (App s t1) (App s t2)
| step_lam s1 s2 : step s1 s2 -> step (Lam s1) (Lam s2).

Definition get {T} `{Ids T} (Gamma : seq T) (n : var) : T :=
  nth (ids 0) Gamma n.
Arguments get {T _} Gamma n.

Lemma get_map {T} `{Ids T} (f : T -> T) Gamma n :
  n < size Gamma -> get (map f Gamma) n = f (get Gamma n).
Proof. exact: nth_map. Qed.

Definition ctx := seq type.
Local Notation "Gamma `_ i" := (get Gamma i).

Inductive Fty (ty : ctx -> term -> type -> Prop) (Gamma : ctx) : term -> type -> Prop :=
| Fty_var (x : var) :
    x < size Gamma -> Fty ty Gamma (Var x) Gamma`_x
| Fty_abs (A B : type) (s : term) :
    ty (A :: Gamma) s B ->
    Fty ty Gamma (Lam s) (TFun A B)
| Fty_app (A B : type) (s t : term) :
    ty Gamma s (TFun A B) ->
    ty Gamma t A ->
    Fty ty Gamma (App s t) B
| Fty_tabs (A : type) (s : term) :
    ty Gamma..[ren (+1)] s A ->
    Fty ty Gamma s (TAll A)
| Fty_tapp (A B : type) (s : term) :
    ty Gamma s (TAll A) ->
    Fty ty Gamma s A.[B/].

Notation Ty := (l Fty).
Notation ty := (Ty top).

Implicit Types (R S : ctx -> term -> type -> Prop) (Gamma Delta : ctx)
         (x y z : var) (s t u : term) (A B C D : type).

Instance Fty_mono : monotone Fty.
Proof.
  move=> ty1 ty2 /(_ _ _ _ _)le12 Gamma s A h.
  inversion_clear h; eauto using Fty.
Qed.

Lemma ty_unfold R Gamma s A : Ty R Gamma s A -> Fty (Ty R) Gamma s A.
Proof. exact: (@l_unfold _ Fty). Qed.

Lemma ty_fold Gamma s A : Fty ty Gamma s A -> ty Gamma s A.
Proof. by rewrite -mu_l mu_fp. Qed.

Lemma ty_ty R Gamma s A : Ty R Gamma s A -> ty Gamma s A.
Proof. apply: (l_monotone Fty). exact: topI. Qed.

Lemma ty_var Gamma x :
  x < size Gamma -> ty Gamma (Var x) Gamma`_x.
Proof. eauto using ty_fold, Fty. Qed.

Lemma ty_abs Gamma s A B :
  ty (A :: Gamma) s B -> ty Gamma (Lam s) (TFun A B).
Proof. eauto using ty_fold, Fty. Qed.

Lemma ty_app Gamma s t A B :
  ty Gamma s (TFun A B) -> ty Gamma t A -> ty Gamma (App s t) B.
Proof. eauto using ty_fold, Fty. Qed.

Lemma ty_tabs Gamma s A :
  ty Gamma..[ren (+1)] s A -> ty Gamma s (TAll A).
Proof. eauto using ty_fold, Fty. Qed.

Lemma ty_tapp Gamma s A B :
  ty Gamma s (TAll A) -> ty Gamma s A.[B/].
Proof. eauto using ty_fold, Fty. Qed.

Definition cRen R Gamma s A :=
  forall Delta xi,
    (forall x, x < size Gamma -> xi x < size Delta) ->
    (forall x, x < size Gamma -> Delta`_(xi x) = Gamma`_x) ->
    R Delta s.[ren xi] A.

Instance cRen_mono : monotone cRen.
Proof.
  move=> R S le_R_S Gamma s A h Delta xi p q. apply: le_R_S. exact: h.
Qed.

Lemma upto_ren R :
  Ty R <= cRen (Ty R).
Proof.
  apply: ind_upto R => /= R h Gamma s A []{s A}.
  - move=> x ltn Delta xi h1 h2 /=. rewrite -h2 //. apply: Fty_var. exact: h1.
  - move=> A B s /h tp Delta xi h1 h2 /=. apply: Fty_abs. asimpl.
    apply: tp => -[|x] //=. exact: h1. exact: h2.
  - move=> A B s t /h tp1 /h tp2 Delta xi h1 h2 /=.
    apply: (Fty_app (A := A)). exact: tp1. exact: tp2.
  - move=> A s /h tp Delta xi h1 h2. apply: Fty_tabs.
    apply tp => x; rewrite !size_map. exact: h1.
    move=> ltn. by rewrite !get_map ?(h1 _ ltn) // h2.
  - move=> A B s /h tp Delta xi h1 h2. apply: Fty_tapp. exact: tp.
Qed.

Lemma ty_weak R Gamma s A B :
  Ty R Gamma s A -> Ty R (B :: Gamma) s.[ren (+1)] A.
Proof. move=> /upto_ren. exact. Qed.

Definition cTy R Gamma s A :=
  forall sigma : var -> type, R Gamma..[sigma] s A.[sigma].

Instance cTy_mono : monotone cTy.
Proof. move=> R S le_R_S Gamma s A h sigma. apply: le_R_S. exact: h. Qed.

Lemma upto_tysubst R :
  Ty R <= cTy (Ty R).
Proof.
  apply: ind_upto R => /= R ih Gamma s A []{s A}.
  - move=> x ltn sigma. rewrite -get_map //. apply: Fty_var. by rewrite size_map.
  - move=> A B s /ih tp sigma. apply: Fty_abs. exact: tp.
  - move=> A B s t /ih tp1 /ih tp2 sigma. apply: Fty_app; by [exact: tp1|exact: tp2].
  - move=> A s /ih tp sigma /=. apply: Fty_tabs. move/(_ (up sigma)): tp. autosubst.
  - move=> A B s /ih tp sigma. move: (tp sigma). asimpl => /(Fty_tapp B.[sigma]). autosubst.
Qed.

Lemma ty_tbeta R Gamma s A B :
  Ty R Gamma..[ren (+1)] s A -> Ty R Gamma s A.[B/].
Proof.
  move=> /upto_tysubst/(_ (B .: ids)). autosubst.
Qed.

Lemma ty_tsubst R Gamma s A sigma :
  Ty R Gamma s A -> Ty R Gamma..[sigma] s A.[sigma].
Proof. move=> /upto_tysubst. exact. Qed.

Lemma ty_subst Gamma Delta sigma s A :
  ty Gamma s A ->
  (forall x, x < size Gamma -> ty Delta (sigma x) Gamma`_x) ->
  ty Delta s.[sigma] A.
Proof.
  move: Gamma Delta sigma s A. pattern ty at 1.
  apply ind => /=[|R ih]. move=> T F ih Gamma Delta sigma s A [i]. exact: ih.
  move=> Gamma Delta sigma s A []{s A}.
  - move=> x ltn /=. exact.
  - move=> A B s tp h /=. apply: ty_abs. apply: ih tp _ => -[_|x/h]; asimpl.
    exact: ty_var. exact: ty_weak.
  - move=> A B s t /ih tp1 /ih tp2 h /=. apply: ty_app; by [exact: tp1|exact: tp2].
  - move=> A s /ih tp h. apply: ty_tabs. apply: tp => x.
    rewrite size_map => ltn. rewrite get_map //. apply: ty_tsubst. exact: h.
  - move=> A B s /ih tp h. apply: ty_tapp. exact: tp.
Qed.

Lemma ty_beta Gamma s t A B :
  ty (A :: Gamma) s B -> ty Gamma t A -> ty Gamma s.[t/] B.
Proof.
  move=> /ty_subst tp1 tp2. apply: tp1 => -[_|x]//=. exact: ty_var.
Qed.

Lemma ty_lam_inv R Gamma s A B :
  Ty R Gamma (Lam s) (TFun A B) -> Ty R (A :: Gamma) s B.
Proof.
  (* First induction *)
  move: Gamma s A B. apply ind => /=[|{R}R ih].
  { move=> /= I F h Gamma s A B [i fx]. exists i. exact: h. }
  move=> Gamma s A B tp. apply: ty_unfold.
  (* proof step *)
  inv tp => //. move: A0 B0 H1 H => C D h1 h2. apply: ih.
  rewrite -h2 => {h2}. move: h1. move: Gamma s {A B} C D.
  (* Second induction *)
  apply ind => /=[|{R}R ih].
  { move=> /= I F h Gamma s A B [i fx]. exists i. exact: h. }
  move=> Gamma s A B tp. apply: ty_unfold.
  (* proof step *)
  inv tp. exact: ty_tbeta. move: H1 => /ih h. move: (h B0).
  rewrite H. exact: ih.
Qed.

Theorem preservation Gamma s t A :
  ty Gamma s A -> step s t -> ty Gamma t A.
Proof.
  move: Gamma s t A. pattern ty at 1.
  apply: ind => /=[T F ih|R ih] Gamma s t A. case=> i. exact: ih. case=> {s A}.
  - move=> x lt st. by inv st.
  - move=> A B s /ih tp st. inv st. apply: ty_abs. exact: tp.
  - move=> A B s a tp1 tp2 st. inv st.
    + apply ty_lam_inv in tp1. exact: ty_beta (ty_ty tp1) (ty_ty tp2).
    + move: tp1 => /ih/(_ H2) tp1. exact: ty_app (ty_ty tp1) (ty_ty tp2).
    + move: tp2 => /ih/(_ H2) tp2. exact: ty_app (ty_ty tp1) (ty_ty tp2).
  - move=> A s /ih tp st. apply ty_tabs. exact: tp.
  - move=> A B s /ih tp st. apply: ty_tapp. exact: tp.
Qed.