Library STLC_Core_Adequacy
Require Import Metatheory.
Require Import
STLC_Core_Definitions
STLC_Core_Infrastructure
STLC_Core_Soundness.
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'.
Lemma term_rename : forall x y t,
x \notin fv t -> term (t ^ x) ->
y \notin fv t -> term (t ^ y).
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.
Hint Constructors term eterm.
Lemma term_to_eterm : forall t,
term t -> eterm t.
Lemma eterm_to_term : forall t,
eterm t -> term t.
Hint Constructors value evalue.
Lemma value_to_evalue : forall t,
value t -> evalue t.
Lemma evalue_to_value : forall t,
evalue t -> value t.
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'.
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.