Library STLC_Data_Soundness
Require Import List Metatheory
STLC_Data_Definitions
STLC_Data_Infrastructure.
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 substitution.
Lemma typing_subst : forall F U E t T z u,
(E & z ~ U & F) |= t ~: T ->
E |= u ~: U ->
(E & F) |= [z ~> u]t ~: T.
Typing is preserved by iterated substitution.
Lemma typing_substs : forall Us E xs ts t T,
length xs = length ts ->
typings E ts Us ->
E & (iter_push xs Us) |= t ~: T ->
E |= substs xs ts t ~: T.
Typing the result of pattern matching.
Lemma typing_pattern_match : forall p t T E ts Us,
Some ts = pat_match p t ->
E |= t ~: T ->
Us \= p ~: T ->
typings E ts Us.
Preservation (typing is preserved by reduction).
Lemma preservation_result : preservation.
Progress (a well-typed term is either a value or it can
take a step of reduction).
Lemma progress_result : progress.