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.