# Set of atoms.

Type of atoms

Parameter Atom : Set.

We require Atom to be decidable, by a boolean function.

Parameter beq_atom : Atom Atom bool.

Axiom beq_atom_refl : a b, reflect (a=b) (beq_atom a b).

The following trivial lemmas will be usefull in the rest of the proofs to simplify statements.

Lemma beq_atom_spec : a b, beq_atom a b = true a = b.
Lemma Atom_eq_dec : x y : Atom, {x = y} + {x y}.
Lemma beq_eq_atom a : beq_atom a a = true.
Lemma beq_neq_atom1 a b : a b beq_atom a b = false.
Lemma beq_neq_atom a b : a b beq_atom a b = false.

Simplification of if then else statements.
Lemma if_Atom_eq_dec_eq {A} : a1 a2 (b c : A),
a1 = a2 (if Atom_eq_dec a1 a2 then b else c) = b.

Lemma if_Atom_eq_dec_neq {A} : a1 a2 (b c : A),
a1a2 (if Atom_eq_dec a1 a2 then b else c) = c.

Boolean equality predicate over lists.
Fixpoint beq_list l m :=
match (l,m) with
| ([],[])true
| (a::l,b::m)(beq_atom a b)&&(beq_list l m)
| _false
end.

Lemma beq_list_spec l m : reflect (l=m) (beq_list l m).

Boolean In predicate

Definition inb a l := (existsb (fun ybeq_atom y a) l).

Lemma inb_spec x l : reflect (In x l) (inb x l).

Lemma in_double_neg : (x : Atom) l, ~~In x l In x l.

# Permutations

Permutations are defined as lists of pairs. This is general enough as every permutation (on an infinite set) can be factored as a product of cycles of length 2.

Definition perm := list (Atom × Atom).

Boolean equality predicate over permutations.

Fixpoint beq_perm l m :=
match (l,m) with
| ([],[])true
| ((a,a')::l,(b,b')::m)
(beq_atom a b)&&(beq_atom a' b')&&(beq_perm l m)
| _false
end.

Lemma beq_perm_spec l m : reflect (l=m) (beq_perm l m).

act p a computes the effect of the permutation p on the atom a.

Definition act (p : perm) a :=
fold_right (fun t a
match t with
| (x,y)if beq_atom a x
then y
else if beq_atom a y
then x
else a
end)
a p.
Notation "p ⋈ x" := (act p x) (at level 20).

The effect of the empty permutation is the identity.

Lemma act_nil : a, [] a = a.

List concatenation corresponds to functionnal composition of permutations.

Lemma act_comp_app (p q : perm) x : p (q x) = (p++q) x.

The inverse of a permutation is computed by reversing the list.

Definition inverse (p : perm) : perm :=
rev p.

Notation "p ⋆" := (inverse p) (at level 35).

The inverse is an involutive operation.

Lemma inverse_inv (p : perm) : (p⋆)⋆ = p.

Application of the inverse of a permutation is the functionnal left inverse of the application of the same permutation.

Lemma inverse_comp_l (p : perm) : x, p (p x) = x.

Application of the inverse of a permutation is the functionnal right inverse of the application of the same permutation.

Lemma inverse_comp_r (p : perm) : x, p (p x) = x.

The inverse of a composite permutation is the reverse composition of the inverses of its parts.
Permutations are injective.

Lemma perm_inj p x y : p x = p y x = y.

Permutations are bijective.

Lemma perm_bij : p x y, p x = p y x = y.

Two permutations p and q are considered equivalent when the functions p_ and q_ are extensionnally equal.

Definition equiv_perm p q := a, p a = q a.
Notation " p ≌ q " := (equiv_perm p q) (at level 60).

The relation is an equivalence relation.

Lemma equiv_perm_refl p : p p.
Lemma equiv_perm_sym p q : p q q p.
Lemma equiv_perm_trans p q r : p q q r p r.
Global Instance equiv_perm_Equivalence : Equivalence equiv_perm.

If pq then p⋆≌q.
If pq and p'q' then p++p'q++q'.

Global Instance equiv_perm_app :
Proper (equiv_perm ==> equiv_perm ==> equiv_perm)
(@app (Atom×Atom)%type).

Paraphrasing of the definition of .

Global Instance equiv_perm_spec a :
Proper (equiv_perm ==> Logic.eq) (fun pp a).

For every atom a, the permutations [a,a] and [] are equivalent.

Lemma perm_a_a_eq_nil {a} : [a,a] [].

For every permutation p, p⋆++p and p++p are also equivalent to [].