LeanPool.NFWeakPartition.SemanticCore.Lowering

NF weak partition development: SemanticCore.Lowering.

source

def NFChoice.SemanticCore.Lowering.lookup {S : Type u_1} {n : ℕ} (xs : DVec S n) (i : Fin n) :

Read a bounded valuation at a Fin index.

Equations

NFChoice.SemanticCore.Lowering.lookup xs i = xs.nth ↑i ⋯

Instances For

source

@[simp]

theorem NFChoice.SemanticCore.Lowering.lookup_cons_zero {S : Type u_1} {n : ℕ} (a : S) (xs : DVec S n) :

lookup (DVec.cons a xs) 0 = a

source

@[simp]

theorem NFChoice.SemanticCore.Lowering.lookup_cons_succ {S : Type u_1} {n : ℕ} (a : S) (xs : DVec S n) (i : Fin n) :

lookup (DVec.cons a xs) i.succ = lookup xs i

source

def NFChoice.SemanticCore.Lowering.liftRho {n : ℕ} (rho : Var → Fin n) :

Var → Fin (n + 1)

Shift an environment under one newly introduced de Bruijn binder.

Equations

NFChoice.SemanticCore.Lowering.liftRho rho x = (rho x).succ

Instances For

source

def NFChoice.SemanticCore.Lowering.bindRho {n : ℕ} (rho : Var → Fin n) (x : Var) :

Var → Fin (n + 1)

Shift an environment and bind nominal name x at de Bruijn index zero.

Equations

NFChoice.SemanticCore.Lowering.bindRho rho x = Function.update (NFChoice.SemanticCore.Lowering.liftRho rho) x 0

Instances For

source

def NFChoice.SemanticCore.Lowering.lowerClassPred {n : ℕ} (rho : Var → Fin n) (candidate : Fin n) :

Class → Foundation.Formula n

Lower class membership-at-a-candidate to the literal membership language.

Equations

NFChoice.SemanticCore.Lowering.lowerClassPred rho candidate (NFChoice.SemanticCore.Class.cv x_1) = NFChoice.Foundation.Formula.mem candidate (rho x_1)
NFChoice.SemanticCore.Lowering.lowerClassPred rho candidate (NFChoice.SemanticCore.Class.cab x_1 p) = NFChoice.SemanticCore.Lowering.lowerWff (Function.update rho x_1 candidate) p

Instances For

source

def NFChoice.SemanticCore.Lowering.lowerWff {n : ℕ} (rho : Var → Fin n) :

Wff → Foundation.Formula n

Compositional lowering of the nominal core to intrinsically scoped FOL.

Equations

One or more equations did not get rendered due to their size.
NFChoice.SemanticCore.Lowering.lowerWff rho NFChoice.SemanticCore.Wff.falsum = NFChoice.Foundation.Formula.falsum
NFChoice.SemanticCore.Lowering.lowerWff rho (p.imp q) = (NFChoice.SemanticCore.Lowering.lowerWff rho p).imp (NFChoice.SemanticCore.Lowering.lowerWff rho q)
NFChoice.SemanticCore.Lowering.lowerWff rho (NFChoice.SemanticCore.Wff.all x_1 p) = (NFChoice.SemanticCore.Lowering.lowerWff (NFChoice.SemanticCore.Lowering.bindRho rho x_1) p).all
NFChoice.SemanticCore.Lowering.lowerWff rho (NFChoice.SemanticCore.Wff.objEq x_1 y) = NFChoice.Foundation.Formula.equal (rho x_1) (rho y)
NFChoice.SemanticCore.Lowering.lowerWff rho (NFChoice.SemanticCore.Wff.objMem x_1 y) = NFChoice.Foundation.Formula.mem (rho x_1) (rho y)

Instances For

source

def NFChoice.SemanticCore.Lowering.FormulaHolds (S : Fol.Structure Foundation.LNF) {n : ℕ} :

DVec S.carrier n → Foundation.Formula n → Prop

Direct semantics of the small intrinsically scoped formula front end.

Equations

One or more equations did not get rendered due to their size.
NFChoice.SemanticCore.Lowering.FormulaHolds S x✝ NFChoice.Foundation.Formula.falsum = False
NFChoice.SemanticCore.Lowering.FormulaHolds S x✝ (NFChoice.Foundation.Formula.equal x_4 y) = (NFChoice.SemanticCore.Lowering.lookup x✝ x_4 = NFChoice.SemanticCore.Lowering.lookup x✝ y)
NFChoice.SemanticCore.Lowering.FormulaHolds S x✝ (p.imp q) = (NFChoice.SemanticCore.Lowering.FormulaHolds S x✝ p → NFChoice.SemanticCore.Lowering.FormulaHolds S x✝ q)
NFChoice.SemanticCore.Lowering.FormulaHolds S x✝ p.all = ∀ (a : S.carrier), NFChoice.SemanticCore.Lowering.FormulaHolds S (NFChoice.DVec.cons a x✝) p

Instances For

source

@[simp]

theorem NFChoice.SemanticCore.Lowering.formulaHolds_neg {S : Fol.Structure Foundation.LNF} {n : ℕ} {xs : DVec S.carrier n} {p : Foundation.Formula n} :

FormulaHolds S xs p.neg ↔ ¬FormulaHolds S xs p

source

@[simp]

theorem NFChoice.SemanticCore.Lowering.formulaHolds_conj {S : Fol.Structure Foundation.LNF} {n : ℕ} {xs : DVec S.carrier n} {p q : Foundation.Formula n} :

FormulaHolds S xs (p.conj q) ↔ FormulaHolds S xs p ∧ FormulaHolds S xs q

source

@[simp]

theorem NFChoice.SemanticCore.Lowering.formulaHolds_biimp {S : Fol.Structure Foundation.LNF} {n : ℕ} {xs : DVec S.carrier n} {p q : Foundation.Formula n} :

FormulaHolds S xs (p.biimp q) ↔ (FormulaHolds S xs p ↔ FormulaHolds S xs q)

source

@[simp]

theorem NFChoice.SemanticCore.Lowering.formulaHolds_ex {S : Fol.Structure Foundation.LNF} {n : ℕ} {xs : DVec S.carrier n} {p : Foundation.Formula (n + 1)} :

FormulaHolds S xs p.ex ↔ ∃ (a : S.carrier), FormulaHolds S (DVec.cons a xs) p

source

theorem NFChoice.SemanticCore.Lowering.lowerClassPred_sound {S : Fol.Structure Foundation.LNF} {n : ℕ} (rho : Var → Fin n) (xs : DVec S.carrier n) (v : Var → S.carrier) (hrho : ∀ (x : Var), lookup xs (rho x) = v x) (candidate : Fin n) (A : Class) :

Class.Holds S v A (lookup xs candidate) ↔ FormulaHolds S xs (lowerClassPred rho candidate A)

Semantic correctness of class-predicate lowering.

source

theorem NFChoice.SemanticCore.Lowering.lowerWff_sound {S : Fol.Structure Foundation.LNF} {n : ℕ} (rho : Var → Fin n) (xs : DVec S.carrier n) (v : Var → S.carrier) (hrho : ∀ (x : Var), lookup xs (rho x) = v x) (p : Wff) :

Wff.Holds S v p ↔ FormulaHolds S xs (lowerWff rho p)

Semantic correctness of nominal-wff lowering.

source

theorem NFChoice.SemanticCore.Lowering.formulaHolds_toFlypitch {S : Fol.Structure Foundation.LNF} {n : ℕ} (xs : DVec S.carrier n) (p : Foundation.Formula n) :

FormulaHolds S xs p ↔ Fol.realizeBoundedFormula xs p.toFlypitch DVec.nil

The direct front-end semantics agrees with Flypitch realization.

source

theorem NFChoice.SemanticCore.Lowering.lowerWff_realize_iff {S : Fol.Structure Foundation.LNF} {n : ℕ} (rho : Var → Fin n) (xs : DVec S.carrier n) (v : Var → S.carrier) (hrho : ∀ (x : Var), lookup xs (rho x) = v x) (p : Wff) :

Wff.Holds S v p ↔ Fol.realizeBoundedFormula xs (lowerWff rho p).toFlypitch DVec.nil

End-to-end correctness of nominal lowering at the Flypitch boundary.