Library STLC_Core_Light
Require Import Metatheory.
Grammar of types.
Inductive typ : Set :=
| typ_var : var -> typ
| typ_arrow : typ -> typ -> typ.
Grammar of pre-terms.
Inductive trm : Set :=
| trm_bvar : nat -> trm
| trm_fvar : var -> trm
| trm_abs : trm -> trm
| trm_app : trm -> trm -> trm.
Opening up abstractions
Fixpoint open_rec (k : nat) (u : trm) (t : trm) {struct t} : trm :=
match t with
| trm_bvar i => if k === i then u else (trm_bvar i)
| trm_fvar x => trm_fvar x
| trm_abs t1 => trm_abs (open_rec (S k) u t1)
| trm_app t1 t2 => trm_app (open_rec k u t1) (open_rec k u t2)
end.
Definition open t u := open_rec 0 u t.
Notation "{ k ~> u } t" := (open_rec k u t) (at level 67).
Notation "t ^^ u" := (open t u) (at level 67).
Notation "t ^ x" := (open t (trm_fvar x)).
Terms are locally-closed pre-terms
Inductive term : trm -> Prop :=
| term_var : forall x,
term (trm_fvar x)
| term_abs : forall L t1,
(forall x, x \notin L -> term (t1 ^ x)) ->
term (trm_abs t1)
| term_app : forall t1 t2,
term t1 ->
term t2 ->
term (trm_app t1 t2).
Environment is an associative list mapping variables to types.
Definition env := Env.env typ.
Typing relation
Reserved Notation "E |= t ~: T" (at level 69).
Inductive typing : env -> trm -> typ -> Prop :=
| typing_var : forall E x T,
ok E ->
binds x T E ->
E |= (trm_fvar x) ~: T
| typing_abs : forall L E U T t1,
(forall x, x \notin L ->
(E & x ~ U) |= t1 ^ x ~: T) ->
E |= (trm_abs t1) ~: (typ_arrow U T)
| typing_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" := (typing E t T).
Definition of values (only abstractions are values)
Inductive value : trm -> Prop :=
| value_abs : forall t1,
term (trm_abs t1) -> value (trm_abs t1).
Reduction relation - one step in call-by-value
Inductive red : trm -> trm -> Prop :=
| red_beta : forall t1 t2,
term (trm_abs t1) ->
value t2 ->
red (trm_app (trm_abs t1) t2) (t1 ^^ t2)
| red_app_1 : forall t1 t1' t2,
term t2 ->
red t1 t1' ->
red (trm_app t1 t2) (trm_app t1' t2)
| red_app_2 : forall t1 t2 t2',
value t1 ->
red t2 t2' ->
red (trm_app t1 t2) (trm_app t1 t2').
Notation "t --> t'" := (red t t') (at level 68).
Computing free variables of a term.
Fixpoint fv (t : trm) {struct t} : vars :=
match t with
| trm_bvar i => {}
| trm_fvar x => {{x}}
| trm_abs t1 => (fv t1)
| trm_app t1 t2 => (fv t1) \u (fv t2)
end.
Substitution for names
Fixpoint subst (z : var) (u : trm) (t : trm) {struct t} : trm :=
match t with
| trm_bvar i => trm_bvar i
| trm_fvar x => if x == z then u else (trm_fvar x)
| trm_abs t1 => trm_abs (subst z u t1)
| trm_app t1 t2 => trm_app (subst z u t1) (subst z u t2)
end.
Notation "[ z ~> u ] t" := (subst z u t) (at level 68).
Definition of the body of an abstraction
Definition body t :=
exists L, forall x, x \notin L -> term (t ^ x).
Tactic
gather_vars
returns a set of variables occurring in
the context of proofs, including domain of environments and
free variables in terms mentionned in the context.
Ltac gather_vars :=
let A := gather_vars_with (fun x : vars => x) in
let B := gather_vars_with (fun x : var => {{ x }}) in
let C := gather_vars_with (fun x : env => dom x) in
let D := gather_vars_with (fun x : trm => fv x) in
constr:(A \u B \u C \u D).
Tactic
pick_fresh x
adds to the context a new variable x
and a proof that it is fresh from all of the other variables
gathered by tactic gather_vars
.
Ltac pick_fresh Y :=
let L := gather_vars in (pick_fresh_gen L Y).
Tactic
apply_fresh T as y
takes a lemma T of the form
forall L ..., (forall x, x \notin L, P x) -> ... -> Q.
instanciate L to be the set of variables occuring in the
context (by gather_vars
), then introduces for the premise
with the cofinite quantification the name x as "y" (the second
parameter of the tactic), and the proof that x is not in L.
Tactic Notation "apply_fresh" constr(T) "as" ident(x) :=
apply_fresh_base T gather_vars x.
Tactic Notation "apply_fresh" "*" constr(T) "as" ident(x) :=
apply_fresh T as x; auto*.
Hint Constructors term value red.
Assume properties of substitution
Axiom subst_open_var : forall x y u t, y <> x -> term u ->
([x ~> u]t) ^ y = [x ~> u] (t ^ y).
Axiom subst_intro : forall x t u,
x \notin (fv t) -> term u ->
t ^^ u = [x ~> u](t ^ x).
Assume well-formedness always holds. The purpose of these tactics is
to save the user from fixing the details when he first wants
to set up the basic architecture of the proof. These assumptions
can be exploited to prove "False" and thus proof any proposition to be
true, but this has to be done on purpose. Completing a proof of
subject reduction without an explicit hack of these assumption is
likely to be a very good starting point towards a complete formalization.
Hint Extern 1 (term _) => skip.
Hint Extern 1 (body _) => skip.
Hint Extern 1 (ok _) => skip.
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 E t T z u 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 : forall E t t' T,
E |= t ~: T ->
t --> t' ->
E |= t' ~: T.
Progress (a well-typed term is either a value or it can
take a step of reduction).
Lemma progress_result : forall t T,
empty |= t ~: T ->
value t
\/ exists t', t --> t'.