Library Lambda_Infrastructure

Require Import Metatheory Lambda_Definitions.

Additional Definitions Used in the Proofs


Computing free variables of a term

Fixpoint fv (t : trm) {struct t} : vars :=
  match t with
  | trm_bvar i => {}
  | trm_fvar x => {{x}}
  | trm_app t1 t2 => (fv t1) \u (fv t2)
  | trm_abs t1 => (fv t1)
  end.

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_app t1 t2 => trm_app (close_var_rec k z t1) (close_var_rec k z t2)
  | trm_abs t1 => trm_abs (close_var_rec (S k) z t1)
  end.

Definition close_var z t := close_var_rec 0 z t.

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_app t1 t2 => trm_app (subst z u t1) (subst z u t2)
  | trm_abs t1 => trm_abs (subst z u t1)
  end.

Notation "[ z ~> u ] t" := (subst z u t) (at level 68).

Definition of parallel relation

Inductive para : relation :=
  | para_red : forall L t1 t1' t2 t2',
      (forall x, x \notin L -> para (t1 ^ x) (t1' ^ x) ) ->
      para t2 t2' ->
      para (trm_app (trm_abs t1) t2) (t1' ^^ t2')
  | para_var : forall x,
      para (trm_fvar x) (trm_fvar x)
  | para_app : forall t1 t1' t2 t2',
      para t1 t1' -> para t2 t2' ->
      para (trm_app t1 t2) (trm_app t1' t2')
  | para_abs : forall L t1 t1',
     (forall x, x \notin L -> para (t1 ^ x) (t1' ^ x) ) ->
     para (trm_abs t1) (trm_abs t1').

Definition of the transitive closure of a relation

Inductive iter_ (R : relation) : relation :=
  | iter_trans : forall t2 t1 t3,
      iter_ R t1 t2 -> iter_ R t2 t3 -> iter_ R t1 t3
  | iter_step : forall t t',
      R t t' -> iter_ R t t'.

Notation "R 'iter'" := (iter_ R) (at level 69).

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,
  x \notin (fv t) -> x \notin (fv t') ->
  R (t ^ x) (t' ^ x) ->
  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).

Tactics


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
  constr:(A \u B \u C).

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*.

Hint Constructors term.

Lemmas


Properties of substitutions


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).

Tactic to permute subst and open var

Ltac cross :=
  rewrite subst_open_var; try cross.

Tactic Notation "cross" "*" :=
  cross; auto*.

Terms are stable through substitutions


Terms are stable by substitution

Lemma subst_term : forall t z u,
  term u -> term t -> term ([z ~> u]t).

Lemma subst_body : forall z u t,
  body t -> term u -> body ([z ~> u]t).

Hint Resolve subst_term subst_body.

Terms are stable through open


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.

Opening a body with a term gives a term


Lemma open_term : forall t u,
  body t -> term u -> term (t ^^ u).

Hint Resolve open_term.

Additional results on primitive operations


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).

Regularity: relations only hold on well-formed terms

Section TermRelations.

Hint Extern 1 (term (trm_abs ?t)) =>
  match goal with H: context [term (t ^ _) ] |- _ =>
   let y := fresh in let K := fresh in
   apply_fresh term_abs as y;
   inst_notin H y as K; destruct K; auto end.

Lemma red_regular_beta : red_regular beta.

Lemma red_regular_beta_star : red_regular (beta star).

Lemma red_regular_para : red_regular para.

Lemma red_regular_para_iter : red_regular (para iter).

End TermRelations.

Hint Resolve red_regular_beta red_regular_beta_star red_regular_para red_regular_para_iter.

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: para t _ |- _ => apply (proj1 (red_regular_para H))
  | H: para _ t |- _ => apply (proj2 (red_regular_para H))
  | H: (beta star) t _ |- _ => apply (proj1 (red_regular_beta_star H))
  | H: (beta star) _ t |- _ => apply (proj2 (red_regular_beta_star H))
  | H: (para iter) t _ |- _ => apply (proj1 (red_regular_para_iter))
  | H: (para iter) _ t |- _ => apply (proj2 (red_regular_para_iter))
  end.

Hint Extern 1 (body ?t) =>
   match goal with H: context [?R (t ^ _) _ ] |- _ =>
     let y := fresh in apply term_abs_to_body;
     apply_fresh term_abs as y;
     inst_notin H y as K; clear H end.