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.loadLAtomic and PdlRule.loadRAtomic: the (L+) rule applied to an atomic diamond ~⌈·a⌉⌈⌈ηs⌉⌉ψ (where ψ is not a box).
• Sequent.modTarget together with PdlRule.modLTarget and PdlRule.modRTarget: 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 PDL.PdlRule.exists_freeL {L R : Finset Formula} {nlf : NegLoadFormula} : Nonempty (PdlRule (L, R, some (Sum.inl nlf)) (L ∪ {negUnload nlf}, R, none))

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

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

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

theorem PDL.Sequent.mem_toFinset_freeL {L R : Finset Formula} {nlf : NegLoadFormula} {f : Formula} : f ∈ toFinset (L, R, some (Sum.inl nlf)) ↔ f ∈ toFinset (L ∪ {negUnload nlf}, R, none)

Unloading does not change which formulas occur in a sequent.

theorem PDL.Sequent.mem_toFinset_freeR {L R : Finset Formula} {nlf : NegLoadFormula} {f : Formula} : f ∈ toFinset (L, R, some (Sum.inr nlf)) ↔ f ∈ toFinset (L, R ∪ {negUnload nlf}, none)

Unloading does not change which formulas occur in a sequent.

The (L+) rule for atomic diamonds

def PDL.PdlRule.loadLAtomic {L R : Finset Formula} {a : ℕ} {ηs : List Program} {ψ : Formula} (h_in : (Formula.box (Program.atom_prog a) (Formula.boxes ηs ψ)).neg ∈ L) (hnb : ¬ψ.isBox) : PdlRule (L, R, none) (L.erase (Formula.box (Program.atom_prog a) (Formula.boxes ηs ψ)).neg, R, some (Sum.inl (NegLoadFormula.neg (LoadFormula.box (Program.atom_prog a) (AnyFormula.loadBoxes ηs (AnyFormula.normal ψ))))))

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

Equations

• PDL.PdlRule.loadLAtomic h_in hnb = ⋯.mpr (⋯.mpr (PDL.PdlRule.loadL ⋯ hnb ⋯))

def PDL.PdlRule.loadRAtomic {L R : Finset Formula} {a : ℕ} {ηs : List Program} {ψ : Formula} (h_in : (Formula.box (Program.atom_prog a) (Formula.boxes ηs ψ)).neg ∈ R) (hnb : ¬ψ.isBox) : PdlRule (L, R, none) (L, R.erase (Formula.box (Program.atom_prog a) (Formula.boxes ηs ψ)).neg, some (Sum.inr (NegLoadFormula.neg (LoadFormula.box (Program.atom_prog a) (AnyFormula.loadBoxes ηs (AnyFormula.normal ψ))))))

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

Equations

• PDL.PdlRule.loadRAtomic h_in hnb = ⋯.mpr (⋯.mpr (PDL.PdlRule.loadR ⋯ hnb ⋯))

The (M) rule

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

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

Equations

• PDL.Sequent.modTargetL A L R (PDL.AnyFormula.normal φ) = ({φ.neg} ∪ Finset.pdlProjection A L, Finset.pdlProjection A R, none)
• PDL.Sequent.modTargetL A L R (PDL.AnyFormula.loaded χ) = (Finset.pdlProjection A L, Finset.pdlProjection A R, some (Sum.inl (PDL.NegLoadFormula.neg χ)))

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

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

Equations

• PDL.Sequent.modTargetR A L R (PDL.AnyFormula.normal φ) = (Finset.pdlProjection A L, {φ.neg} ∪ Finset.pdlProjection A R, none)
• PDL.Sequent.modTargetR A L R (PDL.AnyFormula.loaded χ) = (Finset.pdlProjection A L, Finset.pdlProjection A R, some (Sum.inr (PDL.NegLoadFormula.neg χ)))

def PDL.PdlRule.modLTarget {A : ℕ} {L R : Finset Formula} {ξ : AnyFormula} : PdlRule (L, R, some (Sum.inl (NegLoadFormula.neg (LoadFormula.box (Program.atom_prog A) ξ)))) (Sequent.modTargetL A L R ξ)

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

Equations

• PDL.PdlRule.modLTarget = PDL.PdlRule.modL ⋯ ⋯

def PDL.PdlRule.modRTarget {A : ℕ} {L R : Finset Formula} {ξ : AnyFormula} : PdlRule (L, R, some (Sum.inr (NegLoadFormula.neg (LoadFormula.box (Program.atom_prog A) ξ)))) (Sequent.modTargetR A L R ξ)

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

Equations

• PDL.PdlRule.modRTarget = PDL.PdlRule.modR ⋯ ⋯

theorem PDL.Sequent.mem_modTargetL_unload {A : ℕ} {L R : Finset Formula} {ξ : AnyFormula} : ξ.unload.neg ∈ (modTargetL A L R ξ).toFinset

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

theorem PDL.Sequent.mem_modTargetR_unload {A : ℕ} {L R : Finset Formula} {ξ : AnyFormula} : ξ.unload.neg ∈ (modTargetR A L R ξ).toFinset

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

theorem PDL.Sequent.projection_mem_modTargetL {A : ℕ} {L R : Finset Formula} {ξ : AnyFormula} {ρ : Formula} (h : Formula.box (Program.atom_prog A) ρ ∈ L ∨ Formula.box (Program.atom_prog A) ρ ∈ R) : ρ ∈ (modTargetL A L R ξ).toFinset

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

theorem PDL.Sequent.projection_mem_modTargetR {A : ℕ} {L R : Finset Formula} {ξ : AnyFormula} {ρ : Formula} (h : Formula.box (Program.atom_prog A) ρ ∈ L ∨ Formula.box (Program.atom_prog A) ρ ∈ R) : ρ ∈ (modTargetR A L R ξ).toFinset

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

Combining (L+) and (M)

theorem PDL.Sequent.basic_loadL_atomic {L R : Finset Formula} {a : ℕ} {ηs : List Program} {ψ : Formula} (hbas : basic (L, R, none)) : basic (L.erase (Formula.box (Program.atom_prog a) (Formula.boxes ηs ψ)).neg, R, some (Sum.inl (NegLoadFormula.neg (LoadFormula.box (Program.atom_prog a) (AnyFormula.loadBoxes ηs (AnyFormula.normal ψ))))))

Loading an atomic diamond keeps the sequent basic.

theorem PDL.Sequent.basic_loadR_atomic {L R : Finset Formula} {a : ℕ} {ηs : List Program} {ψ : Formula} (hbas : basic (L, R, none)) : basic (L, R.erase (Formula.box (Program.atom_prog a) (Formula.boxes ηs ψ)).neg, some (Sum.inr (NegLoadFormula.neg (LoadFormula.box (Program.atom_prog a) (AnyFormula.loadBoxes ηs (AnyFormula.normal ψ))))))

Loading an atomic diamond keeps the sequent basic.

theorem PDL.Sequent.exists_atomic_modal_steps {L R : Finset Formula} {a : ℕ} {ηs : List Program} {ψ : Formula} (hnb : ¬ψ.isBox) (hbas : basic (L, R, none)) (h_in : (Formula.box (Program.atom_prog a) (Formula.boxes ηs ψ)).neg ∈ toFinset (L, R, none)) : ∃ (Y1 : Sequent) (Y2 : Sequent), Nonempty (PdlRule (L, R, none) Y1) ∧ Y1.basic ∧ Nonempty (PdlRule Y1 Y2) ∧ (Formula.boxes ηs ψ).neg ∈ Y2.toFinset ∧ ∀ (ρ : Formula), Formula.box (Program.atom_prog a) ρ ∈ toFinset (L, R, none) → ρ ∈ Y2.toFinset

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.