Library STLC_Ref_Soundness

Require Import Metatheory STLC_Ref_Definitions STLC_Ref_Infrastructure.

Proofs


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.