Library CoLoR.Term.Lambda.LAlpha

CoLoR, a Coq library on rewriting and termination.
See the COPYRIGHTS and LICENSE files.
  • Frederic Blanqui, 2012-04-05

Alpha-equivalence


Set Implicit Arguments.


Definition of alpha-equivalence

We exactly follow Curry-Feys definition (pages 59 and 91): alpha-equivalence is defined as the smallest congruence containing the rule aeq_alpha below.

Module Export Def.

  Section aeq.

We assume given decidable sets F and X for function symbols and variables respectively.

    Variables (F X : Type)
      (eq_fun_dec : forall f g : F, {f=g}+{~f=g})
      (eq_var_dec : forall x y : X, {x=y}+{~x=y}).

    Notation Te := (@Te F X).

We assume given a structure for finite sets on X.

    Variable ens_X : Ens X.

    Notation In := (Ens_In ens_X).
    Notation fv := (@fv F X ens_X).

We assume that X is infinite.

    Variable var_notin : Ens_type ens_X -> X.

    Notation rename := (@rename F X eq_fun_dec eq_var_dec ens_X var_notin).

Definition of alpha-equivalence.

    Inductive aeq : relation Te :=
    | aeq_refl : forall u, aeq u u
    | aeq_sym : forall u v, aeq u v -> aeq v u
    | aeq_trans : forall u v w, aeq u v -> aeq v w -> aeq u w
    | aeq_app_l : forall u u' v, aeq u u' -> aeq (App u v) (App u' v)
    | aeq_app_r : forall u v v', aeq v v' -> aeq (App u v) (App u v')
    | aeq_lam : forall x u u', aeq u u' -> aeq (Lam x u) (Lam x u')
    | aeq_alpha : forall x u y,
      ~In y (fv u) -> aeq (Lam x u) (Lam y (rename x y u)).

    Infix "~~" := aeq (at level 70).

Alternative definition of aeq as the equivalence closure of the monotone closure of aeq_top.

    Inductive aeq_top : relation Te :=
    | aeq_top_intro : forall x u y,
      ~In y (fv u) -> aeq_top (Lam x u) (Lam y (rename x y u)).

Closure modulo alpha-equivalence of a relation.

    Section clos_aeq.

      Variable R : relation Te.

      Inductive clos_aeq : relation Te :=
      | clos_aeq_intro :
        forall u u' v v', u ~~ u' -> v ~~ v' -> R u' v' -> clos_aeq u v.

"Alpha-transitive closure" of a relation on terms: S* is the (reflexive) transitive closure of S U aeq.

      Inductive clos_aeq_trans : relation Te :=
      | at_step : forall u v, R u v -> clos_aeq_trans u v
      | at_aeq : forall u v, u ~~ v -> clos_aeq_trans u v
      | at_trans : forall u v w, clos_aeq_trans u v ->
        clos_aeq_trans v w -> clos_aeq_trans u w.

    End clos_aeq.

Alpha-equivalence on vectors of terms.

    Notation vaeq := (Vforall2 aeq).

Component-wise extension to vectors of a relation on terms, modulo vaeq.

    Definition clos_vaeq {n} R := vaeq @ (Vrel1 (n:=n) R @ vaeq).

  End aeq.


End Def.

Properties of alpha-equivalence.


Module Make (Export L : L_Struct).

  Module Export S := LSubs.Make L.

Notations for alpha-equivalence and related definitions.

  Notation aeq := (@aeq F X FOrd.eq_dec XOrd.eq_dec ens_X var_notin).
  Notation aeq_alpha :=
    (@aeq_alpha F X FOrd.eq_dec XOrd.eq_dec ens_X var_notin).
  Notation aeq_top := (@aeq_top F X FOrd.eq_dec XOrd.eq_dec ens_X var_notin).
  Notation clos_aeq := (@clos_aeq F X FOrd.eq_dec XOrd.eq_dec ens_X var_notin).
  Notation clos_aeq_trans :=
    (@clos_aeq_trans F X FOrd.eq_dec XOrd.eq_dec ens_X var_notin).
  Notation clos_vaeq :=
    (@clos_vaeq F X FOrd.eq_dec XOrd.eq_dec ens_X var_notin).

  Notation vaeq := (Vforall2 aeq).
  Infix "~~" := aeq (at level 70).
  Infix "~~~" := vaeq (at level 70).
  Notation "R *" := (clos_aeq_trans R) (at level 35).

aeq is the smallest equivalence containing the monotone closure of aeq_top.
aeq is an equivalence relation.

  Instance aeq_equiv : Equivalence aeq.


  Instance aeq_preorder : PreOrder aeq.


aeq is monotone.

  Instance aeq_mon : Monotone aeq.


Term constructors are compatible with aeq.

  Instance App_aeq : Proper (aeq ==> aeq ==> aeq) App.


  Instance Lam_aeq : Proper (Logic.eq ==> aeq ==> aeq) Lam.


Basic lemmas.

  Lemma aeq_refl_eq : forall u v, u = v -> u ~~ v.

  Lemma aeq_alpha' : forall x u y,
    x = y \/ ~In y (fv u) -> Lam x u ~~ Lam y (rename x y u).

fv is compatible with aeq.

  Instance fv_aeq : Proper (aeq ==> Equal) fv.


var is compatible with aeq.
On variables and function symbols, alpha-equivalence is equivalent to equality.

  Instance var_aeq_l : VarInvL aeq.


  Instance var_aeq_r : VarInvR aeq.


  Lemma fun_aeq_l : forall f v, Fun f ~~ v -> Fun f = v.

  Lemma fun_aeq_r : forall f v, v ~~ Fun f -> v = Fun f.

Tactic for simplifying alpha-equivalence assumptions on variables and function symbols.

  Ltac simpl_aeq := repeat
    match goal with
      | h : Var _ ~~ _ |- _ => apply var_aeq_l in h
      | h : _ ~~ Var _ |- _ => apply var_aeq_r in h
      | h : Fun _ ~~ _ |- _ => apply fun_aeq_l in h
      | h : _ ~~ Fun _ |- _ => apply fun_aeq_r in h
    end.

Inversion lemma for alpha-equivalence on an application.

  Lemma app_aeq_r : forall t v1 v2, t ~~ App v1 v2 ->
    exists u1 u2, t = App u1 u2 /\ u1 ~~ v1 /\ u2 ~~ v2.

  Lemma app_aeq_l : forall v1 v2 t, App v1 v2 ~~ t ->
    exists u1 u2, t = App u1 u2 /\ u1 ~~ v1 /\ u2 ~~ v2.

size is compatible with aeq.

  Instance size_aeq : Proper (aeq ==> Logic.eq) size.


Every term is alpha-equivalent to a term which bound variables are disjoint from some given finite set (CF, Theorem 2b, page 95).

  Lemma aeq_notin_bv : forall xs u,
    exists v, u ~~ v /\ inter (bv v) xs [=] empty.

Compatibility with aeq is preserved by clos_trans.

  Lemma clos_trans_aeq R :
    Proper (aeq ==> aeq ==> impl) R -> Proper (aeq ==> aeq ==> impl) (R!).

Alpha-equivalence on substitutions.


  Notation saeq := (subs_rel aeq).

  Instance fvcodom_saeq xs : Proper (saeq xs ==> Equal) (fvcodom xs).


  Instance var_saeq x u :
    Proper (saeq (remove x (fv u)) ==> Logic.eq) (var x u).



  Lemma subs_saeq u s s' : saeq (fv u) s s' -> subs s u ~~ subs s' u.


  Lemma subs1_saeq u s s' : saeq (fv u) s s' -> subs1 s u ~~ subs1 s' u.


Generalization of aeq_notin_bv (Theorem 2b in CF) to substitutions: every substitution s is alpha-equivalent on any finite set xs to a substitution s' which domain is included in xs and which bound variables are disjoint from any fixed set ys.

  Lemma saeq_notin_bvcodom : forall ys s xs, exists s', saeq xs s s'
    /\ inter (bvcod xs s') ys [=] empty /\ dom_incl xs s'.

Some meta-theorems.

Meta-theorem saying that, for proving subs s u ~~ subs s v, we can assume without lost of generality (w.l.o.g.) that the domain of s is included in union (fv u) (fv v).

  Lemma restrict_domain_subs_aeq : forall u v,
    (forall s, (forall x, ~In x (union (fv u) (fv v)) -> s x = Var x) ->
      subs s u ~~ subs s v) -> forall s, subs s u ~~ subs s v.

Meta-theorem saying that, for proving subs s u ~~ subs s v, we can assume w.l.o.g. that the bound variables of s are disjoint from some fixed finite set ys.

  Lemma restrict_bvcodom_subs_aeq : forall ys u v,
    (forall s, dom_incl (union (fv u) (fv v)) s ->
      inter (bvcod (union (fv u) (fv v)) s) ys [=] empty ->
      subs s u ~~ subs s v) -> forall s, subs s u ~~ subs s v.

Meta-theorem saying that, for proving P s -> subs s u ~~ subs s v, we can assume w.l.o.g. that the domain of s is included in union (fv u) (fv v), and the bound variables of s are disjoint from some fixed finite set ys s, if P and ys are compatible with saeq (union (fv u) (fv v)).

  Lemma restrict_bvcodom_subs_aeq_prop : forall u v ys P,
    Proper (saeq (union (fv u) (fv v)) ==> Equal) ys ->
    Proper (saeq (union (fv u) (fv v)) ==> iff) P ->
    (forall s, dom_incl (union (fv u) (fv v)) s ->
      inter (bvcod (union (fv u) (fv v)) s) (ys s) [=] empty ->
      P s -> subs s u ~~ subs s v) -> forall s, P s -> subs s u ~~ subs s v.

Substitution is compatible with alpha-equivalence

(CF, Theorem 2a, page 95, proof pages 100-103).
This is the most difficult theorem when formalizing lambda-calculus using Curry and Feys approach. The CF paper proof has about 100 lines and the following Coq proof has about 200 lines, but it could certainly be shortened by defining tactics for reasoning on free variables.

  Instance subs_aeq : Proper (Logic.eq ==> aeq ==> aeq) subs.


fun u v => subs (single x u) v is compatible with aeq.
comp is compatible with saeq.

  Lemma comp_saeq : forall xs s1 t1, saeq xs s1 t1 -> forall s2 t2,
    saeq (fvcod xs s1) s2 t2 -> saeq xs (comp s2 s1) (comp t2 t1).

Correctness of substitution composition modulo alpha-equivalence.

Because subs s u may rename some bound variables of u depending on the free variables of u and the free variables of s, the following equality cannot hold syntactically. Take for instance x<>y, u = Lam y (Var x), s1 = single x (Var y) and s2 = single y (Var x). Then, subs s2 (subs s1 u) = subs s2 (Lam y' (Var y)) = Lam y'' (Var x), while subs (comp s1 s2) u = Lam y (Var x) since comp s1 s2 x = s2 y = Var x. And one can define var_notin so that y''<>y.

  Lemma subs_comp u s1 s2 : subs s2 (subs s1 u) ~~ subs (comp s2 s1) u.

  Lemma single_rename x y u v : x = y \/ ~In y (fv u) ->
    subs (single y v) (rename x y u) ~~ subs (single x v) u.

  Lemma rename2 : forall x y z u, x = y \/ ~In y (fv u) ->
    rename y z (rename x y u) ~~ rename x z u.

  Lemma subs_update x y s u : s y = Var y ->
    subs (update x (Var y) s) u ~~ subs (update x (Var x) s) (rename x y u).

Given u, fun s => subs s u is compatible with subs_rel R (fv u).

  Lemma subs_rel_mon_preorder_aeq R :
    PreOrder R -> Monotone R -> Proper (aeq ==> aeq ==> impl) R ->
    forall u s s', subs_rel R (fv u) s s' -> R (subs s u) (subs s' u).

  Instance subs_single_mon_preorder_aeq R :
    PreOrder R -> Monotone R -> Proper (aeq ==> aeq ==> impl) R ->
    Proper (Logic.eq ==> R ==> aeq ==> R) subs_single.


Inversion lemma for alpha-equivalence on a lambda.


  Lemma lam_aeq_r : forall t x u, t ~~ Lam x u -> exists y v,
    t = Lam y v /\ v ~~ rename x y u /\ (x = y \/ ~In y (fv u)).

  Lemma lam_aeq_l : forall t x u, Lam x u ~~ t -> exists y v,
    t = Lam y v /\ v ~~ rename x y u /\ (x = y \/ ~In y (fv u)).

  Lemma permut_rename v x y u :
    v ~~ rename x y u -> (x = y \/ ~In y (fv u)) ->
    u ~~ rename y x v /\ (x = y \/ ~In x (fv v)).


  Ltac permut_rename h :=
    apply permut_rename in h;
    [ let h1 := fresh "i" in let h2 := fresh "i" in destruct h as [h1 h2]
    | try tauto].

Inversion tactic for alpha-equivalence.

  Ltac inv_aeq_0 h :=
    let u1 := fresh "u" in let u2 := fresh "u" in let x := fresh "x" in
      let i1 := fresh "i" in let i2 := fresh "i" in let i3 := fresh "i" in
        match type of h with
          | Var _ ~~ _ => apply var_aeq_l in h
          | _ ~~ Var _ => apply var_aeq_r in h
          | Fun _ ~~ _ => apply fun_aeq_l in h
          | _ ~~ Fun _ => apply fun_aeq_r in h
          | App _ _ ~~ _ => destruct (app_aeq_l h) as [u1 [u2 [i1 [i2 i3]]]]
| _ ~~ App _ _ => destruct (app_aeq_r h) as [u1 [u2 [i1 [i2 i3]]]]
| Lam _ _ ~~ _ => destruct (lam_aeq_l h) as [x [u1 [i1 [i2 i3]]]]
| _ ~~ Lam _ _ => destruct (lam_aeq_r h) as [x [u1 [i1 [i2 i3]]]]
end; simpl_aeq.

Compatibility of some basic predicates/functions with aeq.

  Instance not_lam_aeq : Proper (aeq ==> impl) not_lam.


  Instance head_aeq : Proper (aeq ==> aeq) head.


Properties of clos_aeq.


  Lemma clos_aeq_intro_refl (R : rel Te) t u : R t u -> clos_aeq R t u.


  Lemma clos_aeq_inv R t u :
    clos_aeq R t u -> exists t' u', t ~~ t' /\ u ~~ u' /\ R t' u'.

  Lemma clos_aeq_eq R : clos_aeq R == aeq @ (R @ aeq).

  Lemma incl_clos_aeq R : R << clos_aeq R.

Alpha-closure is compatible with relation inclusion/equivalence.
Alpha-closure distributes overs union.

  Lemma clos_aeq_union : forall R S,
    clos_aeq (R U S) == clos_aeq R U clos_aeq S.

Alpha-closure is compatible with alpha-equivalence.

  Instance clos_aeq_aeq R : Proper (aeq ==> aeq ==> impl) (clos_aeq R).


Alpha-closure preserves monotony.

  Instance clos_aeq_mon R : Monotone R -> Monotone (clos_aeq R).


clos_mon (clos_aeq R) is included in clos_aeq (clos_mon R).
Alpha-closure preserves stability by substitution.
clos_aeq o clos_mon preserves stability by substitution.
Alpha-closure preserves free variables.

  Instance fv_clos_aeq : forall R,
    Proper (R --> Subset) fv -> Proper (clos_aeq R --> Subset) fv.


  Lemma fv_R_notin_fv_lam : forall R x y u v, Proper (R --> Subset) fv ->
    R (Lam x u) (Lam y v) -> y=x \/ ~In x (fv v).


Alpha-closure preserves termination of size-decreasing relations.

  Lemma clos_aeq_wf_size : forall R, R << transp (ltof size) -> WF (clos_aeq R).

Compatibility of apps with aeq and vaeq.


  Instance apps_aeq : forall n, Proper (aeq ==> vaeq ==> aeq) (@apps n).


  Lemma apps_aeq_r : forall n (vs : Tes n) v t, t ~~ apps v vs ->
    exists u us, t = apps u us /\ u ~~ v /\ vaeq us vs.


  Lemma apps_aeq_l : forall n (vs : Tes n) v t, apps v vs ~~ t ->
    exists u us, t = apps u us /\ u ~~ v /\ vaeq us vs.


Extended inversion tactic for alpha-equivalence.

  Ltac inv_aeq h :=
    let u := fresh "u" in let us := fresh "us" in
      let i1 := fresh "i" in let i2 := fresh "i" in let i3 := fresh "i" in
        match type of h with
          | apps _ _ ~~ _ => destruct (apps_aeq_l h) as [u [us [i1 [i2 i3]]]]
| _ ~~ apps _ _ => destruct (apps_aeq_r h) as [u [us [i1 [i2 i3]]]]
end || inv_aeq_0 h; simpl_aeq.

Properties of clos_trans_aeq.


  Section atc_props.

    Variable S : relation Te.

S* is a quasi-ordering.

    Global Instance atc_preorder : PreOrder (S*).


S* is compatible with alpha-equivalence if S so is.

    Section aeq.

      Variable S_aeq : Proper (aeq ==> aeq ==> impl) S.

      Global Instance atc_aeq : Proper (aeq ==> aeq ==> impl) (S*).


      Global Instance atc_aeq_iff : Proper (aeq ==> aeq ==> iff) (S*).


Inversion lemma for clos_aeq_trans.

      Lemma clos_aeq_trans_inv : forall t u,
        S* t u -> t ~~ u \/ exists v, S t v /\ S* v u.

    End aeq.

S* is stable by substitution if S so is.

    Section subs.

      Variable subs_S : Proper (Logic.eq ==> S ==> S) subs.

      Global Instance subs_atc : Proper (Logic.eq ==> S* ==> S*) subs.


      Global Instance rename_atc :
        Proper (Logic.eq ==> Logic.eq ==> S* ==> S*) rename.


    End subs.

S* preserves free variables if S so does.

    Global Instance fv_atc :
      Proper (S --> Subset) fv -> Proper (S* --> Subset) fv.


S* is monotone if S so is.

    Global Instance mon_atc : Monotone S -> Monotone (clos_aeq_trans S).


    Global Instance App_atc : Monotone S -> Proper (S* ==> S* ==> S*) App.


    Global Instance Lam_atc : Monotone S -> Proper (Logic.eq ==> S* ==> S*) Lam.


A predicate is stable by S* if it is stable by ~~ and S.

    Global Instance proper_atc P : Proper (aeq ==> impl) P ->
      Proper (S ==> impl) P -> Proper (S* ==> impl) P.


  End atc_props.

Properties of clos_vaeq.


  Section clos_vaeq.

    Variable R : relation Te.
    Infix "->R" := R (at level 70).

    Notation R_aeq := (clos_aeq R) (only parsing).
    Infix "=>R" := (clos_aeq R) (at level 70).

    Infix "==>R" := (clos_vaeq R) (at level 70).

    Lemma clos_vaeq_cons : forall u v n (us vs : Tes n),
      Vcons u us ==>R Vcons v vs
      <-> (u =>R v /\ us ~~~ vs) \/ (u ~~ v /\ us ==>R vs).

clos_vaeq is compatible with vaeq.

    Global Instance clos_vaeq_vaeq n :
      Proper (vaeq ==> vaeq ==> impl) (clos_vaeq (n:=n) R).


    Lemma clos_vaeq_sub : forall n (us vs : Tes n) p q (h : p+q<=n),
      us ==>R vs -> Vsub us h ~~~ Vsub vs h \/ Vsub us h ==>R Vsub vs h.


A vector of terms is strongly normalizing for clos_vaeq if every component is strongly normalizing for R_aeq.

    Lemma sn_clos_vaeq_intro : forall n (us : Tes n),
      Vforall (SN R_aeq) us -> SN (clos_vaeq R) us.

    Lemma sn_clos_vaeq_elim : forall n i (hi : i<n) (us : Tes n),
      SN (clos_vaeq R) us -> SN R_aeq (Vnth us hi).

  End clos_vaeq.

clos_vaeq is compatible with inclusion and same.

  Instance clos_vaeq_incl n : Proper (incl ==> incl) (@clos_vaeq n).


  Instance clos_vaeq_same n : Proper (same ==> same) (@clos_vaeq n).


clos_vaeq distributes over union.

  Lemma clos_vaeq_union n R S :
    @clos_vaeq n (R U S) == @clos_vaeq n R U @clos_vaeq n S.

End Make.