Library Tagged_Definitions

Definition of Fsub (System F with subtyping).

We collapse the syntax of types of expressions into one inductive datatype. We retain only one constructor each for bound and free variables.

NOTE: We define a number of Notations which are used only for parsing, since the code here is directly copied from another development. The notations help smooth over trivial differences in the names of lemmas and functions.

Require Export Metatheory.
Require Export Common.

Syntax (pre-terms)


Inductive syntax : tag -> Set :=
  | bvar : forall T, nat -> syntax T
  | fvar : forall T, atom -> syntax T
  | typ_top : syntax Typ
  | typ_arrow : syntax Typ -> syntax Typ -> syntax Typ
  | typ_all : syntax Typ -> syntax Typ -> syntax Typ
  | typ_sum : syntax Typ -> syntax Typ -> syntax Typ
  | exp_abs : syntax Typ -> syntax Exp -> syntax Exp
  | exp_app : syntax Exp -> syntax Exp -> syntax Exp
  | exp_tabs : syntax Typ -> syntax Exp -> syntax Exp
  | exp_tapp : syntax Exp -> syntax Typ -> syntax Exp
  | exp_let : syntax Exp -> syntax Exp -> syntax Exp
  | exp_inl : syntax Exp -> syntax Exp
  | exp_inr : syntax Exp -> syntax Exp
  | exp_case : syntax Exp -> syntax Exp -> syntax Exp -> syntax Exp
.

Implicit Arguments bvar [T].
Implicit Arguments fvar [T].

NOTE: We lose the ability to declare bvar and fvar as coercions.

Notation typ_bvar := (@bvar Typ) (only parsing).
Notation typ_fvar := (@fvar Typ) (only parsing).
Notation exp_bvar := (@bvar Exp) (only parsing).
Notation exp_fvar := (@fvar Exp) (only parsing).

Notation typ := (syntax Typ) (only parsing).
Notation exp := (syntax Exp) (only parsing).

Opening terms



Definition tagCheck : forall (A B : tag), syntax A -> syntax B -> syntax B :=
  fun A : tag =>
    match A as t return (forall B : tag, syntax t -> syntax B -> syntax B) with
      | Typ =>
        fun B : tag =>
          match B as t return (syntax Typ -> syntax t -> syntax t) with
            | Typ => fun x _ => x
            | Exp => fun _ y => y
          end
      | Exp =>
        fun B : tag =>
          match B as t return (syntax Exp -> syntax t -> syntax t) with
            | Typ => fun _ y => y
            | Exp => fun x _ => x
          end
    end.

Fixpoint open_rec
  (A B : tag) (K : nat) (U : syntax B) (T : syntax A) {struct T} : syntax A
:=
  match T in syntax A return syntax A with
  | bvar _ J => if K === J then tagCheck U (bvar J) else (bvar J)
  | fvar _ X => fvar X
  | typ_top => typ_top
  | typ_arrow T1 T2 => typ_arrow (open_rec K U T1) (open_rec K U T2)
  | typ_all T1 T2 => typ_all (open_rec K U T1) (open_rec (S K) U T2)
  | typ_sum T1 T2 => typ_sum (open_rec K U T1) (open_rec K U T2)
  | exp_abs V e1 => exp_abs (open_rec K U V) (open_rec (S K) U e1)
  | exp_app e1 e2 => exp_app (open_rec K U e1) (open_rec K U e2)
  | exp_tabs V e1 => exp_tabs (open_rec K U V) (open_rec (S K) U e1)
  | exp_tapp e1 V => exp_tapp (open_rec K U e1) (open_rec K U V)
  | exp_let e1 e2 => exp_let (open_rec K U e1) (open_rec (S K) U e2)
  | exp_inl e1 => exp_inl (open_rec K U e1)
  | exp_inr e2 => exp_inr (open_rec K U e2)
  | exp_case e1 e2 e3 =>
      exp_case (open_rec K U e1) (open_rec (S K) U e2) (open_rec (S K) U e3)
end.

Definition open (A B : tag) (T : syntax B) (U : syntax A) := open_rec 0 U T.


Notation open_tt := open (only parsing).
Notation open_te := open (only parsing).
Notation open_ee := open (only parsing).

Free variables



Fixpoint fv (A : tag) (T : syntax A) {struct T} : atoms :=
  match T with
  | bvar _ J => {}
  | fvar _ X => singleton X
  | typ_top => {}
  | typ_arrow T1 T2 => (fv T1) `union` (fv T2)
  | typ_all T1 T2 => (fv T1) `union` (fv T2)
  | typ_sum T1 T2 => (fv T1) `union` (fv T2)
  | exp_abs V e1 => (fv V) `union` (fv e1)
  | exp_app e1 e2 => (fv e1) `union` (fv e2)
  | exp_tabs V e1 => (fv V) `union` (fv e1)
  | exp_tapp e1 V => (fv V) `union` (fv e1)
  | exp_let e1 e2 => (fv e1) `union` (fv e2)
  | exp_inl e1 => (fv e1)
  | exp_inr e1 => (fv e1)
  | exp_case e1 e2 e3 => (fv e1) `union` (fv e2) `union` (fv e3)
  end.


Notation fv_tt := fv (only parsing).
Notation fv_te := fv (only parsing).
Notation fv_ee := fv (only parsing).

Substitution



Fixpoint subst
  (A B : tag) (Z : atom) (U : syntax B) (T : syntax A) {struct T} : syntax A
:=
  match T in syntax A return syntax A with
  | bvar _ J => bvar J
  | fvar _ X => if X == Z then tagCheck U (fvar X) else (fvar X)
  | typ_top => typ_top
  | typ_arrow T1 T2 => typ_arrow (subst Z U T1) (subst Z U T2)
  | typ_all T1 T2 => typ_all (subst Z U T1) (subst Z U T2)
  | typ_sum T1 T2 => typ_sum (subst Z U T1) (subst Z U T2)
  | exp_abs V e1 => exp_abs (subst Z U V) (subst Z U e1)
  | exp_app e1 e2 => exp_app (subst Z U e1) (subst Z U e2)
  | exp_tabs V e1 => exp_tabs (subst Z U V) (subst Z U e1)
  | exp_tapp e1 V => exp_tapp (subst Z U e1) (subst Z U V)
  | exp_let e1 e2 => exp_let (subst Z U e1) (subst Z U e2)
  | exp_inl e1 => exp_inl (subst Z U e1)
  | exp_inr e1 => exp_inr (subst Z U e1)
  | exp_case e1 e2 e3 =>
      exp_case (subst Z U e1) (subst Z U e2) (subst Z U e3)
  end.


Notation subst_tt := subst (only parsing).
Notation subst_te := subst (only parsing).
Notation subst_ee := subst (only parsing).

Local closure



Inductive lc : forall A : tag, syntax A -> Prop :=
  | lc_var : forall (A : tag) (X : atom),
      lc (@fvar A X)
  | type_top :
      lc typ_top
  | type_arrow : forall T1 T2,
      lc T1 ->
      lc T2 ->
      lc (typ_arrow T1 T2)
  | type_all : forall L T1 T2,
      lc T1 ->
      (forall X : atom, X `notin` L -> lc (open T2 (typ_fvar X))) ->
      lc (typ_all T1 T2)
  | type_sum : forall T1 T2,
      lc T1 ->
      lc T2 ->
      lc (typ_sum T1 T2)
  | expr_abs : forall L T e1,
      lc T ->
      (forall x : atom, x `notin` L -> lc (open e1 (exp_fvar x))) ->
      lc (exp_abs T e1)
  | expr_app : forall e1 e2,
      lc e1 ->
      lc e2 ->
      lc (exp_app e1 e2)
  | expr_tabs : forall L T e1,
      lc T ->
      (forall X : atom, X `notin` L -> lc (open e1 (typ_fvar X))) ->
      lc (exp_tabs T e1)
  | expr_tapp : forall e1 V,
      lc e1 ->
      lc V ->
      lc (exp_tapp e1 V)
  | expr_let : forall L e1 e2,
      lc e1 ->
      (forall x : atom, x `notin` L -> lc (open e2 (exp_fvar x))) ->
      lc (exp_let e1 e2)
  | expr_inl : forall e1,
      lc e1 ->
      lc (exp_inl e1)
  | expr_inr : forall e1,
      lc e1 ->
      lc (exp_inr e1)
  | expr_case : forall L e1 e2 e3,
      lc e1 ->
      (forall x : atom, x `notin` L -> lc (open e2 (exp_fvar x))) ->
      (forall x : atom, x `notin` L -> lc (open e3 (exp_fvar x))) ->
      lc (exp_case e1 e2 e3).


Notation type := lc (only parsing).
Notation expr := lc (only parsing).

Environments


Inductive binding : Set :=
  | bind_sub : typ -> binding
  | bind_typ : typ -> binding.

Notation env := (list (atom * binding)).
Notation empty := (@nil (atom * binding)).

Notation "[ x ]" := (x :: nil).

Definition subst_tb (Z : atom) (P : typ) (b : binding) : binding :=
  match b with
    | bind_sub T => bind_sub (subst_tt Z P T)
    | bind_typ T => bind_typ (subst_tt Z P T)
  end.

Notation senv := (list (atom * tag)).

Definition to_tag (b : binding) : tag :=
  match b with
    | bind_sub _ => Typ
    | bind_typ _ => Exp
  end.

Notation to_senv := (map to_tag).

Well-formedness


Inductive wf_typ : senv -> typ -> Prop :=
  | wf_typ_top : forall E,
      ok E ->
      wf_typ E typ_top
  | wf_typ_var : forall E (X : atom),
      ok E ->
      binds X Typ E ->
      wf_typ E (typ_fvar X)
  | wf_typ_arrow : forall E T1 T2,
      wf_typ E T1 ->
      wf_typ E T2 ->
      wf_typ E (typ_arrow T1 T2)
  | wf_typ_all : forall L E T1 T2,
      wf_typ E T1 ->
      (forall X : atom, X `notin` L ->
        wf_typ ([(X, Typ)] ++ E) (open_tt T2 (@fvar Typ X))) ->
      wf_typ E (typ_all T1 T2)
  | wf_typ_sum : forall E T1 T2,
      wf_typ E T1 ->
      wf_typ E T2 ->
      wf_typ E (typ_sum T1 T2)
.

Inductive wf_exp : senv -> exp -> Prop :=
  | wf_exp_var : forall E (x : atom),
      ok E ->
      binds x Exp E->
      wf_exp E (exp_fvar x)
  | wf_exp_abs : forall L E T e,
      wf_typ E T ->
      (forall x : atom, x `notin` L ->
        wf_exp ([(x,Exp)] ++ E) (open_ee e (@fvar Exp x))) ->
      wf_exp E (exp_abs T e)
  | wf_exp_app : forall E e1 e2,
      wf_exp E e1 ->
      wf_exp E e2 ->
      wf_exp E (exp_app e1 e2)
  | wf_exp_tabs : forall L E T e,
      wf_typ E T ->
      (forall X : atom, X `notin` L ->
        wf_exp ([(X,Typ)] ++ E) (open_te e (@fvar Typ X))) ->
      wf_exp E (exp_tabs T e)
  | wf_exp_tapp : forall E e T,
      wf_exp E e ->
      wf_typ E T ->
      wf_exp E (exp_tapp e T)
  | wf_exp_let : forall L E e1 e2,
      wf_exp E e1 ->
      (forall x : atom, x `notin` L ->
        wf_exp ([(x,Exp)] ++ E) (open_ee e2 (@fvar Exp x))) ->
      wf_exp E (exp_let e1 e2)
  | wf_exp_inl : forall E e,
      wf_exp E e ->
      wf_exp E (exp_inl e)
  | wf_exp_inr : forall E e,
      wf_exp E e ->
      wf_exp E (exp_inr e)
  | wf_exp_case : forall L E e1 e2 e3,
      wf_exp E e1 ->
      (forall x : atom, x `notin` L ->
        wf_exp ([(x,Exp)] ++ E) (open_ee e2 (@fvar Exp x))) ->
      (forall x : atom, x `notin` L ->
        wf_exp ([(x,Exp)] ++ E) (open_ee e3 (@fvar Exp x))) ->
      wf_exp E (exp_case e1 e2 e3).

Inductive wf_env : env -> Prop :=
  | wf_env_empty :
      wf_env empty
  | wf_env_sub : forall (E : env) (X : atom) (T : typ),
      wf_env E ->
      wf_typ (to_senv E) T ->
      X `notin` dom E ->
      wf_env ([(X, bind_sub T)] ++ E)
  | wf_env_typ : forall (E : env) (x : atom) (T : typ),
      wf_env E ->
      wf_typ (to_senv E) T ->
      x `notin` dom E ->
      wf_env ([(x, bind_typ T)] ++ E)
.

Subtyping


Inductive sub : env -> typ -> typ -> Prop :=
  | sub_top : forall E S,
      wf_env E ->
      wf_typ (to_senv E) S ->
      sub E S typ_top
  | sub_refl_tvar : forall E X,
      wf_env E ->
      wf_typ (to_senv E) (typ_fvar X) ->
      sub E (typ_fvar X) (typ_fvar X)
  | sub_trans_tvar : forall U E T X,
      binds X (bind_sub U) E ->
      sub E U T ->
      sub E (typ_fvar X) T
  | sub_arrow : forall E S1 S2 T1 T2,
      sub E T1 S1 ->
      sub E S2 T2 ->
      sub E (typ_arrow S1 S2) (typ_arrow T1 T2)
  | sub_all : forall L E S1 S2 T1 T2,
      sub E T1 S1 ->
      (forall X : atom, X `notin` L ->
          sub ([(X, bind_sub T1)] ++ E) (open_tt S2 (@fvar Typ X)) (open_tt T2 (@fvar Typ X))) ->
      sub E (typ_all S1 S2) (typ_all T1 T2)
  | sub_sum : forall E S1 S2 T1 T2,
      sub E S1 T1 ->
      sub E S2 T2 ->
      sub E (typ_sum S1 S2) (typ_sum T1 T2)
.

Typing


Inductive typing : env -> exp -> typ -> Prop :=
  | typing_var : forall E x T,
      wf_env E ->
      binds x (bind_typ T) E ->
      typing E (exp_fvar x) T
  | typing_abs : forall L E V e1 T1,
      (forall x : atom, x `notin` L ->
        typing ([(x, bind_typ V)] ++ E) (open_ee e1 (@fvar Exp x)) T1) ->
      typing E (exp_abs V e1) (typ_arrow V T1)
  | typing_app : forall T1 E e1 e2 T2,
      typing E e1 (typ_arrow T1 T2) ->
      typing E e2 T1 ->
      typing E (exp_app e1 e2) T2
  | typing_tabs : forall L E V e1 T1,
      (forall X : atom, X `notin` L ->
        typing ([(X, bind_sub V)] ++ E) (open_te e1 (@fvar Typ X)) (open_tt T1 (@fvar Typ X))) ->
      typing E (exp_tabs V e1) (typ_all V T1)
  | typing_tapp : forall T1 E e1 T T2,
      typing E e1 (typ_all T1 T2) ->
      sub E T T1 ->
      typing E (exp_tapp e1 T) (open_tt T2 T)
  | typing_sub : forall S E e T,
      typing E e S ->
      sub E S T ->
      typing E e T
  | typing_let : forall L T1 T2 e1 e2 E,
      typing E e1 T1 ->
      (forall x, x `notin` L ->
        typing ([(x, bind_typ T1)] ++ E) (open_ee e2 (@fvar Exp x)) T2) ->
      typing E (exp_let e1 e2) T2
  | typing_inl : forall T1 T2 e1 E,
      typing E e1 T1 ->
      wf_typ (to_senv E) T2 ->
      typing E (exp_inl e1) (typ_sum T1 T2)
  | typing_inr : forall T1 T2 e1 E,
      typing E e1 T2 ->
      wf_typ (to_senv E) T1 ->
      typing E (exp_inr e1) (typ_sum T1 T2)
  | typing_case : forall L T1 T2 T e1 e2 e3 E,
      typing E e1 (typ_sum T1 T2) ->
      (forall x : atom, x `notin` L ->
        typing ([(x, bind_typ T1)] ++ E) (open_ee e2 (@fvar Exp x)) T) ->
      (forall x : atom, x `notin` L ->
        typing ([(x, bind_typ T2)] ++ E) (open_ee e3 (@fvar Exp x)) T) ->
      typing E (exp_case e1 e2 e3) T
.

Values


Inductive value : exp -> Prop :=
  | value_abs : forall E T e1,
      wf_exp E (exp_abs T e1) ->
      value (exp_abs T e1)
  | value_tabs : forall E T e1,
      wf_exp E (exp_tabs T e1) ->
      value (exp_tabs T e1)
  | value_inl : forall e1,
      value e1 ->
      value (exp_inl e1)
  | value_inr : forall e1,
      value e1 ->
      value (exp_inr e1)
.

Reduction


Inductive red : exp -> exp -> Prop :=
  | red_app_1 : forall E e1 e1' e2,
      wf_exp E (exp_app e1 e2) ->
      red e1 e1' ->
      red (exp_app e1 e2) (exp_app e1' e2)
  | red_app_2 : forall E e1 e2 e2',
      wf_exp E (exp_app e1 e2) ->
      value e1 ->
      red e2 e2' ->
      red (exp_app e1 e2) (exp_app e1 e2')
  | red_tapp : forall E e1 e1' V,
      wf_exp E (exp_tapp e1 V) ->
      red e1 e1' ->
      red (exp_tapp e1 V) (exp_tapp e1' V)
  | red_abs : forall E T e1 v2,
      wf_exp E (exp_app (exp_abs T e1) v2) ->
      value v2 ->
      red (exp_app (exp_abs T e1) v2) (open_ee e1 v2)
  | red_tabs : forall E T1 e1 T2,
      wf_exp E (exp_tapp (exp_tabs T1 e1) T2) ->
      red (exp_tapp (exp_tabs T1 e1) T2) (open_te e1 T2)
  | red_let_1 : forall E e1 e1' e2,
      wf_exp E (exp_let e1 e2) ->
      red e1 e1' ->
      red (exp_let e1 e2) (exp_let e1' e2)
  | red_let : forall E v1 e2,
      wf_exp E (exp_let v1 e2) ->
      value v1 ->
      red (exp_let v1 e2) (open_ee e2 v1)
  | red_inl_1 : forall e1 e1',
      red e1 e1' ->
      red (exp_inl e1) (exp_inl e1')
  | red_inr_1 : forall e1 e1',
      red e1 e1' ->
      red (exp_inr e1) (exp_inr e1')
  | red_case_1 : forall E e1 e1' e2 e3,
      wf_exp E (exp_case e1 e2 e3) ->
      red e1 e1' ->
      red (exp_case e1 e2 e3) (exp_case e1' e2 e3)
  | red_case_inl : forall E v1 e2 e3,
      wf_exp E (exp_case (exp_inl v1) e2 e3) ->
      value v1 ->
      red (exp_case (exp_inl v1) e2 e3) (open_ee e2 v1)
  | red_case_inr : forall E v1 e2 e3,
      wf_exp E (exp_case (exp_inr v1) e2 e3) ->
      value v1 ->
      red (exp_case (exp_inr v1) e2 e3) (open_ee e3 v1)
.

Automation


Hint Constructors lc wf_typ wf_exp wf_env value red.
Hint Resolve sub_top sub_refl_tvar sub_arrow.
Hint Resolve sub_sum typing_inl typing_inr.
Hint Resolve typing_var typing_app typing_tapp typing_sub.
Hint Resolve typing_inl typing_inr.