Library CoC_Infrastructure
Require Import Metatheory CoC_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_type n => {}
| trm_app t1 t2 => (fv t1) \u (fv t2)
| trm_abs t1 t2 => (fv t1) \u (fv t2)
| trm_prod t1 t2 => (fv t1) \u (fv t2)
end.
Substitution for a name
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_type n => trm_type n
| trm_app t1 t2 => trm_app (subst z u t1) (subst z u t2)
| trm_abs t1 t2 => trm_abs (subst z u t1) (subst z u t2)
| trm_prod t1 t2 => trm_prod (subst z u t1) (subst z u t2)
end.
Notation "[ z ~> u ] t" := (subst z u t) (at level 68).
Abstracting a name out of a term
Fixpoint close_var_rec (k : nat) (z : var) (t : trm) {struct t} : trm :=
match t with
| trm_bvar i => trm_bvar i
| trm_fvar x => if x == z then (trm_bvar k) else (trm_fvar x)
| trm_type n => trm_type n
| trm_app t1 t2 => trm_app (close_var_rec k z t1) (close_var_rec k z t2)
| trm_abs t1 t2 => trm_abs (close_var_rec k z t1) (close_var_rec (S k) z t2)
| trm_prod t1 t2 => trm_prod (close_var_rec k z t1) (close_var_rec (S k) z t2)
end.
Definition close_var z t := close_var_rec 0 z t.
An environment contains only terms
Definition contains_terms E :=
forall x U, binds x U E -> term U.
Inclusion between relations (simulation or a relation by another)
Definition simulated (R1 R2 : relation) :=
forall (t t' : trm), R1 t t' -> R2 t t'.
Infix "simulated_by" := simulated (at level 69).
Properties of relations
Definition red_regular (R : relation) :=
forall t t', R t t' -> term t /\ term t'.
Definition red_refl (R : relation) :=
forall t, term t -> R t t.
Definition red_in (R : relation) :=
forall t x u u', term t -> R u u' ->
R ([x ~> u]t) ([x ~> u']t).
Definition red_all (R : relation) :=
forall x t t', R t t' ->
forall u u', R u u' ->
R ([x~>u]t) ([x~>u']t').
Definition red_out (R : relation) :=
forall x u t t', term u -> R t t' ->
R ([x~>u]t) ([x~>u]t').
Definition red_rename (R : relation) :=
forall x t t' y,
R (t ^ x) (t' ^ x) ->
x \notin (fv t) -> x \notin (fv t') ->
R (t ^ y) (t' ^ y).
Definition red_through (R : relation) :=
forall x t1 t2 u1 u2,
x \notin (fv t1) -> x \notin (fv u1) ->
R (t1 ^ x) (u1 ^ x) -> R t2 u2 ->
R (t1 ^^ t2) (u1 ^^ u2).
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 : trm => fv x) in
let D := gather_vars_with (fun x : env => dom x) in
constr:(A \u B \u C \u D).
Ltac pick_fresh X :=
let L := gather_vars in (pick_fresh_gen L X).
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*.
Ltac exists_fresh :=
let L := gather_vars_with (fun x : vars => x) in exists L.
Scheme typing_induct := Induction for typing Sort Prop
with wf_induct := Induction for wf Sort Prop.
Hint Constructors beta star_ equiv_ less typing wf.
Hint Unfold conv.
Properties of substitutions
Section SubstProperties.
Hint Constructors term.
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 e, y <> x -> term u ->
([x ~> u]e) ^ y = [x ~> u] (e ^ 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).
End SubstProperties.
Tactic to permute subst and open var
Ltac cross :=
rewrite subst_open_var; try cross.
Tactic Notation "cross" "*" :=
cross; auto*.
Lifting operations to terms
Hint Constructors term.
Terms are stable by substitution
Lemma subst_term : forall t z u,
term u -> term t -> term ([z ~> u]t).
Terms are stable by open
Lemma open_term : forall t u,
body t -> term u -> term (t ^^ u).
Hint Resolve subst_term open_term.
Properties of Body
Lemma term_abs1 : forall t2 t1,
term (trm_abs t1 t2) -> term t1.
Lemma body_abs2 : forall t1 t2,
term (trm_abs t1 t2) -> body t2.
Lemma body_prod2 : forall t1 t2,
term (trm_prod t1 t2) -> body t2.
Hint Extern 1 (term ?t) =>
match goal with H: term (trm_abs t ?t2) |- _ =>
apply (@term_abs1 t2) end.
Hint Extern 1 (body ?t) =>
match goal with
| H: context [trm_abs ?t1 t] |- _ => apply (@body_abs2 t1)
| H: context [trm_prod ?t1 t] |- _ => apply (@body_prod2 t1)
| H: context [t ^ _] |- _ =>
let x := fresh in let L := gather_vars in
exists L; intros x Fr; destructi (H x); auto
end.
Lemma term_abs_prove : forall t1 t2,
term t1 -> body t2 -> term (trm_abs t1 t2).
Lemma term_prod_prove : forall t1 t2,
term t1 -> body t2 -> term (trm_prod t1 t2).
Hint Resolve term_abs_prove term_prod_prove.
Lemma body_prove : forall L t,
(forall x, x \notin L -> term (t ^ x)) -> body t.
Hint Extern 1 (body ?t) =>
match goal with
| H: forall _, _ \notin ?L -> term (t ^ _) |- _ =>
apply (@body_prove L)
end.
Lemma body_subst : forall x t u,
term u -> body t -> body ([x ~> u]t).
Hint Resolve body_subst.
Section PrimProperties.
Hint Constructors term.
Open_var with fresh names is an injective operation
Lemma open_var_inj : forall x t1 t2,
x \notin (fv t1) -> x \notin (fv t2) ->
(t1 ^ x = t2 ^ x) -> (t1 = t2).
Close var is an operation returning a body of an abstraction
Lemma close_var_fresh : forall x t,
x \notin fv (close_var x t).
Close var is an operation returning a body of an abstraction
Lemma close_var_body : forall x t,
term t -> body (close_var x t).
Close var is the right inverse of open_var
Lemma close_var_open : forall x t,
term t -> t = (close_var x t) ^ x.
An abstract specification of close_var, which packages the
result of the operation and all the properties about it.
Lemma close_var_spec : forall t x, term t ->
exists u, t = u ^ x /\ body u /\ x \notin (fv u).
End PrimProperties.
Lemma red_regular_beta : red_regular beta.
Lemma red_regular_beta_star : red_regular (beta star).
Lemma red_regular_conv : red_regular conv.
Hint Extern 1 (term ?t) => match goal with
| H: beta t _ |- _ => apply (proj1 (red_regular_beta H))
| H: beta _ t |- _ => apply (proj2 (red_regular_beta H))
| H: (beta star) t _ |- _ => apply (proj1 (red_regular_beta_star H))
| H: (beta star) _ t |- _ => apply (proj2 (red_regular_beta_star H))
| H: conv t _ |- _ => apply (proj1 (red_regular_conv H))
| H: conv _ t |- _ => apply (proj2 (red_regular_conv H))
end.
Hint Extern 1 (term (trm_abs ([?x ~> ?u]?t1) ([?x ~> ?u]?t2))) =>
match goal with H: term (trm_abs t1 t2) |- _ =>
unsimpl ([x ~> u](trm_abs t1 t2)) end.
Lemma red_regular_less : red_regular less.
Hint Extern 1 (term ?t) => match goal with
| H: less t _ |- _ => apply (proj1 (red_regular_less H))
| H: less _ t |- _ => apply (proj2 (red_regular_less H))
end.
Lemma regular_typing : forall E t T, typing E t T ->
(wf E /\ ok E /\ contains_terms E /\ term t /\ term T).
Hint Extern 1 (term ?t) => match goal with
| H: typing _ t _ |- _ => apply (proj32 (proj33 (regular_typing H)))
| H: typing _ _ t |- _ => apply (proj33 (proj33 (regular_typing H)))
end.
Lemma ok_from_wf : forall E, wf E -> ok E.
Hint Extern 1 (ok ?E) => match goal with
| H: wf E |- _ => apply (ok_from_wf H)
end.
Hint Extern 1 (wf ?E) => match goal with
| H: typing E _ _ |- _ => apply (proj1 (regular_typing H))
end.
Lemma term_from_binds_in_wf : forall x E U,
wf E -> binds x U E -> term U.
Hint Extern 1 (term ?t) => match goal with
H: binds ?x t ?E |- _ => apply (@term_from_binds_in_wf x E)
end.
Lemma wf_left : forall E F,
wf (E & F) -> wf E.
Implicit Arguments wf_left [E F].
Lemma fv_open_var : forall y x t,
x <> y -> x \notin fv (t ^ y) -> x \notin fv t.
Lemma typing_fresh : forall E T i x,
typing E T (trm_type i) -> x # E -> x \notin fv T.
Lemma notin_fv_from_wf : forall E F x V,
wf (E & x ~ V & F) -> x \notin fv V.
Lemma notin_fv_from_binds : forall x y U E,
wf E -> binds y U E -> x # E -> x \notin fv U.
Lemma notin_fv_from_binds' : forall E F x V y U,
wf (E & x ~ V & F) -> binds y U E -> x \notin fv U.
Hint Extern 1 (?x \notin fv ?V) =>
match goal with H: wf (?E & x ~ V & ?F) |- _ =>
apply (@notin_fv_from_wf E F) end.
Hint Extern 1 (?x \notin fv ?U) =>
match goal with H: wf (?E & x ~ ?V & ?F), B: binds ?y U ?E |- _ =>
apply (@notin_fv_from_binds' E F x V y) end.