PDL-Tableaux (Section 4)

Projections

def PDL.formProjection : ℕ → Formula → Option Formula

Extract the continuation of an atomic box with the specified program index.

Equations

• PDL.formProjection x✝ (PDL.Formula.box (PDL.Program.atom_prog B) φ) = if (x✝ == B) = true then some φ else none
• PDL.formProjection x✝¹ x✝ = none

def PDL.projection : ℕ → List Formula → List Formula

Collect the continuations of matching atomic boxes in a formula list.

Equations

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

@[simp]

theorem PDL.proj {A : ℕ} {X : List Formula} {g : Formula} : g ∈ projection A X ↔ Formula.box (Program.atom_prog A) g ∈ X

def Finset.pdlProjection : ℕ → Finset PDL.Formula → Finset PDL.Formula

Collect the continuations of matching atomic boxes in a formula finset.

Equations

• Finset.pdlProjection x✝¹ x✝ = (Finset.image (fun (x : PDL.Formula) => (PDL.formProjection x✝¹ x).toFinset) x✝).sup id

theorem PDL.Finset.mem_projection {A : ℕ} {g : Formula} {X : Finset Formula} : g ∈ Finset.pdlProjection A X ↔ Formula.box (Program.atom_prog A) g ∈ X

Membership in the projection of a Finset of formulas. This is the Finset analogue of proj.

Histories and Repeats

@[reducible, inline]

abbrev PDL.History : Type

A history is a list of Sequents. In the Tableau type this only tracks "big" steps, not steps happening within a LocalTableau. The list is in reverse order, i.e. the head is the newest Sequent.

Equations

• PDL.History = List PDL.Sequent

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

We have a repeat iff the history contains a node that is setEqTo the current node. Note that this is a Prop, it does not carry a specific number of steps to go back.

Equations

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

@[instance_reducible]

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

Equations

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

@[simp]

theorem PDL.not_rep_empty {X : Sequent} : ¬rep [] X

def PDL.rep.toNat {H : History} {X : Sequent} (rp : rep H X) : ℕ

Given rep H X, get the index of the companion in H using List.findIdx?.

Equations

• rp.toNat = match h : List.findIdx? (fun (Y : PDL.Sequent) => decide (Y = X)) H with | none => ⋯.elim | some k => k

def PDL.rep.toFin {H : History} {X : Sequent} (rp : rep H X) : Fin (List.length H)

Given rep H X, get the index of the companion in H using List.findIdx?.

Equations

• rp.toFin = ⟨rp.toNat, ⋯⟩

theorem PDL.rep.toFin_agrees {H : History} {X : Sequent} (rp : rep H X) : H[rp.toFin] = X

Loaded Path Repeats

def PDL.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

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

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

theorem PDL.LoadedPathRepeat.ext {Hist : History} {X : Sequent} (lprA lprB : LoadedPathRepeat Hist X) : ↑lprA = ↑lprB → lprA = lprB

@[instance_reducible]

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

Equations

• PDL.instDecidableEqLoadedPathRepeat = Subtype.instDecidableEq

def PDL.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 PDL.LoadedPathRepeat_comp_isLoaded {Hist : History} {X : Sequent} (lpr : LoadedPathRepeat Hist X) : (List.get Hist ↑lpr).isLoaded

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

instance PDL.instDecidableIsEmptyLoadedPathRepeat {H : History} {X : Sequent} : Decidable (IsEmpty (LoadedPathRepeat H X))

Equations

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

Free, forbidden and allowed repeats

In Tableau we only want to allow the application of a rule when there is no loaded-path repeat and there is no free repeat. For this we introduce FreeRepeat and the flprep abbreviation.

def PDL.FreeRepeat (Hist : History) (X : Sequent) : Type

A free repeat is a non-loaded sequent that occured before. Values of this type are pairs: the number of steps to go back in the history and a proof that we then find the same set.

Equations

• PDL.FreeRepeat Hist X = { k : Fin (List.length Hist) // List.get Hist k = X ∧ ¬X.isLoaded }

theorem PDL.FreeRepeat_nil_impossible {X : Sequent} : ∀ (a : FreeRepeat [] X), False

theorem PDL.FreeRepeat_iff_rep_and_isFree {H : History} {X : Sequent} : Nonempty (FreeRepeat H X) ↔ rep H X ∧ X.isFree

def PDL.flprep (H : History) (X : Sequent) : Prop

Either a free repeat or a loaded-path repeat. Note that the negation of this is not the same as ¬ rep because it will still allow loaded repeats that are not loaded-path repeats, at which Tableau may continue. See also posOf that is used to define tableauGame later.

Equations

• PDL.flprep H X = (PDL.rep H X ∧ X.isFree ∨ Nonempty (PDL.LoadedPathRepeat H X))

@[simp]

theorem PDL.flprep.nil_not {X : Sequent} : ¬flprep [] X

The PDL rules

inductive PDL.PdlRule (X Y : Sequent) : Type

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

• loadL {L : Finset Formula} {δ : List Program} {α : Program} {φ : Formula} {Y : Finset Formula × Finset Formula × Option (NegLoadFormula ⊕ NegLoadFormula)} {R : Finset Formula} : (Formula.boxes δ (Formula.box α φ)).neg ∈ L → ¬φ.isBox → Y = (L.erase (Formula.boxes δ (Formula.box α φ)).neg, R, some (Sum.inl (NegLoadFormula.neg (LoadFormula.boxes δ (LoadFormula.box α (AnyFormula.normal φ)))))) → PdlRule (L, R, none) Y
• loadR {R : Finset Formula} {δ : List Program} {α : Program} {φ : Formula} {Y : Finset Formula × Finset Formula × Option (NegLoadFormula ⊕ NegLoadFormula)} {L : Finset Formula} : (Formula.boxes δ (Formula.box α φ)).neg ∈ R → ¬φ.isBox → Y = (L, R.erase (Formula.boxes δ (Formula.box α φ)).neg, some (Sum.inr (NegLoadFormula.neg (LoadFormula.boxes δ (LoadFormula.box α (AnyFormula.normal φ)))))) → PdlRule (L, R, none) Y
• freeL {X : Finset Formula × Finset Formula × Option (NegLoadFormula ⊕ NegLoadFormula)} {L R : Finset Formula} {δ : List Program} {α : Program} {φ : Formula} {Y : Finset Formula × Finset Formula × Option (NegLoadFormula ⊕ NegLoadFormula)} : X = (L, R, some (Sum.inl (NegLoadFormula.neg (LoadFormula.boxes δ (LoadFormula.box α (AnyFormula.normal φ)))))) → Y = (L ∪ {(Formula.boxes δ (Formula.box α φ)).neg}, R, none) → PdlRule X Y
• freeR {X : Finset Formula × Finset Formula × Option (NegLoadFormula ⊕ NegLoadFormula)} {L R : Finset Formula} {δ : List Program} {α : Program} {φ : Formula} {Y : Finset Formula × Finset Formula × Option (NegLoadFormula ⊕ NegLoadFormula)} : X = (L, R, some (Sum.inr (NegLoadFormula.neg (LoadFormula.boxes δ (LoadFormula.box α (AnyFormula.normal φ)))))) → Y = (L, R ∪ {(Formula.boxes δ (Formula.box α φ)).neg}, none) → PdlRule X Y
• modL {Y : Sequent} {L R : Finset Formula} {A : ℕ} {X : Sequent} {ξ : AnyFormula} : X = (L, R, some (Sum.inl (NegLoadFormula.neg (LoadFormula.box (Program.atom_prog A) ξ)))) → (Y = match ξ with | AnyFormula.normal φ => ({φ.neg} ∪ Finset.pdlProjection A L, Finset.pdlProjection A R, none) | AnyFormula.loaded χ => (Finset.pdlProjection A L, Finset.pdlProjection A R, some (Sum.inl (NegLoadFormula.neg χ)))) → PdlRule X Y
• modR {Y : Sequent} {L R : Finset Formula} {A : ℕ} {X : Sequent} {ξ : AnyFormula} : X = (L, R, some (Sum.inr (NegLoadFormula.neg (LoadFormula.box (Program.atom_prog A) ξ)))) → (Y = match ξ with | AnyFormula.normal φ => (Finset.pdlProjection A L, {φ.neg} ∪ Finset.pdlProjection A R, none) | AnyFormula.loaded χ => (Finset.pdlProjection A L, Finset.pdlProjection A R, some (Sum.inr (NegLoadFormula.neg χ)))) → PdlRule X Y

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

@[instance_reducible]

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

Equations

• PDL.instDecidableEqPdlRule = PDL.instDecidableEqPdlRule.decEq

def PDL.PdlRule.isModal {X Y : Sequent} : PdlRule X Y → Prop

Whether a PDL rule is one of the two modal rules.

Equations

• (PDL.PdlRule.loadL a a_1 a_2).isModal = False
• (PDL.PdlRule.loadR a a_1 a_2).isModal = False
• (PDL.PdlRule.freeL a a_1).isModal = False
• (PDL.PdlRule.freeR a a_1).isModal = False
• (PDL.PdlRule.modL a a_1).isModal = True
• (PDL.PdlRule.modR a a_1).isModal = True

@[instance_reducible]

instance PDL.instDecidablePdlRuleIsModal {X Y : Sequent} {r : PdlRule X Y} : Decidable r.isModal

Equations

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

inductive PDL.Tableau : History → Sequent → Type

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

This represents a closed tableau for X, constructed by either of:

• a local tableau for X followed by Tableau for all end nodes,
• a PDL rule application followed by Tableau for all results, or
• a loaded-path repeat (also called successful, see [MB1988] condition 6 in Def 14 on page 25).

• loc {Hist : History} {X : Sequent} (nflprep : ¬flprep 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} (nflprep : ¬flprep Hist X) (bas : X.basic) (r : PdlRule X Y) (next : Tableau (X :: Hist) Y) : Tableau Hist X
• lrep {Hist : History} {X : Sequent} (lpr : LoadedPathRepeat Hist X) : Tableau Hist X

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

The number of nodes in a tableau, including every local-rule continuation.

Equations

• (PDL.Tableau.loc nflprep nbas lt next).size = 1 + ∑ x ∈ (PDL.endNodesOf lt).attach, match x with | ⟨Y, Y_in⟩ => (next Y Y_in).size
• (PDL.Tableau.pdl nflprep bas r next).size = 1 + next.size
• (PDL.Tableau.lrep lpr).size = 1

theorem PDL.Tableau.size_next_lt_of_loc {Hist : History} {X : Sequent} {tab : Tableau Hist X} {nrep : ¬flprep Hist X} {nbas : ¬X.basic} {lt : LocalTableau X} {next : (Y : Sequent) → Y ∈ endNodesOf lt → Tableau (X :: Hist) Y} (tab_def : tab = loc nrep nbas lt next) (Y : Sequent) (Y_in : Y ∈ endNodesOf lt) : (next Y Y_in).size < tab.size

theorem PDL.Tableau.size_next_lt_of_pdl {Hist : History} {X Y : Sequent} {tab : Tableau Hist X} {nrep : ¬flprep Hist X} {bas : X.basic} {r : PdlRule X Y} {next : Tableau (X :: Hist) Y} (tab_def : tab = pdl nrep bas r next) : next.size < tab.size

def PDL.decidableExistsEndNodeOf {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)

Decide an existential predicate over the end nodes of a local tableau.

Equations

• PDL.decidableExistsEndNodeOf = decidable_of_iff (∃ x ∈ (PDL.endNodesOf lt).attach, f ↑x ⋯) ⋯

@[instance_reducible]

instance PDL.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 PDL.Tableau.isLrep {Hist : History} {X : Sequent} : Tableau Hist X → Prop

Whether a tableau is a loaded-path-repeat leaf.

Equations

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

inductive PDL.provable : Formula → Prop

Provability witnessed by a tableau closing the negation on either side.

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

def PDL.inconsistent : Sequent → Prop

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

Equations

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

def PDL.consistent : Sequent → Prop

A Sequent is consistent iff it is not inconsistent.

Equations

• PDL.consistent x✝ = ¬PDL.inconsistent x✝