Propositional formulas

inductive Trestle.Model.PropForm (ν : Type u) : Type u

A propositional formula over variables of type ν.

This is the inductively defined syntax of formulas. Later on we can take a quotient to identify x ∨ ¬x with ⊤, for example.

• var {ν : Type u} (x : ν) : PropForm ν
• tr {ν : Type u} : PropForm ν
• fls {ν : Type u} : PropForm ν
• neg {ν : Type u} (φ : PropForm ν) : PropForm ν
• conj {ν : Type u} (φ₁ φ₂ : PropForm ν) : PropForm ν
• disj {ν : Type u} (φ₁ φ₂ : PropForm ν) : PropForm ν
• impl {ν : Type u} (φ₁ φ₂ : PropForm ν) : PropForm ν
• biImpl {ν : Type u} (φ₁ φ₂ : PropForm ν) : PropForm ν

instance Trestle.Model.instReprPropForm {ν✝ : Type u_1} [Repr ν✝] : Repr (PropForm ν✝)

Equations

• Trestle.Model.instReprPropForm = { reprPrec := Trestle.Model.reprPropForm✝ }

instance Trestle.Model.instDecidableEqPropForm {ν✝ : Type u_1} [DecidableEq ν✝] : DecidableEq (PropForm ν✝)

Equations

• Trestle.Model.instDecidableEqPropForm = Trestle.Model.decEqPropForm✝

instance Trestle.Model.instInhabitedPropForm {a✝ : Type u_1} : Inhabited (PropForm a✝)

Equations

• Trestle.Model.instInhabitedPropForm = { default := Trestle.Model.PropForm.tr }

@[irreducible]

def Trestle.Model.PropForm.toString {ν : Type u_1} [ToString ν] : PropForm ν → String

Equations

• (Trestle.Model.PropForm.var a).toString = toString a
• Trestle.Model.PropForm.tr.toString = "⊤"
• Trestle.Model.PropForm.fls.toString = "⊥"
• a.neg.toString = toString "¬" ++ toString (Trestle.Model.PropForm.toString.go a) ++ toString ""
• (a.conj a_1).toString = toString "" ++ toString (Trestle.Model.PropForm.toString.go a) ++ toString " ∧ " ++ toString (Trestle.Model.PropForm.toString.go a_1) ++ toString ""
• (a.disj a_1).toString = toString "" ++ toString (Trestle.Model.PropForm.toString.go a) ++ toString " ∨ " ++ toString (Trestle.Model.PropForm.toString.go a_1) ++ toString ""
• (a.impl a_1).toString = toString "" ++ toString (Trestle.Model.PropForm.toString.go a) ++ toString " → " ++ toString (Trestle.Model.PropForm.toString.go a_1) ++ toString ""
• (a.biImpl a_1).toString = toString "" ++ toString (Trestle.Model.PropForm.toString.go a) ++ toString " ↔ " ++ toString (Trestle.Model.PropForm.toString.go a_1) ++ toString ""

@[irreducible]

def Trestle.Model.PropForm.toString.go {ν : Type u_1} [ToString ν] (n : PropForm ν) : String

Equations

• Trestle.Model.PropForm.toString.go n = if n.toString.contains ' ' = true then toString "(" ++ toString n.toString ++ toString ")" else n.toString

instance Trestle.Model.PropForm.instToString {ν : Type u_1} [ToString ν] : ToString (PropForm ν)

Equations

• Trestle.Model.PropForm.instToString = { toString := Trestle.Model.PropForm.toString }

instance Trestle.Model.PropForm.instCoe {L : Type u_1} : Coe L (PropForm L)

Equations

• Trestle.Model.PropForm.instCoe = { coe := Trestle.Model.PropForm.var }

def Trestle.Model.PropForm.all {L : Type u_1} (fs : List (PropForm L)) : PropForm L

Equations

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

@[reducible, inline, deprecated Trestle.Model.PropForm.all (since := "20 Jan 2025")]

abbrev Trestle.Model.PropForm.conj' {L : Type u_1} (fs : List (PropForm L)) : PropForm L

Equations

• Trestle.Model.PropForm.conj' fs = Trestle.Model.PropForm.all fs

def Trestle.Model.PropForm.any {L : Type u_1} (fs : List (PropForm L)) : PropForm L

Equations

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

@[reducible, inline, deprecated Trestle.Model.PropForm.any (since := "20 Jan 2025")]

abbrev Trestle.Model.PropForm.disj' {L : Type u_1} (fs : List (PropForm L)) : PropForm L

Equations

• Trestle.Model.PropForm.disj' fs = Trestle.Model.PropForm.any fs

def Trestle.Model.PropForm.eval {ν : Type u_1} (τ : PropAssignment ν) : PropForm ν → Bool

The unique extension of τ from variables to formulas.

Equations

• Trestle.Model.PropForm.eval τ (Trestle.Model.PropForm.var a) = τ a
• Trestle.Model.PropForm.eval τ Trestle.Model.PropForm.tr = true
• Trestle.Model.PropForm.eval τ Trestle.Model.PropForm.fls = false
• Trestle.Model.PropForm.eval τ a.neg = !Trestle.Model.PropForm.eval τ a
• Trestle.Model.PropForm.eval τ (a.conj a_1) = (Trestle.Model.PropForm.eval τ a && Trestle.Model.PropForm.eval τ a_1)
• Trestle.Model.PropForm.eval τ (a.disj a_1) = (Trestle.Model.PropForm.eval τ a || Trestle.Model.PropForm.eval τ a_1)
• Trestle.Model.PropForm.eval τ (a.impl a_1) = Trestle.Model.PropForm.eval τ a ⇨ Trestle.Model.PropForm.eval τ a_1
• Trestle.Model.PropForm.eval τ (a.biImpl a_1) = decide (Trestle.Model.PropForm.eval τ a = Trestle.Model.PropForm.eval τ a_1)

Satisfying assignments

def Trestle.Model.PropForm.satisfies {ν : Type u_1} (τ : PropAssignment ν) (φ : PropForm ν) : Prop

An assignment satisfies a formula φ when φ evaluates to ⊤ at that assignment.

Equations

• Trestle.Model.PropForm.satisfies τ φ = (Trestle.Model.PropForm.eval τ φ = true)

def Trestle.Model.PropForm.instSemanticEntailsPropAssignment {ν : Type u_1} : SemanticEntails (PropAssignment ν) (PropForm ν)

This instance is scoped so that τ ⊨ φ : Prop implies φ : PropForm _ via the outParam only when PropForm is open.

Equations

• Trestle.Model.PropForm.instSemanticEntailsPropAssignment = { entails := Trestle.Model.PropForm.satisfies }

instance Trestle.Model.PropForm.instDecidableEntailsPropAssignment {ν : Type u_1} (τ : PropAssignment ν) (φ : PropForm ν) : Decidable (τ ⊨ φ)

Equations

• Trestle.Model.PropForm.instDecidableEntailsPropAssignment τ φ = match h : Trestle.Model.PropForm.eval τ φ with | true => isTrue h | false => isFalse ⋯

instance Trestle.Model.PropForm.instDecidableEntailsPropAssignment_1 {ν : Type u_1} {τ : PropAssignment ν} {φ : PropForm ν} : Decidable (τ ⊨ φ)

Equations

• Trestle.Model.PropForm.instDecidableEntailsPropAssignment_1 = inferInstanceAs (Decidable (Trestle.Model.PropForm.eval τ φ = true))

@[simp]

theorem Trestle.Model.PropForm.satisfies_var {ν : Type u_1} {τ : PropAssignment ν} {x : ν} : τ ⊨ var x ↔ τ x = true

@[simp]

theorem Trestle.Model.PropForm.satisfies_tr {ν : Type u_1} {τ : PropAssignment ν} : τ ⊨ tr

@[simp]

theorem Trestle.Model.PropForm.not_satisfies_fls {ν : Type u_1} {τ : PropAssignment ν} : (fun (M : PropAssignment ν) (φ : PropForm ν) => ¬M ⊨ φ) τ fls

@[simp]

theorem Trestle.Model.PropForm.satisfies_neg {ν : Type u_1} {τ : PropAssignment ν} {φ : PropForm ν} : τ ⊨ φ.neg ↔ (fun (M : PropAssignment ν) (φ : PropForm ν) => ¬M ⊨ φ) τ φ

@[simp]

theorem Trestle.Model.PropForm.satisfies_conj {ν : Type u_1} {τ : PropAssignment ν} {φ₁ φ₂ : PropForm ν} : τ ⊨ φ₁.conj φ₂ ↔ τ ⊨ φ₁ ∧ τ ⊨ φ₂

@[simp]

theorem Trestle.Model.PropForm.satisfies_disj {ν : Type u_1} {τ : PropAssignment ν} {φ₁ φ₂ : PropForm ν} : τ ⊨ φ₁.disj φ₂ ↔ τ ⊨ φ₁ ∨ τ ⊨ φ₂

@[simp]

theorem Trestle.Model.PropForm.satisfies_impl {ν : Type u_1} {τ : PropAssignment ν} {φ₁ φ₂ : PropForm ν} : τ ⊨ φ₁.impl φ₂ ↔ τ ⊨ φ₁ → τ ⊨ φ₂

theorem Trestle.Model.PropForm.satisfies_impl' {ν : Type u_1} {τ : PropAssignment ν} {φ₁ φ₂ : PropForm ν} : τ ⊨ φ₁.impl φ₂ ↔ (fun (M : PropAssignment ν) (φ : PropForm ν) => ¬M ⊨ φ) τ φ₁ ∨ τ ⊨ φ₂

@[simp]

theorem Trestle.Model.PropForm.satisfies_biImpl {ν : Type u_1} {τ : PropAssignment ν} {φ₁ φ₂ : PropForm ν} : τ ⊨ φ₁.biImpl φ₂ ↔ (τ ⊨ φ₁ ↔ τ ⊨ φ₂)

theorem Trestle.Model.PropForm.satisfies_biImpl' {ν : Type u_1} {τ : PropAssignment ν} {φ₁ φ₂ : PropForm ν} : τ ⊨ φ₁.biImpl φ₂ ↔ τ ⊨ φ₁ ∧ τ ⊨ φ₂ ∨ (fun (M : PropAssignment ν) (φ : PropForm ν) => ¬M ⊨ φ) τ φ₁ ∧ (fun (M : PropAssignment ν) (φ : PropForm ν) => ¬M ⊨ φ) τ φ₂

Semantic entailment and equivalence

def Trestle.Model.PropForm.entails {ν : Type u_1} (φ₁ φ₂ : PropForm ν) : Prop

A formula φ₁ semantically entails φ₂ when τ ⊨ φ₁ implies τ ⊨ φ₂.

This is actually defined in terms of the Boolean lattice to reuse various le_blah theorems, and the above statement is a theorem (entails_ext).

Equations

• φ₁.entails φ₂ = ∀ (τ : Trestle.Model.PropAssignment ν), Trestle.Model.PropForm.eval τ φ₁ ≤ Trestle.Model.PropForm.eval τ φ₂

theorem Trestle.Model.PropForm.entails_ext {ν : Type u_1} {φ₁ φ₂ : PropForm ν} : φ₁.entails φ₂ ↔ ∀ (τ : PropAssignment ν), τ ⊨ φ₁ → τ ⊨ φ₂

An equivalent formulation of semantic entailment in terms of satisfying assignments.

theorem Trestle.Model.PropForm.entails_refl {ν : Type u_1} (φ : PropForm ν) : φ.entails φ

theorem Trestle.Model.PropForm.entails.trans {ν : Type u_1} {φ₁ φ₂ φ₃ : PropForm ν} : φ₁.entails φ₂ → φ₂.entails φ₃ → φ₁.entails φ₃

theorem Trestle.Model.PropForm.entails_tr {ν : Type u_1} (φ : PropForm ν) : φ.entails tr

theorem Trestle.Model.PropForm.fls_entails {ν : Type u_1} (φ : PropForm ν) : fls.entails φ

theorem Trestle.Model.PropForm.entails_disj_left {ν : Type u_1} (φ₁ φ₂ : PropForm ν) : φ₁.entails (φ₁.disj φ₂)

theorem Trestle.Model.PropForm.entails_disj_right {ν : Type u_1} (φ₁ φ₂ : PropForm ν) : φ₂.entails (φ₁.disj φ₂)

theorem Trestle.Model.PropForm.disj_entails {ν : Type u_1} {φ₁ φ₂ φ₃ : PropForm ν} : φ₁.entails φ₃ → φ₂.entails φ₃ → (φ₁.disj φ₂).entails φ₃

theorem Trestle.Model.PropForm.conj_entails_left {ν : Type u_1} (φ₁ φ₂ : PropForm ν) : (φ₁.conj φ₂).entails φ₁

theorem Trestle.Model.PropForm.conj_entails_right {ν : Type u_1} (φ₁ φ₂ : PropForm ν) : (φ₁.conj φ₂).entails φ₂

theorem Trestle.Model.PropForm.entails_conj {ν : Type u_1} {φ₁ φ₂ φ₃ : PropForm ν} : φ₁.entails φ₂ → φ₁.entails φ₃ → φ₁.entails (φ₂.conj φ₃)

theorem Trestle.Model.PropForm.entails_disj_conj {ν : Type u_1} (φ₁ φ₂ φ₃ : PropForm ν) : ((φ₁.disj φ₂).conj (φ₁.disj φ₃)).entails (φ₁.disj (φ₂.conj φ₃))

theorem Trestle.Model.PropForm.conj_neg_entails_fls {ν : Type u_1} (φ : PropForm ν) : (φ.conj φ.neg).entails fls

theorem Trestle.Model.PropForm.tr_entails_disj_neg {ν : Type u_1} (φ : PropForm ν) : tr.entails (φ.disj φ.neg)

def Trestle.Model.PropForm.equivalent {ν : Type u_1} (φ₁ φ₂ : PropForm ν) : Prop

Two formulas are semantically equivalent when they always evaluate to the same thing.

This is a strong notion of equivalence. See equivalentOver for a weaker one.

Equations

• φ₁.equivalent φ₂ = ∀ (τ : Trestle.Model.PropAssignment ν), Trestle.Model.PropForm.eval τ φ₁ = Trestle.Model.PropForm.eval τ φ₂

instance Trestle.Model.PropForm.instHasEquiv {ν : Type u_1} : HasEquiv (PropForm ν)

Equations

• Trestle.Model.PropForm.instHasEquiv = { Equiv := Trestle.Model.PropForm.equivalent }

theorem Trestle.Model.PropForm.equivalent_iff_entails {ν : Type u_1} {φ₁ φ₂ : PropForm ν} : φ₁.equivalent φ₂ ↔ φ₁.entails φ₂ ∧ φ₂.entails φ₁

theorem Trestle.Model.PropForm.equivalent_ext {ν : Type u_1} {φ₁ φ₂ : PropForm ν} : φ₁.equivalent φ₂ ↔ ∀ (τ : PropAssignment ν), τ ⊨ φ₁ ↔ τ ⊨ φ₂

theorem Trestle.Model.PropForm.equivalent_refl {ν : Type u_1} (φ : PropForm ν) : φ.equivalent φ

theorem Trestle.Model.PropForm.equivalent.symm {ν : Type u_1} {φ₁ φ₂ : PropForm ν} : φ₁.equivalent φ₂ → φ₂.equivalent φ₁

theorem Trestle.Model.PropForm.equivalent.trans {ν : Type u_1} {φ₁ φ₂ φ₃ : PropForm ν} : φ₁.equivalent φ₂ → φ₂.equivalent φ₃ → φ₁.equivalent φ₃

theorem Trestle.Model.PropForm.equivalent.antisymm {ν : Type u_1} {φ₁ φ₂ : PropForm ν} : φ₁.entails φ₂ → φ₂.entails φ₁ → φ₁.equivalent φ₂

Define notation for PropForms

def Trestle.Model.PropForm.Notation.propform.quot : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.propform : Category

Equations

• Lean.Parser.Category.propform = { }

def Trestle.Model.PropForm.Notation.«term[propform|_]» : Lean.ParserDescr

Equations

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

def Trestle.Model.PropForm.Notation.«propform{_}» : Lean.ParserDescr

Equations

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

def Trestle.Model.PropForm.Notation.«propform(_)» : Lean.ParserDescr

Equations

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

def Trestle.Model.PropForm.Notation.«propform¬_» : Lean.ParserDescr

Equations

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

def Trestle.Model.PropForm.Notation.«propform_∧_» : Lean.TrailingParserDescr

Equations

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

def Trestle.Model.PropForm.Notation.«propform_∨_» : Lean.TrailingParserDescr

Equations

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

def Trestle.Model.PropForm.Notation.«propform_→_» : Lean.TrailingParserDescr

Equations

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

def Trestle.Model.PropForm.Notation.«propform_↔_» : Lean.TrailingParserDescr

Equations

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