PDL-Tableaux (Section 4)

Projections

def formProjection : ℕ → Formula → Option Formula

Equations

• formProjection x✝ (⌈·B⌉φ) = if (x✝ == B) = true then some φ else none
• formProjection x✝¹ x✝ = none

def projection : ℕ → List Formula → List Formula

Equations

• projection x✝¹ x✝ = (List.map (fun (x : Formula) => formProjection x✝¹ x) x✝).reduceOption

@[simp]

theorem proj {A : ℕ} {X : List Formula} {g : Formula} : g ∈ projection A X ↔ (⌈·A⌉g) ∈ X

Loading and Loaded Histories

@[reducible, inline]

abbrev History : Type

A history is a list of Sequents. This only tracks "big" steps, hoping we do not need steps within a local tableau. The head of the first list is the newest Sequent.

Equations

• History = List Sequent

def rep (Hist : History) (X : Sequent) : Prop

We have a repeat iff the history contains a node that is setEqTo the current node.

Equations

• rep Hist X = ∃ Y ∈ Hist, Y.setEqTo X

instance instDecidableRep {H : History} {X : Sequent} : Decidable (rep H X)

Equations

• instDecidableRep = id (List.rec (isFalse ⋯) (fun (head : Sequent) (tail : List Sequent) (tail_ih : Decidable (∃ Y ∈ tail, Y.setEqTo X)) => ⋯.mpr instDecidableOr) H)

def LoadedPathRepeat (Hist : History) (X : Sequent) : Type

A lpr means we can go k steps back in the history to reach an equal node, and all nodes on the way are loaded. Note: k=0 means the first element of Hist is the companion.

Equations

• LoadedPathRepeat Hist X = { k : Fin (List.length Hist) // (List.get Hist k).multisetEqTo X ∧ ∀ m ≤ k, (List.get Hist m).isLoaded = true }

theorem LoadedPathRepeat.to_rep {Hist : History} {X : Sequent} (lpr : LoadedPathRepeat Hist X) : rep Hist X

instance instDecidableEqLoadedPathRepeat {Hist : History} {X : Sequent} : DecidableEq (LoadedPathRepeat Hist X)

Equations

• instDecidableEqLoadedPathRepeat = Subtype.instDecidableEq

def LoadedPathRepeat.choice {H : History} {X : Sequent} (ne : Nonempty (LoadedPathRepeat H X)) : LoadedPathRepeat H X

If there is any loaded path repeat, then we can compute one. FIXME There is probably a more elegant way, avoiding Nonempty and Fin.find. Something like: def getLPR (H : History) (X : Sequent) : Option ... := ... that might also give us uniqueness of LPRs?

Equations

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

theorem LoadedPathRepeat_comp_isLoaded {Hist : History} {X : Sequent} (lpr : LoadedPathRepeat Hist X) : (List.get Hist ↑lpr).isLoaded = true

theorem LoadedPathRepeat_rep_isLoaded {Hist : History} {X : Sequent} (lpr : LoadedPathRepeat Hist X) : X.isLoaded = true

instance instDecidableNonemptyLoadedPathRepeat {H : History} {X : Sequent} : Decidable (Nonempty (LoadedPathRepeat H X))

Equations

• instDecidableNonemptyLoadedPathRepeat = if h : ∃ (k : Fin (List.length H)), (List.get H k).multisetEqTo X ∧ ∀ m ≤ k, (List.get H m).isLoaded = true then isTrue ⋯ else isFalse ⋯

The PDL rules

inductive PdlRule (X Y : Sequent) : Type

A rule to go from X to Y. Note the four variants of the modal rule.

• loadL {L : List Formula} {δ : List Program} {α : Program} {φ : Formula} {Y : List Formula × List Formula × Option (NegLoadFormula ⊕ NegLoadFormula)} {R : List Formula} : (~⌈⌈δ⌉⌉⌈α⌉φ) ∈ L → Y = (L.erase (~⌈⌈δ⌉⌉⌈α⌉φ), R, some (Sum.inl (~'⌊⌊δ⌋⌋⌊α⌋AnyFormula.normal φ))) → PdlRule (L, R, none) Y
• loadR {R : List Formula} {δ : List Program} {α : Program} {φ : Formula} {Y : List Formula × List Formula × Option (NegLoadFormula ⊕ NegLoadFormula)} {L : List Formula} : (~⌈⌈δ⌉⌉⌈α⌉φ) ∈ R → Y = (L, R.erase (~⌈⌈δ⌉⌉⌈α⌉φ), some (Sum.inr (~'⌊⌊δ⌋⌋⌊α⌋AnyFormula.normal φ))) → PdlRule (L, R, none) Y
• freeL {X : List Formula × List Formula × Option (NegLoadFormula ⊕ NegLoadFormula)} {L R : List Formula} {δ : List Program} {α : Program} {φ : Formula} {Y : List Formula × List Formula × Option (NegLoadFormula ⊕ NegLoadFormula)} : X = (L, R, some (Sum.inl (~'⌊⌊δ⌋⌋⌊α⌋AnyFormula.normal φ))) → Y = (List.insert (~⌈⌈δ⌉⌉⌈α⌉φ) L, R, none) → PdlRule X Y
• freeR {X : List Formula × List Formula × Option (NegLoadFormula ⊕ NegLoadFormula)} {L R : List Formula} {δ : List Program} {α : Program} {φ : Formula} {Y : List Formula × List Formula × Option (NegLoadFormula ⊕ NegLoadFormula)} : X = (L, R, some (Sum.inr (~'⌊⌊δ⌋⌋⌊α⌋AnyFormula.normal φ))) → Y = (L, List.insert (~⌈⌈δ⌉⌉⌈α⌉φ) R, none) → PdlRule X Y
• modL {Y : Sequent} {L R : List Formula} {A : ℕ} {X : Sequent} {ξ : AnyFormula} : X = (L, R, some (Sum.inl (~'⌊·A⌋ξ))) → (Y = match ξ with | AnyFormula.normal φ => (~φ :: projection A L, projection A R, none) | AnyFormula.loaded χ => (projection A L, projection A R, some (Sum.inl (~'χ)))) → PdlRule X Y
• modR {Y : Sequent} {L R : List Formula} {A : ℕ} {X : Sequent} {ξ : AnyFormula} : X = (L, R, some (Sum.inr (~'⌊·A⌋ξ))) → (Y = match ξ with | AnyFormula.normal φ => (projection A L, ~φ :: projection A R, none) | AnyFormula.loaded χ => (projection A L, projection A R, some (Sum.inr (~'χ)))) → PdlRule X Y

instance instDecidableEqPdlRule {X✝ Y✝ : Sequent} : DecidableEq (PdlRule X✝ Y✝)

Equations

• instDecidableEqPdlRule = instDecidableEqPdlRule.decEq

def instDecidableEqPdlRule.decEq {X✝ Y✝ : Sequent} (x✝ x✝¹ : PdlRule X✝ Y✝) : Decidable (x✝ = x✝¹)

inductive Tableau : History → Sequent → Type

The Tableau [parent, grandparent, ...] child type.

A closed tableau for X is either of:

• a local tableau for X followed by closed tableaux for all end nodes,
• a PDL rule application
• a successful loaded repeat (MB condition six)

• loc {Hist : History} {X : Sequent} (nrep : ¬rep Hist X) (nbas : ¬X.basic) (lt : LocalTableau X) (next : (Y : Sequent) → Y ∈ endNodesOf lt → Tableau (X :: Hist) Y) : Tableau Hist X
• pdl {Hist : History} {X Y : Sequent} (nrep : ¬rep Hist X) (bas : X.basic) (r : PdlRule X Y) (next : Tableau (X :: Hist) Y) : Tableau Hist X
• lrep {X : Sequent} {Hist : History} (lpr : LoadedPathRepeat Hist X) : Tableau Hist X

def Tableau.size {Hist : History} {X : Sequent} : Tableau Hist X → ℕ

Equations

• One or more equations did not get rendered due to their size.
• (Tableau.pdl nrep bas r next).size = 1 + next.size
• (Tableau.lrep lpr).size = 1

theorem Tableau.size_next_lt_of_loc {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} {nrep : ¬rep a✝ a✝¹} {nbas : ¬a✝¹.basic} {lt : LocalTableau a✝¹} {next : (Y : Sequent) → Y ∈ endNodesOf lt → Tableau (a✝¹ :: a✝) Y} (tab_def : tab = loc nrep nbas lt next) (Y : Sequent) (Y_in : Y ∈ endNodesOf lt) : (next Y Y_in).size < tab.size

theorem Tableau.size_next_lt_of_pdl {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} {nrep : ¬rep a✝ a✝¹} {bas : a✝¹.basic} {Y✝ : Sequent} {r : PdlRule a✝¹ Y✝} {next : Tableau (a✝¹ :: a✝) Y✝} (tab_def : tab = pdl nrep bas r next) : next.size < tab.size

instance instDecidableExistsEndNodeOf {X : Sequent} {lt : LocalTableau X} {f : (Y : Sequent) → Y ∈ endNodesOf lt → Prop} {dec : (Y : Sequent) → (Y_in : Y ∈ endNodesOf lt) → Decidable (f Y Y_in)} : Decidable (∃ (Y : Sequent) (Y_in : Y ∈ endNodesOf lt), f Y Y_in)

Equations

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

@[irreducible]

instance Tableau.instDecidableEq {Hist : History} {X : Sequent} {tab1 tab2 : Tableau Hist X} : Decidable (tab1 = tab2)

Equations

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

def Tableau.isLrep {Hist : History} {X : Sequent} : Tableau Hist X → Prop

Equations

• (Tableau.loc nrep nbas lt next).isLrep = False
• (Tableau.pdl nrep bas r next).isLrep = False
• (Tableau.lrep lpr).isLrep = True

inductive provable : Formula → Prop

• byTableauL {φ : Formula} : ∀ (a : Tableau [] ([~φ], [], none)), provable φ
• byTableauR {φ : Formula} : ∀ (a : Tableau [] ([], [~φ], none)), provable φ

def inconsistent : Sequent → Prop

A Sequent is inconsistent if there exists a closed tableau for it.

Equations

• inconsistent x✝ = Nonempty (Tableau [] x✝)

def consistent : Sequent → Prop

A Sequent is consistent iff it is not inconsistent.

Equations

• consistent x✝ = ¬inconsistent x✝