Propositional Formulas mod Equivalence

This file defines the type of propositional formulas over a set ν of variables, quotiented by strong equivalence.

We show that they form a Boolean algebra with ordering given by semantic entailment. This allows us to use Mathlib's lattice notation & lemmas.

instance Trestle.Model.PropFun.setoid (ν : Type u) : Setoid (PropForm ν)

Equations

• Trestle.Model.PropFun.setoid ν = { r := Trestle.Model.PropForm.equivalent, iseqv := ⋯ }

def Trestle.Model.PropFun (ν : Type u_1) : Type u_1

A propositional function is a propositional formula up to semantic equivalence.

Equations

• Trestle.Model.PropFun ν = Quotient (Trestle.Model.PropFun.setoid ν)

theorem Trestle.Model.PropFun.exact {ν : Type u_1} {φ₁ φ₂ : PropForm ν} : ⟦φ₁⟧ = ⟦φ₂⟧ → φ₁.equivalent φ₂

Applied backwards, this reduces an equivalence between two syntactic formulas to an equality between the functions they denote.

theorem Trestle.Model.PropFun.sound {ν : Type u_1} {φ₁ φ₂ : PropForm ν} : φ₁.equivalent φ₂ → ⟦φ₁⟧ = ⟦φ₂⟧

def Trestle.Model.PropFun.var {ν : Type u_1} (x : ν) : PropFun ν

Equations

• Trestle.Model.PropFun.var x = ⟦Trestle.Model.PropForm.var x⟧

instance Trestle.Model.PropFun.instCoe {ν : Type u_1} : Coe ν (PropFun ν)

Equations

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

def Trestle.Model.PropFun.tr {ν : Type u_1} : PropFun ν

Equations

• Trestle.Model.PropFun.tr = ⟦Trestle.Model.PropForm.tr⟧

def Trestle.Model.PropFun.fls {ν : Type u_1} : PropFun ν

Equations

• Trestle.Model.PropFun.fls = ⟦Trestle.Model.PropForm.fls⟧

def Trestle.Model.PropFun.neg {ν : Type u_1} : PropFun ν → PropFun ν

Equations

• Trestle.Model.PropFun.neg = Quotient.map (fun (x : Trestle.Model.PropForm ν) => x.neg) ⋯

def Trestle.Model.PropFun.conj {ν : Type u_1} : PropFun ν → PropFun ν → PropFun ν

Equations

• Trestle.Model.PropFun.conj = Quotient.map₂ (fun (x1 x2 : Trestle.Model.PropForm ν) => x1.conj x2) ⋯

def Trestle.Model.PropFun.disj {ν : Type u_1} : PropFun ν → PropFun ν → PropFun ν

Equations

• Trestle.Model.PropFun.disj = Quotient.map₂ (fun (x1 x2 : Trestle.Model.PropForm ν) => x1.disj x2) ⋯

def Trestle.Model.PropFun.impl {ν : Type u_1} : PropFun ν → PropFun ν → PropFun ν

Equations

• Trestle.Model.PropFun.impl = Quotient.map₂ (fun (x1 x2 : Trestle.Model.PropForm ν) => x1.impl x2) ⋯

def Trestle.Model.PropFun.biImpl {ν : Type u_1} : PropFun ν → PropFun ν → PropFun ν

Equations

• Trestle.Model.PropFun.biImpl = Quotient.map₂ (fun (x1 x2 : Trestle.Model.PropForm ν) => x1.biImpl x2) ⋯

Evaluation

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

The unique extension of τ from variables to propositional functions.

Equations

• Trestle.Model.PropFun.eval τ = Quotient.lift (Trestle.Model.PropForm.eval τ) ⋯

@[simp]

theorem Trestle.Model.PropFun.eval_mk {ν : Type u_1} (τ : PropAssignment ν) (φ : PropForm ν) : eval τ ⟦φ⟧ = PropForm.eval τ φ

@[simp]

theorem Trestle.Model.PropFun.eval_var {ν : Type u_1} (τ : PropAssignment ν) (x : ν) : eval τ (var x) = τ x

@[simp]

theorem Trestle.Model.PropFun.eval_tr {ν : Type u_1} (τ : PropAssignment ν) : eval τ tr = true

@[simp]

theorem Trestle.Model.PropFun.eval_fls {ν : Type u_1} (τ : PropAssignment ν) : eval τ fls = false

@[simp]

theorem Trestle.Model.PropFun.eval_neg {ν : Type u_1} (τ : PropAssignment ν) (φ : PropFun ν) : eval τ φ.neg = !eval τ φ

@[simp]

theorem Trestle.Model.PropFun.eval_conj {ν : Type u_1} (τ : PropAssignment ν) (φ₁ φ₂ : PropFun ν) : eval τ (φ₁.conj φ₂) = (eval τ φ₁ && eval τ φ₂)

@[simp]

theorem Trestle.Model.PropFun.eval_disj {ν : Type u_1} (τ : PropAssignment ν) (φ₁ φ₂ : PropFun ν) : eval τ (φ₁.disj φ₂) = (eval τ φ₁ || eval τ φ₂)

@[simp]

theorem Trestle.Model.PropFun.eval_impl {ν : Type u_1} (τ : PropAssignment ν) (φ₁ φ₂ : PropFun ν) : eval τ (φ₁.impl φ₂) = eval τ φ₁ ⇨ eval τ φ₂

@[simp]

theorem Trestle.Model.PropFun.eval_biImpl {ν : Type u_1} (τ : PropAssignment ν) (φ₁ φ₂ : PropFun ν) : (eval τ (φ₁.biImpl φ₂) = true) = (eval τ φ₁ = eval τ φ₂)

Satisfying assignments

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

Equations

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

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

This instance is scoped so that when PropFun is open, τ ⊨ φ implies φ : PropFun _ via the outParam.

Equations

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

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

Equations

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

theorem Trestle.Model.PropFun.ext {ν : Type u_1} {φ₁ φ₂ : PropFun ν} : (∀ (τ : PropAssignment ν), τ ⊨ φ₁ ↔ τ ⊨ φ₂) → φ₁ = φ₂

theorem Trestle.Model.PropFun.ext_iff {ν : Type u_1} {φ₁ φ₂ : PropFun ν} : φ₁ = φ₂ ↔ ∀ (τ : PropAssignment ν), τ ⊨ φ₁ ↔ τ ⊨ φ₂

Semantic entailment

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

Equations

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

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

Equations

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

@[simp]

theorem Trestle.Model.PropFun.entails_mk {ν : Type u_1} {φ₁ φ₂ : PropForm ν} : entails ⟦φ₁⟧ ⟦φ₂⟧ ↔ φ₁.entails φ₂

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

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

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

theorem Trestle.Model.PropFun.entails.antisymm {ν✝ : Type u_1} {φ ψ : PropFun ν✝} : φ.entails ψ → ψ.entails φ → φ = ψ

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

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

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

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

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

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

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

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

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

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

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

theorem Trestle.Model.PropFun.impl_eq {ν : Type u_1} (φ ψ : PropFun ν) : φ.impl ψ = ψ.disj φ.neg

theorem Trestle.Model.PropFun.biImpl_eq {ν : Type u_1} (φ ψ : PropFun ν) : φ.biImpl ψ = (φ.impl ψ).conj (ψ.impl φ)

From this point onwards we use lattice notation for PropFuns in order to get the mathlib laws for free.

instance Trestle.Model.PropFun.instBooleanAlgebra {ν : Type u_1} : BooleanAlgebra (PropFun ν)

Equations

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

@[simp]

theorem Trestle.Model.PropFun.eval_neg' {ν : Type u_1} (τ : PropAssignment ν) (φ : PropFun ν) : eval τ φᶜ = !eval τ φ

@[simp]

theorem Trestle.Model.PropFun.eval_conj' {ν : Type u_1} (τ : PropAssignment ν) (φ₁ φ₂ : PropFun ν) : eval τ (φ₁ ⊓ φ₂) = (eval τ φ₁ && eval τ φ₂)

@[simp]

theorem Trestle.Model.PropFun.eval_disj' {ν : Type u_1} (τ : PropAssignment ν) (φ₁ φ₂ : PropFun ν) : eval τ (φ₁ ⊔ φ₂) = (eval τ φ₁ || eval τ φ₂)

@[simp]

theorem Trestle.Model.PropFun.eval_impl' {ν : Type u_1} (τ : PropAssignment ν) (φ₁ φ₂ : PropFun ν) : eval τ (φ₁ ⇨ φ₂) = eval τ φ₁ ⇨ eval τ φ₂

@[simp]

theorem Trestle.Model.PropFun.eval_biImpl' {ν : Type u_1} (τ : PropAssignment ν) (φ₁ φ₂ : PropFun ν) : (eval τ ((fun (φ₁ φ₂ : PropFun ν) => (φ₁ ⇨ φ₂) ⊓ (φ₂ ⇨ φ₁)) φ₁ φ₂) = true) = (eval τ φ₁ = eval τ φ₂)

@[simp]

theorem Trestle.Model.PropFun.satisfies_mk {ν : Type u_1} {τ : PropAssignment ν} {φ : PropForm ν} : τ ⊨ ⟦φ⟧ ↔ τ ⊨ φ

@[simp]

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

@[simp]

theorem Trestle.Model.PropFun.satisfies_set {ν : Type u_1} {x : ν} {τ : PropAssignment ν} [DecidableEq ν] : τ.set x ⊤ ⊨ var x

@[simp]

theorem Trestle.Model.PropFun.satisfies_tr {ν : Type u_1} {τ : PropAssignment ν} : τ ⊨ ⊤

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

theorem Trestle.Model.PropFun.satisfies_biImpl {ν : Type u_1} {φ₁ φ₂ : PropFun ν} {τ : PropAssignment ν} : τ ⊨ (fun (φ₁ φ₂ : PropFun ν) => (φ₁ ⇨ φ₂) ⊓ (φ₂ ⇨ φ₁)) φ₁ φ₂ ↔ (τ ⊨ φ₁ ↔ τ ⊨ φ₂)

instance Trestle.Model.PropFun.instNontrivial {ν : Type u_1} : Nontrivial (PropFun ν)

theorem Trestle.Model.PropFun.eq_top_iff {ν : Type u_1} {φ : PropFun ν} : φ = ⊤ ↔ ∀ (τ : PropAssignment ν), τ ⊨ φ

theorem Trestle.Model.PropFun.eq_bot_iff {ν : Type u_1} {φ : PropFun ν} : φ = ⊥ ↔ ∀ (τ : PropAssignment ν), (fun (M : PropAssignment ν) (φ : PropFun ν) => ¬M ⊨ φ) τ φ

@[simp]

theorem Trestle.Model.PropFun.var_ne_bot {ν : Type u_1} (v : ν) : var v ≠ ⊥

@[simp]

theorem Trestle.Model.PropFun.var_ne_top {ν : Type u_1} (v : ν) : var v ≠ ⊤

@[simp]

theorem Trestle.Model.PropFun.bot_ne_var {ν : Type u_1} (v : ν) : ⊥ ≠ var v

@[simp]

theorem Trestle.Model.PropFun.top_ne_var {ν : Type u_1} (v : ν) : ⊤ ≠ var v

@[simp]

theorem Trestle.Model.PropFun.biImpl_top_left {ν : Type u_1} (φ : PropFun ν) : (fun (φ₁ φ₂ : PropFun ν) => (φ₁ ⇨ φ₂) ⊓ (φ₂ ⇨ φ₁)) ⊤ φ = φ

@[simp]

theorem Trestle.Model.PropFun.biImpl_top_right {ν : Type u_1} (φ : PropFun ν) : (fun (φ₁ φ₂ : PropFun ν) => (φ₁ ⇨ φ₂) ⊓ (φ₂ ⇨ φ₁)) φ ⊤ = φ

@[simp]

theorem Trestle.Model.PropFun.biImpl_bot_left {ν : Type u_1} (φ : PropFun ν) : (fun (φ₁ φ₂ : PropFun ν) => (φ₁ ⇨ φ₂) ⊓ (φ₂ ⇨ φ₁)) ⊥ φ = φᶜ

@[simp]

theorem Trestle.Model.PropFun.biImpl_bot_right {ν : Type u_1} (φ : PropFun ν) : (fun (φ₁ φ₂ : PropFun ν) => (φ₁ ⇨ φ₂) ⊓ (φ₂ ⇨ φ₁)) φ ⊥ = φᶜ

theorem Trestle.Model.PropFun.inf_le_iff_compl_sup {ν : Type u_1} {φ₁ φ₂ φ₃ : PropFun ν} : φ₁ ⊓ φ₂ ≤ φ₃ ↔ φ₁ ≤ φ₂ᶜ ⊔ φ₃

theorem Trestle.Model.PropFun.le_iff_inf_compl_le_bot {ν : Type u_1} {φ₁ φ₂ : PropFun ν} : φ₁ ≤ φ₂ ↔ φ₁ ⊓ φ₂ᶜ ≤ ⊥

theorem Trestle.Model.PropFun.le_iff_inf_compl_eq_bot {ν : Type u_1} {φ₁ φ₂ : PropFun ν} : φ₁ ≤ φ₂ ↔ φ₁ ⊓ φ₂ᶜ = ⊥

theorem Trestle.Model.PropFun.ne_top_left_of_disj_ne_top {ν : Type u_1} {φ₁ φ₂ : PropFun ν} : φ₁ ⊔ φ₂ ≠ ⊤ → φ₁ ≠ ⊤

theorem Trestle.Model.PropFun.ne_top_right_of_disj_ne_top {ν : Type u_1} {φ₁ φ₂ : PropFun ν} : φ₁ ⊔ φ₂ ≠ ⊤ → φ₂ ≠ ⊤

theorem Trestle.Model.PropFun.ne_top_of_disj_ne_top {ν : Type u_1} {φ₁ φ₂ : PropFun ν} : φ₁ ⊔ φ₂ ≠ ⊤ → φ₁ ≠ ⊤ ∧ φ₂ ≠ ⊤

theorem Trestle.Model.PropFun.var.inj {ν : Type u_1} [DecidableEq ν] : Function.Injective var

@[simp]

theorem Trestle.Model.PropFun.var_eq_var_iff {ν : Type u_1} [DecidableEq ν] (v v' : ν) : var v = var v' ↔ v = v'

theorem Trestle.Model.PropFun.eq_compl_iff_neq {ν : Type u_1} {φ₁ φ₂ : PropFun ν} : φ₁ = φ₂ᶜ → φ₁ ≠ φ₂

@[simp]

theorem Trestle.Model.PropFun.var_ne_var_compl {ν : Type u_1} [DecidableEq ν] (v1 v2 : ν) : var v1 ≠ (var v2)ᶜ

@[simp]

theorem Trestle.Model.PropFun.var_compl_ne_var {ν : Type u_1} [DecidableEq ν] (v1 v2 : ν) : (var v1)ᶜ ≠ var v2

theorem Trestle.Model.PropFun.compl_eq_iff_eq_compl {ν : Type u_1} {φ₁ φ₂ : PropFun ν} : φ₁ᶜ = φ₂ ↔ φ₁ = φ₂ᶜ

theorem Trestle.Model.PropFun.eq_compl_iff_compl_eq {ν : Type u_1} {φ₁ φ₂ : PropFun ν} : φ₁ = φ₂ᶜ ↔ φ₁ᶜ = φ₂

Lemmas to push Quotient.mk inwards.

@[simp]

theorem Trestle.Model.PropFun.mk_var {ν : Type u_1} (x : ν) : ⟦PropForm.var x⟧ = var x

@[simp]

theorem Trestle.Model.PropFun.mk_tr {ν : Type u_1} : ⟦PropForm.tr⟧ = ⊤

@[simp]

theorem Trestle.Model.PropFun.mk_fls {ν : Type u_1} : ⟦PropForm.fls⟧ = ⊥

@[simp]

theorem Trestle.Model.PropFun.mk_neg {ν : Type u_1} (φ : PropForm ν) : ⟦φ.neg⟧ = (⟦φ⟧)ᶜ

@[simp]

theorem Trestle.Model.PropFun.mk_conj {ν : Type u_1} (φ₁ φ₂ : PropForm ν) : ⟦φ₁.conj φ₂⟧ = ⟦φ₁⟧ ⊓ ⟦φ₂⟧

@[simp]

theorem Trestle.Model.PropFun.mk_disj {ν : Type u_1} (φ₁ φ₂ : PropForm ν) : ⟦φ₁.disj φ₂⟧ = ⟦φ₁⟧ ⊔ ⟦φ₂⟧

@[simp]

theorem Trestle.Model.PropFun.mk_impl {ν : Type u_1} (φ₁ φ₂ : PropForm ν) : ⟦φ₁.impl φ₂⟧ = ⟦φ₁⟧ ⇨ ⟦φ₂⟧

@[simp]

theorem Trestle.Model.PropFun.mk_biImpl {ν : Type u_1} (φ₁ φ₂ : PropForm ν) : ⟦φ₁.biImpl φ₂⟧ = (fun (φ₁ φ₂ : PropFun ν) => (φ₁ ⇨ φ₂) ⊓ (φ₂ ⇨ φ₁)) ⟦φ₁⟧ ⟦φ₂⟧

All/any

def Trestle.Model.PropFun.all {ν : Type u_1} (a : Multiset (PropFun ν)) : PropFun ν

Equations

• Trestle.Model.PropFun.all a = a.inf

def Trestle.Model.PropFun.any {ν : Type u_1} (a : Multiset (PropFun ν)) : PropFun ν

Equations

• Trestle.Model.PropFun.any a = a.sup

@[simp]

theorem Trestle.Model.PropFun.satisfies_all {ν : Type u_1} {a : Multiset (PropFun ν)} {τ : PropAssignment ν} : τ ⊨ all a ↔ ∀ i ∈ a, τ ⊨ i

@[simp]

theorem Trestle.Model.PropFun.satisfies_any {ν : Type u_1} {a : Multiset (PropFun ν)} {τ : PropAssignment ν} : τ ⊨ any a ↔ ∃ i ∈ a, τ ⊨ i

@[simp]

theorem Trestle.Model.PropFun.any_zero {ν : Type u_1} : any 0 = ⊥

@[simp]

theorem Trestle.Model.PropFun.any_empty {ν : Type u_1} : any ∅ = ⊥

@[simp]

theorem Trestle.Model.PropFun.all_zero {ν : Type u_1} : all 0 = ⊤

@[simp]

theorem Trestle.Model.PropFun.all_empty {ν : Type u_1} : all ∅ = ⊤

Satisfiable and Equisatisfiable

def Trestle.Model.PropFun.Sat {ν : Type u_1} (φ : PropFun ν) : Prop

Equations

• φ.Sat = ∃ (τ : Trestle.Model.PropAssignment ν), τ ⊨ φ

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

Equations

• φ₁.EquiSat φ₂ = (φ₁.Sat ↔ φ₂.Sat)

def Trestle.Model.PropFun.EquiSat.symm {ν : Type u_1} {φ₁ φ₂ : PropFun ν} : φ₁.EquiSat φ₂ ↔ φ₂.EquiSat φ₁

Equations

• ⋯ = ⋯

def Trestle.Model.PropFun.EquiSat.trans {ν : Type u_1} {φ₁ φ₂ φ₃ : PropFun ν} : φ₁.EquiSat φ₂ → φ₂.EquiSat φ₃ → φ₁.EquiSat φ₃

Equations

• ⋯ = ⋯

@[simp]

theorem Trestle.Model.PropFun.top_sat {ν : Type u_1} : ⊤.Sat

@[simp]

theorem Trestle.Model.PropFun.bot_not_sat {ν : Type u_1} : ¬⊥.Sat

@[simp]

theorem Trestle.Model.PropFun.not_sat_iff_eq_bot {ν : Type u_1} {F : PropFun ν} : ¬F.Sat ↔ F = ⊥

theorem Trestle.Model.PropFun.eq_bot_of_equisat {ν : Type u_1} {F C : PropFun ν} : F.EquiSat (F ⊓ C) → F ⊓ C = ⊥ → F = ⊥

theorem Trestle.Model.PropFun.equisat_of_entails {ν : Type u_1} {F C : PropFun ν} : F ≤ C → F.EquiSat (F ⊓ C)

def Lean.Parser.Category.propfun : Category

Equations

• Lean.Parser.Category.propfun = { }

def Trestle.Model.PropFun.Notation.propfun.quot : Lean.ParserDescr

Equations

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

def Trestle.Model.PropFun.Notation.«term[propfun|_]» : Lean.ParserDescr

Equations

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

def Trestle.Model.PropFun.Notation.«propfun{_}» : Lean.ParserDescr

Equations

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

def Trestle.Model.PropFun.Notation.«propfun(_)» : Lean.ParserDescr

Equations

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

def Trestle.Model.PropFun.Notation.«propfun¬_» : Lean.ParserDescr

Equations

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

def Trestle.Model.PropFun.Notation.«propfun_∧_» : Lean.TrailingParserDescr

Equations

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

def Trestle.Model.PropFun.Notation.«propfun_∨_» : Lean.TrailingParserDescr

Equations

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

def Trestle.Model.PropFun.Notation.«propfun_→_» : Lean.TrailingParserDescr

Equations

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

def Trestle.Model.PropFun.Notation.«propfun_↔_» : Lean.TrailingParserDescr

Equations

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