Linglib.Theories.Semantics.Entailment.Basic

source

inductive Semantics.Entailment.World :

Type

A small finite set of worlds for decidable reasoning.

w0 : World
w1 : World
w2 : World
w3 : World

Instances For

source

instance Semantics.Entailment.instDecidableEqWorld :

DecidableEq World

Equations

Semantics.Entailment.instDecidableEqWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

source

instance Semantics.Entailment.instBEqWorld :

BEq World

Equations

Semantics.Entailment.instBEqWorld = { beq := Semantics.Entailment.instBEqWorld.beq }

source

def Semantics.Entailment.instBEqWorld.beq :

World → World → Bool

Equations

Semantics.Entailment.instBEqWorld.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

source

def Semantics.Entailment.instReprWorld.repr :

World → ℕ → Std.Format

Equations

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

Instances For

source

instance Semantics.Entailment.instReprWorld :

Repr World

Equations

Semantics.Entailment.instReprWorld = { reprPrec := Semantics.Entailment.instReprWorld.repr }

source

def Semantics.Entailment.allWorlds :

List World

Equations

Semantics.Entailment.allWorlds = [Semantics.Entailment.World.w0 , Semantics.Entailment.World.w1 , Semantics.Entailment.World.w2 , Semantics.Entailment.World.w3 ]

Instances For

source

def Semantics.Entailment.entails (p q : BProp World) :

Bool

Semantic entailment: p entails q iff q is true whenever p is true.

Equations

Semantics.Entailment.entails p q = Core.Proposition.Decidable.entails Semantics.Entailment.World Semantics.Entailment.allWorlds p q

Instances For

source

def Semantics.Entailment.pnot (p : BProp World) :

BProp World

Negation: (pnot p) w = !(p w).

Equations

Semantics.Entailment.pnot p = Core.Proposition.Decidable.pnot Semantics.Entailment.World p

Instances For

source

def Semantics.Entailment.pand (p q : BProp World) :

BProp World

Conjunction: (pand p q) w = p w && q w.

Equations

Semantics.Entailment.pand p q = Core.Proposition.Decidable.pand Semantics.Entailment.World p q

Instances For

source

def Semantics.Entailment.por (p q : BProp World) :

BProp World

Disjunction: (por p q) w = p w || q w.

Equations

Semantics.Entailment.por p q = Core.Proposition.Decidable.por Semantics.Entailment.World p q

Instances For

source

theorem Semantics.Entailment.pnot_reverses_entailment (p q : BProp World) (h : ∀ (w : World), p w = true → q w = true) (w : World) :

pnot q w = true → pnot p w = true

Negation reverses entailment, specialized to World.

source

def Semantics.Entailment.p0 :

BProp World

Proposition true only in w0.

Equations

Semantics.Entailment.p0 w = (w == Semantics.Entailment.World.w0)

Instances For

source

def Semantics.Entailment.p01 :

BProp World

Proposition true in w0 and w1.

Equations

Semantics.Entailment.p01 w = (w == Semantics.Entailment.World.w0 || w == Semantics.Entailment.World.w1)

Instances For

source

def Semantics.Entailment.p012 :

BProp World

Proposition true in w0, w1, w2.

Equations

Semantics.Entailment.p012 w = (w == Semantics.Entailment.World.w0 || w == Semantics.Entailment.World.w1 || w == Semantics.Entailment.World.w2)

Instances For

source

def Semantics.Entailment.pAll :

BProp World

Proposition true everywhere.

Equations

Semantics.Entailment.pAll x✝ = true

Instances For

source

def Semantics.Entailment.pNone :

BProp World

Proposition false everywhere.

Equations

Semantics.Entailment.pNone x✝ = false

Instances For

source

def Semantics.Entailment.testCases :

List (BProp World × BProp World)

Test cases for monotonicity: pairs where first entails second.

Equations

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

Instances For

source

theorem Semantics.Entailment.p0_entails_p01 :

entails p0 p01 = true

p0 entails p01.

source

theorem Semantics.Entailment.p01_entails_p012 :

entails p01 p012 = true

p01 entails p012.