Library STLC_Dec_Infrastructure
Require Import Metatheory
STLC_Dec_Definitions.
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 U 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 U t1 t2 => trm_app U (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.
Substitution for a fresh name is identity.
Lemma subst_fresh : forall x t u,
x \notin fv t -> [x ~> u] t = t.
Substitution distributes on the open operation.
Lemma subst_open : forall x u t1 t2, term u ->
[x ~> u] (t1 ^^ t2) = ([x ~> u]t1) ^^ ([x ~> u]t2).
Substitution and open_var for distinct names commute.
Lemma subst_open_var : forall x y u t, y <> x -> term u ->
([x ~> u]t) ^ y = [x ~> u] (t ^ y).
Opening up an abstraction of body t with a term u is the same as opening
up the abstraction with a fresh name x and then substituting u for x.
Lemma subst_intro : forall x t u,
x \notin (fv t) -> term u ->
t ^^ u = [x ~> u](t ^ x).
Terms are stable by substitution
Lemma subst_term : forall t z u,
term u -> term t -> term ([z ~> u]t).
Hint Resolve subst_term.
Conversion from locally closed abstractions and bodies
Lemma term_abs_to_body : forall t1,
term (trm_abs t1) -> body t1.
Lemma body_to_term_abs : forall t1,
body t1 -> term (trm_abs t1).
Hint Resolve term_abs_to_body body_to_term_abs.
Lemma open_term : forall t u,
body t -> term u -> term (t ^^ u).
Hint Resolve open_term.
A typing relation holds only if the environment has no
duplicated keys and the pre-term is locally-closed.
Lemma typing_regular : forall E e T,
typing E e T -> ok E /\ term e.
The value predicate only holds on locally-closed terms.
Lemma value_regular : forall e,
value e -> term e.
A reduction relation only holds on pairs of locally-closed terms.
Lemma red_regular : forall e e',
red e e' -> term e /\ term e'.
Automation for reasoning on well-formedness.
Hint Extern 1 (ok ?E) =>
match goal with
| H: typing E _ _ |- _ => apply (proj1 (typing_regular H))
end.
Hint Extern 1 (term ?t) =>
match goal with
| H: typing _ t _ |- _ => apply (proj2 (typing_regular H))
| H: red t _ |- _ => apply (proj1 (red_regular H))
| H: red _ t |- _ => apply (proj2 (red_regular H))
| H: value t |- _ => apply (value_regular H)
end.