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

Definition cmorph {m n} (f : subst m n) (Gamma : ctx m) (Delta : ctx n) :=
  forall s A, Gamma s A -> Delta (inst f s) (inst f A).

Notation "[ Gamma |- sigma -| Delta ]" :=
  (cmorph sigma Gamma Delta).

Lemma tysubst_ids m (Gamma : ctx m) :
  [ Gamma |- @var _ -| Gamma ].
Proof.
  move=> s A e. rewrite !inst_ids. exact: e.
Qed.

Lemma tysubst_var m (Gamma : ctx m) :
  [ Gamma |- @var _ -| has_type Gamma ].
Proof.
  move=> s A e. rewrite !inst_ids. exact: ty_var.
Qed.

Lemma tysubst_comp m n k (Gamma : ctx m) (Delta : ctx n) (Theta : ctx k) (f : subst m n) (g : subst n k) :
  [ Gamma |- f -| Delta ] -> [ Delta |- g -| Theta ] -> [ Gamma |- f >> inst g -| Theta ].
Proof.
  move=> h1 h2 s A /h1/h2. by rewrite !inst_comp.
Qed.

Lemma tysubst_ren_comp m n k (Gamma : ctx m) (Delta : ctx n) (Theta : ctx k) (f : subst m n) (g : ren n k) :
  [ Gamma |- f -| Delta ] -> [ Delta |- g >> @var _ -| Theta ] -> [ Gamma |- f >> rename g -| Theta ].
Proof.
  move=> /tysubst_comp h/h{h}h s A e. rewrite -!inst_ren_comp !ren_inst !inst_comp. exact: h.
Qed.

Lemma tysubst_shift m (A : tm m) (Gamma : ctx m) :
  [ Gamma |- shift >> @var _ -| ext Gamma A ].
Proof.
  move=> s B e. rewrite -!ren_inst. apply: ext_shift. exact: e.
Qed.

Lemma tysubst_cons m n (sigma : subst m n) (Gamma : ctx m) (Delta : ctx n) (s : tm n) (A : tm m) :
  Delta s (inst sigma A) -> [ Gamma |- sigma -| Delta ] -> [ ext Gamma A |- s .: sigma -| Delta ].
Proof.
  move=> h1 h2 t B e. inv e=> /=; rewrite !ren_inst_comp; fsimpl.
  exact: h1. apply: h2. exact: H.
Qed.

Lemma tysubst_up m n (sigma : subst m n) (Gamma : ctx m) (Delta : ctx n) A :
  [ Gamma |- sigma -| Delta ] -> [ ext Gamma A |- upi sigma -| ext Delta (inst sigma A) ].
Proof.
  move=> h. unfold upi. apply: tysubst_cons. rewrite -inst_ren_comp. apply: ext_bound.
  apply: tysubst_ren_comp h _. exact: tysubst_shift.
Qed.

Lemma ty_map m n (sigma : subst m n) (Gamma : ctx m) (Delta : ctx n) s A :
  [ Gamma |- s :- A ] ->
  [ Gamma |- sigma -| Delta ] ->
  [ Delta |- inst sigma s :- inst sigma A ].
Proof.
  move=> tp. elim: tp n sigma Delta => {m Gamma s A} /=
    [m Gamma t B si|m Gamma u|m Gamma A B s t _ ih1 _ ih2|
     m Gamma A B s u _ ih1 _ ih2|m Gamma A B u v _ ih1 _ ih2|
     m Gamma u A B s sub _ ih1 _ ih2]
    n sigma Delta tp //=.
  - apply: ty_var. exact: tp.
  - apply: ty_eapp (ih1 _ _ _ tp) (ih2 _ _ _ tp).
    rewrite !inst_comp; f_equal; fext=>/=; case=>//=i.
    rewrite ren_inst_comp. fsimpl. by rewrite inst_ids.
  - apply: ty_lam. exact: ih1. apply: ih2. exact: tysubst_up.
  - apply: ty_prod. exact: ih1. apply: ih2. exact: tysubst_up.
  - apply: ty_sub; last first. exact: ih2. exact: ih1. exact: sub_inst.
Qed.

Lemma weakening n (Gamma : ctx n) s A B :
  [ Gamma |- s :- A ] -> [ ext Gamma B |- rename shift s :- rename shift A ].
Proof. rewrite !ren_inst => /ty_map. apply. exact: tysubst_shift. Qed.

Lemma eweakening n (Gamma : ctx n) s s' A A' B :
  s' = rename shift s -> A' = rename shift A ->
  [ Gamma |- s :- A ] -> [ ext Gamma B |- s' :- A' ].
Proof. move=>->->. exact: weakening. Qed.

Lemma tysubst_upi m n (sigma : subst m n) (Gamma : ctx m) (Delta : ctx n) A :
  [ Gamma |- sigma -| has_type Delta ] ->
  [ ext Gamma A |- upi sigma -| has_type (ext Delta (inst sigma A)) ].
Proof.
  move=> h. unfold upi. apply: tysubst_cons. rewrite -inst_ren_comp. apply: ty_var. exact: ext_bound.
  apply: tysubst_ren_comp h _. move=> s B /weakening e. rewrite -!ren_inst. exact: e.
Qed.

Lemma ty_subst m n (sigma : subst m n) Gamma Delta s A :
  [ Gamma |- sigma -| has_type Delta ] -> [ Gamma |- s :- A ] ->
  [ Delta |- inst sigma s :- inst sigma A ].
Proof.
  move=> stp tp. elim: tp n sigma Delta stp => {m Gamma s A} /=
    [m Gamma t B si|m Gamma u|m Gamma A B s t _ ih1 _ ih2|
     m Gamma A B s u _ ih1 _ ih2|m Gamma A B u v _ ih1 _ ih2|
     m Gamma u A B s sub _ ih1 _ ih2]
    n sigma Delta tp //=.
  - exact: tp.
  - apply: ty_eapp; last first. exact: ih2. exact: ih1.
    rewrite !inst_comp; f_equal; fext=>/=; case=>//=i.
    rewrite ren_inst_comp. fsimpl. by rewrite inst_ids.
  - eapply ty_lam. by eapply ih1. apply: ih2. exact: tysubst_upi.
  - apply: ty_prod. exact: ih1. apply ih2. exact: tysubst_upi.
  - apply: ty_sub; last first. exact: ih2. exact: ih1. exact: sub_inst.
Qed.

Lemma ty_cut n (Gamma : ctx n) s t A B :
  [ ext Gamma A |- s :- B ] -> [ Gamma |- t :- A ] ->
  [ Gamma |- inst (t .: @var _) s :- inst (t .: @var _) B ].
Proof.
  move=> /ty_subst h tp. apply: h. apply: tysubst_cons; last first.
  exact: tysubst_var. by rewrite inst_ids.
Qed.

Lemma ty_ctx_conv n (Gamma : ctx n) s A B C u :
  [ ext Gamma A |- s :- C ] -> B === A -> [ Gamma |- A :- univ n u ] ->
  [ ext Gamma B |- s :- C ].
Proof.
  move=> tp1 conv tp2. cut ([ ext Gamma B |- inst (@var _) s :- inst (@var _) C ]). by rewrite !inst_ids.
  apply: ty_subst tp1. move=> t T [|]{t T}.
  - rewrite ren_inst_comp /=. rewrite -ren_inst. apply: (@ty_sub _ _ _ (rename shift B)).
    + rewrite !ren_inst. apply: sub_inst. exact: conv_sub.
    + exact: eweakening tp2.
    + apply: ty_var. exact: ext_bound.
  - move=> t T e. rewrite !inst_ids. apply: ty_var. exact: ext_shift.
Qed.