RIS.words: words, binding monoid and alpha-equivalence.
Class Alphabet {a : Set} (A : Atom a) (X : Set) :=
{
dec_X :> decidable_set X;
support_X :> Support A X;
action_X :> Action A X;
nom_X :> Nominal A X
}.
Type of atoms
We take an alphabet Nom.
Letters
Letters are generated by the grammar open a | close a | var x where a ranges over atom and x ranges over X.
Inductive letter {π : Atom atom} {Nom : Alphabet π X}:=
| open : atom β letter
| close : atom β letter
| var : X β letter.
Notation " β¨ a " := (open a) (at level 0).
Notation " a β© " := (close a) (at level 0).
| open : atom β letter
| close : atom β letter
| var : X β letter.
Notation " β¨ a " := (open a) (at level 0).
Notation " a β© " := (close a) (at level 0).
The type letter is decidable.
Definition eq_letter l1 l2 :=
match (l1,l2) with
| (β¨a, β¨b) | (aβ©,bβ©) β a=?= b
| (var x,var y) β x =?= y
| _ β false
end.
Lemma eq_letter_correct : β x y : letter, reflect (x = y) (eq_letter x y).
Global Instance dec_letter : decidable_set letter :=
Build_decidable_set eq_letter_correct.
match (l1,l2) with
| (β¨a, β¨b) | (aβ©,bβ©) β a=?= b
| (var x,var y) β x =?= y
| _ β false
end.
Lemma eq_letter_correct : β x y : letter, reflect (x = y) (eq_letter x y).
Global Instance dec_letter : decidable_set letter :=
Build_decidable_set eq_letter_correct.
We canonically get a nominal structure over letters from the nominal structures of Atom and Nom.
Definition supp_letter (l : letter) : list atom :=
match l with
| β¨a | aβ© β βaβ
| var x β βxβ
end.
Global Instance support_letter : Support π letter := supp_letter.
Definition letter_map Ο l :=
match l with
| open b β open (Οβb)
| close b β close (Οβb)
| var x β var (Οβx)
end.
Global Instance action_letter : Action π letter := letter_map.
Global Instance group_action_letter : Nominal π letter.
match l with
| β¨a | aβ© β βaβ
| var x β βxβ
end.
Global Instance support_letter : Support π letter := supp_letter.
Definition letter_map Ο l :=
match l with
| open b β open (Οβb)
| close b β close (Οβb)
| var x β var (Οβx)
end.
Global Instance action_letter : Action π letter := letter_map.
Global Instance group_action_letter : Nominal π letter.
A word is a list of letters. It is therefore equipped with a nominal structure, following Nominal_list.
Binding monoid
The elements of the binding monoid are triples (m,n,p), where m and p are natural numbers and p is a boolean.
The product (m,n,p)β
(m',n',p') is defined as follows:
- if p < m' then (m+m'-p,n',p');
- if m' < p then (m,n,p'+p-m');
- if p = m' then (m,n||n',p').
Definition prod_binding (a b:π‘) : π‘ :=
match (a,b) with
| ((m,n,p),(m',n',p')) β
if Nat.ltb p m'
then (m+m'-p,n',p')
else
if Nat.ltb m' p
then (m,n,p'+p-m')
else (m,n||n',p')
end.
Infix " β " := prod_binding (at level 50).
match (a,b) with
| ((m,n,p),(m',n',p')) β
if Nat.ltb p m'
then (m+m'-p,n',p')
else
if Nat.ltb m' p
then (m,n,p'+p-m')
else (m,n||n',p')
end.
Infix " β " := prod_binding (at level 50).
The unit of this product is the element (0,false,0).
Definition Ξ΅ := (0,false,0).
Hint Transparent Ξ΅.
Lemma prod_unit_r a : a β Ξ΅ = a.
Lemma prod_unit_l a : Ξ΅ β a = a.
Hint Transparent Ξ΅.
Lemma prod_unit_r a : a β Ξ΅ = a.
Lemma prod_unit_l a : Ξ΅ β a = a.
The product in π‘ is associative.
We will need sometimes to consider the first or last projection of elements from the binding monoid.
Definition c_binding : π‘ β nat := snd.
Definition d_binding (x : π‘) : nat := fst(fst x).
Lemma c_binding_prod x y :
c_binding (xβ y) = c_binding y + (c_binding x - d_binding y).
Lemma d_binding_prod x y :
d_binding (xβ y) = d_binding x + (d_binding y - c_binding x).
Definition d_binding (x : π‘) : nat := fst(fst x).
Lemma c_binding_prod x y :
c_binding (xβ y) = c_binding y + (c_binding x - d_binding y).
Lemma d_binding_prod x y :
d_binding (xβ y) = d_binding x + (d_binding y - c_binding x).
The size of an element (n,m,p) is the sum n+m+p, where the
boolean true is identified with 1 and false with 0.
Definition size (x : π‘) :=
d_binding x + c_binding x.
Lemma size_prod_bound_sup (a b : π‘) : size (aβ b) β€ size a + size b.
Lemma size_prod_bound_inf_left (a b : π‘) : size a β€ size (aβ b) + size b.
Lemma size_prod_bound_inf_right (a b : π‘) : size b β€ size (aβ b) + size a.
d_binding x + c_binding x.
Lemma size_prod_bound_sup (a b : π‘) : size (aβ b) β€ size a + size b.
Lemma size_prod_bound_inf_left (a b : π‘) : size a β€ size (aβ b) + size b.
Lemma size_prod_bound_inf_right (a b : π‘) : size b β€ size (aβ b) + size a.
Binding power
The binding power of a letter l relative to a name a, written π³ a l, is an element of the binding monoid defined as follows:
Definition π³ a l : π‘ :=
match l with
| open b β if a =?= b then (0,false,1) else Ξ΅
| close b β if a =?= b then (1,false,0) else Ξ΅
| var x β (0,inb a βxβ,0)
end.
match l with
| open b β if a =?= b then (0,false,1) else Ξ΅
| close b β if a =?= b then (1,false,0) else Ξ΅
| var x β (0,inb a βxβ,0)
end.
The binding power of a word w relative to a name a, written π a w, is obtained by extending π³ a as a monoid homomorphism from word to π‘.
The following trivial simplification lemmas hold.
Lemma π_singl a x : π a [x] = π³ a x.
Lemma π_cons a l u : π a (l::u) = π³ a l β π a u.
Lemma π_app a u v : π a (u++v) = π a u β π a v.
Lemma π_add a u l : π a (u++[l]) = π a u β π³ a l.
Lemma π³_perm Ο a l : π³ a (Ο β l) = π³ (Οβ β a) l.
Lemma π_perm Ο a u : π a (Οβu) = π (Οβ β a) u.
Lemma π_cons a l u : π a (l::u) = π³ a l β π a u.
Lemma π_app a u v : π a (u++v) = π a u β π a v.
Lemma π_add a u l : π a (u++[l]) = π a u β π³ a l.
Lemma π³_perm Ο a l : π³ a (Ο β l) = π³ (Οβ β a) l.
Lemma π_perm Ο a u : π a (Οβu) = π (Οβ β a) u.
Balance properties
Definition open_balanced a w := c_binding (π a w) = 0.
Infix " β· " := open_balanced (at level 20).
Infix " β· " := open_balanced (at level 20).
a is close-balanced in w, written a β w, if the first component of π a w is 0.
Definition close_balanced a w := d_binding (π a w) = 0.
Infix " β " := close_balanced (at level 20).
Infix " β " := close_balanced (at level 20).
a is balanced in w, written a β w, if it is both open- and close-balanced.
Definition balanced a w := c_binding (π a w) = 0 β§ d_binding (π a w) = 0.
Infix " β " := balanced (at level 20).
Infix " β " := balanced (at level 20).
a is Ξ±-fresh for w, written a #Ξ± w, if π a w=Ξ΅.
The predicate a β· is preserved by taking suffixes.
The predicate a β· is preserved by taking prefixes.
The balance properties commute with the action of permutations.
Lemma open_balanced_perm Ο a u : a β· (Οβu) β (Οββa) β· u.
Lemma close_balanced_perm Ο a u : a β (Οβu) β (Οββa) β u.
Lemma balanced_perm Ο a u : a β (Οβu) β (Οββa) β u.
Lemma Ξ±fresh_perm Ο a u : a #Ξ± (Οβu) β (Οββa)#Ξ± u.
Lemma close_balanced_perm Ο a u : a β (Οβu) β (Οββa) β u.
Lemma balanced_perm Ο a u : a β (Οβu) β (Οββa) β u.
Lemma Ξ±fresh_perm Ο a u : a #Ξ± (Οβu) β (Οββa)#Ξ± u.
For letters, freshness and Ξ±-freshness are equivalent.
If a is fresh for u, then it is Ξ±-fresh. Note however that the converse is not true: a is Ξ±-fresh for [β¨a;aβ©], and yet aββ[β¨a;aβ©]β=[a].
Lemma Ξ±fresh_support a u : a # u β a #Ξ± u.
Lemma open_balanced_no_open u a : Β¬ open a β u β a β· u.
Lemma close_balanced_no_close u a : Β¬ close a β u β a β u.
Lemma balanced_open_close u a : Β¬ open a β u β Β¬ close a β u β a β u.
Lemma open_balanced_no_open u a : Β¬ open a β u β a β· u.
Lemma close_balanced_no_close u a : Β¬ close a β u β a β u.
Lemma balanced_open_close u a : Β¬ open a β u β Β¬ close a β u β a β u.
Decomposition properties
If a is not open-balanced in u, then there is an unmatched β¨a in u, and therefore a last unmatched β¨a. This means that u may be factorised as u1++β¨a::u2, with a being balanced in u2.
Similarly, for closing brackets.
This decomposition is unique.
Lemma Ξ±fresh_close_split_unique u1 u2 v1 v2 a :
u1 ++ open a :: u2 = v1 ++ open a :: v2 β a β u2 β a β v2 β u1 = v1 β§ u2 = v2.
u1 ++ open a :: u2 = v1 ++ open a :: v2 β a β u2 β a β v2 β u1 = v1 β§ u2 = v2.
Alpha-equivalence
We write β‘ for the relation defined as follows:- β‘ is transitive, and []β‘[];
- if uβ‘v, then x::uβ‘x::v and u++[x]β‘v++[x];
- if b is Ξ±-fresh in u and a is balanced in u, then β¨a::u++[aβ©] is equivalent to β¨b::([(a,b)]βu)++[bβ©].
Inductive Ξ±equiv : Equiv word :=
| Ξ±t u v w : u β‘ v β v β‘ w β u β‘ w
| Ξ±Ξ΅ : [] β‘ []
| Ξ±r u v l : u β‘ v β u++[l] β‘ v++[l]
| Ξ±l u v l : u β‘ v β l::u β‘ l::v
| Ξ±Ξ± a b u : b #Ξ± u β a β u β β¨a::u++[aβ©] β‘ β¨b::([(a,b)]βu)++[bβ©].
Hint Constructors Ξ±equiv.
| Ξ±t u v w : u β‘ v β v β‘ w β u β‘ w
| Ξ±Ξ΅ : [] β‘ []
| Ξ±r u v l : u β‘ v β u++[l] β‘ v++[l]
| Ξ±l u v l : u β‘ v β l::u β‘ l::v
| Ξ±Ξ± a b u : b #Ξ± u β a β u β β¨a::u++[aβ©] β‘ β¨b::([(a,b)]βu)++[bβ©].
Hint Constructors Ξ±equiv.
This is an equivalence relation.
This relation is a congruence.
Lemma Ξ±equiv_app_left u v w : u β‘ v β w++uβ‘w++v.
Lemma Ξ±equiv_app_right (u v w : word) : u β‘ v β u++wβ‘v++w.
Global Instance Ξ±equiv_app :
Proper (equiv ==> equiv ==> equiv) (@app letter).
Lemma Ξ±equiv_app_right (u v w : word) : u β‘ v β u++wβ‘v++w.
Global Instance Ξ±equiv_app :
Proper (equiv ==> equiv ==> equiv) (@app letter).
Equivalent words have the same length.
Equivalent words have the same binding power.
This relation commutes with the action of permutations.
Lemma Ξ±equiv_perm u v Ο : u β‘ v β Ο β u β‘ Ο β v.
End s.
Hint Transparent Ξ΅.
Notation " β¨ a " := (open a) (at level 0).
Notation " a β© " := (close a) (at level 0).
Infix " β " := prod_binding (at level 50).
Infix " #Ξ± " := fresh__Ξ± (at level 30).
Infix " β " := balanced (at level 20).
Infix " β " := close_balanced (at level 20).
Infix " β· " := open_balanced (at level 20).
End s.
Hint Transparent Ξ΅.
Notation " β¨ a " := (open a) (at level 0).
Notation " a β© " := (close a) (at level 0).
Infix " β " := prod_binding (at level 50).
Infix " #Ξ± " := fresh__Ξ± (at level 30).
Infix " β " := balanced (at level 20).
Infix " β " := close_balanced (at level 20).
Infix " β· " := open_balanced (at level 20).