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.

Formulas occurring along a list of sequents

def pathForms (L : List Sequent) : Finset Formula

All formulas occurring in the sequents of a list, as a Finset.

Equations

• pathForms L = (Finset.image Sequent.toFinset L.toFinset).sup id

@[simp]

theorem mem_pathForms {L : List Sequent} {f : Formula} : f ∈ pathForms L ↔ ∃ Z ∈ L, f ∈ Z.toFinset

@[simp]

theorem pathForms_cons {Z : Sequent} {L : List Sequent} : pathForms (Z :: L) = Z.toFinset ∪ pathForms L

@[simp]

theorem pathForms_nil : pathForms [] = ∅

def pathWForms (L : List Sequent) : Finset WhateverFormula

All WhateverFormulas occurring in the sequents of a list, as a Finset.

Equations

• pathWForms L = (Finset.image Sequent.wForms L.toFinset).sup id

@[simp]

theorem mem_pathWForms {L : List Sequent} {f : WhateverFormula} : f ∈ pathWForms L ↔ ∃ Z ∈ L, f ∈ Z.wForms

@[simp]

theorem pathWForms_cons {Z : Sequent} {L : List Sequent} : pathWForms (Z :: L) = Z.wForms ∪ pathWForms L

@[simp]

theorem pathWForms_nil : pathWForms [] = ∅

Paths

def LocalTableau.paths {X : Sequent} : LocalTableau X → Finset (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.mem_paths_byLocalRule {X : Sequent} {lra : LocalRuleApp} {X_def : X = lra.X} {next : (Y : Sequent) → Y ∈ lra.C → LocalTableau Y} {L : List Sequent} : L ∈ (byLocalRule lra X_def next).paths ↔ ∃ (Y : Sequent) (h : Y ∈ lra.C), ∃ L' ∈ (next Y h).paths, L = X :: L'

Characterisation of membership in paths for the byLocalRule case.

@[simp]

theorem LocalTableau.mem_paths_sim {X : Sequent} {bas : X.basic} {L : List Sequent} : L ∈ (sim bas).paths ↔ L = [X]

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} : Finset.image (fun (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

theorem LocalTableau.paths_saturated {X : Sequent} {lt : LocalTableau X} (L : List Sequent) : L ∈ lt.paths → saturated (pathForms L)

Formulas that survive to the end of a path

theorem LocalTableau.mem_last_of_preserved {α : Type u_1} {X : Sequent} {lt : LocalTableau X} (κ : Sequent → Finset α) (f : α) (pres : ∀ (lra : LocalRuleApp), ∀ Y ∈ lra.C, f ∈ κ lra.X → f ∈ κ Y) (L : List Sequent) (h : L ∈ lt.paths) : (∃ Z ∈ L, f ∈ κ Z) → f ∈ κ (L.getLast ⋯)

General helper: anything that is preserved by all local rule applications and occurs somewhere along a path also occurs at the end of the path.

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 ∈ pathForms L → f ∈ (L.getLast ⋯).toFinset

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

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 ∈ pathForms L → f ∈ (L.getLast ⋯).toFinset

A basic 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 (pathForms L)

Unfolding of diamonds along paths

theorem LocalTableau.paths_freeUnfoldDia {X : Sequent} {lt : LocalTableau X} {α : Program} {φ : Formula} (notAtom : ¬α.isAtomic) (L : List Sequent) : L ∈ lt.paths → (WhateverFormula.any ∘ AnyFormula.normal) (~⌈α⌉φ) ∈ pathWForms L → ∃ Fδ ∈ Dset α, ((Yset Fδ φ).all fun (f : Formula) => decide ((WhateverFormula.any ∘ AnyFormula.normal) f ∈ pathWForms L)) = 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.

theorem LocalTableau.paths_loadUnfoldDia {X : Sequent} {lt : LocalTableau X} {α : Program} {ξ : AnyFormula} (notAtom : ¬α.isAtomic) (L : List Sequent) : L ∈ lt.paths → WhateverFormula.negLoad (~'⌊α⌋ξ) ∈ pathWForms L → ∃ (ress : Finset (Finset Formula × Option NegLoadFormula)), Nonempty (LoadRule (~'⌊α⌋ξ) ress) ∧ ∃ Fo ∈ ress, ((Fo.1.sort fun (a b : Formula) => a ≤ b).all fun (f : Formula) => decide ((WhateverFormula.any ∘ AnyFormula.normal) f ∈ pathWForms L)) = true ∧ (Fo.2.toList.all fun (nl : NegLoadFormula) => decide (WhateverFormula.negLoad nl ∈ pathWForms L)) = 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.

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) : Finset (List Sequent)

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

Equations

• lt.pathsTo Y = {p ∈ lt.paths | p.getLast? = some Y}

@[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.

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 : Finset (Finset 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.

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⌋ξ) ∈ pathWForms L) : 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.