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.