Strong normalization of STLC with subtyping and intersection type

Inter.v

Require Import Autosubst.Autosubst.
Require Import Arith List Omega Program Relations.

Inductive type :=
  | Top
  | Arrow (S T : type)
  | Inter (S T : type).

Inductive sub : type -> type -> Prop :=
  | S_Refl T : sub T T
  | S_Trans T1 T2 T3 :
      sub T1 T2 ->
      sub T2 T3 ->
      sub T1 T3
  | S_Top T :
      sub T Top
  | S_Arrow S S' T T' :
      sub S' S ->
      sub T T' ->
      sub (Arrow S T) (Arrow S' T')
  | S_Inter1 S T :
      sub (Inter S T) S
  | S_Inter2 S T :
      sub (Inter S T) T
  | S_Inter3 T1 T2 T3 :
      sub T1 T2 ->
      sub T1 T3 ->
      sub T1 (Inter T2 T3)
  | S_Inter4 S T1 T2 :
      sub (Inter (Arrow S T1) (Arrow S T2)) (Arrow S (Inter T1 T2)).

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

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.

Inductive red : term -> term -> Prop :=
  | E_Abs t t' :
      red t t' ->
      red (Abs t) (Abs t')
  | E_AppL s s' t :
      red s s' ->
      red (App s t) (App s' t)
  | E_AppR s t t' :
      red t t' ->
      red (App s t) (App s t')
  | E_AppAbs s t :
      red (App (Abs s) t) s.[t/].

Inductive typed (Gamma : var -> type) : term -> type -> Prop :=
  | T_Var x T :
      Gamma x = T ->
      typed Gamma (Var x) T
  | T_Abs t S T :
      typed (S .: Gamma) t T ->
      typed Gamma (Abs t) (Arrow S T)
  | T_App s t S T :
      typed Gamma s (Arrow S T) ->
      typed Gamma t S ->
      typed Gamma (App s t) T
  | T_Sub t S T :
      typed Gamma t S ->
      sub S T ->
      typed Gamma t T.
Hint Constructors sub red typed Acc.

Lemma red_subst s t :
  red s t ->
  forall Sigma,
  red s.[Sigma] t.[Sigma].
Proof.
  induction 1; intros Sigma; simpl; eauto.
  - replace (s.[t/].[Sigma]) with (s.[up Sigma].[t.[Sigma]/]) by autosubst.
    constructor.
Qed.
Hint Resolve red_subst.

Lemma typed_weakening Delta t S :
  typed Delta t S ->
  forall Gamma T,
    (forall x, sub (Gamma x) (Delta x)) ->
    sub S T ->
    typed Gamma t T.
Proof.
  induction 1; intros Gamma_ T_ Henv HT; subst; eauto.
  - apply T_Sub with (S := Arrow S T); eauto.
    constructor.
    apply IHtyped; eauto.
    intros [| x]; simpl; eauto.
Qed.

Fixpoint reducible t : term -> Prop :=
  match t with
  | Top => Acc (fun s t => red t s)
  | Arrow T1 T2 => fun s => forall t,
      reducible T1 t ->
      reducible T2 (App s t)
  | Inter T1 T2 => fun t =>
      reducible T1 t /\
      reducible T2 t
  end.

Lemma CR2 T : forall s t,
  red s t ->
  reducible T s ->
  reducible T t.
Proof.
  induction T; intros ? ? ? Hreducible; simpl in *; eauto.
  - destruct Hreducible.
    eauto.
  - destruct Hreducible.
    eauto.
Qed.
Hint Resolve CR2.

Definition neutral t :=
  match t with
  | Abs _ => False
  | _ => True
  end.
Hint Unfold neutral.

Lemma CR1_CR3 T :
  (forall t, reducible T t -> Acc (fun s t => red t s) t) /\
  (forall s, neutral s ->
    (forall t, red s t -> reducible T t) -> reducible T s).
Proof.
  induction T;
    (split; [ intros t Hreducible | intros t Hneutral Hred_reducible ]);
    simpl in *;
    repeat match goal with
    | H : _ /\ _ |- _ => destruct H
    end; eauto 7.
  - assert (Hc : reducible T1 (Var 0)).
    { apply H2; eauto.
      intros ? Hred.
      inversion Hred. }
    specialize (H _ (Hreducible _ Hc)).
    clear Hreducible.
    remember (App t (Var 0)) as t'.
    generalize dependent t.
    induction H; intros; subst.
    eauto.
  - intros ? Hreducible1.
    apply H0; eauto.
    specialize (H1 _ Hreducible1).
    induction H1.
    intros ? Hred.
    inversion Hred; subst; eauto.
    inversion Hneutral.
  - split;
      [ apply H2 | apply H0 ]; eauto;
      intros ? Hred;
      destruct (Hred_reducible _ Hred);
      eauto.
Qed.

Definition CR1 t := proj1 (CR1_CR3 t).
Definition CR3 t := proj2 (CR1_CR3 t).
Hint Resolve CR1.

Lemma reducible_abs : forall t12 T1 T2,
  (forall t1, reducible T1 t1 -> reducible T2 (t12.[t1/])) ->
  reducible (Arrow T1 T2) (Abs t12).
Proof.
  simpl.
  intros ? ? ? Hsubst ? Hreducible.
  generalize (CR1 _ _ Hreducible). intros HSN.
  generalize (CR1 _ _ (Hsubst _ Hreducible)). intros HSNsubst.
  generalize dependent t12.
  induction HSN as [? ? IH].
  intros.
  remember (t12.[x/]) as t.
  generalize dependent t12.
  generalize dependent x.
  induction HSNsubst as [? ? IH'].
  intros.
  apply CR3; eauto.
  intros ? Hred.
  inversion Hred; subst; eauto 7.
  inversion H4; subst.
  eapply IH'; try reflexivity; eauto.
Qed.

Lemma sub_reducible : forall t t',
  sub t t' ->
  forall e,
  reducible t e ->
  reducible t' e.
Proof.
  induction 1; simpl; intros;
    repeat match goal with
    | H : _ /\ _ |- _ => destruct H
    end; eauto.
Qed.

Lemma fundamental_property : forall Gamma t T,
  typed Gamma t T ->
  forall Sigma,
    (forall x, reducible (Gamma x) (Sigma x)) ->
    reducible T t.[Sigma].
Proof.
  induction 1; simpl in *; intros Sigma Henv; subst; eauto.
  - apply reducible_abs.
    intros t1 Ht1.
    rewrite subst_comp.
    apply IHtyped.
    intros [| x ]; simpl; eauto.
    autosubst.
  - eapply sub_reducible; eauto.
Qed.

Theorem strong_normalization Gamma t T :
  typed Gamma t T ->
  Acc (fun s t => red t s) t.
Proof.
  intros Htyped.
  eapply CR1.
  rewrite <- subst_id.
  eapply fundamental_property; eauto.
  intros x.
  apply CR3; simpl; eauto.
  intros ? Hcontra.
  inversion Hcontra.
Qed.