Library STLC_Ref_Soundness
Require Import Metatheory STLC_Ref_Definitions STLC_Ref_Infrastructure.
Hint Constructors typing.
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.
Typing is preserved by substitution.
Lemma typing_subst : forall F E P t T z u U,
(E & z ~ U & F) ! P |= t ~: T ->
E ! P |= u ~: U ->
(E & F) ! P |= [z ~> u]t ~: T.
Typing is preserved by an extension of store typing.
Lemma typing_stability : forall P E P' t T,
E ! P |= t ~: T ->
extends P 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).
A simple short-hand to help clarifying the following proof.
It simply destruct the induction hypothesis into smaller pieces.
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']]].
Preservation (typing is preserved by reduction).
Lemma preservation_result : preservation.
Progression (a well-typed term is either a value or it can
take a step of reduction).
Lemma progress_result : progress.