Library STLC_Data_Soundness

Require Import List Metatheory
  STLC_Data_Definitions
  STLC_Data_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.

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.