Documentation

LeanPool.NFWeakPartition.AlphaTransportFV

NF weak partition development: AlphaTransportFV.

Free-variable reflexivity for alpha certificates.

EnvFresh env p.vars is intentionally stronger than the semantic freshness needed when an unchanged subtree is reused beneath renamed external binders: vars also exposes binders internal to p. ReflOn records the exact structural invariant instead. Every free occurrence in the subtree must already possess a reflexive AlphaVar certificate. Extending the environment with an identical binder (x,x) then handles occurrences of x by here and lifts every other certificate by there.

source
def NFChoice.DefinitionLeaves.AlphaTransport.ReflOn (env : BinderEnv) (support : Finset SemanticCore.Var) :
Prop

Every name in support has a reflexive alpha-variable certificate.

Equations
Instances For
    source
    theorem NFChoice.DefinitionLeaves.AlphaTransport.ReflOn.mono {env : BinderEnv} {small large : Finset SemanticCore.Var} (h : ReflOn env large) (hsub : small ⊆ large) :
    ReflOn env small
    source
    theorem NFChoice.DefinitionLeaves.AlphaTransport.EnvFresh.reflOn {env : BinderEnv} {support : Finset SemanticCore.Var} (h : EnvFresh env support) :
    ReflOn env support

    The old external-freshness contract implies the exact reflexive invariant.

    source
    theorem NFChoice.DefinitionLeaves.AlphaTransport.ReflOn.extendSame {x : SemanticCore.Var} {env : BinderEnv} {support : Finset SemanticCore.Var} (h : ReflOn env (support.erase x)) :
    ReflOn ((x, x) :: env) support
    source
    theorem NFChoice.DefinitionLeaves.AlphaTransport.AlphaClass.reflOfReflOn (env : BinderEnv) (A : SemanticCore.Class) (h : ReflOn env A.fv) :
    AlphaClass env A A

    Reflexive class alpha certificate from semantic free-variable support.

    source
    theorem NFChoice.DefinitionLeaves.AlphaTransport.AlphaWff.reflOfReflOn (env : BinderEnv) (p : SemanticCore.Wff) (h : ReflOn env p.fv) :
    AlphaWff env p p

    Reflexive formula alpha certificate from semantic free-variable support.

    source
    theorem NFChoice.DefinitionLeaves.AlphaTransport.AlphaClass.reflOfFvFresh (env : BinderEnv) (A : SemanticCore.Class) (h : EnvFresh env A.fv) :
    AlphaClass env A A

    Drop-in replacement for AlphaClass.refl_of_fresh using only fv.

    source
    theorem NFChoice.DefinitionLeaves.AlphaTransport.AlphaWff.reflOfFvFresh (env : BinderEnv) (p : SemanticCore.Wff) (h : EnvFresh env p.fv) :
    AlphaWff env p p

    Drop-in replacement for AlphaWff.refl_of_fresh using only fv.