Library ML_Core_Soundness
Require Import List Metatheory
ML_Core_Definitions
ML_Core_Infrastructure.
Typing schemes for expressions
Definition has_scheme_vars L E t M := forall Xs,
fresh L (sch_arity M) Xs ->
E |= t ~: (M ^ Xs).
Definition has_scheme E t M := forall Vs,
types (sch_arity M) Vs ->
E |= t ~: (M ^^ Vs).
Type substitution preserves typing
Lemma typing_typ_subst : forall F Z U E t T,
Z \notin (env_fv E) ->
type U ->
E & F |= t ~: T ->
E & (map (sch_subst Z U) F) |= t ~: (typ_subst Z U T).
Iterated type substitution preserves typing
Lemma typing_typ_substs : forall Zs Us E t T,
fresh (env_fv E) (length Zs) Zs ->
types (length Zs) Us ->
E |= t ~: T ->
E |= t ~: (typ_substs Zs Us T).
Type schemes of terms can be instanciated
Lemma has_scheme_from_vars : forall L E t M,
has_scheme_vars L E t M ->
has_scheme E t M.
A term that has type T has type scheme "forall(no_var).T"
Lemma has_scheme_from_typ : forall E t T,
E |= t ~: T -> has_scheme E t (Sch 0 T).
Typing is preserved by weakening
Lemma typing_weaken : forall G E F t T,
(E & G) |= t ~: T ->
ok (E & F & G) ->
(E & F & G) |= t ~: T.
Typing is preserved by term substitution
Lemma typing_trm_subst : forall F M E t T z u,
E & z ~ M & F |= t ~: T ->
has_scheme E u M ->
term u ->
E & F |= (trm_subst z u t) ~: T.
Preservation: typing is preserved by reduction
Lemma preservation_result : preservation.
Progress: typed terms are values or can reduce
Lemma progress_result : progress.