Name Abstraction

This file defines name abstraction [𝔸]α from Pitts' nominal sets (Chapter 4). Name abstraction quotients Atom × α by "same up to fresh renaming", providing the nominal analogue of alpha-equivalence for binders.

Main definitions

• AbsRel - The equivalence relation: (a, x) ~ (b, y) iff for some fresh c, swap a c • x = swap b c • y
• NameAbs α - The quotient type [𝔸]α = (Atom × α) / AbsRel
• abs a x - The abstraction constructor
• concretize - Open an abstraction at a given fresh name

Main results

• abs_rename - Key computation rule: abs a x = abs b (swap a b • x) when b # x
• instMulActionNameAbs - Permutation action: π • abs a x = abs (π a) (π • x)
• instNomSetNameAbs - Name abstraction forms a nominal set
• concretize_abs - Concretion inverts abstraction

References

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

Support-agreement and swap-conjugation lemmas

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

Two permutations that agree on the support of x act the same on x.

theorem CatCrypt.Nominal.swap_mul_comm (π : FinPerm) (a b : Atom) : FinPerm.swap (π.apply a) (π.apply b) * π = π * FinPerm.swap a b

Conjugation identity for swaps through a permutation: swap (π a) (π b) * π = π * swap a b.

theorem CatCrypt.Nominal.swap_smul_conj {α : Type u_1} [NomSet α] (π : FinPerm) (a b : Atom) (x : α) : FinPerm.swap (π.apply a) (π.apply b) • π • x = π • FinPerm.swap a b • x

Conjugation of swap through a permutation on NomSet actions: swap (π a) (π b) • (π • x) = π • (swap a b • x).

theorem CatCrypt.Nominal.swap_fresh_conj {α : Type u_1} [NomSet α] (a c d : Atom) (x : α) (hc : Fresh c x) (hd : Fresh d x) : FinPerm.swap a d • x = FinPerm.swap c d • FinPerm.swap a c • x

If c # x and d # x, then swap a d • x = swap c d • (swap a c • x). Key tool for relating different fresh witnesses.

theorem CatCrypt.Nominal.fresh_act_of_fresh {α : Type u_1} [NomSet α] (π : FinPerm) (c : Atom) (x : α) (h : Fresh c x) : Fresh (π.apply c) (π • x)

Freshness is preserved by permutation actions.

Swap conjugation

theorem CatCrypt.Nominal.FinPerm.swap_conj (a b c : Atom) (hca : c ≠ a) (hcb : c ≠ b) : swap a b * swap a c * swap a b = swap b c

Swap conjugation: (a b)(a c)(a b) = (b c) when c ≠ a and c ≠ b.

The abstraction equivalence relation

def CatCrypt.Nominal.AbsRel {α : Type u_1} [NomSet α] (p q : Atom × α) : Prop

The name abstraction equivalence relation. Two pairs (a, x) and (b, y) are related if for some atom c fresh for both, swap a c • x = swap b c • y.

Equations

• CatCrypt.Nominal.AbsRel p q = ∃ (c : CatCrypt.Nominal.Atom), CatCrypt.Nominal.Fresh c (p, q) ∧ CatCrypt.Nominal.FinPerm.swap p.1 c • p.2 = CatCrypt.Nominal.FinPerm.swap q.1 c • q.2

theorem CatCrypt.Nominal.AbsRel.fresh_pair {α : Type u_1} [NomSet α] (c : Atom) (p q : Atom × α) (h : Fresh c (p, q)) : c ≠ p.1 ∧ Fresh c p.2 ∧ c ≠ q.1 ∧ Fresh c q.2

Decompose freshness for a nested pair (p, q) : (Atom × α) × (Atom × α).

theorem CatCrypt.Nominal.AbsRel.mk_fresh_pair {α : Type u_1} [NomSet α] (c : Atom) (p q : Atom × α) (h1 : c ≠ p.1) (h2 : Fresh c p.2) (h3 : c ≠ q.1) (h4 : Fresh c q.2) : Fresh c (p, q)

Build freshness for a nested pair from components.

theorem CatCrypt.Nominal.AbsRel.refl {α : Type u_1} [NomSet α] (p : Atom × α) : AbsRel p p

AbsRel is reflexive.

theorem CatCrypt.Nominal.AbsRel.symm {α : Type u_1} [NomSet α] {p q : Atom × α} (h : AbsRel p q) : AbsRel q p

AbsRel is symmetric.

theorem CatCrypt.Nominal.AbsRel.trans {α : Type u_1} [NomSet α] {p q r : Atom × α} (hpq : AbsRel p q) (hqr : AbsRel q r) : AbsRel p r

AbsRel is transitive. Uses swap_fresh_conj to unify witnesses.

def CatCrypt.Nominal.absRelSetoid (α : Type u_1) [NomSet α] : Setoid (Atom × α)

The setoid for name abstraction.

Equations

• CatCrypt.Nominal.absRelSetoid α = { r := CatCrypt.Nominal.AbsRel, iseqv := ⋯ }

The quotient type

@[reducible, inline]

abbrev CatCrypt.Nominal.NameAbs (α : Type u_1) [NomSet α] : Type u_1

Name abstraction: the quotient of Atom × α by the equivalence "same up to fresh renaming". This is the nominal analogue of alpha-equivalence classes for binders (Pitts, Chapter 4). Defined as abbrev so instance search can see through it.

Equations

• CatCrypt.Nominal.NameAbs α = Quotient (CatCrypt.Nominal.absRelSetoid α)

def CatCrypt.Nominal.«term[𝔸]_» : Lean.ParserDescr

Equations

• CatCrypt.Nominal.«term[𝔸]_» = Lean.ParserDescr.node `CatCrypt.Nominal.«term[𝔸]_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "[𝔸]") (Lean.ParserDescr.cat `term 0))

def CatCrypt.Nominal.abs {α : Type u_1} [NomSet α] (a : Atom) (x : α) : NameAbs α

Construct a name abstraction from an atom and an element.

Equations

• CatCrypt.Nominal.abs a x = ⟦(a, x)⟧

The renaming rule

theorem CatCrypt.Nominal.abs_rename {α : Type u_1} [NomSet α] (a : Atom) (x : α) (b : Atom) (hb : Fresh b x) (hba : b ≠ a) : abs a x = abs b (FinPerm.swap a b • x)

The fundamental computation rule for name abstraction: abs a x = abs b (swap a b • x) when b is fresh for x.

The permutation action

theorem CatCrypt.Nominal.AbsRel_act {α : Type u_1} [NomSet α] (π : FinPerm) {p q : Atom × α} (h : AbsRel p q) : AbsRel (π • p.1, π • p.2) (π • q.1, π • q.2)

Permutations preserve the abstraction equivalence relation.

@[implicit_reducible]

noncomputable instance CatCrypt.Nominal.instMulActionNameAbs {α : Type u_1} [NomSet α] : MulAction FinPerm (NameAbs α)

MulAction instance for NameAbs: π • abs a x = abs (π a) (π • x).

Equations

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

@[simp]

theorem CatCrypt.Nominal.smul_abs {α : Type u_1} [NomSet α] (π : FinPerm) (a : Atom) (x : α) : π • abs a x = abs (π • a) (π • x)

The permutation action commutes with abs: π • abs a x = abs (π a) (π • x).

The nominal-set instance

@[implicit_reducible]

noncomputable instance CatCrypt.Nominal.instNomSetNameAbs {α : Type u_1} [NomSet α] : NomSet (NameAbs α)

NomSet instance for NameAbs.

Equations

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

The some-any property and concretion

theorem CatCrypt.Nominal.absRel_any_fresh {α : Type u_1} [NomSet α] {p q : Atom × α} (h : AbsRel p q) (d : Atom) (hd : Fresh d (p, q)) : FinPerm.swap p.1 d • p.2 = FinPerm.swap q.1 d • q.2

The "some-any" property: if AbsRel holds with one fresh witness, it holds with any fresh witness.

noncomputable def CatCrypt.Nominal.concretize {α : Type u_1} [NomSet α] (a : Atom) (nabs : NameAbs α) : α

Concretize a name abstraction at atom a: open abs b x as swap a b • x. Uses Quotient.out for the definition; meaningful when a # nabs.

Equations

• CatCrypt.Nominal.concretize a nabs = CatCrypt.Nominal.FinPerm.swap a (Quotient.out nabs).1 • (Quotient.out nabs).2

theorem CatCrypt.Nominal.concretize_abs {α : Type u_1} [NomSet α] (a b : Atom) (x : α) (ha : Fresh a (abs b x)) : concretize a (abs b x) = FinPerm.swap a b • x

Concretize applied to an abstraction.

theorem CatCrypt.Nominal.concretize_abs_self {α : Type u_1} [NomSet α] (a : Atom) (x : α) (ha : Fresh a (abs a x)) : concretize a (abs a x) = x

Concretize applied to an abstraction where a matches.

Equivariance and the functorial map

def CatCrypt.Nominal.Equivariant {α : Type u_1} {β : Type u_2} [MulAction FinPerm α] [MulAction FinPerm β] (f : α → β) : Prop

An equivariant function preserves the permutation action.

Equations

• CatCrypt.Nominal.Equivariant f = ∀ (π : CatCrypt.Nominal.FinPerm) (x : α), f (π • x) = π • f x

theorem CatCrypt.Nominal.supp_sub_of_equivariant {α : Type u_1} {β : Type u_2} [NomSet α] [NomSet β] (f : α → β) (hf : Equivariant f) (x : α) : NomSet.supp (f x) ⊆ NomSet.supp x

Support inclusion for equivariant functions.

noncomputable def CatCrypt.Nominal.NameAbs.map {α : Type u_1} {β : Type u_2} [NomSet α] [NomSet β] (f : α → β) (hf : Equivariant f) : NameAbs α → NameAbs β

Functorial map on name abstractions: lift an equivariant function.

Equations

• CatCrypt.Nominal.NameAbs.map f hf = Quotient.map (fun (p : CatCrypt.Nominal.Atom × α) => (p.1, f p.2)) ⋯

theorem CatCrypt.Nominal.NameAbs.map_abs {α : Type u_1} {β : Type u_2} [NomSet α] [NomSet β] (f : α → β) (hf : Equivariant f) (a : Atom) (x : α) : map f hf (abs a x) = abs a (f x)

Computation rule for NameAbs.map: it acts as f under the abstraction.

The elimination principle (nominal recursion)

Pitts, Nominal Sets, Chapter 8: to define a function out of [𝔸]α one needs a derived eliminator. NameAbs.lift is the underlying Quotient.lift: given an atom-indexed f : Atom → α → β that respects the α-equivalence relation AbsRel, it produces NameAbs.lift f h : [𝔸]α → β together with the computation (β-)rule NameAbs.lift f h (abs a x) = f a x.

NameAbs.liftFCB packages the standard freshness condition for binders (FCB): rather than requiring compatibility on all AbsRel-related inputs directly, it derives it from equivariance of f together with a freshness witness a # f a x (Pitts' "some atom is fresh for its own image"). This is the honest nominal recursor with a genuine freshness side-condition.

def CatCrypt.Nominal.NameAbs.lift {α : Type u_1} {β : Type u_2} [NomSet α] (f : Atom → α → β) (h : ∀ (a a' : Atom) (x x' : α), AbsRel (a, x) (a', x') → f a x = f a' x') : NameAbs α → β

Nominal elimination principle (Pitts, Ch. 8). Lift an atom-indexed function f : Atom → α → β that respects the α-equivalence relation AbsRel to a total function [𝔸]α → β out of the abstraction. This is Quotient.lift over AbsRel, with compatibility supplied by h. See NameAbs.lift_abs for the computation rule.

Equations

• CatCrypt.Nominal.NameAbs.lift f h = Quotient.lift (fun (p : CatCrypt.Nominal.Atom × α) => f p.1 p.2) ⋯

@[simp]

theorem CatCrypt.Nominal.NameAbs.lift_abs {α : Type u_1} {β : Type u_2} [NomSet α] (f : Atom → α → β) (h : ∀ (a a' : Atom) (x x' : α), AbsRel (a, x) (a', x') → f a x = f a' x') (a : Atom) (x : α) : lift f h (abs a x) = f a x

Computation rule (β-rule) for the nominal eliminator: NameAbs.lift f h (abs a x) = f a x.

theorem CatCrypt.Nominal.NameAbs.absRel_respect_of_swap {α : Type u_1} {β : Type u_2} [NomSet α] (f : Atom → α → β) (hswap : ∀ (a c : Atom) (x : α), Fresh c x → c ≠ a → f a x = f c (FinPerm.swap a c • x)) (a a' : Atom) (x x' : α) : AbsRel (a, x) (a', x') → f a x = f a' x'

The FCB compatibility lemma: for an equivariant f (in each fixed atom argument reindexed by the permutation) satisfying the freshness condition "some atom fresh for f's output is also fresh for the abstracted atom", α-equivalent inputs get equal images. Concretely: if f is compatible with swapping the bound name away to any sufficiently fresh atom, then it respects AbsRel.

Here the side condition is packaged as hswap: f commutes with renaming the bound atom by a swap through a fresh c — the derived form of Pitts' FCB ∀ a x, ∃ c, c # (a, x, f a x) ∧ …. Given this, AbsRel (a,x) (a',x') forces f a x = f a' x'.