Propositional Predicates

This file defines the type of arbitrary predicates over PropAssignment ν. This allows us to use arbitrary Lean Prop constructs like ∀ and ∃.

@[reducible, inline]

abbrev Trestle.Model.PropPred (ν : Type u_1) : Type u_1

Equations

• Trestle.Model.PropPred ν = (Trestle.Model.PropAssignment ν → Prop)

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

Equations

• Trestle.Model.PropPred.instCoePropFun = { coe := fun (F : Trestle.Model.PropFun ν) (τ : Trestle.Model.PropAssignment ν) => τ ⊨ F }

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

Equations

• Trestle.Model.PropPred.instBooleanAlgebra = inferInstanceAs (BooleanAlgebra (Trestle.Model.PropAssignment ν → Prop))

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

Equations

• Trestle.Model.PropPred.instSemanticEntailsPropAssignment = { entails := fun (x1 : Trestle.Model.PropAssignment ν) (x2 : Trestle.Model.PropPred ν) => x2 x1 }

@[simp]

theorem Trestle.Model.PropPred.satisfies_def {ν : Type u_1} (τ : PropAssignment ν) (f : PropPred ν) : τ ⊨ f ↔ f τ