Atoms for Nominal Sets

This file defines atoms, which are abstract names used in nominal set theory. Atoms are represented as wrapped natural numbers, providing a countably infinite supply of distinguishable names.

Main definitions

• Atom - The type of atoms (wrapped naturals)
• Atom.fresh - Generate a fresh atom not in a given finite set
• Atom.freshN - Generate n fresh atoms

References

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

structure CatCrypt.Nominal.Atom : Type

Atoms are abstract names, represented as wrapped natural numbers. This provides a countably infinite supply of distinguishable names.

• val : ℕ

def CatCrypt.Nominal.instDecidableEqAtom.decEq (x✝ x✝¹ : Atom) : Decidable (x✝ = x✝¹)

Equations

• CatCrypt.Nominal.instDecidableEqAtom.decEq { val := a } { val := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance CatCrypt.Nominal.instDecidableEqAtom : DecidableEq Atom

Equations

• CatCrypt.Nominal.instDecidableEqAtom = CatCrypt.Nominal.instDecidableEqAtom.decEq

@[implicit_reducible]

instance CatCrypt.Nominal.instHashableAtom : Hashable Atom

Equations

• CatCrypt.Nominal.instHashableAtom = { hash := CatCrypt.Nominal.instHashableAtom.hash }

def CatCrypt.Nominal.instHashableAtom.hash : Atom → UInt64

Equations

• CatCrypt.Nominal.instHashableAtom.hash { val := a } = mixHash 0 (hash a)

@[implicit_reducible]

instance CatCrypt.Nominal.instReprAtom : Repr Atom

Equations

• CatCrypt.Nominal.instReprAtom = { reprPrec := CatCrypt.Nominal.instReprAtom.repr }

def CatCrypt.Nominal.instReprAtom.repr : Atom → ℕ → Std.Format

Equations

• CatCrypt.Nominal.instReprAtom.repr x✝ prec✝ = Std.Format.bracket "{ " (Std.Format.nil ++ Std.Format.text "val" ++ Std.Format.text " := " ++ (Std.Format.nest 7 (repr x✝.val)).group) " }"

def CatCrypt.Nominal.instOrdAtom.ord : Atom → Atom → Ordering

Equations

• CatCrypt.Nominal.instOrdAtom.ord { val := a } { val := b } = (compare a b).then Ordering.eq

@[implicit_reducible]

instance CatCrypt.Nominal.instOrdAtom : Ord Atom

Equations

• CatCrypt.Nominal.instOrdAtom = { compare := CatCrypt.Nominal.instOrdAtom.ord }

theorem CatCrypt.Nominal.Atom.ext {a b : Atom} (h : a.val = b.val) : a = b

theorem CatCrypt.Nominal.Atom.ext_iff {a b : Atom} : a = b ↔ a.val = b.val

@[implicit_reducible]

instance CatCrypt.Nominal.Atom.instInhabited : Inhabited Atom

Equations

• CatCrypt.Nominal.Atom.instInhabited = { default := { val := 0 } }

@[implicit_reducible]

instance CatCrypt.Nominal.Atom.instCoeNat : Coe Atom ℕ

Coercion to natural numbers

Equations

• CatCrypt.Nominal.Atom.instCoeNat = { coe := CatCrypt.Nominal.Atom.val }

@[implicit_reducible]

instance CatCrypt.Nominal.Atom.instLinearOrder : LinearOrder Atom

Linear order on atoms inherited from naturals

Equations

• CatCrypt.Nominal.Atom.instLinearOrder = LinearOrder.lift' CatCrypt.Nominal.Atom.val ⋯

@[implicit_reducible]

instance CatCrypt.Nominal.Atom.instOrderBot : OrderBot Atom

Equations

• CatCrypt.Nominal.Atom.instOrderBot = { bot := { val := 0 }, bot_le := CatCrypt.Nominal.Atom.instOrderBot._proof_1 }

instance CatCrypt.Nominal.Atom.instCountable : Countable Atom

Atoms are countable

def CatCrypt.Nominal.Atom.ofNat (n : ℕ) : Atom

Constructor from natural number

Equations

• CatCrypt.Nominal.Atom.ofNat n = { val := n }

@[simp]

theorem CatCrypt.Nominal.Atom.ofNat_val (n : ℕ) : (ofNat n).val = n

@[simp]

theorem CatCrypt.Nominal.Atom.val_ofNat (a : Atom) : ofNat a.val = a

noncomputable def CatCrypt.Nominal.Atom.offset (s : Finset Atom) : ℕ

Offset: one plus the maximum in a set, used for fresh generation

Equations

• CatCrypt.Nominal.Atom.offset s = if h : s.Nonempty then s.sup' h CatCrypt.Nominal.Atom.val + 1 else 0

theorem CatCrypt.Nominal.Atom.offset_pos_of_nonempty {s : Finset Atom} (h : s.Nonempty) : 0 < offset s

noncomputable def CatCrypt.Nominal.Atom.fresh (s : Finset Atom) : Atom

Fresh atom: the smallest atom not in the given set

Equations

• CatCrypt.Nominal.Atom.fresh s = { val := CatCrypt.Nominal.Atom.offset s }

theorem CatCrypt.Nominal.Atom.fresh_not_mem (s : Finset Atom) : fresh s ∉ s

The fresh atom is not in the original set

theorem CatCrypt.Nominal.Atom.fresh_val_gt {s : Finset Atom} {a : Atom} (ha : a ∈ s) : a.val < (fresh s).val

Fresh atom has value greater than all atoms in the set

noncomputable def CatCrypt.Nominal.Atom.freshN (s : Finset Atom) (n : ℕ) : Finset Atom

Generate n fresh atoms not in the given set

Equations

• CatCrypt.Nominal.Atom.freshN s n = Finset.image (fun (i : ℕ) => { val := CatCrypt.Nominal.Atom.offset s + i }) (Finset.range n)

theorem CatCrypt.Nominal.Atom.freshN_card (s : Finset Atom) (n : ℕ) : (freshN s n).card = n

theorem CatCrypt.Nominal.Atom.freshN_disjoint (s : Finset Atom) (n : ℕ) : Disjoint s (freshN s n)

def CatCrypt.Nominal.Atom.a₀ : Atom

Two distinct atoms

Equations

• CatCrypt.Nominal.Atom.a₀ = { val := 0 }

def CatCrypt.Nominal.Atom.a₁ : Atom

Equations

• CatCrypt.Nominal.Atom.a₁ = { val := 1 }

theorem CatCrypt.Nominal.Atom.a₀_ne_a₁ : a₀ ≠ a₁