structure DecidableKripkeModel (W : Type) : Type

A Kripke model where the relation and valuation are decidable. Moreover, to get computable composition and transitive closure we want the type of worlds to be finite and enumerable. In fact, to avoid choice, we want a list of all worlds. -- TODO: weaken List to Fintype, should still be possible to define distance?

• M : KripkeModel W
• allW : List W
• h (w : W) : w ∈ self.allW
• deceq : DecidableEq W
• decrel (n : ℕ) : DecidableRel (self.M.Rel n)
• decval (w : W) (n : ℕ) : Decidable (self.M.val w n)

theorem Finset.sdiff_ssubset_sdiff {α : Type u_1} [DecidableEq α] {A B C : Finset α} (h1 : B ⊆ A) (h3 : C ⊂ B) : A \ B ⊂ A \ C

theorem reachableFrom_terminationHelper {α : Type u_1} (r : α → α → Prop) [DecidableRel r] [DecidableEq α] [α_fin : Fintype α] (here : Finset α) (h : (Finset.filter (fun (y : α) => ∃ x ∈ here, y ∉ here ∧ r x y) Fintype.elems).Nonempty) : (Fintype.elems \ (here ∪ Finset.filter (fun (y : α) => ∃ x ∈ here, y ∉ here ∧ r x y) Fintype.elems)).card < (Fintype.elems \ here).card

@[irreducible]

def reachableFrom {α : Type u_1} (r : α → α → Prop) [DecidableRel r] [DecidableEq α] [α_fin : Fintype α] (here : Finset α) : Finset α

Computable definition to close a finset under the reflexive transitive closure of a relation.

Equations

• One or more equations did not get rendered due to their size.

@[irreducible]

theorem reachableFrom.subset {α : Type u_1} (r : α → α → Prop) [DecidableRel r] [DecidableEq α] [α_fin : Fintype α] (here : Finset α) : here ⊆ reachableFrom r here

@[irreducible]

theorem reachableFrom.mem_iff {α : Type u_1} (r : α → α → Prop) [DecidableRel r] [DecidableEq α] [α_fin : Fintype α] (here : Finset α) (y : α) : y ∈ reachableFrom r here ↔ ∃ x ∈ here, Relation.ReflTransGen r x y

instance decidableReflTransGen_of_decidableRel_on_finite {α : Type u_1} [DecidableEq α] [Fintype α] (r : α → α → Prop) (h : DecidableRel r) : DecidableRel (Relation.ReflTransGen r)

Used for case star in relate.instDecidable below.

Equations

• decidableReflTransGen_of_decidableRel_on_finite r h x y = if h_1 : y ∈ reachableFrom r {x} then isTrue ⋯ else isFalse ⋯

def localMeasureOfProg (n : ℕ) : Program → ℕ

In models of size n this is a strict upper bound for the distance. Used only for the termination proofs below.

Equations

• localMeasureOfProg n (·a) = 1
• localMeasureOfProg n (α;'β) = 1 + localMeasureOfProg n α + localMeasureOfProg n β
• localMeasureOfProg n (α⋓β) = 1 + localMeasureOfProg n α + localMeasureOfProg n β
• localMeasureOfProg n (∗α) = 1 + (1 + n) * localMeasureOfProg n α
• localMeasureOfProg n (?'a) = 1

theorem Program.nonZeroSize {n : ℕ} {α : Program} : localMeasureOfProg n α > 0

theorem distance_helper (x y k : ℕ) (h : k ≤ y) (h2 : x ≠ 0) : x + y + k < 1 + x + y * x + y

@[irreducible]

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

Equations

• One or more equations did not get rendered due to their size.
• distance Mod v w (·c) = if decide (Mod.M.Rel c v w) = true then 1 else ⊤
• distance Mod v w (?'τ) = if v = w ∧ evaluate Mod.M v τ then 0 else ⊤
• distance Mod v w (α⋓β) = distance Mod v w α ⊓ distance Mod v w β
• distance Mod v w (α;'β) = (List.map (fun (x : W) => distance Mod v x α + distance Mod x w β) Mod.allW).reduceOption.min?

@[irreducible]

noncomputable def distance.mdist {W : Type} (Mod : DecidableKripkeModel W) (v : W) (α : Program) (k : ℕ) : ℕ∞

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• distance_list Mod v w [] = if v = w then 0 else ⊤
• distance_list Mod v w (α :: δ) = (List.map (fun (x : W) => distance Mod v x α + distance_list Mod x w δ) Mod.allW).reduceOption.min?

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

theorem ENat.add_neq_top_iff {M N : ℕ∞} : M + N ≠ ⊤ ↔ M ≠ ⊤ ∧ N ≠ ⊤

theorem distance_iff_relate {W : Type} (Mod : DecidableKripkeModel W) (α : Program) (v w : W) : distance Mod v w α ≠ ⊤ ↔ relate Mod.M α v w

theorem relate_existsH_distance {W : Type} {v w : W} (Mod : DecidableKripkeModel W) (α : Program) (v_α_w : relate Mod.M α v w) : ∃ Fδ ∈ H α, evaluate Mod.M v (Con Fδ.1) ∧ distance_list Mod v w Fδ.2 = distance Mod v w α