Local Box Unfolding (Section 3.1)

Preparation for Boxes: Test Profiles

@[reducible, inline]

abbrev PDL.TP (α : Program) : Type

Type of test profiles for a given program.

Equations

• PDL.TP α = ({ τ : PDL.Formula // τ ∈ PDL.testsOfProgram α } → Bool)

@[instance_reducible]

instance PDL.instFintypeTP {α : Program} : Fintype (TP α)

Equations

• PDL.instFintypeTP = Pi.instFintype

theorem PDL.TP_eq_iff {α : Program} {ℓ ℓ' : TP α} : ℓ = ℓ' ↔ ∀ τ ∈ (testsOfProgram α).attach, ℓ τ = ℓ' τ

@[instance_reducible]

instance PDL.instCoeOutTPUnion {α β : Program} : CoeOut (TP (α.union β)) (TP α)

Equations

• PDL.instCoeOutTPUnion = { coe := fun (ℓ : PDL.TP (α.union β)) (τ : { τ : PDL.Formula // τ ∈ PDL.testsOfProgram α }) => ℓ ⟨↑τ, ⋯⟩ }

@[instance_reducible]

instance PDL.instCoeOutTPUnion_1 {α β : Program} : CoeOut (TP (α.union β)) (TP β)

Equations

• PDL.instCoeOutTPUnion_1 = { coe := fun (ℓ : PDL.TP (α.union β)) (τ : { τ : PDL.Formula // τ ∈ PDL.testsOfProgram β }) => ℓ ⟨↑τ, ⋯⟩ }

@[instance_reducible]

instance PDL.instCoeOutTPSequence {α β : Program} : CoeOut (TP (α.sequence β)) (TP α)

Equations

• PDL.instCoeOutTPSequence = { coe := fun (ℓ : PDL.TP (α.sequence β)) (τ : { τ : PDL.Formula // τ ∈ PDL.testsOfProgram α }) => ℓ ⟨↑τ, ⋯⟩ }

@[instance_reducible]

instance PDL.instCoeOutTPSequence_1 {α β : Program} : CoeOut (TP (α.sequence β)) (TP β)

Equations

• PDL.instCoeOutTPSequence_1 = { coe := fun (ℓ : PDL.TP (α.sequence β)) (τ : { τ : PDL.Formula // τ ∈ PDL.testsOfProgram β }) => ℓ ⟨↑τ, ⋯⟩ }

@[instance_reducible]

instance PDL.instCoeOutTPStar {α : Program} : CoeOut (TP α.star) (TP α)

Equations

• PDL.instCoeOutTPStar = { coe := fun (l : PDL.TP α.star) (x : { τ : PDL.Formula // τ ∈ PDL.testsOfProgram α }) => match x with | ⟨f, f_in⟩ => l ⟨f, ⋯⟩ }

def PDL.allTP (α : Program) : List (TP α)

List of all test profiles for a given program. Note that in contrast to Fintype.elems : Finset (TP α) here we get a computable List (TP α).

Equations

• One or more equations did not get rendered due to their size.

theorem PDL.allTP_mem {α : Program} (ℓ : TP α) : ℓ ∈ allTP α

All test profiles are in the list of all test profiles. Thanks to Floris van Doorn https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/List.20of.20.28provably.29.20all.20functions.20from.20given.20List.20to.20Bool

def PDL.signature (α : Program) (ℓ : TP α) : Formula

σ^ℓ

Equations

• PDL.signature α ℓ = PDL.con (List.map (fun (τ : { τ : PDL.Formula // τ ∈ PDL.testsOfProgram α }) => if ℓ τ = true then ↑τ else (↑τ).neg) (PDL.testsOfProgram α).attach)

theorem PDL.signature_iff {α : Program} {ℓ : TP α} {W : Type} {M : KripkeModel W} {w : W} : evaluate M w (signature α ℓ) ↔ ∀ τ ∈ (testsOfProgram α).attach, ℓ τ = true ↔ evaluate M w ↑τ

A signature assigns each test exactly the truth value recorded by its profile.

theorem PDL.top_equiv_disj_TP (α : Program) : tautology (dis (List.map (signature α) (allTP α)))

This is currently unused.

theorem PDL.signature_contradiction_of_neq_TPs {α : Program} {ℓ ℓ' : TP α} : ℓ ≠ ℓ' → contradiction ((signature α ℓ).and (signature α ℓ'))

This is currently unused.

theorem PDL.equiv_iff_TPequiv {φ ψ : Formula} {α : Program} : semEquiv φ ψ ↔ ∀ (ℓ : TP α), semEquiv (φ.and (signature α ℓ)) (ψ.and (signature α ℓ))

This is currently unused.

Boxes: F, P, Bset and unfoldBox

Note: In F, P and Bset we use lists not sets, to eventually make formulas.

def PDL.F (α : Program) (ℓ : TP α) : List Formula

The test constraints produced by box unfolding under a test profile.

Equations

• PDL.F (PDL.Program.atom_prog a) x_2 = ∅
• PDL.F (PDL.Program.test τ) ℓ = if ℓ ⟨τ, ⋯⟩ = true then ∅ else [τ.neg]
• PDL.F (α.union β) ℓ = (PDL.F α fun (τ : { τ : PDL.Formula // τ ∈ PDL.testsOfProgram α }) => ℓ ⟨↑τ, ⋯⟩) ∪ PDL.F β fun (τ : { τ : PDL.Formula // τ ∈ PDL.testsOfProgram β }) => ℓ ⟨↑τ, ⋯⟩
• PDL.F (α.sequence β) ℓ = (PDL.F α fun (τ : { τ : PDL.Formula // τ ∈ PDL.testsOfProgram α }) => ℓ ⟨↑τ, ⋯⟩) ∪ PDL.F β fun (τ : { τ : PDL.Formula // τ ∈ PDL.testsOfProgram β }) => ℓ ⟨↑τ, ⋯⟩
• PDL.F α.star ℓ = PDL.F α ℓ

theorem PDL.F_sub_testsOfProgram_map_neg (α : Program) (ℓ : TP α) : F α ℓ ⊆ List.map Formula.neg (testsOfProgram α)

def PDL.P (α : Program) (ℓ : TP α) : List (List Program)

The residual program sequences produced by box unfolding under a test profile.

Equations

• One or more equations did not get rendered due to their size.
• PDL.P (PDL.Program.atom_prog a) x_2 = [[PDL.Program.atom_prog a]]
• PDL.P (PDL.Program.test τ) ℓ = if ℓ ⟨τ, ⋯⟩ = true then [[]] else ∅
• PDL.P (α.union β) ℓ = (PDL.P α fun (τ : { τ : PDL.Formula // τ ∈ PDL.testsOfProgram α }) => ℓ ⟨↑τ, ⋯⟩) ∪ PDL.P β fun (τ : { τ : PDL.Formula // τ ∈ PDL.testsOfProgram β }) => ℓ ⟨↑τ, ⋯⟩
• PDL.P α.star ℓ = [[]] ∪ List.map (fun (as : List PDL.Program) => as ++ [α.star]) (List.filter (fun (x : List PDL.Program) => x != []) (PDL.P α ℓ))

def PDL.Bset (α : Program) (ℓ : TP α) (ψ : Formula) : List Formula

The test constraints and residual boxes in one branch of box unfolding.

Equations

• PDL.Bset α ℓ ψ = PDL.F α ℓ ++ List.map (fun (as : List PDL.Program) => PDL.Formula.boxes as ψ) (PDL.P α ℓ)

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

unfold_□(α,ψ)

Equations

• PDL.unfoldBox α φ = List.map (fun (ℓ : PDL.TP α) => PDL.Bset α ℓ φ) (PDL.allTP α)

theorem PDL.F_mem_iff_neg (α : Program) (ℓ : TP α) (φ : Formula) : φ ∈ F α ℓ ↔ ∃ (τ : Formula) (h : τ ∈ testsOfProgram α), φ = τ.neg ∧ ℓ ⟨τ, h⟩ = false

theorem PDL.P_monotone (α : Program) (ℓ ℓ' : TP α) (h : ∀ (τ : { τ : Formula // τ ∈ testsOfProgram α }), ℓ τ = true → ℓ' τ = true) (δ : List Program) : δ ∈ P α ℓ → δ ∈ P α ℓ'

theorem PDL.F_goes_down {α : Program} {ℓ : TP α} {φ : Formula} : φ ∈ F α ℓ → lengthOfFormula φ < lengthOfProgram α

theorem PDL.keepFreshF {x : ℕ ⊕ ℕ} (α : Program) (ℓ : TP α) (x_notin : x ∉ α.voc) (φ : Formula) : φ ∈ F α ℓ → x ∉ φ.voc

theorem PDL.keepFreshP {x : ℕ ⊕ ℕ} (α : Program) (ℓ : TP α) (x_notin : x ∉ α.voc) (δ : List Program) : δ ∈ P α ℓ → x ∉ δ.pdlPvoc

theorem PDL.boxHelperTermination (α : Program) (ℓ : TP α) (δ : List Program) : δ ∈ P α ℓ → (α.isAtomic → δ = [α]) ∧ (∀ (β : Program), α = β.star → δ = [] ∨ ∃ (a : ℕ) (δ1n : List Program), δ = Program.atom_prog a :: δ1n ++ [β.star] ∧ Program.atom_prog a :: δ1n ⊆ (subprograms α).erase α) ∧ (¬α.isAtomic ∧ ¬α.isStar → δ = [] ∨ ∃ (a : ℕ) (δ1n : List Program), δ = Program.atom_prog a :: δ1n ∧ Program.atom_prog a :: δ1n ⊆ (subprograms α).erase α)

Depending on α we know what can occur inside δ ∈ P α ℓ and thus later in unfoldBox.

theorem PDL.PgoesDown {δ : List Program} {γ α : Program} {ℓ : TP α} : γ ∈ δ → δ ∈ P α ℓ → if α.isAtomic then γ = α else if α.isStar then lengthOfProgram γ ≤ lengthOfProgram α else lengthOfProgram γ < lengthOfProgram α

Proven from boxHelperTermination.

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

Where formulas in the unfolding can come from. The article also says φ ∈ fischerLadner [⌈α⌉ψ] which we prove later in unfoldBox_in_FL.

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

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

Finset version of unfoldBox_voc.

theorem PDL.boxHelperTP (α : Program) (ℓ : TP α) : (∀ (τ : { τ : Formula // τ ∈ testsOfProgram α }), (↑τ).neg ∈ F α ℓ → ℓ τ = false) ∧ semEquiv ((con (F α ℓ)).and (signature α ℓ)) (signature α ℓ) ∧ ∀ (ψ : Formula), semEquiv ((con (Bset α ℓ ψ)).and (signature α ℓ)) ((con (List.map (fun (αs : List Program) => Formula.boxes αs ψ) (P α ℓ))).and (signature α ℓ))

A helper theorem about Bset and signature. Note that the paper only states the third conjunct.

theorem PDL.guardToStar (x : ℕ) (β : Program) (χ0 χ1 ρ ψ : Formula) (x_notin_beta : Sum.inl x ∉ β.voc) (beta_equiv : semEquiv (Formula.box β (Formula.atom_prop x)) (((Formula.atom_prop x).and χ0).or χ1)) (rho_imp_repl : vDash.SemImplies ρ (replInF x ρ (χ0.or χ1))) (rho_imp_psi : vDash.SemImplies ρ ψ) : vDash.SemImplies ρ (Formula.box β.star ψ)

theorem PDL.localBoxTruth_connector (γ : Program) (ψ : Formula) (goal : ∀ (ℓ : TP γ), semEquiv ((Formula.box γ ψ).and (signature γ ℓ)) ((con (Bset γ ℓ ψ)).and (signature γ ℓ))) : semEquiv (Formula.box γ ψ) (dis (List.map (fun (ℓ : TP γ) => con (Bset γ ℓ ψ)) (allTP γ)))

Show "suffices" part outside, to use localBoxTruth for star case in localBoxTruthI.

theorem PDL.localBoxTruthI (γ : Program) (ψ : Formula) (ℓ : TP γ) : semEquiv ((Formula.box γ ψ).and (signature γ ℓ)) ((con (Bset γ ℓ ψ)).and (signature γ ℓ))

Induction claim for localBoxTruth.

theorem PDL.localBoxTruth (γ : Program) (ψ : Formula) : semEquiv (Formula.box γ ψ) (dis (List.map (fun (ℓ : TP γ) => con (Bset γ ℓ ψ)) (allTP γ)))

theorem PDL.existsBoxFP {W✝ : Type} {M : KripkeModel W✝} {v w : W✝} (γ : Program) (v_γ_w : relate M γ v w) (ℓ : TP γ) (v_conF : vDash.SemImplies (M, v) (con (F γ ℓ))) : ∃ δ ∈ P γ ℓ, relateSeq M δ v w