Library STLC_Core_Soundness

Require Import Metatheory
  STLC_Core_Definitions
  STLC_Core_Infrastructure.

Proofs


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.

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.