Definitions, lemmas and theorems listed in order

This file contains links to all definitions, lemmas and theorems from the paper.

They are listed roughly in the order they appear in the paper. This file should serve as a jumping off point to navigate and explore the formalization, and not as a reference to how things are defined. We invite the reader to click on the names in each definition to jump to their original definition. In Visual Studio Code one can Ctrl/CMD+Click on symbols to jump to their definition.

See Links for a glossary of list things listed in the paper, including Mathlib definitions.

Section 4 – Expected Total Costs in Markov Decision Processes

def Paper.Section4.Definition1 : Link MarkovChain

Equations

• Paper.Section4.Definition1 = True.intro

def Paper.Section4.Definition2 {S : Type u_5} {MC : MarkovChain S} : Link MarkovChain.Path.Cyl

Equations

• ⋯ = True.intro

theorem Paper.Section4.Theorem3 {S : Type u_5} [DecidableEq S] {MC : MarkovChain S} : LinkThm (∀ (π : MC.Path), MarkovChain.Pr π.Cyl = ∏ i : Fin (π.length - 1), (MC.P π.states[i]) π.states[↑i + 1])

def Paper.Section4.Definition4 : Link MDP

Equations

• Paper.Section4.Definition4 = True.intro

def Paper.Section4.Definition5 {S : Type u_5} {A : Type u_6} {M : MDP S A} : Link M.inducedMC'

Equations

• ⋯ = True.intro

theorem Paper.Section4.Theorem6 {S : Type u_5} {A : Type u_6} [DecidableEq S] {M : MDP S A} [M.FiniteBranching] {𝒮 : 𝔖[M]} : LinkThm (∀ (π : M.Path) (h' : MDP.Path.Prob 𝒮 π ≠ 0), MarkovChain.Pr (π.toMC' h' ⋯).Cyl = MDP.Path.Prob 𝒮 π)

def Paper.Section4.Definition7 {S : Type u_5} {A : Type u_6} {M : MDP S A} : Link M.ECost

Equations

• ⋯ = True.intro

def Paper.Section4.Definition8 {S : Type u_5} {A : Type u_6} {M : MDP S A} : Link MDP.OEC

Equations

• ⋯ = True.intro

theorem Paper.Section4.Lemma9 {S : Type u_5} [DecidableEq S] : LinkLem (CompleteLattice (S → ENNReal))

def Paper.Section4.Definition10 {S : Type u_5} {A : Type u_6} {M : MDP S A} : Link MDP.Φ

Equations

• ⋯ = True.intro

theorem Paper.Section4.Lemma11 {S : Type u_5} {A : Type u_6} [DecidableEq S] {M : MDP S A} [M.FiniteBranching] {c : M.Costs} : LinkLem (Monotone ⇑(MDP.Φ Optimization.Angelic c) ×' OmegaCompletePartialOrder.ωScottContinuous ⇑(MDP.Φ Optimization.Angelic c))

theorem Paper.Section4.Theorem12 {S : Type u_5} {A : Type u_6} [DecidableEq S] {M : MDP S A} [M.FiniteBranching] {c : M.Costs} : LinkThm (⨆ (n : ℕ), ⨆ (𝒮 : 𝔖[M]), MDP.EC c 𝒮 n = OrderHom.lfp (MDP.Φ Optimization.Angelic c))

theorem Paper.Section4.Lemma13 {S : Type u_5} {A : Type u_6} [DecidableEq S] {M : MDP S A} [M.FiniteBranching] {c : M.Costs} : LinkLem (Monotone ⇑(MDP.Φ Optimization.Demonic c) ×' OmegaCompletePartialOrder.ωScottContinuous ⇑(MDP.Φ Optimization.Demonic c))

theorem Paper.Section4.Lemma14 {S : Type u_5} {A : Type u_6} [DecidableEq S] {M : MDP S A} [M.FiniteBranching] {c : M.Costs} : LinkLem (⨆ (n : ℕ), ⨅ (𝒮 : 𝔖[M]), MDP.EC c 𝒮 n = OrderHom.lfp (MDP.Φ Optimization.Demonic c))

def Paper.Section4.Definition15 {S : Type u_5} {A : Type u_6} {M : MDP S A} : Link 𝔏[M]

Equations

• ⋯ = True.intro

theorem Paper.Section4.Lemma16 {S : Type u_5} {A : Type u_6} [DecidableEq S] {M : MDP S A} [M.FiniteBranching] {c : M.Costs} : LinkLem (∀ (ℒ : 𝔏[M]) [M.FiniteBranching], ⨆ (n : ℕ), MDP.EC c (↑ℒ) n = MDP.lfp_Φℒ ℒ c)

def Paper.Section4.Definition17 {S : Type u_5} {A : Type u_6} {M : MDP S A} [M.FiniteBranching] : Link MDP.optℒ

Equations

• ⋯ = True.intro

theorem Paper.Section4.Lemma18 {S : Type u_5} {A : Type u_6} [DecidableEq S] {M : MDP S A} [M.FiniteBranching] {c : M.Costs} : LinkLem (MDP.lfp_Φℒ (MDP.optℒ c) c = OrderHom.lfp (MDP.Φ Optimization.Demonic c))

theorem Paper.Section4.Theorem19 {S : Type u_5} {A : Type u_6} [DecidableEq S] {M : MDP S A} [M.FiniteBranching] {c : M.Costs} : LinkThm (⨅ (𝒮 : 𝔖[M]), ⨆ (n : ℕ), MDP.EC c 𝒮 n = OrderHom.lfp (MDP.Φ Optimization.Demonic c))

Section 5 – pGCL: probabilistic Guarded Command Language

def Paper.Section5.Definition20 {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} : Link (Conf (pGCL Γ) (pGCL.State Γ) pGCL.Termination)

Equations

• ⋯ = True.intro

def Paper.Section5.Definition21 {𝒱 : Type u_1} [DecidableEq 𝒱] {Γ : 𝒱 → Type u_2} : Link pGCL.SmallStep

Equations

• ⋯ = True.intro

def Paper.Section5.Definition22 {𝒱 : Type u_1} [DecidableEq 𝒱] {Γ : 𝒱 → Type u_2} : Link pGCL.𝒪

Equations

• ⋯ = True.intro

def Paper.Section5.Definition23 {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} : Link ((pGCL.cost_p, pGCL.cost_t), pGCL.cost_p', pGCL.cost_t')

In Lean the cost functions are split for programs and terminations where ct = cost_p, cost_t and cp = cost_p', cost_t'.

Equations

• ⋯ = True.intro

def Paper.Section5.Definition24 {𝒱 : Type u_1} [DecidableEq 𝒱] {Γ : 𝒱 → Type u_2} {f : (pGCL.State Γ → ENNReal) →o pGCL.Termination × pGCL.State Γ → ENNReal} {g : pGCL Γ × pGCL.State Γ → ENNReal} : Link SmallStepSemantics.op

Equations

• ⋯ = True.intro

theorem Paper.Section5.Lemma25 {𝒱 : Type u_1} [DecidableEq 𝒱] {Γ : 𝒱 → Type u_2} {O : Optimization} {f : (pGCL.State Γ → ENNReal) →o pGCL.Termination × pGCL.State Γ → ENNReal} {g : pGCL Γ × pGCL.State Γ → ENNReal} [O.ΦContinuous SmallStepSemantics.mdp] {C C' : pGCL Γ} : LinkLem (∀ (seq : pGCL Γ → pGCL Γ → pGCL Γ) (after : pGCL Γ → (pGCL Γ ⊕ pGCL.Termination) × pGCL.State Γ → (pGCL Γ ⊕ pGCL.Termination) × pGCL.State Γ) (t_const : pGCL.State Γ → ENNReal), (∀ (C C' : pGCL Γ) (σ : pGCL.State Γ), SmallStepSemantics.cost_p pGCL.Termination pGCL.Act (seq C C', σ) = SmallStepSemantics.cost_p pGCL.Termination pGCL.Act (C, σ)) → (∀ (C C' : pGCL Γ) (σ : pGCL.State Γ), SmallStepSemantics.act (Conf.prog (seq C C') σ) = SmallStepSemantics.act (Conf.prog C σ)) → (∀ {C C' : pGCL Γ} {σ : pGCL.State Γ} {p : ENNReal} {α : pGCL.Act} {s : (pGCL Γ ⊕ pGCL.Termination) × pGCL.State Γ}, (p, s) ∈ SmallStepSemantics.psucc C σ α → (p, after C' s) ∈ SmallStepSemantics.psucc (seq C C') σ α) → (∀ {C C' : pGCL Γ} {σ : pGCL.State Γ}, after C' (Sum.inl C, σ) = (Sum.inl (seq C C'), σ)) → (∀ {t : pGCL.Termination} {C : pGCL Γ} {C' : (pGCL Γ ⊕ pGCL.Termination) × pGCL.State Γ} {σ : pGCL.State Γ}, after C (Sum.inr t, σ) = C' → C' = (Sum.inl C, σ) ∨ C' = (Sum.inr t, σ) ∧ ∀ (X : pGCL.State Γ → ENNReal), (SmallStepSemantics.cost_t (pGCL Γ) pGCL.Act) X (t, σ) = t_const σ) → (∀ {X : pGCL.State Γ → ENNReal} {t : pGCL.Termination} {σ : pGCL.State Γ} {C' : pGCL Γ}, after C' (Sum.inr t, σ) = (Sum.inl C', σ) → (SmallStepSemantics.cost_t (pGCL Γ) pGCL.Act) ((SmallStepSemantics.op O C') X) (t, σ) ≤ (SmallStepSemantics.op O C') X σ) → (∀ (x : pGCL Γ), Function.Injective (after x)) → ⇑(SmallStepSemantics.op O C) ∘ ⇑(SmallStepSemantics.op O C') ≤ ⇑(SmallStepSemantics.op O (seq C C')))

def Paper.Section5.Definition26 {𝒱 : Type u_1} [DecidableEq 𝒱] {Γ : 𝒱 → Type u_2} {f : (pGCL.State Γ → ENNReal) →o pGCL.Termination × pGCL.State Γ → ENNReal} {g : pGCL Γ × pGCL.State Γ → ENNReal} : Link SmallStepSemantics.ξ

Equations

• ⋯ = True.intro

theorem Paper.Section5.Lemma27 {𝒱 : Type u_1} [DecidableEq 𝒱] {Γ : 𝒱 → Type u_2} {O : Optimization} {f : (pGCL.State Γ → ENNReal) →o pGCL.Termination × pGCL.State Γ → ENNReal} {g : pGCL Γ × pGCL.State Γ → ENNReal} [O.ΦContinuous SmallStepSemantics.mdp] : LinkLem (OrderHom.lfp (SmallStepSemantics.ξ O) = SmallStepSemantics.op O)

theorem Paper.Section5.Lemma28 {𝒱 : Type u_1} [DecidableEq 𝒱] {Γ : 𝒱 → Type u_2} {O : Optimization} {f : (pGCL.State Γ → ENNReal) →o pGCL.Termination × pGCL.State Γ → ENNReal} {g : pGCL Γ × pGCL.State Γ → ENNReal} [O.ΦContinuous SmallStepSemantics.mdp] {et : pGCL Γ → (pGCL.State Γ → ENNReal) →o pGCL.State Γ → ENNReal} [(pGCL.𝕊 f g).ET O et] : LinkLem (et = SmallStepSemantics.op O)

theorem Paper.Section5.Lemma29 {𝒱 : Type u_1} [DecidableEq 𝒱] {Γ : 𝒱 → Type u_2} {O : Optimization} {C₁ C₂ : pGCL Γ} : LinkLem ((SmallStepSemantics.ξ O) (pGCL.wp O) C₁ = wp[O]⟦@C₁⟧ → (SmallStepSemantics.ξ O) (pGCL.wp O) (pgcl {@C₁ ; @C₂}) = wp[O]⟦@C₁⟧.comp wp[O]⟦@C₂⟧)

theorem Paper.Section5.Theorem30 {𝒱 : Type u_1} [DecidableEq 𝒱] {Γ : 𝒱 → Type u_2} {O : Optimization} {C : pGCL Γ} : LinkThm (wp[O]⟦@C⟧ = SmallStepSemantics.op O C)

def Paper.Section5.Definition31 {𝒱 : Type u_1} [DecidableEq 𝒱] {Γ : 𝒱 → Type u_2} : Link pGCL.wfp

Equations

• ⋯ = True.intro

theorem Paper.Section5.Lemma32 {𝒱 : Type u_1} [DecidableEq 𝒱] {Γ : 𝒱 → Type u_2} {O : Optimization} {C : pGCL Γ} : LinkLem (wfp[O]⟦@C⟧ = SmallStepSemantics.op O C)

theorem Paper.Section5.Theorem33 {𝒱 : Type u_1} [DecidableEq 𝒱] {Γ : 𝒱 → Type u_2} {O : Optimization} {C : pGCL Γ} : LinkThm (∀ (X : pGCL.ProbExp Γ), wlp'[O]⟦@C⟧ X = 1 - wfp'[O.dual]⟦@C⟧ (1 - X))

theorem Paper.Section5.Lemma34 {α : Type u_3} [CompleteLattice α] {Δ : α →o α} {f' : α} : LinkLem ((∀ (k : ℕ), Δ ((fun (x : α) => Δ x ⊓ f')^[k] f') ≤ f' → OrderHom.lfp Δ ≤ f') ×' ∀ (k : ℕ), f' ≤ Δ ((fun (x : α) => Δ x ⊔ f')^[k] f') → f' ≤ OrderHom.gfp Δ)

theorem Paper.Section5.Theorem35 {𝒱 : Type u_1} [DecidableEq 𝒱] {Γ : 𝒱 → Type u_2} {O : Optimization} {b : pGCL.BExpr Γ} {C : pGCL Γ} {φ I : pGCL.State Γ → ENNReal} : LinkThm (∀ (k : ℕ), pGCL.ParkKInvariant wp[O]⟦@C⟧ b φ k I → wp[O]⟦while @b { @C }⟧ φ ≤ I)

theorem Paper.Section5.Theorem36 {𝒱 : Type u_1} [DecidableEq 𝒱] {Γ : 𝒱 → Type u_2} {O : Optimization} {b : pGCL.BExpr Γ} {C : pGCL Γ} {φ I : pGCL.ProbExp Γ} : LinkThm (∀ (k : ℕ), pGCL.ParkKCoinvariant wlp'[O]⟦@C⟧ b φ k I → I ≤ wlp'[O]⟦while @b { @C }⟧ φ)

def Paper.Section5.Definition37 {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} : Link pGCL.State.EQ

Equations

• ⋯ = True.intro

theorem Paper.Section5.Theorem38 {𝒱 : Type u_1} [DecidableEq 𝒱] {Γ : 𝒱 → Type u_2} {O : Optimization} {b : pGCL.BExpr Γ} {C : pGCL Γ} {φ I : pGCL.State Γ → ENNReal} {σ₀ : pGCL.State Γ} : LinkThm (pGCL.IdleInvariant wp[O]⟦@C⟧ b φ I (~ C.mods) σ₀ → wp[O]⟦while @b { @C }⟧ φ σ₀ ≤ I σ₀)

theorem Paper.Section5.Theorem39 {𝒱 : Type u_1} [DecidableEq 𝒱] {Γ : 𝒱 → Type u_2} {O : Optimization} {b : pGCL.BExpr Γ} {C : pGCL Γ} {φ I : pGCL.State Γ → ENNReal} {σ₀ : pGCL.State Γ} : LinkThm (pGCL.IdleCoinvariant wlp[O]⟦@C⟧ b φ I (~ C.mods) σ₀ → I ≤ 1 → φ ≤ 1 → I σ₀ ≤ wlp[O]⟦while @b { @C }⟧ φ σ₀)

Section 6 – Sound Encodings into an Intermediate Verification Language

def Paper.Section6.Definition40 : Link HeyVL.Verifies

Equations

• Paper.Section6.Definition40 = True.intro

theorem Paper.Section6.Theorem41 {O : Optimization} {φ : HeyLo HeyLo.Ty.ENNReal} {C : spGCL} : LinkThm (wp[O]⟦@C.pGCL⟧ ⟦@φ⟧' ≤ ⟦@(C.vp O Encoding.wp φ)⟧')

theorem Paper.Section6.Theorem42 {O : Optimization} {φ : HeyLo HeyLo.Ty.ENNReal} {C : spGCL} : LinkThm (⟦@φ⟧' ≤ 1 → (∀ I ∈ C.invs, ⟦@I⟧' ≤ 1) → ⟦@(C.vp O Encoding.wlp φ)⟧' ≤ wlp[O]⟦@C.pGCL⟧ ⟦@φ⟧')

theorem Paper.Section6.Theorem43 {E✝ : Encoding} {C : Conditions E✝} : LinkThm (⟦@C.post⟧' ≤ 1 → (∀ I ∈ C.original.invs, ⟦@I⟧' ≤ 1) → heyvl {assume(@C.pre) ; @(C.original.enc C.O Encoding.wlp (C.original.fv ∪ C.post.fv)).2 ; assert(@C.post)}.Verifies → ⟦@C.pre⟧' ≤ wlp[C.O]⟦@C.original.pGCL⟧ ⟦@C.post⟧')