Library ML_Soundness

Require Import List Metatheory ML_Definitions ML_Infrastructure.

Lemma factorize_map : forall Z U xs Us,
   iter_push xs (List.map (Sch 0) (List.map (typ_subst Z U) Us))
 = (map (sch_subst Z U) (iter_push xs (List.map (Sch 0) Us))).

Typing schemes for expressions

Definition has_scheme_vars L E P t M := forall Xs,
  fresh L (sch_arity M) Xs ->
  E ! P |= t ~: (M ^ Xs).

Definition has_scheme E P t M := forall Vs,
  types (sch_arity M) Vs ->
  E ! P |= t ~: (M ^^ Vs).

Type substitution preserves typing of patterns

Lemma pat_typing_typ_subst : forall Z U Us p T,
  Us \= p ~: T ->
  List.map (typ_subst Z U) Us \= p ~: typ_subst Z U T.

Type substitution preserves typing of expressions

Lemma typing_typ_subst : forall F P Z U E t T,
  Z \notin (env_fv E) -> Z \notin (phi_fv P) ->   type U ->
  E & F ! P |= t ~: T ->
  E & (map (sch_subst Z U) F) ! P |= t ~: (typ_subst Z U T).

Iterated type substitution preserves typing

Lemma typing_typ_substs : forall Zs Us E P t T,
  fresh (env_fv E \u phi_fv P) (length Zs) Zs ->
  types (length Zs) Us ->
  E ! P |= t ~: T ->
  E ! P |= t ~: (typ_substs Zs Us T).

Type schemes can be instanciated

Lemma has_scheme_from_vars : forall L E P t M,
  has_scheme_vars L E P t M ->
  has_scheme E P t M.

A term that has type T has type scheme "forall(no_var).T"

Lemma has_scheme_from_typ : forall E P t T,
  E ! P |= t ~: T ->
  has_scheme E P t (Sch 0 T).

Typing is preserved by weakening

Lemma typing_weaken : forall G E F P t T,
   (E & G) ! P |= t ~: T ->
   ok (E & F & G) ->
   (E & F & G) ! P |= t ~: T.

Values are preserved by term substitution

Lemma value_fv : forall z u t,
  value u -> value t -> value ([z ~> u]t).

Typing is preserved by term substitution

Lemma typing_trm_subst : forall F M E P t T z u,
  E & z ~ M & F ! P |= t ~: T ->
  has_scheme E P u M ->
  value u ->
  E & F ! P |= (trm_subst z u t) ~: T.

Typing is preserved by iterated term substitution.

Lemma typing_trm_substs : forall Us E P xs ts t T,
   length xs = length ts ->
   typings E P ts Us ->
   (E & (iter_push xs (List.map (Sch 0) Us))) ! P |= t ~: T ->
   list_forall value ts ->
   E ! P |= substs xs ts t ~: T.

The result of pattern matching is a list of well-typed terms.

Lemma typing_pattern_match : forall p t T E P ts Us,
  Some ts = pat_match p t ->
  E ! P |= t ~: T ->
  Us \= p ~: T ->
  typings E P ts Us.

The result of pattern matching applied to a value is a list of values.

Lemma pattern_match_values : forall p t ts,
  Some ts = pat_match p t ->
  value t ->
  list_forall value ts.

Typing is preserved by an extension of store typing. (This result is added to hints because we use it many times.

Lemma typing_stability : forall P E P' t T,
  E ! P |= t ~: T ->
  extends P P' ->
  phi_ok P' ->
  E ! P' |= t ~: T.

Hint Resolve typing_stability.

Store typing preserved by allocation of a well-typed term.

Lemma sto_typing_push : forall P mu l t T,
  P |== mu ->
  empty ! P |= t ~: T ->
  l # mu -> l # P ->
  (P & l ~ T) |== (mu & l ~ t).

Fails always returns an exception.

Lemma fails_to_exception : forall E P t T e,
  fails t e ->
  E ! P |= t ~: T ->
  E ! P |= e ~: typ_exn.

Preservation: typing is preserved by reduction

Ltac pres H t' mu' :=
  let P' := fresh "P'" in
  let Ext := fresh "Ext" in
  let Typt' := fresh "Typt'" in
  let TypSto' := fresh "TypSto'" in
  destruct~ (H (@refl_equal env empty) t' mu')
                  as [P' [Ext [Typt' TypSto']]].

Lemma preservation_result : preservation.

A value cannot be reduced (needed for the let case of progress).

Lemma red_value_false : forall t, value t ->
  forall t' mu mu', (t, mu) --> (t', mu') -> False.

Progress: typed terms are values or can reduce

Hint Constructors fails.

Lemma progress_result : progress.