NF weak partition development: NominalAlphaTransport.

Proof-relevant alpha certificates for the direct syntactic replay.

The semantic replay's AlphaVar/AlphaWff/AlphaClass live in Prop, so Lean may not eliminate them into the proof-object type Fol.prf. These parallel Type-valued certificates retain the same constructor shapes. Their eliminator proves that paired nominal binders lower to identical de-Bruijn formulas; the public handlers then reduce alpha transport to reflexivity.

@[reducible, inline]

abbrev NFChoice.DirectNominalPrf.Nominal.TBinderEnv : Type

Paired nominal binders, nearest binder first.

Equations

• NFChoice.DirectNominalPrf.Nominal.TBinderEnv = List (NFChoice.SemanticCore.Var × NFChoice.SemanticCore.Var)

inductive NFChoice.DirectNominalPrf.Nominal.TAlphaVar : TBinderEnv → SemanticCore.Var → SemanticCore.Var → Type

Proof-relevant correspondence of variable occurrences.

• here (env : TBinderEnv) (x y : SemanticCore.Var) : TAlphaVar ((x, y) :: env) x y
• there {env : TBinderEnv} {x y a b : SemanticCore.Var} (ha : a ≠ x) (hb : b ≠ y) (h : TAlphaVar env a b) : TAlphaVar ((x, y) :: env) a b
• free {env : TBinderEnv} {x : SemanticCore.Var} (hl : x ∉ List.map Prod.fst env) (hr : x ∉ List.map Prod.snd env) : TAlphaVar env x x

inductive NFChoice.DirectNominalPrf.Nominal.TAlphaClass : TBinderEnv → SemanticCore.Class → SemanticCore.Class → Type

Proof-relevant alpha equivalence of nominal classes.

• cv {env : TBinderEnv} {x y : SemanticCore.Var} (h : TAlphaVar env x y) : TAlphaClass env (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)
• cab {env : TBinderEnv} {x y : SemanticCore.Var} {p q : SemanticCore.Wff} (h : TAlphaWff ((x, y) :: env) p q) : TAlphaClass env (SemanticCore.Class.cab x p) (SemanticCore.Class.cab y q)

inductive NFChoice.DirectNominalPrf.Nominal.TAlphaWff : TBinderEnv → SemanticCore.Wff → SemanticCore.Wff → Type

Proof-relevant alpha equivalence of nominal formulas.

• falsum {env : TBinderEnv} : TAlphaWff env SemanticCore.Wff.falsum SemanticCore.Wff.falsum
• imp {env : TBinderEnv} {p p' q q' : SemanticCore.Wff} (hp : TAlphaWff env p p') (hq : TAlphaWff env q q') : TAlphaWff env (p.imp q) (p'.imp q')
• all {env : TBinderEnv} {x y : SemanticCore.Var} {p q : SemanticCore.Wff} (h : TAlphaWff ((x, y) :: env) p q) : TAlphaWff env (SemanticCore.Wff.all x p) (SemanticCore.Wff.all y q)
• objEq {env : TBinderEnv} {x x' y y' : SemanticCore.Var} (hx : TAlphaVar env x x') (hy : TAlphaVar env y y') : TAlphaWff env (SemanticCore.Wff.objEq x y) (SemanticCore.Wff.objEq x' y')
• objMem {env : TBinderEnv} {x x' y y' : SemanticCore.Var} (hx : TAlphaVar env x x') (hy : TAlphaVar env y y') : TAlphaWff env (SemanticCore.Wff.objMem x y) (SemanticCore.Wff.objMem x' y')
• classEq {env : TBinderEnv} {A A' B B' : SemanticCore.Class} (hA : TAlphaClass env A A') (hB : TAlphaClass env B B') : TAlphaWff env (SemanticCore.Wff.classEq A B) (SemanticCore.Wff.classEq A' B')
• classMem {env : TBinderEnv} {A A' B B' : SemanticCore.Class} (hA : TAlphaClass env A A') (hB : TAlphaClass env B B') : TAlphaWff env (SemanticCore.Wff.classMem A B) (SemanticCore.Wff.classMem A' B')

def NFChoice.DirectNominalPrf.Nominal.TRhoAgree (env : TBinderEnv) (rho sigma : SemanticCore.Var → ℕ) : Prop

The two de-Bruijn environments agree on every paired occurrence.

Equations

• NFChoice.DirectNominalPrf.Nominal.TRhoAgree env rho sigma = ∀ ⦃x y : NFChoice.SemanticCore.Var⦄ (a : NFChoice.DirectNominalPrf.Nominal.TAlphaVar env x y), rho x = sigma y

theorem NFChoice.DirectNominalPrf.Nominal.TRhoAgree.bind {env : TBinderEnv} {rho sigma : SemanticCore.Var → ℕ} (h : TRhoAgree env rho sigma) (x y : SemanticCore.Var) : TRhoAgree ((x, y) :: env) (bindRho rho x) (bindRho sigma y)

theorem NFChoice.DirectNominalPrf.Nominal.TRhoAgree.update {env : TBinderEnv} {rho sigma : SemanticCore.Var → ℕ} (h : TRhoAgree env rho sigma) (x y : SemanticCore.Var) (candidate : ℕ) : TRhoAgree ((x, y) :: env) (updateRho rho x candidate) (updateRho sigma y candidate)

theorem NFChoice.DirectNominalPrf.Nominal.TRhoAgree.lift {env : TBinderEnv} {rho sigma : SemanticCore.Var → ℕ} (h : TRhoAgree env rho sigma) : TRhoAgree env (liftRho rho) (liftRho sigma)

theorem NFChoice.DirectNominalPrf.Nominal.tRhoAgree_empty (rho : SemanticCore.Var → ℕ) : TRhoAgree [] rho rho

theorem NFChoice.DirectNominalPrf.Nominal.TAlphaClass.lower_eq {env : TBinderEnv} {A B : SemanticCore.Class} (h : TAlphaClass env A B) {rho sigma : SemanticCore.Var → ℕ} (hrho : TRhoAgree env rho sigma) (candidate : ℕ) : lowerClassPred rho candidate A = lowerClassPred sigma candidate B

Alpha-equivalent classes lower to the same candidate predicate.

theorem NFChoice.DirectNominalPrf.Nominal.TAlphaWff.lower_eq {env : TBinderEnv} {p q : SemanticCore.Wff} (h : TAlphaWff env p q) {rho sigma : SemanticCore.Var → ℕ} (hrho : TRhoAgree env rho sigma) : lowerWff rho p = lowerWff sigma q

Alpha-equivalent formulas lower to the same de-Bruijn formula.

def NFChoice.DirectNominalPrf.Nominal.TAlphaWff.neg {env : TBinderEnv} {p q : SemanticCore.Wff} (h : TAlphaWff env p q) : TAlphaWff env p.neg q.neg

Proof-translation construction identified upstream as neg.

Equations

• h.neg = h.imp NFChoice.DirectNominalPrf.Nominal.TAlphaWff.falsum

def NFChoice.DirectNominalPrf.Nominal.TAlphaWff.conj {env : TBinderEnv} {p p' q q' : SemanticCore.Wff} (hp : TAlphaWff env p p') (hq : TAlphaWff env q q') : TAlphaWff env (p.conj q) (p'.conj q')

Proof-translation construction identified upstream as conj.

Equations

• hp.conj hq = (hp.imp hq.neg).neg

def NFChoice.DirectNominalPrf.Nominal.TAlphaWff.biimp {env : TBinderEnv} {p p' q q' : SemanticCore.Wff} (hp : TAlphaWff env p p') (hq : TAlphaWff env q q') : TAlphaWff env (p.biimp q) (p'.biimp q')

Proof-translation construction identified upstream as biimp.

Equations

• hp.biimp hq = (hp.imp hq).conj (hq.imp hp)

def NFChoice.DirectNominalPrf.Nominal.TAlphaWff.ex {env : TBinderEnv} {x y : SemanticCore.Var} {p q : SemanticCore.Wff} (h : TAlphaWff ((x, y) :: env) p q) : TAlphaWff env (SemanticCore.Wff.ex x p) (SemanticCore.Wff.ex y q)

Proof-translation construction identified upstream as ex.

Equations

• h.ex = h.neg.all.neg

def NFChoice.DirectNominalPrf.Nominal.TEnvFresh (env : TBinderEnv) (support : Finset SemanticCore.Var) : Prop

Freshness condition used by mechanically emitted reflexive subtrees.

Equations

• NFChoice.DirectNominalPrf.Nominal.TEnvFresh env support = ∀ ⦃x y : NFChoice.SemanticCore.Var⦄, (x, y) ∈ env → x ≠ y → x ∉ support ∧ y ∉ support

theorem NFChoice.DirectNominalPrf.Nominal.TEnvFresh.of_empty {env : TBinderEnv} {support : Finset SemanticCore.Var} (h : support = ∅) : TEnvFresh env support

Every binder environment is fresh for an empty support.

theorem NFChoice.DirectNominalPrf.Nominal.TEnvFresh.cons {env : TBinderEnv} {support : Finset SemanticCore.Var} {x y : SemanticCore.Var} (hx : x ∉ support) (hy : y ∉ support) (htail : TEnvFresh env support) : TEnvFresh ((x, y) :: env) support

Extend a fresh binder environment by two fresh endpoints.

theorem NFChoice.DirectNominalPrf.Nominal.TEnvFresh.mono {env : TBinderEnv} {small large : Finset SemanticCore.Var} (h : TEnvFresh env large) (hsub : small ⊆ large) : TEnvFresh env small

def NFChoice.DirectNominalPrf.Nominal.TAlphaVar.reflOfFresh (env : TBinderEnv) (u : SemanticCore.Var) (h : TEnvFresh env {u}) : TAlphaVar env u u

Proof-translation construction identified upstream as TAlphaVar.refl_of_fresh.

Equations

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

def NFChoice.DirectNominalPrf.Nominal.TReflOn (env : TBinderEnv) (support : Finset SemanticCore.Var) : Type

Proof-relevant reflexivity for every free variable in a support.

Equations

• NFChoice.DirectNominalPrf.Nominal.TReflOn env support = (⦃u : NFChoice.SemanticCore.Var⦄ → u ∈ support → NFChoice.DirectNominalPrf.Nominal.TAlphaVar env u u)

def NFChoice.DirectNominalPrf.Nominal.TReflOn.mono {env : TBinderEnv} {small large : Finset SemanticCore.Var} (h : TReflOn env large) (hsub : small ⊆ large) : TReflOn env small

Proof-translation construction identified upstream as TReflOn.mono.

Equations

• h.mono hsub hu = h ⋯

def NFChoice.DirectNominalPrf.Nominal.TEnvFresh.reflOn {env : TBinderEnv} {support : Finset SemanticCore.Var} (h : TEnvFresh env support) : TReflOn env support

Proof-translation construction identified upstream as TEnvFresh.reflOn.

Equations

• h.reflOn hu = NFChoice.DirectNominalPrf.Nominal.TAlphaVar.reflOfFresh env u ⋯

def NFChoice.DirectNominalPrf.Nominal.TReflOn.extendSame {x : SemanticCore.Var} {env : TBinderEnv} {support : Finset SemanticCore.Var} (h : TReflOn env (support.erase x)) : TReflOn ((x, x) :: env) support

Proof-translation construction identified upstream as TReflOn.extend_same.

Equations

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

def NFChoice.DirectNominalPrf.Nominal.TAlphaClass.reflOfReflOn (env : TBinderEnv) (A : SemanticCore.Class) (h : TReflOn env A.fv) : TAlphaClass env A A

Reflexive class certificate from exact semantic free-variable support.

Equations

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

def NFChoice.DirectNominalPrf.Nominal.TAlphaWff.reflOfReflOn (env : TBinderEnv) (p : SemanticCore.Wff) (h : TReflOn env p.fv) : TAlphaWff env p p

Reflexive formula certificate from exact semantic free-variable support.

Equations

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

def NFChoice.DirectNominalPrf.Nominal.TAlphaClass.reflOfFvFresh (env : TBinderEnv) (A : SemanticCore.Class) (h : TEnvFresh env A.fv) : TAlphaClass env A A

Drop-in fv-based reflexivity expected by the frozen AlphaEmitter.

Equations

• NFChoice.DirectNominalPrf.Nominal.TAlphaClass.reflOfFvFresh env A h = NFChoice.DirectNominalPrf.Nominal.TAlphaClass.reflOfReflOn env A h.reflOn

def NFChoice.DirectNominalPrf.Nominal.TAlphaClass.reflOfClosed (env : TBinderEnv) (A : SemanticCore.Class) (hclosed : A.fv = ∅) : TAlphaClass env A A

A closed nominal class is alpha-reflexive in every binder environment.

Equations

• NFChoice.DirectNominalPrf.Nominal.TAlphaClass.reflOfClosed env A hclosed = NFChoice.DirectNominalPrf.Nominal.TAlphaClass.reflOfFvFresh env A ⋯

def NFChoice.DirectNominalPrf.Nominal.TAlphaWff.reflOfFvFresh (env : TBinderEnv) (p : SemanticCore.Wff) (h : TEnvFresh env p.fv) : TAlphaWff env p p

Drop-in fv-based reflexivity expected by the frozen AlphaEmitter.

Equations

• NFChoice.DirectNominalPrf.Nominal.TAlphaWff.reflOfFvFresh env p h = NFChoice.DirectNominalPrf.Nominal.TAlphaWff.reflOfReflOn env p h.reflOn

def NFChoice.DirectNominalPrf.Nominal.TAlphaClass.reflOfFresh (env : TBinderEnv) (A : SemanticCore.Class) (h : TEnvFresh env A.vars) : TAlphaClass env A A

Reflexive class certificate under externally fresh renamed binders.

Equations

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

def NFChoice.DirectNominalPrf.Nominal.TAlphaWff.reflOfFresh (env : TBinderEnv) (p : SemanticCore.Wff) (h : TEnvFresh env p.vars) : TAlphaWff env p p

Reflexive formula certificate under externally fresh renamed binders.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.Nominal.alphaBiimp {p q : SemanticCore.Wff} (h : TAlphaWff [] p q) : NPrf (p.biimp q)

Direct syntactic transport for Wff-valued alpha definitions.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.Nominal.alphaClassEq {A B : SemanticCore.Class} (h : TAlphaClass [] A B) : NPrf (SemanticCore.Wff.classEq A B)

Direct syntactic transport for class-valued alpha definitions.

Equations

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