RIS.representative: generic representation of nominal sets.

Set Implicit Arguments.

Require Export nominalsetoid bijection words.

Orbits

Section orbits.

Definitions

We fix for this section a set of atoms atom.

Context {atom : Set}{𝐀 : Atom atom}.

The base type for orbits is as follows:

Definition orbit_base : Set := list atom × list (list (list atom)).

It naturally forms a nominal set over atom.

Global Instance Nominal_orbit_base : Nominal 𝐀 orbit_base :=
Nominal_Pair (list atom) (list (list (list atom))).

If A is a list of lists atoms, E is a partition of A if

the lists appearing in A are exactly the lists appearing inside some c ∈ E, i.e.: {m|m∈A}={m|∃c∈E: m∈c};
and the lists appearing in E are pairwise disjoint, meaning that if c1 and c2 are in E and there exists a list l appearing both in c1 and c2, then c1 and c2 must contain exactly the same elements.

  Definition partition E (A : list (list atom)) :=
    (∀ m, m ∈ A ↔ ∃ c, c ∈ E ∧ m ∈ c )
    ∧ (∀ l c1 c2, c1 ∈ E → c2 ∈ E → l ∈ c1 → l ∈ c2 → c1 ≈ c2 ).

This property is decidable, and may be checked by the following boolean function.

  Definition partitionb E (A : list (list atom)) :=
    (equivalentb A (concat E))
      && (forallb
            (fun c1 ⇒ forallb
                      (fun c2 ⇒ (equivalentb c1 c2 )
                              ||(forallb (fun l ⇒ negb (inb l c2))c1 ))
                      E)
            E ).

  Lemma partitionb_spec E A : partitionb E A = true ↔ partition E A.

A pair l,E of the orbit base type is an orbit if:

l is duplication-free;
and E is a partition of the shuffles of l.

Definition is_orbit (o : orbit_base) :=
NoDup (fst o) ∧ partition (snd o) (shuffles (fst o)).

This property is decidable.

  Definition is_orbitb (o : orbit_base) :=
    (NoDupb (fst o)) && partitionb (snd o) (shuffles (fst o)).

  Lemma is_orbitb_spec o : is_orbitb o = true ↔ is_orbit o.

We can use set comprehension to define the type of orbits. Formally, orbit is a sigma-type, meaning its elements are pairs o,P, where o has the orbit base type and P is a proof that is_orbitb o=true. Since we the latter is a boolean property, proof irrelevance holds, meaning that (o,P)=(o',P') if and only if o=o'.

Definition orbit : Set := { o : orbit_base | is_orbitb o = true }.

Lemma orbit_eq (o1 o2 : orbit) : $ o1 = $ o2 ↔ o1 = o2.

If o=((l,E),P) is an orbit, we will call l the index of o, and E the relation associated with o.

Notation index := (fun o : orbit ⇒fst ($ o)).
Notation rel := (fun o : orbit ⇒ snd ($ o)).

When o is an orbit, we may see its relation as binary relation between lists of atoms. l1 and l2 are said to be equivalent according to o if both l1 and l2 appear in some c in o's relation. Notice that despite it being called an equivalence, this relation is not actually reflexive, as lists that are not mentioned in o's relation are not related to anybody, including themselves.

  Definition eq_lists (o : orbit) : relation (list atom) :=
    fun l1 l2 ⇒ (∃ c, c ∈ rel o ∧ l1 ∈ c ∧ l2 ∈ c).

  Notation " l1 ={ o }= l2" := (eq_lists o l1 l2) (at level 70).

This relation is decidable.

  Definition eq_listsb (o : orbit) (l1 l2 : list atom) :=
    (existsb (fun c ⇒ inb l1 c && inb l2 c) (snd ($o))).

  Lemma eq_listsb_spec o l1 l2 : eq_listsb o l1 l2 = true ↔ l1 ={o }= l2.

We finally define the equivalence of orbits by stating that o1 ≃ o2 when:

the relations ={o1}= and ={o2}= coincide;
and the index of o1 is related to the index of o2 by the relation of o1.

Global Instance equiv_orbits : SemEquiv orbit :=
fun o1 o2 ⇒ (∀ l1 l2, l1 ={o1 }= l2 ↔ l1 ={o2 }= l2 ) ∧ index o1 ={o1 }= index o2.

Properties of orbits' relations

Whenever l1={o}=l2, l1 must be a shuffle of the index of o.

Lemma eq_lists_shuffle o l1 l2 : l1 ={o }= l2 → l1 ∈ shuffles (index o).

The index of o is related to itself in o's relation.

Lemma eq_lists_fst o : index o ={o }= index o.

Furthermore, every shuffle of the index of o is related to itself in o's relation.

Lemma eq_lists_refl o l : l ∈ shuffles (index o) → l ={o }= l.

The relation of o is transitive and symmetric.

Global Instance eq_lists_trans o : Transitive (eq_lists o).

Global Instance eq_lists_symmetric o : Symmetric (eq_lists o).

From these we can prove that the equivalence of orbits is indeed an equivalence relation.

Global Instance equiv_orbits_Equivalence : Equivalence (@sequiv _ equiv_orbits).

The equivalence of orbits is a decidable relation.

  Definition equiv_orbitsb (o1 o2 : orbit) :=
    (forallb (fun l1 ⇒ forallb (fun l2 ⇒ eq_listsb o1 l1 l2 =?= eq_listsb o2 l1 l2)
                             (shuffles (index o1)))
             (shuffles (index o1)))
      && eq_listsb o1 (index o1) (index o2).

  Lemma equiv_orbitsb_eq_shuffle o1 o2 :
    equiv_orbitsb o1 o2 = true → shuffles (index o1) ≈ shuffles (index o2).

  Lemma equiv_orbitsb_spec o1 o2 : equiv_orbitsb o1 o2 = true ↔ o1 ≃ o2.

Nominal setoid structure.

If E is a partition of A, then π∙E is a partition of π∙A.

Lemma partition_act (π : perm) E A : partition E A → partition (π ∙E) (π ∙A).

If o is an orbit, so is π∙o.

Lemma is_orbit_act (π : perm) o : is_orbit o → is_orbit (π ∙o).

Lemma is_orbitb_act (π : perm) (o : orbit) : is_orbitb (π ∙($o )) = true.

This means that we may lift the action from the base type of orbits to the type of orbits.

Global Instance ActOrb : ActionSetoid _ 𝐀 orbit :=
(fun p o ⇒ exist _ (p ∙ ($ o )) (is_orbitb_act p o)).

We define the support of an orbit to be its index.

Global Instance SuppOrbit : SupportSetoid _ 𝐀 orbit := fun o ⇒ index o.

This structure satisfies the axioms of nominal setoids over 𝐀.

Global Instance NomOrbit : NominalSetoid 𝐀 orbit.

End orbits.

Notation index := (fun o : orbit _ ⇒fst ($ o)).

Notation rel := (fun o : orbit _ ⇒ snd ($ o)).

Notation " l1 ={ o }= l2" := (eq_lists o l1 l2) (at level 70).

Lifting injections between sets of atoms as injective morphisms between sets of orbits.

Section eta.

In this section, we fix two sets of atoms A and B, and an injective function f:A→B.

Context {A B : Set} {𝐀: Atom A} {𝐁 : Atom B}.
Context {f : A → B} {inj : injective f}.

Given a permutation π over A, we can define a permutation ⦅π⦆ over B by applying f to every atom appearing in π.

Definition lift : @perm A _ → @perm B _ := map (fun x ⇒ (f (fst x),f (snd x))).
Notation " ⦅ p ⦆ " := (lift p).

This lifting satisfies the following identity.

Lemma lift_f π a : ⦅π ⦆ ∙ (f a ) = f (π ∙ a).

It preserves permutation equivalence.

Global Instance lift_equiv : Proper (sequiv ==> sequiv) lift.

Lifting commutes with taking the inverse of a permutation.

Lemma lift_perm_inverse π : ⦅π ⦆∗ = ⦅π ∗⦆.

We can lift an orbit over A into an orbit over B by applying f pointwise.

Definition inject_aux : orbit 𝐀 → orbit_base B :=
fun o ⇒ (map f (index o),map (map (map f)) (rel o)).

This function indeed produces a valid orbit.

Lemma inject_orbit (o : orbit 𝐀) : is_orbit (inject_aux o).

Lemma inject_orbitb (o : orbit 𝐀) : is_orbitb (inject_aux o) = true.

We encapsulate this in the following function between sigma-types.

Definition inject : orbit 𝐀 → orbit 𝐁 := fun o ⇒ exist _ (inject_aux o) (inject_orbitb o).

This function is injective up-to equivalence.

Lemma inject_injection o1 o2 : inject o1 ≃ inject o2 → o1 ≃ o2.

The support of the image of o is the image of the support of o by f.

Lemma inject_support o : ⌈inject o ⌉ = (map f ⌈o ⌉).

inject is an equivariant function.

Lemma inject_equivariant : ∀ π o, inject (π ⊙ o) ≃ ⦅π ⦆ ⊙ (inject o ).

It preserves equivalence.

Lemma inject_equiv : Proper (sequiv ==> sequiv) inject.

End eta.

Representation of a nominal set

Section orbitX.

We fix a set of atoms atom and an alphabet X, that is a decidable set nominal in atom.

Context {atom X: Set}{𝐀 : Atom atom} {𝐗 : Alphabet 𝐀 X}.

Hypothesis

We assume to be given a function ⦃_⦄ from X to lists of atoms. We call it the normalised support.

Parameter nf_supp : X → list atom.
Notation " ⦃ x ⦄ " := (nf_supp x).

This function should satisfy the following properties:

⦃x⦄ is a shuffle of the list {{⌊x⌋}}, meaning it contains exactly the elements of the support of x and it is duplication-free;
for every x∈X and every permutation p, there exists a permutation q such that
- p and q produce the same element when applied to x, i.e. p∙x=q∙x;
- the normalised support of p∙x can be obtained by applying q to the normalised support of x.

  Axiom nf_supp_shuffle_support : ∀ x : X, ⦃x ⦄ ∈ shuffles {{⌊x ⌋}}.
  Axiom coherent_support : ∀ (x : X) (p : perm), ∃ q, ⦃p ∙x ⦄ = q ∙⦃x ⦄ ∧ p ∙x = q ∙x.

  Remark nf_supp_support : ∀ x : X, ⦃x ⦄ ≈ ⌊x ⌋.

  Remark nf_supp_nodup : ∀ x, NoDup ⦃x ⦄.

  Remark nf_supp_action x π : ⦃π ∙x ⦄ ≈ π ∙ ⦃x ⦄.

The normalised support function enjoys a form of injectivity: the permutation π leaves x unchanged if and only if the normalised supports of x and π∙x coincide.

Proposition nf_supp_inj (x : X) π : ⦃x ⦄ = ⦃π ∙x ⦄ ↔ x = π ∙ x.

The proof of the following proposition relies on lemma RIS.atoms.support_eq_action_eq, i.e. the fact that for any two permutations π,π' and any element x, if π∙a=π'∙a for every a in the support of x, then π∙x=π'∙x.

Proposition act_make_perm (x : X) π : π ∙ x = (⦃x ⦄ >> π ∙⦃x ⦄) ∙ x.

Group-theoretic orbits

x and y are said to be in the same orbit if there is a permutation sending y to x.

Definition same_orbit (x y : X) := ∃ π, x = π ∙ y.

The relation "being in the same orbit" is an equivalence.

Global Instance same_orbit_Equivalence : Equivalence same_orbit.

If x and y are in the same orbit, then we may build a witnessing permutation by simply taking ⦃y⦄ >> ⦃x⦄. The converse holds trivially.

Corollary same_orbit_get_perm x y : same_orbit x y ↔ x = (⦃y ⦄ >> ⦃x ⦄) ∙ y.

Using this last result, we can build the following boolean function to check whether two elements are in the same orbit.

Definition same_orbitb (x y : X) := x =?= ((⦃y ⦄ >> ⦃x ⦄) ∙ y ).

Lemma same_orbitb_spec x y : same_orbitb x y = true ↔ same_orbit x y.

Representation

We can now map X into a set of orbits. First we define the function orbitX_aux sending elements of X to the base type of orbits.

Definition orbitX_aux (x : X) : orbit_base atom :=
(⦃x ⦄,group_by_fst (map (fun l ⇒ ((⦃x ⦄ >> l )∙x ,l )) (shuffles ⦃x ⦄))).

We then proceed to show that for any x to the pair produced by orbitX_aux x is indeed an orbit.

Lemma is_orbit_orbitX x : is_orbit (orbitX_aux x).

Corollary is_orbitb_orbitX x : is_orbitb (orbitX_aux x) = true.

Finally, we use these to build a valid orbit from any x.

Definition orbitX x : orbit 𝐀 := exist _ (orbitX_aux x) (is_orbitb_orbitX x).

This function satisfies the same kind of injectivity as normalised supports.

Lemma orbitX_inj x π : orbitX x ≃ orbitX (π ∙x) → x = π ∙x.

The following observation will be useful later on: two lists l1 and l2 are equivalent according to orbitX x if and only if there are two permutations p1 and p2 such that:

p1 sends elements of the support of x to elements of the support of x;
the actions of p1 and p2 on x coincide;
l1 is p1∙⦃x⦄ and l2 is p2∙⦃x⦄.

  Remark eq_lists_orbitX x l1 l2 :
    l1 ={orbitX x }= l2 ↔ (∃ p1 p2 : perm , p1 ∙ ⦃x ⦄ ≈ ⦃x ⦄ ∧ p1 ∙ x = p2 ∙x
                                          ∧ p1 ∙ ⦃x ⦄ = l1 ∧ p2 ∙ ⦃x ⦄ = l2 ).

orbitX is an equivariant function.

Lemma orbitX_perm π x : orbitX (π ∙x) ≃ π ⊙ orbitX x.

End orbitX.

Pointers

Section pointers.

We fix a set of atoms atom.

Context {atom: Set}{𝐀 : Atom atom}.

A pointer over atom is either a free name a! or a natural number n?.

  Inductive pointer := free : atom → pointer | bound : nat → pointer.
  Notation " a ! " := (free a)(at level 20).
  Notation " a ? " := (bound a)(at level 20).

Pointers can be treated as atoms.

Global Instance 𝐏 : Atom pointer.

As any constructor, the function free is injective.

Global Instance injective_free : injective free.

The set of pointers is nominal in atom.

  Global Instance act_pointer : Action 𝐀 pointer :=
    fun p b ⇒ match b with a! ⇒ (p ∙a)! | _ ⇒ b end.
  Global Instance support_pointer : Support 𝐀 pointer :=
    fun b ⇒ match b with a! ⇒ ⌊a⌋ | _ ⇒ [] end.

  Global Instance groupAct_pointer : Nominal 𝐀 pointer.

  Notation " ⦅ π ⦆ " := (lift free π).

Notice that applying a lifted permutation ⦅p⦆ to a free name is the same as applying p to that name, and applying it to a bound number leaves it unchanged.

Remark act_free (π : @perm _ 𝐀) (a : atom) : ⦅π ⦆ ∙ (a !) = (π ∙ a )!.

Remark act_bound π n : ⦅π ⦆ ∙ (n ?) = n ?.

Furthermore, the action of ⦅π⦆ on any pointer p coincide with the action of π on p. The first action comes from the nominal structure RIS.atoms.Nominal_Atom pointer, while the second is an instance of groupAct_pointer.

Remark lift_perm_invisible π (p : pointer) : ⦅π ⦆ ∙ p = π ∙ p.

End pointers.

The function η

Section s.

We again fix a set of atoms and an alphabet.

  Context {atom X: Set}{𝐀 : Atom atom} {𝐗 : Alphabet 𝐀 X}.
  Notation " a ! " := (free a)(at level 20).
  Notation " a ? " := (@bound atom a)(at level 20).
  Notation " ⦅ p ⦆ " := (lift free p).

We now proceed to map elements from X to elements of a nominal setoid over pointer, namely the set Repr built out of pairs of an element from X, considered up-to same_orbit, and an orbit over pointer, considered up-to ≃.

  Definition Repr : Set := X × (orbit 𝐏 ).

  Global Instance eqRepr : SemEquiv Repr :=
    fun r1 r2 ⇒ (same_orbit (fst r1) (fst r2)) ∧ snd r1 ≃ snd r2.

The equivalence of representatives is decidable.

  Definition eqReprb : Repr → Repr → bool :=
    fun r1 r2 ⇒ same_orbitb (fst r1) (fst r2) && equiv_orbitsb (snd r1) (snd r2).

  Lemma eqReprb_spec : ∀ x y, reflect (x ≃ y) (eqReprb x y).

Repr is a nominal setoid over pointer.

  Global Instance ActRepr : ActionSetoid _ 𝐏 Repr :=
    fun π r ⇒ (fst r ,π ⊙snd r ).

  Global Instance SuppRepr : SupportSetoid _ 𝐏 Repr :=
    fun r ⇒ ⌈snd r ⌉.

  Global Instance NomSetRepr : NominalSetoid 𝐏 Repr.

The function η maps x to the pair x,inject free (orbitX x).

Definition η : X → Repr := fun x ⇒ (x ,inject free (orbitX x)).

It is injective up-to ≃.

Lemma η_inj : ∀ x y, η x ≃ η y → x = y.

η is equivariant.

Lemma η_equivariant : ∀ p x, η (p ∙x) ≃ ⦅p ⦆⊙(η x ).

The support of η x is the set of a! such that a is in the support of x.

Lemma η_support : ∀ x, ⌈η x ⌉ ≈ (map free ⌊x ⌋).

End s.

Notation " ⦅ p ⦆ " := (lift free p).
Notation " a ! " := (free a)(at level 20).