Distance between states in a Kripke model

In the article these are used for the correctness of cluster interpolants in Section 7. Here we also use them to state and prove localLoadedDiamondList, a local version of the loadedDiamondPaths lemma that is part of the Soundness proof in Section 6.

Walks

inductive PDL.Walk {W : Type} : KripkeModel W → Program → W → W → Type

A finite program walk whose recorded edges change the world.

• nil {W : Type} {M : KripkeModel W} {w : W} (a : Program) : Walk M a w w
• cons {W : Type} {M : KripkeModel W} {α : Program} {w x v : W} (h : relate M α w x) (p : Walk M α x v) (wx : w ≠ x) : Walk M α w v

noncomputable def PDL.Walk.cons' {W✝ : Type} {M : KripkeModel W✝} {α : Program} {w x v : W✝} (h : relate M α w x) (p : Walk M α x v) : Walk M α w v

Prepend a program step, omitting it when its endpoints coincide.

Equations

• PDL.Walk.cons' h p = if c : w = x then match x, c, h, p with | .(w), ⋯, h, p => p else PDL.Walk.cons h p c

def PDL.Walk.flength' {W : Type} {M : KripkeModel W} {α : Program} {w v : W} : Walk M α w v → (W → W → ℕ) → ℕ

Sum natural-valued edge weights along a walk.

Equations

• (PDL.Walk.nil α).flength' x✝ = 0
• (PDL.Walk.cons h p wx).flength' x✝ = x✝ w x_2 + p.flength' x✝

def PDL.Walk.flength {W : Type} {M : KripkeModel W} {α : Program} {w v : W} : Walk M α w v → (W → W → ℕ∞) → ℕ∞

Sum possibly infinite edge weights along a walk.

Equations

• (PDL.Walk.nil α).flength x✝ = 0
• (PDL.Walk.cons h p wx).flength x✝ = x✝ w x_2 + p.flength x✝

def PDL.Walk.append {W : Type} {α : Program} {M : KripkeModel W} {w v x : W} : Walk M α w x → Walk M α x v → Walk M α w v

Concatenate two program walks with a shared endpoint.

Equations

• (PDL.Walk.nil α).append x✝ = x✝
• (PDL.Walk.cons h p wx).append x✝ = PDL.Walk.cons h (p.append x✝) wx

noncomputable def PDL.fdist' {W : Type} (M : KripkeModel W) (α : Program) (w v : W) (f : W → W → ℕ) : ℕ∞

The infimum of natural-weighted lengths of program walks.

Equations

• PDL.fdist' M α w v f = ⨅ (p : PDL.Walk M α w v), ↑(p.flength' f)

noncomputable def PDL.fdist {W : Type} (M : KripkeModel W) (α : Program) (w v : W) (f : W → W → ℕ∞) : ℕ∞

The infimum of possibly infinite weighted lengths of program walks.

Equations

• PDL.fdist M α w v f = ⨅ (p : PDL.Walk M α w v), p.flength f

theorem PDL.fdist_cast {W : Type} {M : KripkeModel W} {α : Program} {f : W → W → ℕ∞} {w v : W} (h : ∀ {x y : W}, relate M α x y → f x y ≠ ⊤) : fdist M α w v f = fdist' M α w v fun (x1 x2 : W) => (f x1 x2).toNat

def PDL.Reachable {W : Type} (M : KripkeModel W) (α : Program) (w v : W) : Prop

Existence of a finite program walk between two worlds.

Equations

• PDL.Reachable M α w v = Nonempty (PDL.Walk M α w v)

theorem PDL.Reachable.refl {W : Type} {M : KripkeModel W} {α : Program} (w : W) : Reachable M α w w

theorem PDL.Reachable.trans {W : Type} {M : KripkeModel W} {α : Program} {w v u : W} (hwv : Reachable M α w v) (hvu : Reachable M α v u) : Reachable M α w u

theorem PDL.reachable_iff_star_relate {W : Type} {M : KripkeModel W} {α : Program} {w v : W} : Reachable M α w v ↔ relate M α.star w v

theorem PDL.star_relate_of_Chain {W : Type} {M : KripkeModel W} {α : Program} {w : W} {l : List W} {v : W} : List.IsChain (relate M α) (w :: l ++ [v]) → relate M α.star w v

Unused

Distance

noncomputable def PDL.distance {W : Type} (M : KripkeModel W) (α : Program) (w v : W) : ℕ∞

The recursively weighted distance of a program between two worlds.

Equations

• PDL.distance M (PDL.Program.atom_prog a) w v = if PDL.relate M (PDL.Program.atom_prog a) w v then 1 else ⊤
• PDL.distance M (PDL.Program.test a) w v = if PDL.relate M (PDL.Program.test a) w v then 0 else ⊤
• PDL.distance M (α_2.union β) w v = min (PDL.distance M α_2 w v) (PDL.distance M β w v)
• PDL.distance M α_2.star w v = PDL.fdist' M α_2 w v fun (x1 x2 : W) => (PDL.distance M α_2 x1 x2).toNat
• PDL.distance M (α_2.sequence β) w v = ⨅ (x : W), PDL.distance M α_2 w x + PDL.distance M β x v

theorem PDL.distance_self_star {W : Type} {M : KripkeModel W} {α : Program} {w : W} : distance M α.star w w = 0

noncomputable def PDL.distanceList {W : Type} (M : KripkeModel W) (w v : W) (δ : List Program) : ℕ∞

The minimum total distance for a sequence of programs, allowing infinity.

Equations

• PDL.distanceList M w v [] = if w = v then 0 else ⊤
• PDL.distanceList M w v (α :: δ) = ⨅ (x : W), PDL.distance M α w x + PDL.distanceList M x v δ

theorem PDL.dist_iff_rel {W : Type} {M : KripkeModel W} {α : Program} {w v : W} : distance M α w v ≠ ⊤ ↔ relate M α w v

7.47 (a)

theorem PDL.distance_cast {W : Type} {M : KripkeModel W} {α : Program} {w v : W} : distance M α.star w v = fdist M α w v fun (x1 x2 : W) => distance M α x1 x2

theorem PDL.distance_list_nil_self {W : Type} {M : KripkeModel W} {w : W} : distanceList M w w [] = 0

theorem PDL.eq_of_distance_nil {W : Type} {M : KripkeModel W} {w v : W} (h : distanceList M w v [] ≠ ⊤) : w = v

theorem PDL.distance_list_singleton {W : Type} {M : KripkeModel W} {w v : W} {α : Program} : distanceList M w v [α] = distance M α w v

theorem PDL.ENat.min_neq_top_iff {M N : ℕ∞} : min M N ≠ ⊤ ↔ M ≠ ⊤ ∨ N ≠ ⊤

theorem PDL.List.exists_mem_singleton {α : Type u_1} {a : α} {p : α → Prop} : (∃ x ∈ [a], p x) ↔ p a

theorem PDL.ite_eq_right_of_ne_left {c : Prop} {α✝ : Sort u_1} {t e : α✝} [Decidable c] (h : (if c then t else e) ≠ t) : (if c then t else e) = e

def PDL.WithTop.domain {ι : Sort u_1} {α : Type u_2} (f : ι → WithTop α) : Set α

The elements of α attained by a function into WithTop α.

Equations

• PDL.WithTop.domain f a = ∃ (i : ι), f i = ↑a

theorem PDL.domain_nonempty_of_iInf_ne_top {ι : Sort u_1} {f : ι → ℕ∞} (h : iInf f ≠ ⊤) : (WithTop.domain f).Nonempty

theorem PDL.ENat.iInf_eq_find_of_ne_top {ι : Sort u_1} {f : ι → ℕ∞} (h : iInf f ≠ ⊤) : iInf f = ↑(Nat.find ⋯)

theorem PDL.iInf_exists_eq_of_ne_top {ι : Sort u_1} {f : ι → ℕ∞} (h : iInf f ≠ ⊤) : ∃ (i : ι), iInf f = f i

theorem PDL.iInf_exists_eq {ι : Sort u_1} [NE : Nonempty ι] (f : ι → ℕ∞) : ∃ (i : ι), iInf f = f i

theorem PDL.iInf_of_min {ι : Sort u_1} {f : ι → ℕ∞} {i : ι} (h : ∀ (j : ι), f i ≤ f j) : iInf f = f i

theorem PDL.add_iInf {ι : Sort u_1} {f : ι → ℕ∞} {a : ℕ∞} : a + ⨅ (i : ι), f i = ⨅ (i : ι), a + f i

theorem PDL.iInf_add {ι : Sort u_1} {f : ι → ℕ∞} {a : ℕ∞} : (⨅ (i : ι), f i) + a = ⨅ (i : ι), f i + a

theorem PDL.distance_list_append {W : Type} {M : KripkeModel W} {w v : W} (δ₁ δ₂ : List Program) : distanceList M w v (δ₁ ++ δ₂) = ⨅ (x : W), distanceList M w x δ₁ + distanceList M x v δ₂

theorem PDL.distance_list_cons {W : Type} {M : KripkeModel W} {w v : W} {α : Program} {δ : List Program} : distanceList M w v (α :: δ) = ⨅ (x : W), distance M α w x + distanceList M x v δ

theorem PDL.distance_list_concat {W : Type} {M : KripkeModel W} {w v : W} {δ : List Program} {α : Program} : distanceList M w v (δ ++ [α]) = ⨅ (x : W), distanceList M w x δ + distance M α x v

theorem PDL.distance_comp_eq_distList {W : Type} {M : KripkeModel W} {β β' : Program} {w v : W} : distance M (β.sequence β') w v = distanceList M w v [β, β']

theorem PDL.distance_star_le {W : Type} {M : KripkeModel W} {α : Program} {w v : W} (x : W) : distance M α.star w v ≤ distance M α w x + distance M α.star x v

Distance of diamond unfoldings

Here we relate distance to H.

theorem PDL.distance_list_eq_distance_steps {W : Type} (M : KripkeModel W) (v w : W) (δ : List Program) : distanceList M v w δ = distance M (Program.steps δ) v w

7.47 (b)

theorem PDL.distance_list_iff_relate_Seq {W : Type} {M : KripkeModel W} {w v : W} {δ : List Program} : distanceList M w v δ ≠ ⊤ ↔ relateSeq M δ w v

like 7.47 (a) but for lists

theorem PDL.dist_le_of_distList_le {W : Type} {M : KripkeModel W} {α : Program} {v : W} {δ γ : List Program} (h : ∀ (u : W), distance M α v u ≤ distanceList M v u δ) (u : W) : distanceList M v u (α :: γ) ≤ distanceList M v u (δ ++ γ)

7.47 (c)

theorem PDL.distance_le_Hdistance {W : Type} {M : KripkeModel W} {α : Program} {X : List Formula} {δ : List Program} {w v : W} (in_D : (X, δ) ∈ Dset α) : vDash.SemImplies (M, w) (con X) → distance M α w v ≤ distanceList M w v δ

7.47 (d)

theorem PDL.distList_le_of_Hsat {Xδ : List Formula × List Program} {W : Type} (M : KripkeModel W) (v w : W) (α : Program) (γ : List Program) (in_D : Xδ ∈ Dset α) (v_X : evaluate M v (con Xδ.1)) : distanceList M v w (α :: γ) ≤ distanceList M v w (Xδ.2 ++ γ)

7.47 (e)

theorem PDL.rel_existsD_dist {W : Type} {M : KripkeModel W} {α : Program} {w v : W} (w_α_v : relate M α w v) : ∃ Xδ ∈ Dset α, evaluate M w (con Xδ.1) ∧ distanceList M w v Xδ.2 = distance M α w v

7.47 (f)

theorem PDL.relateSeq_existsD_dist {W : Type} {M : KripkeModel W} {α : Program} {γ : List Program} {v w : W} (v_αγ_w : relateSeq M (α :: γ) v w) : ∃ Xδ ∈ Dset α, evaluate M v (con Xδ.1) ∧ distanceList M v w (Xδ.2 ++ γ) = distanceList M v w (α :: γ)

7.47 (g)

theorem PDL.existsD_of_true_diamond {W : Type} {M : KripkeModel W} {v : W} (α : Program) (γ : List Program) (ψ : Formula) (v_ : evaluate M v (Formula.boxes (α :: γ) ψ).neg) : ∃ Xδ ∈ Dset α, evaluate M v (con Xδ.1) ∧ evaluate M v (Formula.boxes Xδ.2 (Formula.boxes γ ψ)).neg ∧ ⨅ (w : { w : W // evaluate M w ψ.neg }), distanceList M v (↑w) (Xδ.2 ++ γ) = ⨅ (w : { w : W // evaluate M w ψ.neg }), distanceList M v (↑w) (α :: γ)

7.47 (h) In the article this uses loaded formulas, we just use normal boxes.

theorem PDL.distanceProps {γ : List Program} {X : List Formula} {ψ : Formula} {Xδ : List Formula × List Program} (W : Type) (M : KripkeModel W) (α : Program) {w v : W} (δ : List Program) : (distance M α w v ≠ ⊤ ↔ relate M α w v) ∧ distanceList M v w δ = distance M (Program.steps δ) v w ∧ ((∀ (u : W), distance M α v u ≤ distanceList M v u δ) → ∀ (u : W), distanceList M v u (α :: γ) ≤ distanceList M v u (δ ++ γ)) ∧ ((X, δ) ∈ Dset α → vDash.SemImplies (M, w) (con X) → distance M α w v ≤ distanceList M w v δ) ∧ (Xδ ∈ Dset α → evaluate M v (con Xδ.1) → distanceList M v w (α :: γ) ≤ distanceList M v w (Xδ.2 ++ γ)) ∧ (relate M α w v → ∃ Xδ ∈ Dset α, evaluate M w (con Xδ.1) ∧ distanceList M w v Xδ.2 = distance M α w v) ∧ (relateSeq M (α :: γ) v w → ∃ Xδ ∈ Dset α, evaluate M v (con Xδ.1) ∧ distanceList M v w (Xδ.2 ++ γ) = distanceList M v w (α :: γ)) ∧ (evaluate M v (Formula.boxes (α :: γ) ψ).neg → ∃ Xδ ∈ Dset α, evaluate M v (con Xδ.1) ∧ evaluate M v (Formula.boxes Xδ.2 (Formula.boxes γ ψ)).neg ∧ ⨅ (w : { w : W // evaluate M w ψ.neg }), distanceList M v (↑w) (Xδ.2 ++ γ) = ⨅ (w : { w : W // evaluate M w ψ.neg }), distanceList M v (↑w) (α :: γ))

Summary definition of Lemma 7.47

theorem PDL.exists_same_distance_of_relateSeq_cons {W : Type} {M : KripkeModel W} {α : Program} {δ : List Program} {w v : W} (w_αδ_v : relateSeq M (α :: δ) w v) : ∃ (x : W), relate M α w x ∧ relateSeq M δ x v ∧ distanceList M w v (α :: δ) = distance M α w x + distanceList M x v δ

theorem PDL.exists_same_distance_list_relateSeq_concat {W : Type} {M : KripkeModel W} {δ : List Program} {α : Program} {w v : W} (w_δα_v : relateSeq M (δ ++ [α]) w v) : ∃ (x : W), relateSeq M δ w x ∧ relate M α x v ∧ distanceList M w v (δ ++ [α]) = distanceList M w x δ + distance M α x v