Paths in Local Tableaux

Here we collect the paths of sequents within a LocalTableau, i.e. the lists of sequents from the root to an end node, and show that they are saturated and locally consistent.

This is used for the pre-states in the completeness proof, see BuildTree.lean.

@[irreducible]

def LocalTableau.paths {X : Sequent} : LocalTableau X → List (List Sequent)

Equations

• One or more equations did not get rendered due to their size.
• (LocalTableau.sim a).paths = [[x✝]]

theorem LocalTableau.paths_mem_nonempty {X : Sequent} (lt : LocalTableau X) (L : List Sequent) : L ∈ lt.paths → L ≠ []

theorem LocalTableau.pathsHead_eq_self {X : Sequent} {lt : LocalTableau X} {L : List Sequent} (h : L ∈ lt.paths) : L.head ⋯ = X

theorem LocalTableau.pathsLast_eq_endNodes {X : Sequent} {lt : LocalTableau X} : List.map (fun (x : { x : List Sequent // x ∈ lt.paths }) => match x with | ⟨L, h⟩ => L.getLast ⋯) lt.paths.attach = endNodesOf lt

theorem OpenLocalTableau.paths_nonempty {X : Sequent} (lt : OpenLocalTableau X) : (↑lt).paths ≠ []

Any open local tableau has at least one path (from root to some end node). Does not hold for LocalTableau which might end with "contradiction/closing" rule applications.

theorem LocalTableau.paths_last_basic {X : Sequent} {lt : LocalTableau X} (L : List Sequent) (h : L ∈ lt.paths) : (L.getLast ⋯).basic

@[irreducible]

theorem LocalTableau.paths_saturated {X : Sequent} {lt : LocalTableau X} (L : List Sequent) : L ∈ lt.paths → saturated (List.map Sequent.bothSides L).flatten.toFinset

@[irreducible]

theorem LocalTableau.paths_local_atom_mem_last {X : Sequent} {lt : LocalTableau X} {L : List Sequent} (L_in : L ∈ lt.paths) (f : Formula) : (f = ⊥ ∨ ∃ (p : ℕ), f = ·p ∨ f = ~·p) → f ∈ (List.map Sequent.bothSides L).flatten → f ∈ (L.getLast ⋯).bothSides

An atomic formula anywhere in a local tableau path still occurs at the end of the path.

theorem LocalTableau.paths_locallyConsistent {X : Sequent} {lt : LocalTableau X} (L : List Sequent) : L ∈ lt.paths → locallyConsistent (List.map Sequent.bothSides L).flatten.toFinset

@[irreducible]

theorem LocalTableau.paths_freeUnfoldDia {X : Sequent} {lt : LocalTableau X} {α : Program} {φ : Formula} (notAtom : ¬α.isAtomic) (L : List Sequent) : L ∈ lt.paths → (WhateverFormula.any ∘ AnyFormula.normal) (~⌈α⌉φ) ∈ (List.map Sequent.wForms L).flatten → ∃ Fδ ∈ Dset α, ((Yset Fδ φ).all fun (f : Formula) => decide ((WhateverFormula.any ∘ AnyFormula.normal) f ∈ (List.map Sequent.wForms L).flatten)) = true

Along any path in a local tableau, a non-atomic free diamond must be unfolded: if ~⌈α⌉φ occurs (unloaded) somewhere on the path and α is not atomic, then all formulas of one of the unfoldings Yset Fδ φ occur (unloaded) on the path as well. Analogous to LocalTableau.paths_saturated, but for Sequent.wForms.

@[irreducible]

theorem LocalTableau.paths_loadUnfoldDia {X : Sequent} {lt : LocalTableau X} {α : Program} {ξ : AnyFormula} (notAtom : ¬α.isAtomic) (L : List Sequent) : L ∈ lt.paths → WhateverFormula.negLoad (~'⌊α⌋ξ) ∈ (List.map Sequent.wForms L).flatten → ∃ (ress : List (List Formula × Option NegLoadFormula)), Nonempty (LoadRule (~'⌊α⌋ξ) ress) ∧ ∃ Fo ∈ ress, (Fo.1.all fun (f : Formula) => decide ((WhateverFormula.any ∘ AnyFormula.normal) f ∈ (List.map Sequent.wForms L).flatten)) = true ∧ (Fo.2.toList.all fun (nl : NegLoadFormula) => decide (WhateverFormula.negLoad nl ∈ (List.map Sequent.wForms L).flatten)) = true

Along any path in a local tableau, a non-atomic loaded diamond must be unfolded: if ~'⌊α⌋ξ occurs (loaded) somewhere on the path and α is not atomic, then the results of one application of the corresponding LoadRule occur on the path as well. This is the loaded analogue of LocalTableau.paths_freeUnfoldDia.

@[irreducible]

theorem LocalTableau.paths_basic_mem_last {X : Sequent} {lt : LocalTableau X} {L : List Sequent} (L_in : L ∈ lt.paths) (f : Formula) : f.basic = true → f ∈ (List.map Sequent.bothSides L).flatten → f ∈ (L.getLast ⋯).bothSides

A basic formula anywhere in a local tableau path still occurs at the end of the path. Analogous to LocalTableau.paths_local_atom_mem_last, but for all basic formulas.

Paths ending at a given end node

In the completeness proof (see Pdl/BuildTree.lean) Builder picks one end node of a local tableau, and only the paths ending at that end node should be used as pre-states.

def LocalTableau.pathsTo {X : Sequent} (lt : LocalTableau X) (Y : Sequent) : List (List Sequent)

The paths of a local tableau that end at a given node.

Equations

• lt.pathsTo Y = List.filter (fun (p : List Sequent) => decide (p.getLast? = some Y)) lt.paths

@[simp]

theorem LocalTableau.mem_pathsTo {X : Sequent} {lt : LocalTableau X} {Y : Sequent} {p : List Sequent} : p ∈ lt.pathsTo Y ↔ p ∈ lt.paths ∧ p.getLast? = some Y

theorem LocalTableau.pathsTo_ne_nil {X : Sequent} {lt : LocalTableau X} {Y : Sequent} (h : Y ∈ endNodesOf lt) : lt.pathsTo Y ≠ []

There is at least one path to each end node.

@[irreducible]

theorem LocalTableau.endNodesOf_free {X : Sequent} (lt : LocalTableau X) (hfree : X.O = none) (Y : Sequent) : Y ∈ endNodesOf lt → Y.O = none

All end nodes of a local tableau for a free sequent are free. Consequence of LocalRuleApp.preserve_free.

Atomic loaded diamonds are preserved

A loaded diamond ~'⌊·a⌋ξ with an atomic program cannot be "used up" by a local rule: the only LoadRule applicable to it gives back the very same loaded formula. This is the counterpart of LocalTableau.paths_loadUnfoldDia for atomic programs.

theorem LoadRule.atomic_ress_eq {a : ℕ} {ξ : AnyFormula} {ress : List (List Formula × Option NegLoadFormula)} (lr : LoadRule (~'⌊·a⌋ξ) ress) : ress = [([], some (~'⌊·a⌋ξ))]

The only LoadRule result for an atomic loaded diamond is the loaded diamond itself.

theorem LocalRuleApp.preserve_negLoad_atomic_down (lra : LocalRuleApp) {a : ℕ} {ξ : AnyFormula} (h : WhateverFormula.negLoad (~'⌊·a⌋ξ) ∈ lra.X.wForms) (Y : Sequent) : Y ∈ lra.C → WhateverFormula.negLoad (~'⌊·a⌋ξ) ∈ Y.wForms

A local rule application preserves an atomic loaded diamond.

@[irreducible]

theorem LocalTableau.paths_negLoad_atomic_mem_last {X : Sequent} {lt : LocalTableau X} {L : List Sequent} (L_in : L ∈ lt.paths) {a : ℕ} {ξ : AnyFormula} (hmem : WhateverFormula.negLoad (~'⌊·a⌋ξ) ∈ (List.map Sequent.wForms L).flatten) : WhateverFormula.negLoad (~'⌊·a⌋ξ) ∈ (L.getLast ⋯).wForms

An atomic loaded diamond anywhere in a local tableau path still occurs at the end of it. Analogous to LocalTableau.paths_basic_mem_last, but for the loaded formula.

theorem LocalTableau.paths_last_free {X : Sequent} {lt : LocalTableau X} (hfree : X.O = none) {L : List Sequent} (L_in : L ∈ lt.paths) : (L.getLast ⋯).O = none

The last node of a path in a local tableau for a free sequent is free. Consequence of LocalTableau.endNodesOf_free.