Support Utilities for Nominal Sets

This file provides additional utilities and notations for working with support in nominal sets. It builds on top of the core definitions in Nominal.lean and Fresh.lean.

Main definitions

• supp - Convenient alias for NomSet.supp
• Notation a # x for freshness (using Fresh from Fresh.lean)

References

• Pitts, Nominal Sets: Names and Symmetry in Computer Science, Cambridge University Press, 2013, Chapter 2.
• 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

Support utilities

@[reducible, inline]

noncomputable abbrev CatCrypt.Nominal.supp {α : Type u_1} [NomSet α] (x : α) : Finset Atom

Get the support of a value in a nominal set (convenient alias for NomSet.supp)

Equations

• CatCrypt.Nominal.supp x = CatCrypt.Nominal.NomSet.supp x

Notation

def CatCrypt.Nominal.«term_#_» : Lean.TrailingParserDescr

Notation for freshness: a # x means atom a is fresh for x

Equations

• CatCrypt.Nominal.«term_#_» = Lean.ParserDescr.trailingNode `CatCrypt.Nominal.«term_#_» 50 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " # ") (Lean.ParserDescr.cat `term 0))

Additional lemmas

theorem CatCrypt.Nominal.Disj.symm {α : Type u_1} {β : Type u_2} [NomSet α] [NomSet β] {x : α} {y : β} (h : Disj x y) : Disj y x

Disjointness is symmetric

noncomputable def CatCrypt.Nominal.freshForOne {α : Type u_1} [NomSet α] (x : α) : Atom

Fresh atom generation for a single element

Equations

• CatCrypt.Nominal.freshForOne x = CatCrypt.Nominal.Atom.fresh (CatCrypt.Nominal.NomSet.supp x)

theorem CatCrypt.Nominal.freshForOne_fresh {α : Type u_1} [NomSet α] (x : α) : Fresh (freshForOne x) x