# Library CoLoR.Term.Lambda.LAlphaAlt

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
• Frederic Blanqui, 2013-09-24

# Alternative definitions of alpha-equivalence

Set Implicit Arguments.

# Other definitions of alpha-equivalence.

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).
Notation Var := (@Var F X).
Notation Fun := (@Fun F X).
Notation rename1 := (@rename1 F X eq_var_dec).

We assume given a structure for finite sets on X.

Variable ens_X : Ens X.

Notation In := (@Ens_In X ens_X).
Notation union := (@Ens_union X ens_X).
Notation fv := (@fv F X ens_X).
Notation bv := (@bv 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).

Replace every occurrence of a variable x by y, including binding occurrences.

Definition replace_var x y z :=
match eq_var_dec z x with left _ => y | _ => z end.

Fixpoint replace_all x y u :=
match u with
| Def.Var z => Var (replace_var x y z)
| Def.Fun _ => u
| Def.App u1 u2 => App (replace_all x y u1) (replace_all x y u2)
| Def.Lam z v => Lam (replace_var x y z) (replace_all x y v)
end.

Lemma size_replace_all : forall x y t, size (replace_all x y t) = size t.

Action of a function on variables, including binding occurrences.

Fixpoint action (f : X -> X) u :=
match u with
| Def.Var x => Var (f x)
| Def.Fun f => Fun f
| Def.App u1 u2 => App (action f u1) (action f u2)
| Def.Lam x v => Lam (f x) (action f v)
end.

Permutation of x and y.

Definition transpose_var x y z :=
match eq_var_dec z x with
| left _ => y
| _ => match eq_var_dec z y with left _ => x | _ => z end
end.

Definition transpose x y := action (transpose_var x y).

## Church's definition (1932)

in his first paper on lambda-calculus, "A set of postulates for the foundations of logic", Annals of Mathematics, 33(2):346–366, 1932.

Inductive aeq_ch_top : relation Te :=
| aeq_ch_top_intro : forall L x y, ~In x (fv L) -> ~In y (fv L) ->
~In y (bv L) -> aeq_ch_top L (replace_all x y L).

Definition aeq_ch : relation Te := clos_refl_trans (clos_mon aeq_ch_top).

## Krivine's definition (1993)

in his book (in French) "Lambda-calcul, types et modèles", Ellis Horwood, 1993. English translation due to René Cori available on http://cel.archives-ouvertes.fr/cel-00574575/fr/ .

Inductive aeq_kr : relation Te :=
| aeq_kr_fun : forall f, aeq_kr (Fun f) (Fun f)
| aeq_kr_var : forall x, aeq_kr (Var x) (Var x)
| aeq_kr_app : forall u v u' v',
aeq_kr u u' -> aeq_kr v v' -> aeq_kr (App u v) (App u' v')
| aeq_kr_lam : forall x u x' u' xs,
(forall y, ~In y xs -> aeq_kr (rename1 x y u) (rename1 x' y u')) ->
aeq_kr (Lam x u) (Lam x' u').

## Gabbay and Pitts's definition (1999)

in their paper "A New Approach to Abstract Syntax Involving Binders", Proceedings of the 14th IEEE Symposium on Logic in Computer Science (LICS), 1999.

Inductive aeq_gp : relation Te :=
| aeq_gp_refl_fun : forall f, aeq_gp (Fun f) (Fun f)
| aeq_gp_refl_var : forall x, aeq_gp (Var x) (Var x)
| aeq_gp_app : forall u v u' v',
aeq_gp u u' -> aeq_gp v v' -> aeq_gp (App u v) (App u' v')
| aeq_gp_lam : forall x u x' u' z,
~In z (union (add x (union (fv u) (bv u)))
(add x' (union (fv u') (bv u')))) ->
aeq_gp (transpose z x u) (transpose z x' u') ->
aeq_gp (Lam x u) (Lam x' u').

End aeq.

End Def.

# Properties of and relations between these different definitions.

Module Make (Export L : L_Struct).

Module Export A := LAlpha.Make L.

Notation replace_var := (@replace_var X XOrd.eq_dec).
Notation replace_all := (@replace_all F X XOrd.eq_dec).
Notation transpose_var := (@transpose_var X XOrd.eq_dec).
Notation transpose := (@transpose F X XOrd.eq_dec).
Notation aeq_ch_top := (@aeq_ch_top F X XOrd.eq_dec ens_X).
Notation aeq_ch := (@aeq_ch F X XOrd.eq_dec ens_X).
Notation aeq_kr := (@aeq_kr F X XOrd.eq_dec ens_X).
Notation aeq_gp := (@aeq_gp F X XOrd.eq_dec ens_X).
Notation action := (@action F X).

## Properties of replace_var.

Lemma replace_var_eq x y : replace_var x y x = y.

Lemma replace_var_id x y : replace_var x x y = y.

Lemma replace_var2 x y z :
x = z \/ y <> z -> replace_var y x (replace_var x y z) = z.

## Properties of replace_all.

Lemma replace_all_id x : forall u, replace_all x x u = u.

Lemma replace_all2 x y : forall u, ~In y (fv u) -> ~In y (bv u) ->
replace_all y x (replace_all x y u) = u.

Lemma notin_fv_replace_all x y : x <> y ->
forall u, ~In x (fv (replace_all x y u)).

Lemma notin_bv_replace_all x y : x <> y ->
forall u, ~In x (bv (replace_all x y u)).

Lemma fv_replace_all x y : forall u,
~In y (bv u) -> ~In y (fv u) -> fv (replace_all x y u)
[=] if mem x (fv u) then add y (remove x (fv u)) else fv u.

Lemma replace_all_aeq_rename x y : forall u,
~In y (fv u) -> ~In y (bv u) -> replace_all x y u ~~ rename x y u.

## Properties of action.

Lemma action_eq f g : forall u,
(forall x, In x (fv u) \/ In x (bv u) -> f x = g x) ->
action f u = action g u.

Lemma size_action f : forall u, size (action f u) = size u.

Lemma action_comp f g :
forall u, action f (action g u) = action (fun x => f (g x)) u.

## Properties of transpose.

Lemma transpose_id x : forall u, transpose x x u = u.

Lemma transpose_sym x y : forall u, transpose x y u = transpose y x u.

Lemma transpose_comp a b c : forall u, ~In b (fv u) -> ~In b (bv u) ->
~In c (fv u) -> ~In c (bv u) ->
transpose b c (transpose a b u) = transpose a c u.

## Substitution corresponding to transpose_var.

Definition subs_transpose a b x := Var (transpose_var a b x).

Lemma domain_subs_transpose a b : forall xs, domain xs (subs_transpose a b)
[=] if eqb a b then empty else inter xs (add a (singleton b)).

Lemma fvcod_subs_transpose a b : forall xs, fvcod xs (subs_transpose a b)
[=] union (remove a (remove b xs))
(union (if mem a xs then singleton b else empty)
(if mem b xs then singleton a else empty)).

Lemma fvcodom_subs_transpose a b xs :
fvcodom xs (subs_transpose a b) [=] if eqb a b then empty
else union (if mem a xs then singleton b else empty)
(if mem b xs then singleton a else empty).

Lemma transpose_subs a b : forall u, ~In a (bv u) -> ~In b (bv u) ->
transpose a b u = subs (subs_transpose a b) u.

Lemma transpose_rename x y :
forall u, ~In y (fv u) -> ~In y (bv u) -> transpose x y u ~~ rename x y u.

transpose is invariant by aeq.

Instance transpose_aeq a b : Proper (aeq ==> aeq) (transpose a b).

## Properties of Church's definition.

aeq_ch is a congruence relation.

Instance aeq_ch_refl : Reflexive aeq_ch.

Instance aeq_ch_trans : Transitive aeq_ch.

Instance aeq_ch_top_sym : Symmetric aeq_ch_top.

Instance aeq_ch_sym : Symmetric aeq_ch.

Instance aeq_ch_mon : Monotone aeq_ch.

aeq_ch is equivalent to aeq.

Lemma aeq_ch_le_aeq : aeq_ch << aeq.

Lemma aeq_le_aeq_ch : aeq << aeq_ch.

## Properties of Krivine's definition.

aeq_kr is an equivalence relation.

Instance aeq_kr_refl : Reflexive aeq_kr.

Instance aeq_kr_sym : Symmetric aeq_kr.

Instance aeq_kr_trans : Transitive aeq_kr.

aeq_kr is equivalent to aeq.

Lemma aeq_le_aeq_kr : aeq << aeq_kr.

Lemma aeq_kr_le_aeq : aeq_kr << aeq.

## Properties of Gabbay and Pitts's definition.

aeq_gp is reflexive.

Instance aeq_gp_refl : Reflexive aeq_gp.

aeq_gp is symmetric.

Instance aeq_gp_sym : Symmetric aeq_gp.

aeq_gp is included in aeq.

Lemma aeq_gp_incl_aeq : aeq_gp << aeq.

transpose is invariant by aeq_gp.

Instance transpose_aeq_gp a b : Proper (aeq_gp ==> aeq_gp) (transpose a b).

aeq_gp is transitive.

Instance aeq_gp_trans : Transitive aeq_gp.

aeq is included in aeq_gp.

Lemma aeq_incl_aeq_gp : aeq << aeq_gp.

End Make.