Nominal Sets

This file defines the typeclass for nominal sets - sets equipped with a permutation action and finite support.

Main definitions

• NomSet - A typeclass for nominal sets (with finite support)

The permutation action uses Mathlib's MulAction FinPerm α, giving access to π • x notation, one_smul, mul_smul, inv_smul_smul, smul_inv_smul, orbit/stabilizer theory, etc.

References

• Pitts, Nominal Sets: Names and Symmetry in Computer Science, Cambridge University Press, 2013, Chapters 2-3.
• Larsen and Schürmann, Nominal State-Separating Proofs, IACR ePrint 2025/598 — the SSProve Nominal/ layer this development ports.
• SSProve theories/Crypt/nominal/Nominal.v

Backward-Compatible Aliases

These aliases provide backward compatibility for code that used the old NominalAction API. They are definitionally equal to the Mathlib equivalents.

@[reducible, inline]

abbrev CatCrypt.Nominal.NominalAction.act {α : Type u_1} [MulAction FinPerm α] (π : FinPerm) (x : α) : α

Backward-compatible alias for π • x.

Equations

• CatCrypt.Nominal.NominalAction.act π x = π • x

@[simp]

theorem CatCrypt.Nominal.NominalAction.one_act {α : Type u_1} [MulAction FinPerm α] (x : α) : act 1 x = x

theorem CatCrypt.Nominal.NominalAction.mul_act {α : Type u_1} [MulAction FinPerm α] (π₁ π₂ : FinPerm) (x : α) : act (π₁ * π₂) x = act π₁ (act π₂ x)

@[simp]

theorem CatCrypt.Nominal.NominalAction.inv_act_act {α : Type u_1} [MulAction FinPerm α] (π : FinPerm) (x : α) : act π⁻¹ (act π x) = x

@[simp]

theorem CatCrypt.Nominal.NominalAction.act_inv_act {α : Type u_1} [MulAction FinPerm α] (π : FinPerm) (x : α) : act π (act π⁻¹ x) = x

theorem CatCrypt.Nominal.NominalAction.act_one {α : Type u_1} [MulAction FinPerm α] (x : α) : act 1 x = x

Backward-compatible alias: act_one = one_smul.

theorem CatCrypt.Nominal.NominalAction.act_mul {α : Type u_1} [MulAction FinPerm α] (π₁ π₂ : FinPerm) (x : α) : act (π₁ * π₂) x = act π₁ (act π₂ x)

Backward-compatible alias: act_mul = mul_smul.

def CatCrypt.Nominal.Supports {α : Type u_1} [MulAction FinPerm α] (s : Finset Atom) (x : α) : Prop

A set S supports an element x if every permutation fixing S pointwise also fixes x.

Equations

• CatCrypt.Nominal.Supports s x = ∀ (π : CatCrypt.Nominal.FinPerm), (∀ a ∈ s, π.apply a = a) → π • x = x

def CatCrypt.Nominal.HasFinSupp {α : Type u_1} [MulAction FinPerm α] (x : α) : Prop

An element is finitely supported if some finite set supports it.

Equations

• CatCrypt.Nominal.HasFinSupp x = ∃ (s : Finset CatCrypt.Nominal.Atom), CatCrypt.Nominal.Supports s x

class CatCrypt.Nominal.NomSet (α : Type u_1) extends MulAction CatCrypt.Nominal.FinPerm α : Type u_1

Typeclass for nominal sets - types where every element has finite support and support transforms equivariantly under permutations.

The equivariance property supp_equivariant is essential for reasoning about how supports transform under permutation actions, particularly for the move operation in nominal CatCrypt.

• smul : CatCrypt.Nominal.FinPerm → α → α
• mul_smul (x y : CatCrypt.Nominal.FinPerm) (b : α) : (x * y) • b = x • y • b
• one_smul (b : α) : 1 • b = b
• supp : α → Finset Atom

  The support of an element

• supp_supports (x : α) : Supports (supp x) x

  The support supports the element

• supp_equivariant (x : α) (π : FinPerm) : supp (π • x) = Finset.image (fun (x : Atom) => π.apply x) (supp x)

  Support transforms equivariantly: supp(π • x) = π '' (supp x)

theorem CatCrypt.Nominal.NomSet.supp_supports' {α : Type u_1} [NomSet α] (x : α) : Supports (supp x) x

theorem CatCrypt.Nominal.NomSet.act_eq_of_supp_fixed {α : Type u_1} [NomSet α] (x : α) (π : FinPerm) (h : ∀ a ∈ supp x, π.apply a = a) : π • x = x

If all atoms in the support are fixed, the element is fixed

theorem CatCrypt.Nominal.NomSet.supp_act_eq_image {α : Type u_1} [NomSet α] (x : α) (π : FinPerm) : supp (π • x) = Finset.image (fun (x : Atom) => π.apply x) (supp x)

Support transforms equivariantly

Instances

@[implicit_reducible]

instance CatCrypt.Nominal.instMulActionFinPermAtom : MulAction FinPerm Atom

Atoms form a nominal set with the natural action

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance CatCrypt.Nominal.instNomSetAtom : NomSet Atom

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance CatCrypt.Nominal.instMulActionFinPermProd {α : Type u_1} {β : Type u_2} [MulAction FinPerm α] [MulAction FinPerm β] : MulAction FinPerm (α × β)

Products of MulAction instances are MulAction instances

Equations

• CatCrypt.Nominal.instMulActionFinPermProd = { smul := fun (π : CatCrypt.Nominal.FinPerm) (p : α × β) => (π • p.1, π • p.2), mul_smul := ⋯, one_smul := ⋯ }

@[implicit_reducible]

instance CatCrypt.Nominal.instNomSetProd {α : Type u_1} {β : Type u_2} [NomSet α] [NomSet β] : NomSet (α × β)

Equations

• One or more equations did not get rendered due to their size.