Documentation

Pdl.StayingInFL

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.

source
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
Instances For
    source
    @[simp]
    theorem Sequent.subseteq_FL_refl (X : Sequent) :
    X.subseteq_FL X
    source
    @[simp]
    theorem Sequent.subseteq_FL_trans (X Y Z : Sequent) :
    X.subseteq_FL Y → Y.subseteq_FL Z → X.subseteq_FL Z
    source
    theorem testsOfProgram_in_FLb {φ : Formula} {α : Program} (φ_in : φ ∈ testsOfProgram α) (ψ : Formula) :
    φ ∈ FLb α ψ
    source
    theorem neg_testsOfProgram_in_FLb {φ : Formula} {α : Program} (φ_in : φ ∈ testsOfProgram α) (ψ : Formula) :
    ~φ ∈ FLb α ψ
    source
    theorem Dset_tests_in_FL (α : Program) (F : List Formula) (δ : List Program) (in_D : (F, δ) ∈ Dset α) (ψ : Formula) :
    F ⊆ FLb α ψ
    source
    theorem Dset_progs_in_FL (F : List Formula) (δ : List Program) (α : Program) (in_D : (F, δ) ∈ Dset α) (ψ : Formula) :
    δ ≠ [] → (~⌈⌈δ⌉⌉ψ) ∈ FLb α ψ
    source
    theorem unfoldDiamond_in_FL (α : Program) (ψ : Formula) (X : List Formula) :
    X ∈ unfoldDiamond α ψ → ∀ φ ∈ X, φ ∈ FL (⌈α⌉ψ)
    source
    theorem pairUnload.stays_in_FL (F : List Formula) (oχ : Option NegLoadFormula) {α : Program} {φ : Formula} (pU_in_unfD : pairUnload (F, oχ) ∈ unfoldDiamond α φ) :
    F ⊆ FL (~⌈α⌉φ) ∧ Olf.L (Option.map Sum.inl oχ) ⊆ (FL (~⌈α⌉φ)).toFinset ∧ Olf.R (Option.map Sum.inr oχ) ⊆ (FL (~⌈α⌉φ)).toFinset

    Helper for LoadRule.stays_in_FL_left and LoadRule.stays_in_FL_right.

    source
    theorem pairUnloadSet.stays_in_FL {F : List Formula} {oχ : Option NegLoadFormula} {α : Program} {φ : Formula} (pU_in_unfD : pairUnload (F, oχ) ∈ unfoldDiamond α φ) :
    F.toFinset ⊆ {~⌈α⌉φ}.FL ∧ Olf.L (Option.map Sum.inl oχ) ⊆ {~⌈α⌉φ}.FL ∧ Olf.R (Option.map Sum.inr oχ) ⊆ {~⌈α⌉φ}.FL

    Finset version of pairUnload.stays_in_FL.

    source
    theorem LoadRule.stays_in_FL_left {χ : LoadFormula} {ress : Finset (Finset Formula × Option NegLoadFormula)} (lr : LoadRule (~'χ) ress) (Y : Finset 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.

    source
    theorem LoadRule.stays_in_FL_right {χ : LoadFormula} {ress : Finset (Finset Formula × Option NegLoadFormula)} (lr : LoadRule (~'χ) ress) (Y : Finset 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

    source
    theorem P_in_FL (α : Program) (δ : List Program) (ℓ : TP α) (ψ : Formula) :
    δ ∈ P α ℓ → (⌈⌈δ⌉⌉ψ) ∈ FL (⌈α⌉ψ)
    source
    theorem unfoldBox_in_FL (α : Program) (ψ : Formula) (X : List Formula) :
    X ∈ unfoldBox α ψ → ∀ φ ∈ X, φ ∈ FL (⌈α⌉ψ)
    source
    theorem OneSidedLocalRule.stays_in_FL {precond : Finset Formula} {ress : Finset (Finset Formula)} (rule : OneSidedLocalRule precond ress) (res : Finset Formula) :
    res ∈ ress → res ⊆ precond.FL

    Helper for LocalRule.stays_in_FL

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

    Helper for LocalTableau.stays_in_FL

    source
    theorem Olf.sdiff_L_sub (O Ocond : Olf) :
    (O \ Ocond).L ⊆ O.L

    Removing something from an Olf can only remove formulas on the left.

    source
    theorem Olf.sdiff_R_sub (O Ocond : Olf) :
    (O \ Ocond).R ⊆ O.R

    Removing something from an Olf can only remove formulas on the right.

    source
    theorem Olf.L_sub_of_sub {O Ocond : Olf} (h : Ocond ⊆ O) :
    Ocond.L ⊆ O.L

    If Ocond ⊆ O then the left part of Ocond is included in that of O.

    source
    theorem Olf.R_sub_of_sub {O Ocond : Olf} (h : Ocond ⊆ O) :
    Ocond.R ⊆ O.R

    If Ocond ⊆ O then the right part of Ocond is included in that of O.

    source
    theorem LocalRuleApp.stays_in_FL (lra : LocalRuleApp) (W : Sequent) :
    W ∈ lra.C → W.subseteq_FL lra.X

    Helper for LocalTableau.stays_in_FL: applying a local rule stays in the FL closure.

    source
    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.

    source
    theorem projection_sub_FLL {a : ℕ} {L : List Formula} :
    projection a L ⊆ FLL L
    source
    theorem Finset.mem_FL_of_mem {X : Finset Formula} {ψ x : Formula} (hψ : ψ ∈ X) (hx : x ∈ _root_.FL ψ) :
    x ∈ X.FL

    Anything in the FL closure of a member of X is in the FL closure of X.

    source
    theorem Finset.projection_sub_FL {a : ℕ} {X : Finset Formula} :
    projection a X ⊆ X.FL
    source
    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.