RIS.atoms: Nominal sets.

Set Implicit Arguments.

Require Import tools.
Require Export Bool.

Section perm.

Set of atoms

Type of atoms

  Class Atom (atom : Set) :=
    {

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

dec_atom :> decidable_set atom;

We also want an infinite number of atoms to be available.

      exists_fresh : ∀ l : list atom, ∃ a, ¬ a ∈ l
    }.
  Context {atom : Set}{Atoms : Atom atom}.

Permutations

Definitions and elementary properties

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 (we will provide a formal proof of this fact later on).

Definition perm {Atoms : Atom atom} := list (atom × atom).

Boolean equality predicate over permutations.

Global Instance dec_perm : decidable_set perm.

Notation for the action of a permutation on a set X.

Class Action (Atoms : Atom atom) X := act : perm → X → X.
Infix " ∙ " := act (at level 20).

Notation for support functions

Class Support (Atoms : Atom atom) (T : Set) := support : T → list atom.
Notation " ⌊ e ⌋ " := (support e).

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

  Global Instance act_atom : (Action Atoms atom) :=
    fun p a ⇒
      fold_right (fun t a ⇒
                    match t with
                    | (x,y) ⇒ if a =?= x
                              then y
                              else if a =?= y
                                   then x
                                   else a
                    end)
                 a p.

The effect of the empty permutation is the identity.

Lemma act_atom_nil : ∀ a, [] ∙ a = a.

List concatenation corresponds to functional composition of permutations.

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

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.

Inverse of a permutation

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).
  Hint Unfold inverse.

The inverse is an involutive operation.

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

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

Lemma inverse_comp_l (p : perm) : ∀ x, p ∗ ∙ (p ∙ x ) = x.
Ltac inv1 p x := replace x with (p∗∙(p∙x));[|apply inverse_comp_l].

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

Lemma inverse_comp_r (p : perm) : ∀ x, p ∙ (p ∗ ∙ x ) = x.
Ltac inv2 p x := replace x with (p∙(p∗∙x));[|apply inverse_comp_r].

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 ∗.

  Hint Resolve inverse_inv inverse_comp_l inverse_comp_r.
  Ltac aux_perm :=
    (rewrite inverse_comp_l in × )
    || (rewrite inverse_comp_r in × )
    || (rewrite inverse_inv in × ).

Equivalence of permutations

Two permutations p and q are considered equivalent when the functions p∙_ and q∙_ are extensionally equal.

Global Instance equiv_perm : SemEquiv perm := fun p q ⇒ ∀ a, p ∙ a = q ∙ a.

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.

  Hint Resolve equiv_perm_refl equiv_perm_sym equiv_perm_trans.

  Global Instance equiv_perm_Equivalence : Equivalence sequiv.

If p≃q then p∗≃q∗.

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

If p≃q and p'≃q' then p++p'≃q++q'.

Global Instance equiv_perm_app :
Proper (sequiv ==> sequiv ==> sequiv) (@app (atom ×atom)%type).

Paraphrasing of the definition of ≃.

Global Instance equiv_perm_spec a :
Proper (sequiv ==> 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 ∗) ≃ [].

Elements

The elements of a permutation are the atoms appearing in it.

Definition elements (p:perm) :=
flat_map (fun ab ⇒ (fst ab )::(snd ab )::[]) p.

Atoms not appearing in p are fixpoints of p.

Lemma elements_inv_act_atom x p : ¬ In x (elements p) → p ∙x = x.

The function elements distributes over concatenations.

Lemma elements_app p q : elements (p ++q) = elements p ++elements q.

The inverse function preserves elements.

Lemma elements_inv_eq q : elements q ≈ elements (q ∗).

For any atom a not mentioned in p and any atom b, p is equivalent to the permutation [(a,p∙b)]++p++[(a,b)].

Lemma factor_perm a b p : ¬ a ∈ elements p → p ≃ [(a ,p ∙b )]++p ++[(a ,b )].

Lifting an action on S to an action on list S

We can lift an action over A to an action over list A by applying it pointwise.

  Global Instance act_lists {S : Set} `{@Action Atoms S} : Action Atoms (list S):=
    fun p l ⇒ map (fun x ⇒ p ∙x) l.

  Lemma act_lists_app {S : Set} `{@Action Atoms S} p (l m : list S) :
    p ∙(l ++m ) = p ∙l ++p ∙m.

  Lemma act_lists_cons {S : Set} `{@Action Atoms S} p (a :S) l :
    p ∙(a ::l ) = p ∙a ::p ∙l.

  Lemma act_lists_length {S : Set} `{@Action Atoms S} p (l : list S) : ⎢p ∙l ⎥ = ⎢l ⎥.

Nominal sets

Definitions

For S to be nominal, it needs to be equipped with an action and a support, and they must satisfy these three axioms.

  Class Nominal (S : Set) {action:Action Atoms S} {supp:Support Atoms S} :=
    {
      action_invariant : ∀ (x : S) π, π ∙ ⌊x ⌋ = ⌊x ⌋ → π ∙ x = x;
      support_action : ∀ (x : S) π, ⌊π ∙ x ⌋ ≈ π ∙ ⌊x ⌋ ;
      action_compose : ∀ (x : S) π π', π ∙ (π' ∙ x ) = (π ++π') ∙ x;
    }.

If x is an element of a nominal set N, a name a is fresh for x if it does not appear in the support of x.

Notation " a # x " := (¬ a ∈ ⌊x⌋) (at level 80).

Canonical nominal structures

Atoms

The support of a is [a].

Global Instance SupportAtom : Support Atoms atom := fun a ⇒ [a ].

The set of atoms is nominal.

Global Instance Nominal_Atom : Nominal atom.

Lists

The support of a list is the union of the supports of its elements. Because we encode supports as duplication-free lists, we remove duplicates using the {{}} function.

Global Instance SupportList (S : Set) `{Support S} : Support Atoms (list S) :=
fun l ⇒ {{flat_map support l }}.

If A is nominal, so is list A.

Global Instance Nominal_list (S : Set) `{Nominal S} : Nominal (list S).

Pairs

We extend the action to pairs by applying the permutation to both components.

Global Instance act_pair {A B : Set} `{@Action Atoms A,@Action Atoms B} : Action Atoms (A ×B):=
fun p l ⇒ (p ∙ (fst l ),p ∙ (snd l )).

The support of a pair is the union of the supports of its components.

Global Instance SupportPair (A B: Set) `{@Support Atoms A,@Support Atoms B}
: Support Atoms (A ×B) := fun p ⇒ {{⌊fst p ⌋++⌊snd p ⌋}}.

If A and B are nominal, so is A×B.

Global Instance Nominal_Pair (A B : Set) `{Nominal A,Nominal B}
: Nominal (A × B).

Natural numbers

We can endow natural numbers with a trivial nominal structure.

  Global Instance action_nat : Action Atoms nat := fun _ n ⇒ n.
  Global Instance support_nat : Support Atoms nat := fun n ⇒ [].
  Global Instance groupAct_nat : Nominal nat.

Option types

If A is nominal, so is option A.

  Global Instance Action_option {A : Set} `{@Action Atoms A} : Action Atoms (option A):=
    fun p l ⇒ match l with None ⇒ None | Some a ⇒ Some (p ∙a) end.

  Global Instance Support_option (A : Set) `{@Support Atoms A}
    : Support Atoms (option A) := fun l ⇒ match l with None ⇒ [] | Some l ⇒ ⌊l ⌋ end.

  Global Instance Nominal_option (A : Set) `{Nominal A} : Nominal (option A).

Sum types

If A and B are nominal, so is A+B.

  Global Instance Action_sum {A B : Set} `{@Action Atoms A,@Action Atoms B} : Action Atoms (A +B):=
    fun p l ⇒ match l with inl a ⇒ inl (p ∙a) | inr b ⇒ inr (p ∙b) end.

  Global Instance Support_sum {A B : Set} `{@Support Atoms A,@Support Atoms B} : Support Atoms (A +B) :=
    fun l ⇒ match l with inl x ⇒ ⌊x⌋ | inr x ⇒ ⌊x⌋ end.

  Global Instance Nominal_sum {A B : Set} `{Nominal A,Nominal B} : Nominal (A +B).

Properties of group actions

Section group.

Context {A : Set} `{Nominal A}.

Equivalent permutations yield the same action.

    Global Instance equiv_perm_act :
      Proper (sequiv ==> Logic.eq ==> Logic.eq) act.

    Lemma act_nil : ∀ a : A, [] ∙ a = a.

    Lemma act_p_pinv p (a : A) : p ∙ (p ∗ ∙ a ) = a.

    Lemma act_pinv_p p (a : A) : p ∗ ∙ (p ∙ a ) = a.

If the support of x is disjoint from the elements of p then x is a fixpoint of p∙.

Lemma elements_inv_act p x :
(∀ a, a ∈ ⌊x ⌋ → ¬ a ∈ elements p ) → p ∙x = x.

The function p∙ is a bijection.

Lemma act_bij p x y : p ∙ x = p ∙ y ↔ x = y.

We can relate the elements appearing in l with those appearing in p∙l.

Lemma In_act_lists a p (l : list A) :
a ∈ (p ∙ l ) ↔ (p ∗ ∙ a ) ∈ l.

A name a is in the support of a list if and only if it is in the support of one of its elements.

Lemma In_support_list a l : a ∈ ⌊l ⌋ ↔ ∃ x, x ∈ l ∧ a ∈ ⌊x ⌋.

The support of a concatenation is equivalent to the concatenation of the supports.

Lemma support_list_app (l m : list A) : ⌊l ++m ⌋ ≈ ⌊l ⌋++⌊m ⌋.

The support of a cons is equivalent to the concatenation of the supports.

Lemma support_list_cons l (w : list A) : ⌊l :: w ⌋ ≈ ⌊l ⌋++⌊w ⌋.

rmfst commutes with the action of permutations.

Remark rmfst_perm `{decidable_set A} p l a : (p ∙l ) ⊖ a = p ∙(l ⊖ p ∗∙a ).

If two permutations coincide on the support of x, then applying either to x yields the same result.

Lemma support_eq_action_eq p q (x : A) :
(∀ a, a ∈⌊x ⌋ → p ∙ a = q ∙ a ) → p ∙ x = q ∙ x.

Simplification lemma.

    Lemma act_cons_a_a :
      ∀ (a : atom) p (x : A), ((a ,a )::p ) ∙ x = p ∙ x.

    Context {B : Set} `{Nominal B}.

The function p∙ distributes over ⊗.

Lemma combine_act p (l : list A)(m : list B) : p ∙ (l ⊗m ) = (p ∙l )⊗(p ∙m ).
End group.

Minimality of support

If a list l supports an element x, then ⌊x⌋ is contained in l.

Lemma minimal_support {X: Set} `{Nominal X} l x :
(∀ π, (∀ a, a ∈ l → π ∙ a = a ) → π ∙ x = x ) → ⌊x ⌋ ⊆ l.

Useful remarks

If l is a list of atoms, then it is equivalent to its support.

Remark support_list_atoms (l : list atom) : ⌊l ⌋ ≈ l.

The action of p on its list of elements yields an equivalent list.

Remark elements_act_lists p : elements p ≈ p ∙(elements p ).

The number of occurrences of a in p∙l is the number of occurrences of p∗∙a in l.

Remark nb_act {A} `{Nominal A,decidable_set A} (a : A) l p :
nb a (p ∙l) = nb (p ∗∙a) l.

The functions {{_}}, prj1, and prj2 commute with the action of permutations.

  Lemma undup_act {A : Set} `{decidable_set A,Nominal A}
        (l : list A) (π : perm) : {{π ∙l }} = π ∙{{l }}.

  Lemma proj1_act {A B : Set} `{Nominal A,Nominal B} (l : list (A ×B)) π :
    π ∙(prj1 l ) = prj1 (π ∙l).

  Lemma proj2_act {A B : Set} `{Nominal A,Nominal B} (l : list (A ×B)) π :
    π ∙(prj2 l ) = prj2 (π ∙l).

Applying permutations preserves duplication-freeness.

Lemma NoDup_act {A : Set} `{Nominal A} (l : list A) (π : perm) :
NoDup l → NoDup (π ∙l).

For any permutation π, the function π∙_ is injective and surjective.

Global Instance injective_perm {A} `{Nominal A} π : injective (act π).
Global Instance surjective_perm {A} `{Nominal A} π : surjective (act π).

The function π∙_ is supported, and its support can be computed from the elements of π.

  Global Instance has_support_perm (π : perm) :
    has_support (act π) ((fun a ⇒ negb (π ∙a =?=a)) :> elements π).
  Hint Resolve injective_perm surjective_perm has_support_perm.

The group_by_fst function commutes with group actions.

  Lemma group_by_fst_act
        {A B : Set} `{Nominal A,Nominal B} `{decidable_set A} :
    ∀ (l : list (A ×B)) π, π ∙ (group_by_fst l ) = group_by_fst (π ∙l).

  Remark reform {N} `{Nominal N} (l : list N) π :
    map (act π) l = π ∙l.

  Remark act_eq_equivalent {N} `{Nominal N} (π π': perm) (l m : list N) :
    l ≈ m → π ∙ m = π' ∙ m ↔ π ∙ l = π' ∙ l.

  Global Instance equivalent_act {N} `{Nominal N} :
    Proper (sequiv ==> (@equivalent N ) ==> (@equivalent N )) act.

Equivariant functions

A function between two nominal sets is equivalent if it commutes with the group actions.

Class Equivariant {A B} `{Nominal A,Nominal B} (f : A → B) :=
equivariant : ∀ a p, p ∙(f a ) = f (p ∙a).

If f is equivariant, then the support of f x is contained in that of x.

Lemma support_image_equivariant {A B : Set}`{Nominal A,Nominal B} :
∀ (f : A → B) x, Equivariant f → ⌊f x ⌋ ⊆ ⌊x ⌋.

End perm.