Local Box Unfolding (Section 3.1)

Preparation for Boxes: Test Profiles

@[reducible, inline]

abbrev TP (α : Program) : Type

Type of test profiles for a given program.

Equations

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

@[instance_reducible]

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

Equations

• instFintypeTP = Pi.instFintype

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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 ↑τ

This is currently unused.

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

This is currently unused.

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

This is currently unused.

theorem equiv_iff_TPequiv {φ ψ : Formula} {α : Program} : φ ≡ ψ ↔ ∀ (ℓ : TP α), φ ⋀ signature α ℓ ≡ ψ ⋀ 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 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 α ℓ

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

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 Bset (α : Program) (ℓ : TP α) (ψ : Formula) : List Formula

Equations

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

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

unfold_□(α,ψ)

Equations

• unfoldBox α φ = List.map (fun (ℓ : TP α) => Bset α ℓ φ) (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 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

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

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

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

Proven from boxHelperTermination.

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 prove later in unfoldBox_in_FL.

theorem 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 unfoldBox_voc_fin {x : ℕ ⊕ ℕ} {α : Program} {φ : Formula} {X : Finset Formula} (X_in : X ∈ (unfoldBox α φ).toFinFin) {ψ : Formula} (ψ_in : ψ ∈ X) (x_in_voc_ψ : x ∈ ψ.voc) : x ∈ α.voc ∨ x ∈ φ.voc

Finset version of unfoldBox_voc.

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

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

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 (Bset γ ℓ ψ) ⋀ signature γ ℓ) : (⌈γ⌉ψ) ≡ dis (List.map (fun (ℓ : TP γ) => con (Bset γ ℓ ψ)) (allTP γ))

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

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

Induction claim for localBoxTruth.

theorem localBoxTruth (γ : Program) (ψ : Formula) : (⌈γ⌉ψ) ≡ dis (List.map (fun (ℓ : TP γ) => con (Bset γ ℓ ψ)) (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