Supporting results for pointwise provable equality.

inductive PointwiseComposition.FFL.Meta.Litform (α : Type u_1) : Type u_1

Data and laws for Litform in FFL.Meta.

• atom {α : Type u_1} (a : α) : Litform α
• verum {α : Type u_1} : Litform α
• falsum {α : Type u_1} : Litform α
• and {α : Type u_1} : Litform α → Litform α → Litform α
• or {α : Type u_1} : Litform α → Litform α → Litform α
• neg {α : Type u_1} : Litform α → Litform α
• imply {α : Type u_1} : Litform α → Litform α → Litform α
• iff {α : Type u_1} : Litform α → Litform α → Litform α

@[instance_reducible]

instance PointwiseComposition.FFL.Meta.Litform.instLogicalConnective {α : Type u_1} : LogicalConnective (Litform α)

Equations

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

@[instance_reducible]

instance PointwiseComposition.FFL.Meta.Litform.instLogicalNeutral {α : Type u_1} : LogicalNeutral (Litform α)

Equations

• PointwiseComposition.FFL.Meta.Litform.instLogicalNeutral = { top := PointwiseComposition.FFL.Meta.Litform.verum, bot := PointwiseComposition.FFL.Meta.Litform.falsum }

def PointwiseComposition.FFL.Meta.Litform.toStr {α : Type u_1} [ToString α] : Litform α → String

The to Str construction in FFL.Meta.Litform.

Equations

• PointwiseComposition.FFL.Meta.Litform.verum.toStr = "⊤"
• PointwiseComposition.FFL.Meta.Litform.falsum.toStr = "⊥"
• (PointwiseComposition.FFL.Meta.Litform.atom a).toStr = toString "atom " ++ toString (toString a)
• φ.neg.toStr = "(¬" ++ φ.toStr ++ ")"
• (φ.and ψ).toStr = "(" ++ φ.toStr ++ " ∧ " ++ ψ.toStr ++ ")"
• (φ.or ψ).toStr = "(" ++ φ.toStr ++ " ∨ " ++ ψ.toStr ++ ")"
• (φ.imply ψ).toStr = "(" ++ φ.toStr ++ " → " ++ ψ.toStr ++ ")"
• (φ.iff ψ).toStr = "(" ++ φ.toStr ++ " ↔ " ++ ψ.toStr ++ ")"

@[instance_reducible]

instance PointwiseComposition.FFL.Meta.Litform.instToString {α : Type u_1} [ToString α] : ToString (Litform α)

Equations

• PointwiseComposition.FFL.Meta.Litform.instToString = { toString := PointwiseComposition.FFL.Meta.Litform.toStr }

def PointwiseComposition.FFL.Meta.Litform.format {α : Type u_1} [Repr α] : Litform α → Std.Format

The format construction in FFL.Meta.Litform.

Equations

• PointwiseComposition.FFL.Meta.Litform.verum.format = Std.Format.text (toString "⊤")
• PointwiseComposition.FFL.Meta.Litform.falsum.format = Std.Format.text (toString "⊥")
• (PointwiseComposition.FFL.Meta.Litform.atom a).format = repr a
• φ.neg.format = Std.Format.text (toString "(¬" ++ toString φ.format ++ toString ")")
• (φ.and ψ).format = Std.Format.text (toString "(" ++ toString φ.format ++ toString " ∧ " ++ toString ψ.format ++ toString ")")
• (φ.or ψ).format = Std.Format.text (toString "(" ++ toString φ.format ++ toString " ∨ " ++ toString ψ.format ++ toString ")")
• (φ.imply ψ).format = Std.Format.text (toString "(" ++ toString φ.format ++ toString " → " ++ toString ψ.format ++ toString ")")
• (φ.iff ψ).format = Std.Format.text (toString "(" ++ toString φ.format ++ toString " ↔ " ++ toString ψ.format ++ toString ")")

@[instance_reducible]

instance PointwiseComposition.FFL.Meta.Litform.instRepr {α : Type u_1} [Repr α] : Repr (Litform α)

Equations

• PointwiseComposition.FFL.Meta.Litform.instRepr = { reprPrec := fun (t : PointwiseComposition.FFL.Meta.Litform α) (x : ℕ) => t.format }

@[reducible, inline]

abbrev PointwiseComposition.FFL.Meta.Lit : Type

The Lit construction in FFL.Meta.

Equations

• PointwiseComposition.FFL.Meta.Lit = PointwiseComposition.FFL.Meta.Litform Lean.Expr

@[reducible, inline]

abbrev PointwiseComposition.FFL.Meta.Litform.toExpr {u_1 : Lean.Level} {F : Q(Type u_1)} (ls : Q(LogicalConnective «$F»)) (ln : Q(LogicalNeutral «$F»)) : Lit → Q(«$F»)

The to Expr construction in FFL.Meta.Litform.

Equations

• One or more equations did not get rendered due to their size.
• PointwiseComposition.FFL.Meta.Litform.toExpr ls ln (PointwiseComposition.FFL.Meta.Litform.atom e) = e
• PointwiseComposition.FFL.Meta.Litform.toExpr ls ln PointwiseComposition.FFL.Meta.Litform.verum = q(⊤)
• PointwiseComposition.FFL.Meta.Litform.toExpr ls ln PointwiseComposition.FFL.Meta.Litform.falsum = q(⊥)
• PointwiseComposition.FFL.Meta.Litform.toExpr ls ln (PointwiseComposition.FFL.Meta.Litform.neg φ) = let toExpr_1 := PointwiseComposition.FFL.Meta.Litform.toExpr ls ln φ; q(∼«$toExpr_1»)

def PointwiseComposition.FFL.Meta.Litform.summandsAtDepth {u : Lean.Level} {α : have u := u; Q(Type u)} (inst : Q(Add «$α»)) : ℕ → Q(«$α») → Lean.MetaM (List Q(«$α»))

The summands At Depth construction in FFL.Meta.Litform.

Equations

• One or more equations did not get rendered due to their size.
• PointwiseComposition.FFL.Meta.Litform.summandsAtDepth inst 0 x✝ = pure [x✝]

def PointwiseComposition.FFL.Meta.Litform.summands {u : Lean.Level} {α : have u := u; Q(Type u)} (inst : Q(Add «$α»)) (expression : Q(«$α»)) : Lean.MetaM (List Q(«$α»))

The summands construction in FFL.Meta.Litform.

Equations

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

def PointwiseComposition.FFL.Meta.Litform.denoteAtDepth {u_1 : Lean.Level} {F : Q(Type u_1)} (ls : Q(LogicalConnective «$F»)) (ln : Q(LogicalNeutral «$F»)) : ℕ → Q(«$F») → Lean.MetaM Lit

The denote At Depth construction in FFL.Meta.Litform.

Equations

• One or more equations did not get rendered due to their size.
• PointwiseComposition.FFL.Meta.Litform.denoteAtDepth ls ln 0 x✝ = pure (PointwiseComposition.FFL.Meta.Litform.atom x✝)

def PointwiseComposition.FFL.Meta.Litform.denote {u_1 : Lean.Level} {F : Q(Type u_1)} (ls : Q(LogicalConnective «$F»)) (ln : Q(LogicalNeutral «$F»)) (expression : Q(«$F»)) : Lean.MetaM Lit

Reify the input's structural depth, keeping any remaining subexpression atomic.

Equations

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

def PointwiseComposition.FFL.Meta.Litform.complexity {α : Type u_1} : Litform α → ℕ

The complexity construction in FFL.Meta.Litform.

Equations

• (PointwiseComposition.FFL.Meta.Litform.atom a).complexity = 0
• PointwiseComposition.FFL.Meta.Litform.verum.complexity = 0
• PointwiseComposition.FFL.Meta.Litform.falsum.complexity = 0
• (φ.and ψ).complexity = max φ.complexity ψ.complexity + 1
• (φ.or ψ).complexity = max φ.complexity ψ.complexity + 1
• φ.neg.complexity = φ.complexity + 1
• (φ.imply ψ).complexity = max φ.complexity ψ.complexity + 1
• (φ.iff ψ).complexity = max φ.complexity ψ.complexity + 1

def PointwiseComposition.FFL.Meta.Lit.DEq : Lit → Lit → Lean.MetaM Bool

The DEq construction in FFL.Meta.Lit.

Equations

• One or more equations did not get rendered due to their size.
• PointwiseComposition.FFL.Meta.Lit.DEq (PointwiseComposition.FFL.Meta.Litform.atom e) (PointwiseComposition.FFL.Meta.Litform.atom e') = Lean.Meta.isDefEq e e'
• PointwiseComposition.FFL.Meta.Lit.DEq PointwiseComposition.FFL.Meta.Litform.verum PointwiseComposition.FFL.Meta.Litform.verum = pure true
• PointwiseComposition.FFL.Meta.Lit.DEq PointwiseComposition.FFL.Meta.Litform.falsum PointwiseComposition.FFL.Meta.Litform.falsum = pure true
• PointwiseComposition.FFL.Meta.Lit.DEq (PointwiseComposition.FFL.Meta.Litform.neg φ) (PointwiseComposition.FFL.Meta.Litform.neg ψ) = φ.DEq ψ
• x✝¹.DEq x✝ = pure false

def PointwiseComposition.FFL.Meta.Lit.dMem (φ : Lit) (Δ : List Lit) : Lean.MetaM Bool

The d Mem construction in FFL.Meta.Lit.

Equations

• φ.dMem Δ = List.foldrM (fun (ψ : PointwiseComposition.FFL.Meta.Lit) (ih : Bool) => do let __do_lift ← φ.DEq ψ pure (__do_lift || ih)) false Δ

def PointwiseComposition.FFL.Meta.Lit.dSubsetList (Γ Δ : List Lit) : Lean.MetaM Bool

The d Subset List construction in FFL.Meta.Lit.

Equations

• PointwiseComposition.FFL.Meta.Lit.dSubsetList [] Δ = pure true
• PointwiseComposition.FFL.Meta.Lit.dSubsetList (φ :: Γ_2) Δ = do let __do_lift ← φ.dMem Δ let __do_lift_1 ← PointwiseComposition.FFL.Meta.Lit.dSubsetList Γ_2 Δ pure (__do_lift && __do_lift_1)