Tableau Examples

As a sanity check we construct tableaux/proofs for some examples.

theorem Sequent.not_basic_of_mem_L {L R : Finset Formula} {O : Olf} (φ : Formula) (h : φ ∈ L) (hφ : ¬φ.basic = true) : ¬basic (L, R, O)

Helper: a sequent that contains a non-basic formula on the left is not basic. (This might also fit into Pdl/Sequent.lean.)

def atP : ℕ

Equations

• atP = 1

def atQ : ℕ

Equations

• atQ = 2

def atR : ℕ

Equations

• atR = 3

def atA : ℕ

Equations

• atA = 4

@[reducible, inline]

abbrev p : Formula

Equations

• p = ·atP

@[reducible, inline]

abbrev q : Formula

Equations

• q = ·atQ

@[reducible, inline]

abbrev r : Formula

Equations

• r = ·atR

@[reducible, inline]

abbrev a : Program

Equations

• a = ·atA

def subTabForEx2 : Tableau [({r ⋀ ~⌈a⌉p, ~(r ⋀ ~⌈a⌉p ⋀ q)}, ∅, none)] ({r, ~⌈a⌉p, ⌈a⌉p ⋀ q}, ∅, none)

Preparation for Example 2 from MB.

Equations

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

def ltForEx2 : LocalTableau ({r ⋀ ~⌈a⌉p, ~(r ⋀ ~⌈a⌉p ⋀ q)}, ∅, none)

The local tableau used for Example 2 from MB.

Note that we never substitute the child sequents by their concrete values here. Doing so would leave Eq.recs in the term that block the computation of endNodesOf.

Equations

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

theorem endNodesOf_cast_helper {X Y : Sequent} {h : X = Y} (ltX : LocalTableau X) : endNodesOf (h ▸ ltX) = endNodesOf ltX

def ltEx419 : LocalTableau ({⌈∗a⌉q, ~⌈a⌉⌈∗a⋓(?'p)⌉q}, ∅, none)

The first local tableau used for Example 4.19: one application of the (□) rule.

Equations

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

def ltEx419b : LocalTableau ({⌈∗a⌉q}, ∅, some (Sum.inl (~'⌊∗a⋓(?'p)⌋AnyFormula.normal q)))

The second local tableau used for Example 4.19: the (□) rule and then the (◇) rule.

Equations

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