Staying inside the Fischer-Ladner closure

Here we define what it means for a Sequent to be inside the FL closure of another, and then prove several helper lemmas to show that all rules of our tableau system stay in the closure.

The main two results are LocalTableau.stays_in_FL and PdlRule.stays_in_FL.

Intuitively, we want to say that each step from (L,R,O) in a tableau to (L',R',O') stays in the FL of (L,R,O). To be precise, each side left/right stays within its own FL closure. However, this does not mean that L' must be in the FL of L, because the O may also contribute to the left part. This makes Sequent.subseteq_FL tricky to define.

def Sequent.subseteq_FL (X Y : Sequent) : Prop

Sequent Y is a component-wise subset of the FL-closure of X. Note that by component we mean left and right (and not L, R, O).

WORRY: Is using Sequent.O.L here a problem because it might not be injective? (Because it calls unload where both ⌊a⌋⌊b⌋p and ⌊a⌋⌈b⌉p become ⌈a⌉⌈b⌉p.)

Equations

• X.subseteq_FL Y = (X.L ⊆ FLL (Y.L ++ Y.O.L) ∧ X.O.L ⊆ FLL (Y.L ++ Y.O.L) ∧ X.R ⊆ FLL (Y.R ++ Y.O.R) ∧ X.O.R ⊆ FLL (Y.R ++ Y.O.R))

@[simp]

theorem Sequent.subseteq_FL_refl (X : Sequent) : X.subseteq_FL X

@[simp]

theorem Sequent.subseteq_FL_trans (X Y Z : Sequent) : X.subseteq_FL Y → Y.subseteq_FL Z → X.subseteq_FL Z

theorem Sequent.subseteq_FL_of_setEq_right {X Y : Sequent} (h : X.setEqTo Y) {Z : Sequent} : Z.subseteq_FL X → Z.subseteq_FL Y

theorem Sequent.subseteq_FL_of_setEq_left {X Y : Sequent} (h : X.setEqTo Y) {Z : Sequent} : X.subseteq_FL Z → Y.subseteq_FL Z

theorem testsOfProgram_in_FLb {φ : Formula} {α : Program} (φ_in : φ ∈ testsOfProgram α) (ψ : Formula) : φ ∈ FLb α ψ

theorem neg_testsOfProgram_in_FLb {φ : Formula} {α : Program} (φ_in : φ ∈ testsOfProgram α) (ψ : Formula) : ~φ ∈ FLb α ψ

theorem H_tests_in_FL (α : Program) (F : List Formula) (δ : List Program) (in_H : (F, δ) ∈ H α) (ψ : Formula) : F ⊆ FLb α ψ

theorem H_progs_in_FL (F : List Formula) (δ : List Program) (α : Program) (in_H : (F, δ) ∈ H α) (ψ : Formula) : δ ≠ [] → (~⌈⌈δ⌉⌉ψ) ∈ FLb α ψ

theorem unfoldDiamond_in_FL (α : Program) (ψ : Formula) (X : List Formula) : X ∈ unfoldDiamond α ψ → ∀ φ ∈ X, φ ∈ FL (⌈α⌉ψ)

theorem LoadRule.stays_in_FL_left {χ : LoadFormula} {ress : List (List Formula × Option NegLoadFormula)} (lr : LoadRule (~'χ) ress) (Y : List Formula × Option NegLoadFormula) : Y ∈ ress → Sequent.subseteq_FL (Y.1, ∅, Option.map Sum.inl Y.2) (∅, ∅, some (Sum.inl (~'χ)))

Helper for LocalRule.stays_in_FL

theorem LoadRule.stays_in_FL_right {χ : LoadFormula} {ress : List (List Formula × Option NegLoadFormula)} (lr : LoadRule (~'χ) ress) (Y : List Formula × Option NegLoadFormula) : Y ∈ ress → Sequent.subseteq_FL (∅, Y.1, Option.map Sum.inr Y.2) (∅, ∅, some (Sum.inr (~'χ)))

Helper for LocalRule.stays_in_FL

theorem P_in_FL (α : Program) (δ : List Program) (ℓ : TP α) (ψ : Formula) : δ ∈ P α ℓ → (⌈⌈δ⌉⌉ψ) ∈ FL (⌈α⌉ψ)

theorem unfoldBox_in_FL (α : Program) (ψ : Formula) (X : List Formula) : X ∈ unfoldBox α ψ → ∀ φ ∈ X, φ ∈ FL (⌈α⌉ψ)

theorem OneSidedLocalRule.stays_in_FL {precond : List Formula} {ress : List (List Formula)} (rule : OneSidedLocalRule precond ress) (res : List Formula) : res ∈ ress → res ⊆ FLL precond

Helper for LocalRule.stays_in_FL

theorem LocalRule.stays_in_FL {X : Sequent} {B : List Sequent} (rule : LocalRule X B) (Y : Sequent) : Y ∈ B → Y.subseteq_FL X

Helper for LocalTableau.stays_in_FL

@[irreducible]

theorem LocalTableau.stays_in_FL {X : Sequent} (ltX : LocalTableau X) (Y : Sequent) : Y ∈ endNodesOf ltX → Y.subseteq_FL X

End nodes of a local tableau are FischerLadner-subsets of the root. This is used for move_inside_FL.

theorem projection_sub_FLL {a : ℕ} {L : List Formula} : projection a L ⊆ FLL L

theorem PdlRule.stays_in_FL {X Y : Sequent} (rule : PdlRule X Y) : Y.subseteq_FL X

Making a PDL rule step stays in the Fischer-Ladner closure. This is used for move_inside_FL.