Realization machinery for the ZF first-order language

This module sets up the first-order language 𝓛ZF of ZF set theory with a single membership relation, together with notation and metaprogramming infrastructure for building and realizing bounded formulas in models of ZF.

inductive memRel : ℕ → Type

The memRel type.

• mem : memRel 2

def instDecidableEqMemRel.decEq {a✝ : ℕ} (x✝ x✝¹ : memRel a✝) : Decidable (x✝ = x✝¹)

Equations

• instDecidableEqMemRel.decEq memRel.mem memRel.mem = isTrue instDecidableEqMemRel.decEq._proof_1

@[implicit_reducible]

instance instDecidableEqMemRel {a✝ : ℕ} : DecidableEq (memRel a✝)

Equations

• instDecidableEqMemRel = instDecidableEqMemRel.decEq

def 𝓛ZF : FirstOrder.Language

The first-order language of ZF set theory, with a single binary membership relation.

Equations

• 𝓛ZF = { Functions := fun (x : ℕ) => Empty, Relations := memRel }

instance instIsRelational𝓛ZF : 𝓛ZF.IsRelational

theorem FirstOrder.Language.BoundedFormula.realize_isFormula {α : Type u_3} {L : Language} {M : Type u_4} [L.Structure M] (v : α → M) (φ : L.BoundedFormula α 0) (w : Fin 0 → M) : φ.Realize v w ↔ Formula.Realize φ v

def FirstOrder.Language.BoundedFormula.exUnique {α : Type u_1} {n : ℕ} {L : Language} (φ : L.BoundedFormula α (n + 1)) : L.BoundedFormula α n

The exUnique declaration.

Equations

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

def FirstOrder.Language.BoundedFormula.ite {α : Type u_1} {n : ℕ} {L : Language} (φ ψ χ : L.BoundedFormula α n) : L.BoundedFormula α n

The ite declaration.

Equations

• φ.ite ψ χ = φ ⊓ ψ ⊔ φ.not ⊓ χ

theorem FirstOrder.Language.BoundedFormula.realize_ite {α : Type u_3} {n : ℕ} {L : Language} {M : Type u_4} [L.Structure M] (v : α → M) (w : Fin n → M) (φ ψ χ : L.BoundedFormula α n) : (φ.ite ψ χ).Realize v w ↔ φ.Realize v w ∧ ψ.Realize v w ∨ ¬φ.Realize v w ∧ χ.Realize v w

theorem FirstOrder.Language.BoundedFormula.realize_exUnique {α : Type u_3} {n : ℕ} {L : Language} {M : Type u_4} [L.Structure M] (v : α → M) (w : Fin n → M) (φ : L.BoundedFormula α (n + 1)) : φ.exUnique.Realize v w ↔ ∃! a : M, φ.Realize v (Fin.snoc w a)

class FormulaToFunction {L : FirstOrder.Language} {M : Type u_3} [L.Structure M] {k : ℕ} (φ : L.Formula (Fin (k + 1))) (f : outParam ((Fin k → M) → M)) : Prop

The FormulaToFunction type.

• realize_iff_fn {v : Fin (k + 1) → M} : φ.Realize v ↔ f (v ∘ Fin.castSucc) = v (Fin.last k)

def FirstOrder.Language.BoundedFormula.ofFunc {α : Type u_1} {n : ℕ} {L : Language} {k : ℕ} (φ : L.Formula (Fin (k + 1))) (vars : Fin k → α ⊕ Fin n) (ψ : L.BoundedFormula α (n + 1)) : L.BoundedFormula α n

The ofFunc declaration.

Equations

• FirstOrder.Language.BoundedFormula.ofFunc φ vars ψ = (FirstOrder.Language.BoundedFormula.relabel (Fin.snoc (Sum.map id Fin.castSucc ∘ vars) (Sum.inr (Fin.last n))) φ ⊓ ψ).ex

theorem FirstOrder.Language.BoundedFormula.realize_ofFunc {α : Type u_4} {n : ℕ} {L : Language} {M : Type u_3} [L.Structure M] (v : α → M) (w : Fin n → M) {k : ℕ} (φ : L.Formula (Fin (k + 1))) (vars : Fin k → α ⊕ Fin n) (ψ : L.BoundedFormula α (n + 1)) {f : (Fin k → M) → M} [FormulaToFunction φ f] : (ofFunc φ vars ψ).Realize v w ↔ ψ.Realize v (Fin.snoc w (f (Sum.elim v w ∘ vars)))

def FirstOrder.«term#_» : Lean.ParserDescr

The #_ notation.

Equations

• FirstOrder.«term#_» = Lean.ParserDescr.node `FirstOrder.«term#_» 1023 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "#") (Lean.ParserDescr.cat `term 1023))

def FirstOrder.«term_∈ᶻ'_» : Lean.TrailingParserDescr

The _∈ᶻ'_ notation: membership in the ZF first-order language 𝓛ZF.

Equations

• FirstOrder.«term_∈ᶻ'_» = Lean.ParserDescr.trailingNode `FirstOrder.«term_∈ᶻ'_» 88 89 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∈ᶻ' ") (Lean.ParserDescr.cat `term 89))

def Lean.Parser.Category.label : Category

The label declaration.

Equations

• Lean.Parser.Category.label = { }

def FirstOrder.Language.BoundedFormula.label.quot : Lean.ParserDescr

Equations

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

def FirstOrder.Language.BoundedFormula.«label#_» : Lean.ParserDescr

The label#_ declaration.

Equations

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

def FirstOrder.Language.BoundedFormula.«label&_» : Lean.ParserDescr

The label&_ declaration.

Equations

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

def FirstOrder.Language.BoundedFormula.«termValue_of_labels(_)» : Lean.ParserDescr

The Value_of_labels(_) declaration.

Equations

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

def FirstOrder.Language.BoundedFormula.«term_@(_)» : Lean.TrailingParserDescr

The _@(_) notation.

Equations

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

@[reducible, inline]

abbrev ZFFormula (n : ℕ) : Type

The ZFFormula declaration.

Equations

• ZFFormula n = 𝓛ZF.Formula (Fin n)

@[reducible, inline]

abbrev ZFStructure (M : Type u_1) : Type u_1

The ZFStructure declaration.

Equations

• ZFStructure M = 𝓛ZF.Structure M

@[implicit_reducible, instance 10000]

instance instMembershipZFStructure {M : Type u_1} [sM : ZFStructure M] : Membership M M

Equations

• instMembershipZFStructure = { mem := fun (x y : M) => FirstOrder.Language.Structure.RelMap memRel.mem ![y, x] }

@[implicit_reducible]

instance instHasSubsetM {M : Type u_1} [sM : ZFStructure M] : HasSubset M

Equations

• instHasSubsetM = { Subset := fun (x y : M) => ∀ ⦃z : M⦄, z ∈ x → z ∈ y }

class ElementaryEmbeddingClass (F : Type u_3) (M : outParam (Type u_4)) (N : outParam (Type u_5)) [ZFStructure M] [ZFStructure N] [FunLike F M N] : Prop

The ElementaryEmbeddingClass type.

• map_formula (f : F) ⦃n : ℕ⦄ (φ : 𝓛ZF.Formula (Fin n)) (x : Fin n → M) : φ.Realize (⇑f ∘ x) ↔ φ.Realize x

instance instElementaryEmbeddingClassElementaryEmbedding𝓛ZF {M : Type u_1} {N : Type u_2} [sM : ZFStructure M] [sN : ZFStructure N] : ElementaryEmbeddingClass (𝓛ZF.ElementaryEmbedding M N) M N

theorem Fin.two_def {α : Type u_3} (x : Fin 2 → α) : x = ![x 0, x 1]

theorem relMap_mem_iff_membership {M : Type u_1} [sM : ZFStructure M] {v : Fin 2 → M} : FirstOrder.Language.Structure.RelMap memRel.mem v ↔ v 0 ∈ v 1

class HasEmpty (M : Type u_3) [ZFStructure M] : Prop

The HasEmpty type.

• exists_empty : ∃! x : M, ∀ (y : M), y ∉ x

def EqEmptyN (n : ℕ) : ZFFormula (n + 1)

The EqEmptyN declaration.

Equations

• EqEmptyN n = (FirstOrder.Language.Relations.boundedFormula₂ memRel.mem ((FirstOrder.Language.var ∘ Sum.inr) 0) ((FirstOrder.Language.var ∘ Sum.inl) (Fin.last n))).not.all

@[implicit_reducible, instance 100]

noncomputable instance instEmptyCollectionM {M : Type u_1} [sM : ZFStructure M] [HasEmpty M] : EmptyCollection M

Equations

• instEmptyCollectionM = { emptyCollection := Exists.choose ⋯ }

theorem EqEmptyN.realize_iff {M : Type u_1} [sM : ZFStructure M] {n : ℕ} [HasEmpty M] {v : Fin (n + 1) → M} : FirstOrder.Language.Formula.Realize (EqEmptyN n) v ↔ ∅ = v (Fin.last n)

inductive EncodeExpr.WeakLevel : Type

The WeakLevel type.

• a : WeakLevel
• b : WeakLevel → WeakLevel
• c : WeakLevel → WeakLevel → WeakLevel
• d : WeakLevel → WeakLevel → WeakLevel
• e : String → WeakLevel

@[implicit_reducible]

instance EncodeExpr.instFromJsonWeakLevel : Lean.FromJson WeakLevel

Equations

• EncodeExpr.instFromJsonWeakLevel = { fromJson? := EncodeExpr.instFromJsonWeakLevel.fromJson }

partial def EncodeExpr.instFromJsonWeakLevel.fromJson : Lean.Json → Except String WeakLevel

@[implicit_reducible]

instance EncodeExpr.instToJsonWeakLevel : Lean.ToJson WeakLevel

Equations

• EncodeExpr.instToJsonWeakLevel = { toJson := EncodeExpr.instToJsonWeakLevel.toJson }

def EncodeExpr.instToJsonWeakLevel.toJson : WeakLevel → Lean.Json

Equations

• EncodeExpr.instToJsonWeakLevel.toJson EncodeExpr.WeakLevel.a = Lean.toJson "a"
• EncodeExpr.instToJsonWeakLevel.toJson a.b = Lean.Json.mkObj [("b", EncodeExpr.instToJsonWeakLevel.toJson a)]
• EncodeExpr.instToJsonWeakLevel.toJson (a.c a_1) = Lean.Json.mkObj [("c", Lean.Json.arr #[EncodeExpr.instToJsonWeakLevel.toJson a, EncodeExpr.instToJsonWeakLevel.toJson a_1])]
• EncodeExpr.instToJsonWeakLevel.toJson (a.d a_1) = Lean.Json.mkObj [("d", Lean.Json.arr #[EncodeExpr.instToJsonWeakLevel.toJson a, EncodeExpr.instToJsonWeakLevel.toJson a_1])]
• EncodeExpr.instToJsonWeakLevel.toJson (EncodeExpr.WeakLevel.e a) = Lean.Json.mkObj [("e", Lean.toJson a)]

@[implicit_reducible]

instance EncodeExpr.instInhabitedWeakLevel : Inhabited WeakLevel

Equations

• EncodeExpr.instInhabitedWeakLevel = { default := EncodeExpr.instInhabitedWeakLevel.default }

def EncodeExpr.instReprWeakLevel.repr : WeakLevel → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• EncodeExpr.instReprWeakLevel.repr EncodeExpr.WeakLevel.a prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "EncodeExpr.WeakLevel.a")).group prec✝

@[implicit_reducible]

instance EncodeExpr.instReprWeakLevel : Repr WeakLevel

Equations

• EncodeExpr.instReprWeakLevel = { reprPrec := EncodeExpr.instReprWeakLevel.repr }

inductive EncodeExpr.WeakBinderInfo : Type

The WeakBinderInfo type.

• a : WeakBinderInfo
• b : WeakBinderInfo
• c : WeakBinderInfo
• d : WeakBinderInfo

@[implicit_reducible]

instance EncodeExpr.instFromJsonWeakBinderInfo : Lean.FromJson WeakBinderInfo

Equations

• EncodeExpr.instFromJsonWeakBinderInfo = { fromJson? := EncodeExpr.instFromJsonWeakBinderInfo.fromJson }

def EncodeExpr.instFromJsonWeakBinderInfo.fromJson : Lean.Json → Except String WeakBinderInfo

Equations

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

@[implicit_reducible]

instance EncodeExpr.instToJsonWeakBinderInfo : Lean.ToJson WeakBinderInfo

Equations

• EncodeExpr.instToJsonWeakBinderInfo = { toJson := EncodeExpr.instToJsonWeakBinderInfo.toJson }

def EncodeExpr.instToJsonWeakBinderInfo.toJson : WeakBinderInfo → Lean.Json

Equations

• EncodeExpr.instToJsonWeakBinderInfo.toJson EncodeExpr.WeakBinderInfo.a = Lean.toJson "a"
• EncodeExpr.instToJsonWeakBinderInfo.toJson EncodeExpr.WeakBinderInfo.b = Lean.toJson "b"
• EncodeExpr.instToJsonWeakBinderInfo.toJson EncodeExpr.WeakBinderInfo.c = Lean.toJson "c"
• EncodeExpr.instToJsonWeakBinderInfo.toJson EncodeExpr.WeakBinderInfo.d = Lean.toJson "d"

@[implicit_reducible]

instance EncodeExpr.instInhabitedWeakBinderInfo : Inhabited WeakBinderInfo

Equations

• EncodeExpr.instInhabitedWeakBinderInfo = { default := EncodeExpr.instInhabitedWeakBinderInfo.default }

@[implicit_reducible]

instance EncodeExpr.instReprWeakBinderInfo : Repr WeakBinderInfo

Equations

• EncodeExpr.instReprWeakBinderInfo = { reprPrec := EncodeExpr.instReprWeakBinderInfo.repr }

def EncodeExpr.instReprWeakBinderInfo.repr : WeakBinderInfo → ℕ → Std.Format

Equations

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

inductive EncodeExpr.WeakExprItem : Type

The WeakExprItem type.

• a : ℕ → WeakExprItem
• b : WeakLevel → WeakExprItem
• c : ℕ → List WeakLevel → WeakExprItem
• d : ℕ → ℕ → WeakExprItem
• e : ℕ → ℕ → ℕ → ℕ → WeakExprItem
• f : ℕ → ℕ → ℕ → ℕ → WeakExprItem
• g : ℕ → ℕ → ℕ → ℕ → Bool → WeakExprItem
• h : ℕ → WeakExprItem
• i : String → WeakExprItem
• j : ℕ → ℕ → ℕ → WeakExprItem

def EncodeExpr.instFromJsonWeakExprItem.fromJson : Lean.Json → Except String WeakExprItem

Equations

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

@[implicit_reducible]

instance EncodeExpr.instFromJsonWeakExprItem : Lean.FromJson WeakExprItem

Equations

• EncodeExpr.instFromJsonWeakExprItem = { fromJson? := EncodeExpr.instFromJsonWeakExprItem.fromJson }

@[implicit_reducible]

instance EncodeExpr.instToJsonWeakExprItem : Lean.ToJson WeakExprItem

Equations

• EncodeExpr.instToJsonWeakExprItem = { toJson := EncodeExpr.instToJsonWeakExprItem.toJson }

def EncodeExpr.instToJsonWeakExprItem.toJson : WeakExprItem → Lean.Json

Equations

• One or more equations did not get rendered due to their size.
• EncodeExpr.instToJsonWeakExprItem.toJson (EncodeExpr.WeakExprItem.a a) = Lean.Json.mkObj [("a", Lean.toJson a)]
• EncodeExpr.instToJsonWeakExprItem.toJson (EncodeExpr.WeakExprItem.b a) = Lean.Json.mkObj [("b", Lean.toJson a)]
• EncodeExpr.instToJsonWeakExprItem.toJson (EncodeExpr.WeakExprItem.c a a_1) = Lean.Json.mkObj [("c", Lean.Json.arr #[Lean.toJson a, Lean.toJson a_1])]
• EncodeExpr.instToJsonWeakExprItem.toJson (EncodeExpr.WeakExprItem.d a a_1) = Lean.Json.mkObj [("d", Lean.Json.arr #[Lean.toJson a, Lean.toJson a_1])]
• EncodeExpr.instToJsonWeakExprItem.toJson (EncodeExpr.WeakExprItem.e a a_1 a_2 a_3) = Lean.Json.mkObj [("e", Lean.Json.arr #[Lean.toJson a, Lean.toJson a_1, Lean.toJson a_2, Lean.toJson a_3])]
• EncodeExpr.instToJsonWeakExprItem.toJson (EncodeExpr.WeakExprItem.f a a_1 a_2 a_3) = Lean.Json.mkObj [("f", Lean.Json.arr #[Lean.toJson a, Lean.toJson a_1, Lean.toJson a_2, Lean.toJson a_3])]
• EncodeExpr.instToJsonWeakExprItem.toJson (EncodeExpr.WeakExprItem.h a) = Lean.Json.mkObj [("h", Lean.toJson a)]
• EncodeExpr.instToJsonWeakExprItem.toJson (EncodeExpr.WeakExprItem.i a) = Lean.Json.mkObj [("i", Lean.toJson a)]
• EncodeExpr.instToJsonWeakExprItem.toJson (EncodeExpr.WeakExprItem.j a a_1 a_2) = Lean.Json.mkObj [("j", Lean.Json.arr #[Lean.toJson a, Lean.toJson a_1, Lean.toJson a_2])]

@[implicit_reducible]

instance EncodeExpr.instInhabitedWeakExprItem : Inhabited WeakExprItem

Equations

• EncodeExpr.instInhabitedWeakExprItem = { default := EncodeExpr.instInhabitedWeakExprItem.default }

def EncodeExpr.instReprWeakExprItem.repr : WeakExprItem → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance EncodeExpr.instReprWeakExprItem : Repr WeakExprItem

Equations

• EncodeExpr.instReprWeakExprItem = { reprPrec := EncodeExpr.instReprWeakExprItem.repr }

def Lean.Level.toWeakLevel : Level → EncodeExpr.WeakLevel

The toWeakLevel declaration.

Equations

• Lean.Level.zero.toWeakLevel = EncodeExpr.WeakLevel.a
• u.succ.toWeakLevel = u.toWeakLevel.b
• (u.max v).toWeakLevel = u.toWeakLevel.c v.toWeakLevel
• (u.imax v).toWeakLevel = u.toWeakLevel.d v.toWeakLevel
• (Lean.Level.param name).toWeakLevel = EncodeExpr.WeakLevel.e name.toString
• (Lean.Level.mvar a).toWeakLevel = default

def EncodeExpr.WeakLevel.toLevel : WeakLevel → Lean.Level

The toLevel declaration.

Equations

• EncodeExpr.WeakLevel.a.toLevel = Lean.Level.zero
• a.b.toLevel = a.toLevel.succ
• (a.c a_1).toLevel = a.toLevel.max a_1.toLevel
• (a.d a_1).toLevel = a.toLevel.imax a_1.toLevel
• (EncodeExpr.WeakLevel.e a).toLevel = Lean.Level.param a.toName

def Lean.BinderInfo.toNat : BinderInfo → ℕ

The toNat declaration.

Equations

• Lean.BinderInfo.default.toNat = 0
• Lean.BinderInfo.implicit.toNat = 1
• Lean.BinderInfo.strictImplicit.toNat = 2
• Lean.BinderInfo.instImplicit.toNat = 3

def Nat.toBinderInfo : ℕ → Lean.BinderInfo

The toBinderInfo declaration.

Equations

• Nat.toBinderInfo 0 = Lean.BinderInfo.default
• Nat.toBinderInfo 1 = Lean.BinderInfo.implicit
• Nat.toBinderInfo 2 = Lean.BinderInfo.strictImplicit
• Nat.toBinderInfo 3 = Lean.BinderInfo.instImplicit
• x✝.toBinderInfo = Lean.BinderInfo.default

theorem Lean.BinderInfo.toNat_toBinderInfo (bi : BinderInfo) : bi.toNat.toBinderInfo = bi

The numeric encoding of binder information round-trips back to the original.

theorem Lean.BinderInfo.toNat_injective {bi bj : BinderInfo} (h : bi.toNat = bj.toNat) : bi = bj

The numeric BinderInfo encoding is injective on the four valid binder kinds.

structure EncodeExpr.WeakExprState : Type

Mutable state threaded through expression serialization: deduplicating maps from subexpressions and names to their indices, together with the output arrays.

• hashExpr : Std.HashMap Lean.Expr ℕ

  Cache from already-serialized subexpressions to their indices.

• hashName : Std.HashMap Lean.Name ℕ

  Cache from already-serialized names to their indices.

• arrayExpr : Array WeakExprItem

  The serialized expression items, indexed in insertion order.

• arrayName : Array String

  The serialized name strings, indexed in insertion order.

@[reducible, inline]

abbrev EncodeExpr.WeakExpr : Type

A serialized closed expression: the array of expression items together with the array of referenced name strings.

Equations

• EncodeExpr.WeakExpr = (Array EncodeExpr.WeakExprItem × Array String)

@[reducible, inline]

abbrev EncodeExpr.SerializeM (α : Type) : Type

The serialization monad: a state monad over WeakExprState with failure.

Equations

• EncodeExpr.SerializeM = OptionT (StateM EncodeExpr.WeakExprState)

def EncodeExpr.add (e : Lean.Expr) (i : WeakExprItem) : SerializeM ℕ

Append a new serialized item for e, recording its index in the cache.

Equations

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

def EncodeExpr.addName (name : Lean.Name) : SerializeM ℕ

Serialize a name, returning the index of its (deduplicated) string.

Equations

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

def EncodeExpr.toWeakExprAux (e : Lean.Expr) : SerializeM ℕ

Recursively serialize an expression into the state, returning its index.

Equations

• One or more equations did not get rendered due to their size.
• EncodeExpr.toWeakExprAux (Lean.Expr.fvar fvarId) = do let __do_lift ← get match __do_lift.hashExpr.get? (Lean.Expr.fvar fvarId) with | some n => pure n | x => failure
• EncodeExpr.toWeakExprAux (Lean.Expr.mvar mvarId) = do let __do_lift ← get match __do_lift.hashExpr.get? (Lean.Expr.mvar mvarId) with | some n => pure n | x => failure

def Lean.Expr.toWeakExpr (e : Expr) : EncodeExpr.WeakExpr

Serialize a closed expression into its WeakExpr representation.

Equations

• e.toWeakExpr = ((OptionT.run (EncodeExpr.toWeakExprAux e) { }).2.arrayExpr, (OptionT.run (EncodeExpr.toWeakExprAux e) { }).2.arrayName)

def EncodeExpr.WeakExpr.toExpr (e : WeakExpr) : Lean.Expr

The toExpr declaration.

Equations

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

def EncodeExpr.«termHeadBeta(_)» : Lean.ParserDescr

The HeadBeta(_) declaration.

Equations

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

def EncodeExpr.«termExpr(_)» : Lean.ParserDescr

The Expr(_) declaration.

Equations

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

def Lean.Expr.toSyntax' {m : Type → Type} [Monad m] [MonadQuotation m] (e : Expr) : m Term

The toSyntax' declaration.

Equations

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

inductive VariableParam : Type

The VariableParam type.

• freeVariable (binderInfo : Lean.BinderInfo) : VariableParam
• hypothesis (t : Lean.Term) : VariableParam

@[implicit_reducible]

instance instInhabitedVariableParam : Inhabited VariableParam

Equations

• instInhabitedVariableParam = { default := instInhabitedVariableParam.default }

def VariableParam.isFreeVariable : VariableParam → Bool

The isFreeVariable declaration.

Equations

• (VariableParam.freeVariable binderInfo).isFreeVariable = true
• x✝.isFreeVariable = false

def VariableParam.isHypothesis : VariableParam → Bool

The isHypothesis declaration.

Equations

• (VariableParam.hypothesis t).isHypothesis = true
• x✝.isHypothesis = false

def VariableParam.toTerm : VariableParam → Lean.Term

The toTerm declaration.

Equations

• (VariableParam.hypothesis t).toTerm = t
• x✝.toTerm = default

theorem VariableParam.isFreeVariable_eq_not_isHypothesis (p : VariableParam) : p.isFreeVariable = !p.isHypothesis

A variable parameter is a free variable exactly when it is not a hypothesis.

@[reducible, inline]

abbrev VariableParams : Type

The VariableParams declaration.

Equations

• VariableParams = Array VariableParam

def VariableParams.numFreeVariables (ps : VariableParams) : ℕ

The numFreeVariables declaration.

Equations

• ps.numFreeVariables = Array.countP (fun (x : VariableParam) => x.isFreeVariable) ps

def VariableParams.numHypotheses (ps : VariableParams) : ℕ

The numHypotheses declaration.

Equations

• ps.numHypotheses = Array.countP (fun (x : VariableParam) => x.isHypothesis) ps

def VariableParams.freeVarsBefore (ps : VariableParams) (n : ℕ) : ℕ

The freeVarsBefore declaration.

Equations

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

structure BuildFormulaState : Type

The BuildFormulaState type.

• attrDeclName : Lean.Name

  The attrDeclName declaration.

• hasEmptyInstance? : Bool

  The hasEmptyInstance? declaration.

• classParams : Array Lean.Term

  The classParams declaration.

• variableParams : VariableParams

  The variableParams declaration.

• variableType : Lean.Expr

  The variableType declaration.

• localVars : Array Lean.Expr

  The localVars declaration.

• termIntermediates : Array (Lean.Name × Array ℕ)

  The Intermediates declaration.

@[reducible, inline]

abbrev BuildFormulaM (α : Type) : Type

The BuildFormulaM declaration.

Equations

• BuildFormulaM = StateT BuildFormulaState Lean.MetaM

def BuildFormula.removeNameSuffix (name : Lean.Name) : Lean.Name

The removeNameSuffix declaration.

Equations

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

theorem BuildFormula.removeNameSuffix_anonymous : removeNameSuffix Lean.Name.anonymous = Lean.Name.anonymous

Stripping the recognized suffixes from the anonymous name leaves it unchanged.

def BuildFormula.attrDeclName : BuildFormulaM Lean.Name

The attrDeclName declaration.

Equations

• BuildFormula.attrDeclName = do let __do_lift ← get pure __do_lift.attrDeclName

def BuildFormula.name : BuildFormulaM Lean.Name

The name declaration.

Equations

• BuildFormula.name = do let __do_lift ← get pure (BuildFormula.removeNameSuffix __do_lift.attrDeclName)

def BuildFormula.isFunction : BuildFormulaM Bool

The isFunction declaration.

Equations

• BuildFormula.isFunction = do let __do_lift ← Lean.getEnv let __do_lift_1 ← BuildFormula.name pure (__do_lift.contains (__do_lift_1 ++ `eu))

def BuildFormula.isRealizeIffStage : BuildFormulaM Bool

The isRealizeIffStage declaration.

Equations

• BuildFormula.isRealizeIffStage = do let __do_lift ← BuildFormula.attrDeclName pure (__do_lift.lastComponentAsString == "realize_iff")

def BuildFormula.hasEmptyInstanceState : BuildFormulaM Bool

The hasEmptyInstanceState declaration.

Equations

• BuildFormula.hasEmptyInstanceState = do let __do_lift ← get pure __do_lift.hasEmptyInstance?

def BuildFormula.classParams : BuildFormulaM (Array Lean.Term)

The classParams declaration.

Equations

• BuildFormula.classParams = do let __do_lift ← get pure __do_lift.classParams

def BuildFormula.variableParams : BuildFormulaM VariableParams

The variableParams declaration.

Equations

• BuildFormula.variableParams = do let __do_lift ← get pure __do_lift.variableParams

def BuildFormula.getHypothesis (i : ℕ) : BuildFormulaM Lean.Term

The getHypothesis declaration.

Equations

• BuildFormula.getHypothesis i = do let __do_lift ← BuildFormula.variableParams pure (Array.filter (fun (x : VariableParam) => x.isHypothesis) __do_lift)[i]!.toTerm

def BuildFormula.freeVarsBefore (i : ℕ) : BuildFormulaM ℕ

The freeVarsBefore declaration.

Equations

• BuildFormula.freeVarsBefore i = do let __do_lift ← BuildFormula.variableParams pure (__do_lift.freeVarsBefore i)

def BuildFormula.numFreeVars (adjust? : Bool := false) : BuildFormulaM ℕ

The numFreeVars declaration.

Equations

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

def BuildFormula.numHypotheses : BuildFormulaM ℕ

The numHypotheses declaration.

Equations

• BuildFormula.numHypotheses = do let __do_lift ← get pure __do_lift.variableParams.numHypotheses

def BuildFormula.numAllVars : BuildFormulaM ℕ

The numAllVars declaration.

Equations

• BuildFormula.numAllVars = do let __do_lift ← BuildFormula.classParams let __do_lift_1 ← BuildFormula.variableParams pure (2 + __do_lift.size + Array.size __do_lift_1)

def BuildFormula.variableType : BuildFormulaM Lean.Expr

The variableType declaration.

Equations

• BuildFormula.variableType = do let __do_lift ← get pure __do_lift.variableType

def BuildFormula.localVars : BuildFormulaM (Array Lean.Expr)

The localVars declaration.

Equations

• BuildFormula.localVars = do let __do_lift ← get pure __do_lift.localVars

def BuildFormula.termIntermediates : BuildFormulaM (Array (Lean.Name × Array ℕ))

The Intermediates declaration.

Equations

• BuildFormula.termIntermediates = do let __do_lift ← get pure __do_lift.termIntermediates

def BuildFormula.addIntermediate (name : Lean.Name) (args : Array ℕ) : BuildFormulaM ℕ

The addIntermediate declaration.

Equations

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

def BuildFormula.clearIntermediates : BuildFormulaM Unit

The clearIntermediates declaration.

Equations

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

def BuildFormula.findVar (e : Lean.Expr) : BuildFormulaM ℕ

The findVar declaration.

Equations

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

def BuildFormula.getIndexSeq (extraBinders : ℕ) (idx : Array ℕ) : BuildFormulaM Lean.Expr

The getIndexSeq declaration.

Equations

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

def BuildFormula.withNewVars {α : Type} (vars : Array Lean.Expr) (f : BuildFormulaM α) : BuildFormulaM α

The withNewVars declaration.

Equations

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

theorem BuildFormula.numFreeVariables_empty : VariableParams.numFreeVariables #[] = 0

The empty parameter list contributes no free variables.

def BuildFormula.throwTranslateError {α : Type} (e : Lean.Expr) : BuildFormulaM α

The throwTranslateError declaration.

Equations

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

def BuildFormula.decomposeApp (e : Lean.Expr) : BuildFormulaM (Lean.Name × Array Lean.Expr)

The decomposeApp declaration.

Equations

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

def BuildFormula.goTerm (fuel : ℕ) (e : Lean.Expr) : BuildFormulaM ℕ

Translate a term-level subexpression into an intermediate index, using fuel to bound the recursion (any fuel at least the expression depth suffices).

Equations

• One or more equations did not get rendered due to their size.
• BuildFormula.goTerm 0 e = BuildFormula.throwTranslateError e
• BuildFormula.goTerm fuel_2.succ (Lean.Expr.fvar fvarId) = BuildFormula.findVar (Lean.Expr.fvar fvarId)
• BuildFormula.goTerm fuel_2.succ e = BuildFormula.throwTranslateError e

def BuildFormula.go (fuel : ℕ) (e : Lean.Expr) : BuildFormulaM Lean.Expr

Translate a proposition into a BoundedFormula, using fuel to bound the recursion (any fuel at least the expression depth suffices).

Equations

• One or more equations did not get rendered due to their size.
• BuildFormula.go 0 e = BuildFormula.throwTranslateError e
• BuildFormula.go fuel_2.succ e = BuildFormula.throwTranslateError e

def BuildFormula.checkSorry (name : Lean.Name) : BuildFormulaM Unit

The checkSorry declaration.

Equations

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

def BuildFormula.addDeclSimple (name : Lean.Name) (type value : Lean.Expr) : BuildFormulaM Unit

The addDeclSimple declaration.

Equations

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

def BuildFormula.explicitize : Lean.Expr → ℕ → Lean.Expr

The explicitize declaration.

Equations

• BuildFormula.explicitize (Lean.Expr.lam name type body binderInfo) n.succ = Lean.Expr.lam name type (BuildFormula.explicitize body n) Lean.BinderInfo.default
• BuildFormula.explicitize x✝¹ x✝ = x✝¹

def BuildFormula.mkLambdaFVarsExplicit (xs : Array Lean.Expr) (e : Lean.Expr) : BuildFormulaM Lean.Expr

The mkLambdaFVarsExplicit declaration.

Equations

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

def BuildFormula.init : BuildFormulaM Unit

The init declaration.

Equations

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

def BuildFormula.simpFormulaPre (e : Lean.Expr) : BuildFormulaM Lean.Expr

The simpFormulaPre declaration.

Equations

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

def BuildFormula.simpFormula (e : Lean.Expr) : BuildFormulaM Lean.Expr

The simpFormula declaration.

Equations

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

def BuildFormula.definitionProp : BuildFormulaM Lean.Expr

The definitionProp declaration.

Equations

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

def BuildFormula.buildFormula (formulaName : Lean.Name) : BuildFormulaM Unit

The buildFormula declaration.

Equations

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

def BuildFormula.prefixIdents (typeLetter : String := "M") : Array Lean.Ident

The prefixIdents declaration.

Equations

• BuildFormula.prefixIdents typeLetter = #[Lean.mkIdent typeLetter.toName, Lean.mkIdent ("s" ++ typeLetter).toName]

theorem BuildFormula.prefixIdents_size (typeLetter : String) : (prefixIdents typeLetter).size = 2

The prefix identifiers are exactly the carrier type and its structure instance.

def BuildFormula.classIdents (typeLetter : String := "M") : BuildFormulaM (Array Lean.Ident)

The classIdents declaration.

Equations

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

def BuildFormula.varIdents (adjust? : Bool := false) (varLetter : String := "x") : BuildFormulaM (Array Lean.Ident)

The varIdents declaration.

Equations

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

def BuildFormula.hypothesisIdents (hypothesisLetter : String := "h") : BuildFormulaM (Array Lean.Ident)

The hypothesisIdents declaration.

Equations

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

def BuildFormula.identsBefore (i : ℕ) (typeLetter : String := "M") (varLetter : String := "x") : BuildFormulaM (Array Lean.Ident)

The identsBefore declaration.

Equations

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

def BuildFormula.allIdentsWithHypotheses (typeLetter : String := "M") (varLetter : String := "x") (hypothesisLetter : String := "h") : BuildFormulaM (Array Lean.Ident)

The allIdentsWithHypotheses declaration.

Equations

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

def BuildFormula.classParamBinders (typeLetter : String := "M") : BuildFormulaM (Lean.TSyntaxArray `Lean.Parser.Term.bracketedBinder)

The classParamBinders declaration.

Equations

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

def BuildFormula.mkBinders (adjust? : Bool := false) (typeLetter : String := "M") (varLetter : String := "x") : BuildFormulaM (Lean.TSyntaxArray `Lean.Parser.Term.bracketedBinder)

The mkBinders declaration.

Equations

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

def BuildFormula.mkTermApp (x : Lean.Term) (xs : Array Lean.Term) : BuildFormulaM Lean.Term

The mkTermApp declaration.

Equations

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

def BuildFormula.mkParam (i : ℕ) (typeLetter : String := "M") (varLetter : String := "x") : BuildFormulaM Lean.Term

The mkParam declaration.

Equations

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

def BuildFormula.mkBindersWithHypotheses (typeLetter : String := "M") (varLetter : String := "x") (hypothesisLetter : String := "h") : BuildFormulaM (Lean.TSyntaxArray `Lean.Parser.Term.bracketedBinder)

The mkBindersWithHypotheses declaration.

Equations

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

def BuildFormula.mkIdent' (name : Lean.Name) : Lean.Ident

The mkIdent' declaration.

Equations

• BuildFormula.mkIdent' name = Lean.mkIdent (`_root_ ++ name)

def BuildFormula.buildFunction (funcName : Lean.Name) : BuildFormulaM Unit

The buildFunction declaration.

Equations

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

def BuildFormula.realizedTerm (typeLetter : String := "M") : BuildFormulaM Lean.Term

The realizedTerm declaration.

Equations

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

def BuildFormula.buildRealizeIff (thmName : Lean.Name) : BuildFormulaM Unit

The buildRealizeIff declaration.

Equations

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

def BuildFormula.buildInstFormulaToFunction (instName : Lean.Name) : BuildFormulaM Unit

The buildInstFormulaToFunction declaration.

Equations

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

def BuildFormula.mkVarVec (typeLetter : String := "M") (varLetter : String := "x") : BuildFormulaM Lean.Term

The mkVarVec declaration.

Equations

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

def BuildFormula.buildToRealize (toRealizeName : Lean.Name) : BuildFormulaM Unit

The buildToRealize declaration.

Equations

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

def BuildFormula.buildElementarity (elementarityName : Lean.Name) : BuildFormulaM Unit

The buildElementarity declaration.

Equations

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

def BuildFormula.runIfNotFound (names : List Lean.Name) (f : Lean.Name → BuildFormulaM Unit) : BuildFormulaM Unit

The runIfNotFound declaration.

Equations

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

def BuildFormula.realizeAttrAdd (attrDeclName : Lean.Name) : Lean.AttrM Unit

Build all the Formula.Realize companion declarations for the decl attrDeclName tagged with @[realize].

Equations

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