Local Box Unfolding (Section 3.1)

Preparation for Boxes: Test Profiles

def TP (α : Program) : Type

Type of test profiles for a given program.

Equations

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

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

Equations

• instFintypeTP = id Pi.instFintype

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

instance instCoeOutTPUnion {α β : Program} : CoeOut (TP (α⋓β)) (TP α)

Equations

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

instance instCoeOutTPUnion_1 {α β : Program} : CoeOut (TP (α⋓β)) (TP β)

Equations

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

instance instCoeOutTPSequence {α β : Program} : CoeOut (TP (α;'β)) (TP α)

Equations

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

instance instCoeOutTPSequence_1 {α β : Program} : CoeOut (TP (α;'β)) (TP β)

Equations

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

instance instCoeOutTPStar {α : Program} : CoeOut (TP (∗α)) (TP α)

Equations

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

def 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

• allTP α = List.map (fun (l : List Formula) (x : { τ : Formula // τ ∈ testsOfProgram α }) => match x with | ⟨τ, property⟩ => decide (τ ∈ l)) (testsOfProgram α).sublists

theorem 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 signature (α : Program) (ℓ : TP α) : Formula

σ^ℓ

Equations

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

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

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

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

theorem equiv_iff_TPequiv {φ ψ : Formula} {α : Program} : φ≡ψ ↔ ∀ (ℓ : TP α), φ⋀signature α ℓ≡ψ⋀signature α ℓ

Boxes: F, P, X and unfoldBox

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

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

Equations

• F (·a) x_2 = ∅
• F (?'τ) ℓ = if ℓ ⟨τ, ⋯⟩ = true then ∅ else [~τ]
• F (α⋓β) ℓ = (F α fun (τ : { τ : Formula // τ ∈ testsOfProgram α }) => ℓ ⟨↑τ, ⋯⟩) ∪ F β fun (τ : { τ : Formula // τ ∈ testsOfProgram β }) => ℓ ⟨↑τ, ⋯⟩
• F (α;'β) ℓ = (F α fun (τ : { τ : Formula // τ ∈ testsOfProgram α }) => ℓ ⟨↑τ, ⋯⟩) ∪ F β fun (τ : { τ : Formula // τ ∈ testsOfProgram β }) => ℓ ⟨↑τ, ⋯⟩
• F (∗α) ℓ = F α ℓ

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

Equations

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

def Xset (α : Program) (ℓ : TP α) (ψ : Formula) : List Formula

Equations

• Xset α ℓ ψ = F α ℓ ++ List.map (fun (as : List Program) => ⌈⌈as⌉⌉ψ) (P α ℓ)

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

unfold_□(α,ψ)

Equations

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

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

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

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

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

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

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

@[irreducible]

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

Depending on α we know what can occur inside δ ∈ P α ℓ for unfoldBox.

theorem unfoldBoxContent (α : Program) (ψ : Formula) (X : List Formula) : X ∈ unfoldBox α ψ → ∀ φ ∈ X, φ = ψ ∨ (∃ τ ∈ testsOfProgram α, φ = (~τ)) ∨ ∃ (a : ℕ) (δ : List Program), (φ = ⌈·a⌉⌈⌈δ⌉⌉ψ) ∧ ∀ γ ∈ (·a) :: δ, γ ∈ subprograms α

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

theorem boxHelperTP (α : Program) (ℓ : TP α) : (∀ (τ : { τ : Formula // τ ∈ testsOfProgram α }), (~↑τ) ∈ F α ℓ → ℓ τ = false) ∧ Con (F α ℓ)⋀signature α ℓ≡signature α ℓ ∧ ∀ (ψ : Formula), Con (Xset α ℓ ψ)⋀signature α ℓ≡Con (List.map (fun (αs : List Program) => ⌈⌈αs⌉⌉ψ) (P α ℓ))⋀signature α ℓ

theorem guardToStar (x : ℕ) (β : Program) (χ0 χ1 ρ ψ : Formula) (x_notin_beta : Sum.inl x ∉ β.voc) (beta_equiv : (⌈β⌉·x)≡(·x)⋀χ0⋁χ1) (rho_imp_repl : ρ⊨repl_in_F x ρ (χ0⋁χ1)) (rho_imp_psi : ρ⊨ψ) : ρ⊨⌈∗β⌉ψ

theorem localBoxTruth_connector (γ : Program) (ψ : Formula) (goal : ∀ (ℓ : TP γ), (⌈γ⌉ψ)⋀signature γ ℓ≡Con (Xset γ ℓ ψ)⋀signature γ ℓ) : (⌈γ⌉ψ)≡dis (List.map (fun (ℓ : TP γ) => Con (Xset γ ℓ ψ)) (allTP γ))

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

theorem localBoxTruthI (γ : Program) (ψ : Formula) (ℓ : TP γ) : (⌈γ⌉ψ)⋀signature γ ℓ≡Con (Xset γ ℓ ψ)⋀signature γ ℓ

Induction claim for localBoxTruth.

theorem localBoxTruth (γ : Program) (ψ : Formula) : (⌈γ⌉ψ)≡dis (List.map (fun (ℓ : TP γ) => Con (Xset γ ℓ ψ)) (allTP γ))

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