Add NominalIris: nominal separation as a model of BI (iris-lean)

[spitters]

Add NominalIris: nominal separation as a model of BI (iris-lean)

Summary

Adds nominal separation — separation by disjoint name support — as a model
of (classical, non-affine) bunched implications, with its camera and iOwn
ghost-state reading. This is the separation-logic / Iris counterpart to the
existing mathlib-only nominal-sets development: where Nominal.* gives names,
permutations, support, and the Schanuel-topos categorical layer, NominalIris.*
gives the spatial logic — ∗ as disjoint-support splitting, with atom
permutation (α-renaming) as the group action.

The headline law is the nominal analogue of ℓ₁ ↦ ∗ ℓ₂ ↦ ⊢ ℓ₁ ≠ ℓ₂:

theorem freshName_sep_ne (a b : Atom) :
    (freshName a ∗ freshName b : NomProp) ⊢ iprop(⌜a ≠ b⌝)

realised three ways that are proved to agree: a concrete HeapProp model, the
DisjointLeibnizSet camera, and iOwn/|==> ghost state with an in-logic
name-allocation view-shift.

Packaging

• Self-contained and independent. NominalIris neither depends on nor is
  depended on by the Nominal core; it fixes Atom := ℕ and uses
  Equiv.Perm Atom directly, so it stands alone. (A follow-up could rebase it on
  Nominal.Atom / the Nominal typeclass to share the support theory.)
• The Nominal core stays mathlib-only. iris-lean is required by a separate
  lean_lib NominalIris target only; the default Nominal target is untouched.
• Namespace NominalIris; module root NominalIris.*.

What it adds

Two modules under NominalIris/:

Separation.lean — the nominal-separation BI (reuse route)

NomProp := Iris.Instances.Classical.HeapProp Unit, so the ~40 BI laws are
inherited from iris-lean's classical separation-algebra instance and ∗ is
exactly disjoint-name-support splitting. On top of it:

• the disjoint-union separation algebra on name-worlds (Finset Atom);
• the permutation action on states/propositions, with equivariance of ∗
  (psmulP_sep) and emp;
• the fresh-name resource freshName a and freshName_sep_ne;
• freshness Avoids a P, closed under ∗;
• the И/new quantifier Nnew and the Gabbay–Pitts some = any principle
  (exists_fresh_iff_forall_fresh) for equivariant families;
• proof-mode payoff (freshName_swap / freshName_frame by iintro/iframe).

Camera.lean — the camera and iOwn reading

• The name-set camera is iris-lean's DisjointLeibnizSet (the gset/copset RA);
  NameSet wraps Finset Atom in the Iris.Std.LawfulSet interface.
• den : NameRA → NomProp is proved a monoid morphism into the concrete BI:
  den_unit, den_op (• ↦ ∗, unconditional), den_valid_iff; hence
  concrete_sep_iff_camera_valid — distinctness is camera validity.
• name_alloc — the frame-preserving update ● S ~~> ● (S ∪ {a}) • ◯ {a}.
• ownAuth / ownFresh in IProp GF (the camera as a constOF functor), with
  own_name_alloc, own_name_alloc_init, ownFresh_distinct, a HasNameAlloc
  class + points-to notation (γ ⊨fresh a, γ ⊨auth S).
• A curated Pitts tour (Nominal Sets, CUP 2013): distinctness (§3.1),
  allocation / ν-calculus new (demo_alloc_two_distinct, proof mode),
  equivariance (§1.5), И some = any (§3.2).

Design notes

• Reuse, not from-scratch. NomProp = HeapProp Unit reuses the classical BI
  instance rather than declaring a new Iris.BI; the concrete σ = toNS w
  reading is kept deliberately ("∗ is literally disjoint support").
• Classical fragment only — no ▷/OFE/guarded recursion. Name resources are
  flat and first-order; step-indexing would buy nothing. name_alloc is a
  discrete ghost update.
• Scope — the propositional/state-carrier model, not the categorical
  Schanuel-topos monoidal-closed BI (that lives in Nominal.Category.*).

Dependencies / hygiene

• Adds require iris (iris-lean, v4.30.0) to the lakefile, used only by the
  NominalIris target.
• Extra Mathlib imports over the core: Mathlib.Data.Finset.Card,
  Mathlib.Data.Fintype.EquivFin.
• No sorry. Axioms: propext, Classical.choice, Quot.sound only.
• Builds with lake build NominalIris.

Open questions

1. Rebase on Nominal.Atom / the Nominal typeclass to share support theory?
2. First-class Iris.BI instance vs. the HeapProp Unit reuse route?
3. Hoist the NameSet (Finset-as-Iris.Std.LawfulSet) adapter upstream?

---

🤖 Generated with Claude Code