Local Diamond Unfolding (Section 3.2 and 3.3)

Diamonds: Dset, Y and Φ_⋄

def PDL.Dset : Program → List (List Formula × List Program)

Unfold a given program into combinations of test formulas and lists of programs, assuming the program is used inside a diamond.

Equations

• One or more equations did not get rendered due to their size.
• PDL.Dset (PDL.Program.atom_prog a) = [([], [PDL.Program.atom_prog a])]
• PDL.Dset (PDL.Program.test τ) = [([τ], [])]
• PDL.Dset (α.union β) = PDL.Dset α ∪ PDL.Dset β

def PDL.Dl : List Program → List (List Formula × List Program)

Like Dset, but applied to a whole list of programs. This is used to deal with loaded diamonds.

Equations

• One or more equations did not get rendered due to their size.
• PDL.Dl [] = [([], [])]
• PDL.Dl [α] = PDL.Dset α

@[simp]

theorem PDL.Dl_singleton {α : Program} : Dl [α] = Dset α

@[simp]

theorem PDL.Dl_atomic_cons {a : ℕ} {αs : List Program} : Dl (Program.atom_prog a :: αs) = [([], Program.atom_prog a :: αs)]

theorem PDL.relateSeq_Dset_imp_relate {α : Program} {W✝ : Type} {M : KripkeModel W✝} {w v : W✝} {X : List Formula} {δ : List Program} : (X, δ) ∈ Dset α → vDash.SemImplies (M, w) (con X) → relateSeq M δ w v → relate M α w v

theorem PDL.Dset_mem_test (α : Program) (φ : Formula) {Fs : List Formula} {δ : List Program} (in_D : (Fs, δ) ∈ Dset α) (φ_in_Fs : φ ∈ Fs) : ∃ (τ : Formula) (_ : τ ∈ testsOfProgram α), φ = τ

A test formula coming from Dset comes from a test in the given program.

theorem PDL.Dset_mem_sequence (α : Program) {Fs : List Formula} {δ : List Program} (in_D : (Fs, δ) ∈ Dset α) : δ = [] ∨ ∃ (a : ℕ) (δ' : List Program), δ = Program.atom_prog a :: δ'

A list of programs coming from H is either empty or starts with an atom.

theorem PDL.keepFreshDset {x : ℕ ⊕ ℕ} (α : Program) : x ∉ α.voc → ∀ (F : List Formula) (δ : List Program), (F, δ) ∈ Dset α → x ∉ F.pdlFvoc ∧ x ∉ δ.pdlPvoc

theorem PDL.Dset_goes_down_prog (α : Program) {Fs : List Formula} {δ : List Program} (in_D : (Fs, δ) ∈ Dset α) {γ : Program} (in_δ : γ ∈ δ) : if α.isAtomic then γ = α else if α.isStar then lengthOfProgram γ ≤ lengthOfProgram α else lengthOfProgram γ < lengthOfProgram α

This is used by PreState.loadedExists

def PDL.Yset : List Formula × List Program → Formula → List Formula

An intermediate step to define unfoldDiamond. This is not used in the paper.

Equations

• PDL.Yset (F, δ) x✝ = F ∪ [(PDL.Formula.boxes δ x✝).neg]

def PDL.unfoldDiamond (α : Program) (φ : Formula) : List (List Formula)

Φ_◇(α,ψ)

Equations

• PDL.unfoldDiamond α φ = List.map (fun (Fδ : List PDL.Formula × List PDL.Program) => PDL.Yset Fδ φ) (PDL.Dset α)

theorem PDL.unfoldDiamondContent (α : Program) (ψ : Formula) (X : List Formula) : X ∈ unfoldDiamond α ψ → ∀ φ ∈ X, φ = ψ.neg ∨ (∃ τ ∈ testsOfProgram α, φ = τ) ∨ ∃ (a : ℕ) (δ : List Program), φ = (Formula.box (Program.atom_prog a) (Formula.boxes δ ψ)).neg

Where formulas in the diamond unfolding can come from. Inspired by unfoldBoxContent.

theorem PDL.unfoldDiamond_voc {x : ℕ ⊕ ℕ} {α : Program} {φ : Formula} {L : List Formula} (L_in : L ∈ unfoldDiamond α φ) {ψ : Formula} (ψ_in : ψ ∈ L) (x_in_voc_ψ : x ∈ ψ.voc) : x ∈ α.voc ∨ x ∈ φ.voc

theorem PDL.unfoldDiamond_voc_fin {x : ℕ ⊕ ℕ} {α : Program} {φ : Formula} {X : Finset Formula} (X_in : X ∈ (unfoldDiamond α φ).pdlToFinFin) {ψ : Formula} (ψ_in : ψ ∈ X) (x_in_voc_ψ : x ∈ ψ.voc) : x ∈ α.voc ∨ x ∈ φ.voc

Finset version of unfoldDiamond_voc.

theorem PDL.guardToStarDiamond {β : Program} {σ0 σ1 ρ ψ : Formula} (x : ℕ) (x_notin_beta : Sum.inl x ∉ β.voc) (beta_equiv : semEquiv (Formula.box β (Formula.atom_prop x).neg).neg (((Formula.atom_prop x).and σ0).or σ1)) (repl_imp_rho : vDash.SemImplies (replInF x ρ σ1) ρ) (notPsi_imp_rho : vDash.SemImplies ψ.neg ρ) : vDash.SemImplies (Formula.box β.star ψ).neg ρ

theorem PDL.localDiamondTruth (γ : Program) (ψ : Formula) : semEquiv (Formula.box γ ψ).neg (dis (List.map (fun (Fδ : List Formula × List Program) => con (Yset Fδ ψ)) (Dset γ)))

def PDL.pairRel {W : Type} (M : KripkeModel W) : Program × W → Program × W → Prop

Helper function to trick "List.Chain r" to use a different r at each step.

Equations

• PDL.pairRel M (fst, v) (α, w) = PDL.relate M α v w

theorem PDL.relateSeq_toChain' {W : Type} {M : KripkeModel W} {δ : List Program} {v w : W} : relateSeq M δ v w → δ ≠ [] → ∃ (l : List W), l.length + 1 = δ.length ∧ List.IsChain (pairRel M) ((Program.test ⊤ :: δ).zip (v :: l ++ [w]))

theorem PDL.existsDiamondDset {W✝ : Type} {M : KripkeModel W✝} {γ : Program} {v w : W✝} (v_γ_w : relate M γ v w) : ∃ Fδ ∈ Dset γ, vDash.SemImplies (M, v) Fδ.1 ∧ relateSeq M Fδ.2 v w

Loaded Diamonds (Section 3.3)

The Option is used here because unfolding of tests can lead to free nodes.

def PDL.YsetLoad : List Formula × List Program → LoadFormula → List Formula × Option NegLoadFormula

Attach a residual program sequence to an already loaded continuation.

Equations

• PDL.YsetLoad (F, δ) x✝ = (F, some (PDL.NegLoadFormula.neg (PDL.LoadFormula.boxes δ x✝)))

def PDL.YsetLoad' : List Formula × List Program → Formula → List Formula × Option NegLoadFormula

Load a residual sequence over an ordinary formula, or unload it when the sequence is empty.

Equations

• PDL.YsetLoad' (F, δ) x✝ = match PDL.splitLast δ with | none => (F ∪ [x✝.neg], none) | some (δ, β) => (F, some (PDL.NegLoadFormula.neg (PDL.loadMulti δ β x✝)))

def PDL.unfoldDiamondLoaded (α : Program) (χ : LoadFormula) : List (List Formula × Option NegLoadFormula)

Loaded unfolding for ~'⌊α⌋(χ : LoadFormula)

Equations

• PDL.unfoldDiamondLoaded α χ = List.map (fun (Fδ : List PDL.Formula × List PDL.Program) => PDL.YsetLoad Fδ χ) (PDL.Dset α)

def PDL.unfoldDiamondLoaded' (α : Program) (φ : Formula) : List (List Formula × Option NegLoadFormula)

Loaded unfolding for ~'⌊α⌋(φ : Formula)

Equations

• PDL.unfoldDiamondLoaded' α φ = List.map (fun (Fδ : List PDL.Formula × List PDL.Program) => PDL.YsetLoad' Fδ φ) (PDL.Dset α)

def PDL.pairUnload : List Formula × Option NegLoadFormula → List Formula

Merge an optional loaded formula into a list of ordinary formulas by unloading it.

Equations

• PDL.pairUnload (xs, none) = xs
• PDL.pairUnload (xs, some nlf) = xs ∪ [PDL.negUnload nlf]

def PDL.pairUnloadSet : Finset Formula × Option NegLoadFormula → Finset Formula

Merge an optional loaded formula into a finset of ordinary formulas by unloading it.

Equations

• PDL.pairUnloadSet (xs, none) = xs
• PDL.pairUnloadSet (xs, some nlf) = xs ∪ {PDL.negUnload nlf}

theorem PDL.unfoldDiamondLoaded_eq (α : Program) (χ : LoadFormula) : List.map pairUnload (unfoldDiamondLoaded α χ) = unfoldDiamond α χ.unload

theorem PDL.unfoldDiamondLoaded'_eq (α : Program) (φ : Formula) : List.map pairUnload (unfoldDiamondLoaded' α φ) = unfoldDiamond α φ