RIS.nominalsetoid: Nominal sets up-to equivalence.
We fix a decidable set of atoms.
We use the notation π ⊙ x for the group action of a nominal setoid, and ⌈x⌉ for its support.
Class ActionSetoid (X : Set) := actoid : perm → X → X.
Infix " ⊙ " := actoid (at level 50).
Class SupportSetoid {A : Atom atom} (X : Set) := suppoid : X → list atom.
Notation " ⌈ x ⌉ " := (suppoid x).
Infix " ⊙ " := actoid (at level 50).
Class SupportSetoid {A : Atom atom} (X : Set) := suppoid : X → list atom.
Notation " ⌈ x ⌉ " := (suppoid x).
A nominal setoid is a set X equipped with a relation ≃, an action ⊙ and a support function ⌈_⌉ satisfying the following axioms:
Class NominalSetoid (X : Set) (equiv : SemEquiv X) (act : ActionSetoid X)
(supp : SupportSetoid X) :=
{
(supp : SupportSetoid X) :=
{
≃ is an equivalence relation;
equivalent elements have equivalent support : if x≃y, then a∈⌈x⌉ ↔ a∈⌈y⌉;
the action in compatible with the equivalence relation ;
the remaining axioms are the same as for nominal sets, except that equality of elements in X has been substituted with ≃.
action_invariant_eq : ∀ (x : X) π, (π ∙ ⌈x⌉ = ⌈x⌉) → (π ⊙ x) ≃ x;
support_action_eq : ∀ x π, ⌈π ⊙ x⌉ ≈ π∙⌈x⌉;
action_compose_eq : ∀ x π π', π ⊙ (π' ⊙ x) ≃ (π++π') ⊙ x
}.
support_action_eq : ∀ x π, ⌈π ⊙ x⌉ ≈ π∙⌈x⌉;
action_compose_eq : ∀ x π π', π ⊙ (π' ⊙ x) ≃ (π++π') ⊙ x
}.
The following observations are straightforward to check directly from the axioms we just listed.
Remark actoid_pinv_p {X : Set} `{NominalSetoid X}:
∀ π x, π∗ ⊙ (π ⊙ x) ≃ x.
Remark actoid_p_pinv {X : Set} `{NominalSetoid X}:
∀ π x, π ⊙ (π∗ ⊙ x) ≃ x.
∀ π x, π∗ ⊙ (π ⊙ x) ≃ x.
Remark actoid_p_pinv {X : Set} `{NominalSetoid X}:
∀ π x, π ⊙ (π∗ ⊙ x) ≃ x.
Permutations that are equivalent as functions yield the same action (even if they are syntactically different): if for every atom a we have π ∙ a = π' ∙ a and if x≃y, then π⊙x≃π'⊙y.
Global Instance eq_act {X : Set} `{NominalSetoid X} :
Proper (sequiv ==> sequiv ==> sequiv) actoid.
Lemma minimal_support_eq {X: Set} `{NominalSetoid X} l x :
(∀ π, (∀ a, a ∈ l → π ∙ a = a) → π ⊙ x ≃ x) → ⌈x⌉ ⊆ l.
Remark ActionSetoid_ext_In {X:Set} `{NominalSetoid X}:
∀ π π' x, (∀ a, a ∈ ⌈x⌉ → π ∙ a = π' ∙ a) → π ⊙ x ≃ π' ⊙ x.
End s.
Proper (sequiv ==> sequiv ==> sequiv) actoid.
Lemma minimal_support_eq {X: Set} `{NominalSetoid X} l x :
(∀ π, (∀ a, a ∈ l → π ∙ a = a) → π ⊙ x ≃ x) → ⌈x⌉ ⊆ l.
Remark ActionSetoid_ext_In {X:Set} `{NominalSetoid X}:
∀ π π' x, (∀ a, a ∈ ⌈x⌉ → π ∙ a = π' ∙ a) → π ⊙ x ≃ π' ⊙ x.
End s.
Let us fix a nominal setoid S over a set of atoms Atom.
Context {atom : Set}{A: Atom atom}.
Context {S : Set} {eqS : SemEquiv S} {actS : ActionSetoid _ A S}
{suppS : SupportSetoid _ A S}.
Context {N: NominalSetoid A S}.
Context {S : Set} {eqS : SemEquiv S} {actS : ActionSetoid _ A S}
{suppS : SupportSetoid _ A S}.
Context {N: NominalSetoid A S}.
We define the action of π on a list by apply π pointwise.
To compute the support of a list, we compute the support of each element, take the union of those, and remove duplicates.
Two lists are equivalent if they have the same length, and if their elements are pointwise equivalent. For instance if l=l1...ln and m=m1...mn, then l≃m if and only if ∀ 1<=i≤n, li≃mi.
Fixpoint semeq_list (l1 l2 : list S) :=
match (l1,l2) with
| ([],[]) ⇒ True
| (a::l1,b::l2) ⇒ (a≃b) ∧ semeq_list l1 l2
| (_::_,[]) | ([],_::_) ⇒ False
end.
Instance SemEquiv_listS : SemEquiv (list S) := semeq_list.
match (l1,l2) with
| ([],[]) ⇒ True
| (a::l1,b::l2) ⇒ (a≃b) ∧ semeq_list l1 l2
| (_::_,[]) | ([],_::_) ⇒ False
end.
Instance SemEquiv_listS : SemEquiv (list S) := semeq_list.
It is a simple matter to check that the operations we have defined indeed define a nominal setoid structure over list S.