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
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.
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).
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).
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).
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).
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).
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).
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)
.
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)
.
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
.
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)
.
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)
.
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.