Distance between states

This is used for the correctness of cluster interpolants in Section 7.

Walks

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

• 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 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

Equations

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

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

Equations

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

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

Equations

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

@[irreducible]

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

Equations

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

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

Equations

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

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

Equations

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

theorem 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 Reachable {W : Type} (M : KripkeModel W) (α : Program) (w v : W) : Prop

Equations

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

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

theorem 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 reachable_iff_star_relate {W : Type} {M : KripkeModel W} {α : Program} {w v : W} : Reachable M α w v ↔ relate M (∗α) w v

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

Distance

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

Equations

• distance M (·a) w v = if relate M (·a) w v then 1 else ⊤
• distance M (?'a) w v = if relate M (?'a) w v then 0 else ⊤
• distance M (α_2⋓β) w v = distance M α_2 w v ⊓ distance M β w v
• distance M (∗α_2) w v = fdist' M α_2 w v fun (x1 x2 : W) => (distance M α_2 x1 x2).toNat
• distance M (α_2;'β) w v = ⨅ (x : W), distance M α_2 w x + distance M β x v

theorem distance_self_star {W : Type} {M : KripkeModel W} {α : Program} {w : W} : distance M (∗α) w w = 0

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

Equations

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

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

7.47 (a)

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

theorem distance_list_nil_self {W : Type} {M : KripkeModel W} {w : W} : distance_list M w w [] = 0

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

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

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

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

theorem 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 WithTop.domain {ι : Sort u_1} {α : Type u_2} (f : ι → WithTop α) : Set α

Equations

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

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

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

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

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

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

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

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

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

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

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

theorem distance_comp_eq_distList {W : Type} {M : KripkeModel W} {β β' : Program} {w v : W} : distance M (β;'β') w v = distance_list M w v [β, β']

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

Distance of diamond unfoldings

Here we relate distance to H.

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

7.47 (b)

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

like 7.47 (a) but for lists

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

7.47 (c)

theorem distance_le_Hdistance {W : Type} {M : KripkeModel W} {α : Program} {X : List Formula} {δ : List Program} {w v : W} (in_H : (X, δ) ∈ H α) : (M, w)⊨Con X → distance M α w v ≤ distance_list M w v δ

7.47 (d)

theorem distList_le_of_Hsat {Xδ : List Formula × List Program} {W : Type} (M : KripkeModel W) (v w : W) (α : Program) (γ : List Program) (in_H : Xδ ∈ H α) (v_X : evaluate M v (Con Xδ.1)) : distance_list M v w (α :: γ) ≤ distance_list M v w (Xδ.2 ++ γ)

7.47 (e)

theorem rel_existsH_dist {W : Type} {M : KripkeModel W} {α : Program} {w v : W} (w_α_v : relate M α w v) : ∃ Xδ ∈ H α, evaluate M w (Con Xδ.1) ∧ distance_list M w v Xδ.2 = distance M α w v

7.47 (f)

theorem relateSeq_existsH_dist {W : Type} {M : KripkeModel W} {α : Program} {γ : List Program} {v w : W} (v_αγ_w : relateSeq M (α :: γ) v w) : ∃ Xδ ∈ H α, evaluate M v (Con Xδ.1) ∧ distance_list M v w (Xδ.2 ++ γ) = distance_list M v w (α :: γ)

7.47 (g)

theorem existsH_of_true_diamond {W : Type} {M : KripkeModel W} {v : W} (α : Program) (γ : List Program) (ψ : Formula) (v_ : evaluate M v (~⌈⌈α :: γ⌉⌉ψ)) : ∃ Xδ ∈ H α, evaluate M v (Con Xδ.1) ∧ evaluate M v (~⌈⌈Xδ.2⌉⌉⌈⌈γ⌉⌉ψ) ∧ ⨅ (w : { w : W // evaluate M w (~ψ) }), distance_list M v (↑w) (Xδ.2 ++ γ) = ⨅ (w : { w : W // evaluate M w (~ψ) }), distance_list M v (↑w) (α :: γ)

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

theorem distanceProps {γ : List Program} {X : List Formula} {Xδ : List Formula × List Program} {ψ : Formula} (W : Type) (M : KripkeModel W) (α : Program) {w v : W} (δ : List Program) : (distance M α w v ≠ ⊤ ↔ relate M α w v) ∧ distance_list M v w δ = distance M (Program.steps δ) v w ∧ ((∀ (u : W), distance M α v u ≤ distance_list M v u δ) → ∀ (u : W), distance_list M v u (α :: γ) ≤ distance_list M v u (δ ++ γ)) ∧ ((X, δ) ∈ H α → (M, w)⊨Con X → distance M α w v ≤ distance_list M w v δ) ∧ (Xδ ∈ H α → evaluate M v (Con Xδ.1) → distance_list M v w (α :: γ) ≤ distance_list M v w (Xδ.2 ++ γ)) ∧ (relate M α w v → ∃ Xδ ∈ H α, evaluate M w (Con Xδ.1) ∧ distance_list M w v Xδ.2 = distance M α w v) ∧ (relateSeq M (α :: γ) v w → ∃ Xδ ∈ H α, evaluate M v (Con Xδ.1) ∧ distance_list M v w (Xδ.2 ++ γ) = distance_list M v w (α :: γ)) ∧ (evaluate M v (~⌈⌈α :: γ⌉⌉ψ) → ∃ Xδ ∈ H α, evaluate M v (Con Xδ.1) ∧ evaluate M v (~⌈⌈Xδ.2⌉⌉⌈⌈γ⌉⌉ψ) ∧ ⨅ (w : { w : W // evaluate M w (~ψ) }), distance_list M v (↑w) (Xδ.2 ++ γ) = ⨅ (w : { w : W // evaluate M w (~ψ) }), distance_list M v (↑w) (α :: γ))

Summary definition of Lemma 7.47