Library STLC_Core_Adequacy

Require Import Metatheory.

Require Import
  STLC_Core_Definitions
  STLC_Core_Infrastructure
  STLC_Core_Soundness.

Definitions with the exists-fresh quantification


Terms are locally-closed pre-terms

Inductive eterm : trm -> Prop :=
  | eterm_var : forall x,
      eterm (trm_fvar x)
  | eterm_abs : forall x t1,
      x \notin fv t1 ->
      eterm (t1 ^ x) ->
      eterm (trm_abs t1)
  | eterm_app : forall t1 t2,
      eterm t1 ->
      eterm t2 ->
      eterm (trm_app t1 t2).

Typing relation

Reserved Notation "E |== t ~: T" (at level 69).

Inductive etyping : env -> trm -> typ -> Prop :=
  | etyping_var : forall E x T,
      ok E ->
      binds x T E ->
      E |== (trm_fvar x) ~: T
  | etyping_abs : forall x E U T t1,
      x \notin dom E \u fv t1 ->
      (E & x ~ U) |== (t1 ^ x) ~: T ->
      E |== (trm_abs t1) ~: (typ_arrow U T)
  | etyping_app : forall S T E t1 t2,
      E |== t1 ~: (typ_arrow S T) ->
      E |== t2 ~: S ->
      E |== (trm_app t1 t2) ~: T

where "E |== t ~: T" := (etyping E t T).

Definition of values (only abstractions are values)

Inductive evalue : trm -> Prop :=
  | evalue_abs : forall t1,
      eterm (trm_abs t1) -> evalue (trm_abs t1).

Reduction relation - one step in call-by-value

Inductive ered : trm -> trm -> Prop :=
  | ered_beta : forall t1 t2,
      eterm (trm_abs t1) ->
      evalue t2 ->
      ered (trm_app (trm_abs t1) t2) (t1 ^^ t2)
  | ered_app_1 : forall t1 t1' t2,
      eterm t2 ->
      ered t1 t1' ->
      ered (trm_app t1 t2) (trm_app t1' t2)
  | ered_app_2 : forall t1 t2 t2',
      evalue t1 ->
      ered t2 t2' ->
      ered (trm_app t1 t2) (trm_app t1 t2').

Notation "t -->> t'" := (ered t t') (at level 68).

Goal is to prove preservation and progress

Definition epreservation := forall E t t' T,
  E |== t ~: T ->
  t -->> t' ->
  E |== t' ~: T.

Definition eprogress := forall t T,
  empty |== t ~: T ->
     evalue t
  \/ exists t', t -->> t'.

Detailed Proofs of Renaming Lemmas (without high automation)


Proving the renaming lemma for term.


Lemma term_rename : forall x y t,
  x \notin fv t -> term (t ^ x) ->
  y \notin fv t -> term (t ^ y).

Proving the renaming lemma for typing.


Lemma typing_rename : forall x y E t U T,
  x \notin dom E \u fv t -> (E & x ~ U) |= (t ^ x) ~: T ->
  y \notin dom E \u fv t -> (E & y ~ U) |= (t ^ y) ~: T.

Proofs of equivalence.


Proving the equivalence of term and eterm


Hint Constructors term eterm.

Lemma term_to_eterm : forall t,
  term t -> eterm t.

Lemma eterm_to_term : forall t,
  eterm t -> term t.

Proving the equivalence of value and evalue


Hint Constructors value evalue.

Lemma value_to_evalue : forall t,
  value t -> evalue t.

Lemma evalue_to_value : forall t,
  evalue t -> value t.

Proving the equivalence of red and ered


Hint Constructors red ered.

Lemma red_to_ered : forall t t',
  red t t' -> ered t t'.

Lemma ered_to_red : forall t t',
  ered t t' -> red t t'.

Proving the equivalence of typing and etyping


Hint Constructors typing etyping.

Lemma typing_to_etyping : forall E t T,
  E |= t ~: T -> E |== t ~: T.

Lemma etyping_to_typing : forall E t T,
  E |== t ~: T -> E |= t ~: T.