Library atoms



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),
    a1≠a2 → (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 y ⇒ beq_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.

Lemma inverse_app p q : (p++q)⋆ = q⋆++p⋆.

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 p≌q then p⋆≌q⋆.

Global Instance equiv_perm_inverse :
  Proper (equiv_perm ==> equiv_perm) inverse.

If p≌q 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 p ⇒ p ⋈ 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 [].

Lemma perm_pinv_p_eq_nil {p} : (p⋆++p) ≌ [].

Lemma perm_p_pinv_eq_nil {p} : (p++p⋆) ≌ [].