Documentation

LeanPool.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.subseteqFL tricky to define.

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

    Helper for LoadRule.stays_in_FL_left and LoadRule.stays_in_FL_right.

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

    Finset version of pairUnload.stays_in_FL.

    source
    theorem PDL.LoadRule.stays_in_FL_left {χ : LoadFormula} {ress : Finset (Finset Formula × Option NegLoadFormula)} (lr : LoadRule (NegLoadFormula.neg χ) ress) (Y : Finset Formula × Option NegLoadFormula) :
    Y ∈ ress → Sequent.subseteqFL (Y.1, ∅, Option.map Sum.inl Y.2) (∅, ∅, some (Sum.inl (NegLoadFormula.neg χ)))

    Helper for LocalRule.stays_in_FL.

    source
    theorem PDL.LoadRule.stays_in_FL_right {χ : LoadFormula} {ress : Finset (Finset Formula × Option NegLoadFormula)} (lr : LoadRule (NegLoadFormula.neg χ) ress) (Y : Finset Formula × Option NegLoadFormula) :
    Y ∈ ress → Sequent.subseteqFL (∅, Y.1, Option.map Sum.inr Y.2) (∅, ∅, some (Sum.inr (NegLoadFormula.neg χ)))

    Helper for LocalRule.stays_in_FL

    source
    theorem PDL.P_in_FL (α : Program) (δ : List Program) (ℓ : TP α) (ψ : Formula) :
    δ ∈ P α ℓ → Formula.boxes δ ψ ∈ FL (Formula.box α ψ)
    source
    theorem PDL.unfoldBox_in_FL (α : Program) (ψ : Formula) (X : List Formula) :
    X ∈ unfoldBox α ψ → ∀ φ ∈ X, φ ∈ FL (Formula.box α ψ)
    source
    theorem PDL.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 PDL.LocalRule.stays_in_FL {X : Sequent} {B : Finset Sequent} (rule : LocalRule X B) (Y : Sequent) :
    Y ∈ B → Y.subseteqFL X

    Helper for LocalTableau.stays_in_FL

    source
    theorem PDL.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 PDL.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 PDL.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 PDL.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 PDL.LocalRuleApp.stays_in_FL (lra : LocalRuleApp) (W : Sequent) :
    W ∈ lra.C → W.subseteqFL lra.X

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

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

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

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

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

    source
    theorem PDL.Finset.projection_sub_FL {a : ℕ} {X : Finset Formula} :
    Finset.pdlProjection a X ⊆ X.FL
    source
    theorem PDL.PdlRule.stays_in_FL {X Y : Sequent} (rule : PdlRule X Y) :
    Y.subseteqFL X

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