Local Diamond Unfolding (Section 3.2 and 3.3)

Diamonds: H, Y and Φ_⋄

def H : Program → List (List Formula × List Program)

Equations

• One or more equations did not get rendered due to their size.
• H (·a) = [([], [·a])]
• H (?'τ) = [([τ], [])]
• H (α⋓β) = H α ∪ H β
• H (∗α) = [(∅, [])] ∪ (List.map (fun (x : List Formula × List Program) => match x with | (F, δ) => if δ = [] then [] else [(F, δ ++ [∗α])]) (H α)).flatten

def Hl : List Program → List (List Formula × List Program)

Like H, 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.
• Hl [] = [([], [])]
• Hl [α] = H α

@[simp]

theorem Hl_singleton {α : Program} : Hl [α] = H α

@[simp]

theorem Hl_atomic_cons {a : ℕ} {αs : List Program} : Hl (·a :: αs) = [([], ·a :: αs)]

theorem relateSeq_H_imp_relate {α : Program} {W✝ : Type} {M : KripkeModel W✝} {w v : W✝} {X : List Formula} {δ : List Program} : (X, δ) ∈ H α → (M, w)⊨Con X → relateSeq M δ w v → relate M α w v

theorem H_mem_test (α : Program) (φ : Formula) {Fs : List Formula} {δ : List Program} (in_H : (Fs, δ) ∈ H α) (φ_in_Fs : φ ∈ Fs) : ∃ (τ : Formula) (_ : τ ∈ testsOfProgram α), φ = τ

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

theorem H_mem_sequence (α : Program) {Fs : List Formula} {δ : List Program} (in_H : (Fs, δ) ∈ H α) : δ = [] ∨ ∃ (a : ℕ) (δ' : List Program), δ = ·a :: δ'

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

theorem keepFreshH {x : ℕ ⊕ ℕ} (α : Program) : x ∉ α.voc → ∀ (F : List Formula) (δ : List Program), (F, δ) ∈ H α → x ∉ F.fvoc ∧ x ∉ δ.pvoc

theorem H_goes_down_prog (α : Program) {Fs : List Formula} {δ : List Program} (in_H : (Fs, δ) ∈ H α) {γ : Program} (in_δ : γ ∈ δ) : if α.isAtomic then γ = α else if α.isStar then lengthOfProgram γ ≤ lengthOfProgram α else lengthOfProgram γ < lengthOfProgram α

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

Equations

• Yset (F, δ) x✝ = F ∪ [~⌈⌈δ⌉⌉x✝]

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

Φ_◇(α,ψ)

Equations

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

theorem unfoldDiamondContent (α : Program) (ψ : Formula) (X : List Formula) : X ∈ unfoldDiamond α ψ → ∀ φ ∈ X, φ = (~ψ) ∨ (∃ τ ∈ testsOfProgram α, φ = τ) ∨ ∃ (a : ℕ) (δ : List Program), φ = (~⌈·a⌉⌈⌈δ⌉⌉ψ)

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

theorem guardToStarDiamond {β : Program} {σ0 σ1 ρ ψ : Formula} (x : ℕ) (x_notin_beta : Sum.inl x ∉ β.voc) (beta_equiv : (~⌈β⌉~·x)≡·x⋀σ0⋁σ1) (repl_imp_rho : repl_in_F x ρ σ1⊨ρ) (notPsi_imp_rho : (~ψ)⊨ρ) : (~⌈∗β⌉ψ)⊨ρ

theorem localDiamondTruth (γ : Program) (ψ : Formula) : (~⌈γ⌉ψ)≡dis (List.map (fun (Fδ : List Formula × List Program) => Con (Yset Fδ ψ)) (H γ))

def 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

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

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

theorem existsDiamondH {W✝ : Type} {M : KripkeModel W✝} {γ : Program} {v w : W✝} (v_γ_w : relate M γ v w) : ∃ Fδ ∈ H γ, (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w

splitLast

def splitLast {α : Type u_1} : List α → Option (List α × α)

Helper function for YsetLoad' to get last list element.

Equations

• splitLast [] = none
• splitLast (x_1 :: xs) = some (match splitLast xs with | none => ([], x_1) | some (ys, y) => (x_1 :: ys, y))

@[simp]

theorem splitLast_nil {α : Type u_1} : splitLast [] = none

theorem splitLast_cons_eq_some {α : Type u_1} (x : α) (xs : List α) : splitLast (x :: xs) = some ((x :: xs).dropLast, (x :: xs).getLast ⋯)

@[simp]

theorem splitLast_append_singleton {α✝ : Type u_1} {xs : List α✝} {x : α✝} : splitLast (xs ++ [x]) = some (xs, x)

theorem splitLast_inj {α✝ : Type u_1} {αs βs : List α✝} (h : splitLast αs = splitLast βs) : αs = βs

theorem splitLast_undo_of_some {α✝ : Type u_1} {αs : List α✝} {βs_b : List α✝ × α✝} (h : splitLast αs = some βs_b) : βs_b.1 ++ [βs_b.2] = αs

theorem loadMulti_of_splitLast_cons {α : Program} {αs βs : List Program} {β : Program} {φ : Formula} (h : splitLast (α :: αs) = some (βs, β)) : loadMulti βs β φ = ⌊α⌋AnyFormula.loadBoxes αs (AnyFormula.normal φ)

Loaded Diamonds (Section 3.3)

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

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

Equations

• YsetLoad (F, δ) x✝ = (F, some (~'⌊⌊δ⌋⌋x✝))

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

Equations

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

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

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

Equations

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

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

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

Equations

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

def pairUnload : List Formula × Option NegLoadFormula → List Formula

Equations

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

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

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