Concrete PDL rule applications

Helpers to construct PdlRule applications, and to describe the sequents they lead to. These are used in Pdl/BuildTree.lean to walk through a BuildTree when proving the existence lemmas for the model graph.

The main results are:

• PdlRule.exists_freeL and PdlRule.exists_freeR: the (L-) rule is always applicable to a loaded sequent, and it does not change the set of formulas.
• PdlRule.loadL_atomic and PdlRule.loadR_atomic: the (L+) rule applied to an atomic diamond ~⌈·a⌉⌈⌈ηs⌉⌉ψ (where ψ is not a box).
• Sequent.modTarget together with PdlRule.modL_target and PdlRule.modR_target: the (M) rule applied to an atomic loaded box.
• Sequent.exists_atomic_modal_steps: the combination of (L+) and (M), giving the a-successor of a free basic sequent.

The (L-) rule

theorem PdlRule.exists_freeL {L R : List Formula} {nlf : NegLoadFormula} : Nonempty (PdlRule (L, R, some (Sum.inl nlf)) (List.insert (negUnload nlf) L, R, none))

The (L-) rule is applicable to any left-loaded sequent, and the resulting sequent is obtained by inserting the unloaded formula on the left.

theorem PdlRule.exists_freeR {L R : List Formula} {nlf : NegLoadFormula} : Nonempty (PdlRule (L, R, some (Sum.inr nlf)) (L, List.insert (negUnload nlf) R, none))

The (L-) rule is applicable to any right-loaded sequent.

theorem Sequent.mem_bothSides_freeL {L R : List Formula} {nlf : NegLoadFormula} {f : Formula} : f ∈ bothSides (L, R, some (Sum.inl nlf)) ↔ f ∈ bothSides (List.insert (negUnload nlf) L, R, none)

Unloading does not change which formulas occur in a sequent.

theorem Sequent.mem_bothSides_freeR {L R : List Formula} {nlf : NegLoadFormula} {f : Formula} : f ∈ bothSides (L, R, some (Sum.inr nlf)) ↔ f ∈ bothSides (L, List.insert (negUnload nlf) R, none)

Unloading does not change which formulas occur in a sequent.

The (L+) rule for atomic diamonds

def PdlRule.loadL_atomic {L R : List Formula} {a : ℕ} {ηs : List Program} {ψ : Formula} (h_in : (~⌈·a⌉⌈⌈ηs⌉⌉ψ) ∈ L) (hnb : ¬ψ.isBox) : PdlRule (L, R, none) (L.erase (~⌈·a⌉⌈⌈ηs⌉⌉ψ), R, some (Sum.inl (~'⌊·a⌋AnyFormula.loadBoxes ηs (AnyFormula.normal ψ))))

The (L+) rule applied to a free atomic diamond on the left.

Equations

• PdlRule.loadL_atomic h_in hnb = ⋯.mpr (⋯.mpr (PdlRule.loadL ⋯ hnb ⋯))

def PdlRule.loadR_atomic {L R : List Formula} {a : ℕ} {ηs : List Program} {ψ : Formula} (h_in : (~⌈·a⌉⌈⌈ηs⌉⌉ψ) ∈ R) (hnb : ¬ψ.isBox) : PdlRule (L, R, none) (L, R.erase (~⌈·a⌉⌈⌈ηs⌉⌉ψ), some (Sum.inr (~'⌊·a⌋AnyFormula.loadBoxes ηs (AnyFormula.normal ψ))))

The (L+) rule applied to a free atomic diamond on the right.

Equations

• PdlRule.loadR_atomic h_in hnb = ⋯.mpr (⋯.mpr (PdlRule.loadR ⋯ hnb ⋯))

The (M) rule

def Sequent.modTargetL (A : ℕ) (L R : List Formula) (ξ : AnyFormula) : Sequent

The sequent reached by the (M) rule from ⟨L, R, some (Sum.inl (~'⌊·A⌋ξ))⟩.

Equations

• Sequent.modTargetL A L R (AnyFormula.normal φ) = (~φ :: projection A L, projection A R, none)
• Sequent.modTargetL A L R (AnyFormula.loaded χ) = (projection A L, projection A R, some (Sum.inl (~'χ)))

def Sequent.modTargetR (A : ℕ) (L R : List Formula) (ξ : AnyFormula) : Sequent

The sequent reached by the (M) rule from ⟨L, R, some (Sum.inr (~'⌊·A⌋ξ))⟩.

Equations

• Sequent.modTargetR A L R (AnyFormula.normal φ) = (projection A L, ~φ :: projection A R, none)
• Sequent.modTargetR A L R (AnyFormula.loaded χ) = (projection A L, projection A R, some (Sum.inr (~'χ)))

def PdlRule.modL_target {A : ℕ} {L R : List Formula} {ξ : AnyFormula} : PdlRule (L, R, some (Sum.inl (~'⌊·A⌋ξ))) (Sequent.modTargetL A L R ξ)

The (M) rule applied to a left-loaded atomic box.

Equations

• PdlRule.modL_target = PdlRule.modL ⋯ ⋯

def PdlRule.modR_target {A : ℕ} {L R : List Formula} {ξ : AnyFormula} : PdlRule (L, R, some (Sum.inr (~'⌊·A⌋ξ))) (Sequent.modTargetR A L R ξ)

The (M) rule applied to a right-loaded atomic box.

Equations

• PdlRule.modR_target = PdlRule.modR ⋯ ⋯

theorem Sequent.mem_modTargetL_unload {A : ℕ} {L R : List Formula} {ξ : AnyFormula} : ~ξ.unload ∈ (modTargetL A L R ξ).bothSides

The negation of the unloaded rest is in the sequent reached by (M).

theorem Sequent.mem_modTargetR_unload {A : ℕ} {L R : List Formula} {ξ : AnyFormula} : ~ξ.unload ∈ (modTargetR A L R ξ).bothSides

The negation of the unloaded rest is in the sequent reached by (M).

theorem Sequent.projection_mem_modTargetL {A : ℕ} {L R : List Formula} {ξ : AnyFormula} {ρ : Formula} (h : (⌈·A⌉ρ) ∈ L ∨ (⌈·A⌉ρ) ∈ R) : ρ ∈ (modTargetL A L R ξ).bothSides

The (M) rule keeps the A-projection of the free part of the sequent.

theorem Sequent.projection_mem_modTargetR {A : ℕ} {L R : List Formula} {ξ : AnyFormula} {ρ : Formula} (h : (⌈·A⌉ρ) ∈ L ∨ (⌈·A⌉ρ) ∈ R) : ρ ∈ (modTargetR A L R ξ).bothSides

The (M) rule keeps the A-projection of the free part of the sequent.

Combining (L+) and (M)

theorem Sequent.basic_loadL_atomic {L R : List Formula} {a : ℕ} {ηs : List Program} {ψ : Formula} (hbas : basic (L, R, none)) : basic (L.erase (~⌈·a⌉⌈⌈ηs⌉⌉ψ), R, some (Sum.inl (~'⌊·a⌋AnyFormula.loadBoxes ηs (AnyFormula.normal ψ))))

Loading an atomic diamond keeps the sequent basic.

theorem Sequent.basic_loadR_atomic {L R : List Formula} {a : ℕ} {ηs : List Program} {ψ : Formula} (hbas : basic (L, R, none)) : basic (L, R.erase (~⌈·a⌉⌈⌈ηs⌉⌉ψ), some (Sum.inr (~'⌊·a⌋AnyFormula.loadBoxes ηs (AnyFormula.normal ψ))))

Loading an atomic diamond keeps the sequent basic.

theorem Sequent.exists_atomic_modal_steps {L R : List Formula} {a : ℕ} {ηs : List Program} {ψ : Formula} (hnb : ¬ψ.isBox) (hbas : basic (L, R, none)) (h_in : (~⌈·a⌉⌈⌈ηs⌉⌉ψ) ∈ bothSides (L, R, none)) : ∃ (Y1 : Sequent) (Y2 : Sequent), Nonempty (PdlRule (L, R, none) Y1) ∧ Y1.basic ∧ Nonempty (PdlRule Y1 Y2) ∧ (~⌈⌈ηs⌉⌉ψ) ∈ Y2.bothSides ∧ ∀ (ρ : Formula), (⌈·a⌉ρ) ∈ bothSides (L, R, none) → ρ ∈ Y2.bothSides

Two PDL steps, first (L+) and then (M), lead from a free basic sequent containing the atomic diamond ~⌈·a⌉⌈⌈ηs⌉⌉ψ (with ψ not a box) to a sequent that contains ~⌈⌈ηs⌉⌉ψ and the whole a-projection of the sequent we started from.