Glossary of Lean theorems and definitions

This file contains links to all references, 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.

The names of the definitions on this file bear no semantic meaning, and are purely to nominally distinguish them for documentation generation.

See Paper for a list of just definitions theorems and lemmas as they appear in the paper.

Section 3 – Preliminaries

def Paper.Section3.link₁ : Link ENNReal

Equations

• Paper.Section3.link₁ = True.intro

def Paper.Section3.link₂ {𝒱 : Type u_1} : Link pGCL.ProbExp

Written $\mathbb{R}_{[0, 1]}$ in the paper

Equations

• ⋯ = True.intro

def Paper.Section3.link₃ : Link CompleteLattice

Equations

• Paper.Section3.link₃ = True.intro

def Paper.Section3.link₄ : Link Bot

Equations

• Paper.Section3.link₄ = True.intro

def Paper.Section3.link₅ : Link Top

Equations

• Paper.Section3.link₅ = True.intro

def Paper.Section3.link₆ {α : Type u_3} {β : Type u_4} [CompleteLattice α] [CompleteLattice β] : Link Monotone

Equations

• ⋯ = True.intro

def Paper.Section3.link₇ {α : Type u_3} {β : Type u_4} [CompleteLattice α] [CompleteLattice β] : Link OmegaCompletePartialOrder.ωScottContinuous

For continuity we use ωScottContinuous

Equations

• ⋯ = True.intro

def Paper.Section3.link₈ {α : Type u_3} {β : Type u_4} [CompleteLattice α] [CompleteLattice β] : Link OmegaCompletePartialOrder.ωScottContinuous

And for co-continuity we use OrderDual to flip the order of the order

Equations

• ⋯ = True.intro

def Paper.Section3.thm₉ {α : Type u_3} [CompleteLattice α] : LinkThm (∀ (f : α →o α), OmegaCompletePartialOrder.ωScottContinuous ⇑f → OrderHom.lfp f = ⨆ (n : ℕ), (⇑f)^[n] ⊥)

Kleene fixed point theorem for lfp

Equations

• ⋯ = True.intro

def Paper.Section3.thm₁₀ {α : Type u_3} [CompleteLattice α] : LinkThm (∀ (f : α →o α), OmegaCompletePartialOrder.ωScottContinuous ⇑(OrderHom.dual f) → OrderHom.gfp f = ⨅ (n : ℕ), (⇑f)^[n] ⊤)

Kleene fixed point theorem for gfp

Equations

• ⋯ = True.intro

def Paper.Section3.link₁₁ : Link MeasurableSpace

Equations

• Paper.Section3.link₁₁ = True.intro

def Paper.Section3.link₁₂ {α✝ : Type u_5} {inst✝ : MeasurableSpace α✝} {μ : MeasureTheory.Measure α✝} : Link (MeasureTheory.IsProbabilityMeasure μ)

Equations

• ⋯ = True.intro

def Paper.Section3.link₁₃ : Link PMF

Equations

• Paper.Section3.link₁₃ = True.intro

Section 4 – Expected Total Costs in Markov Decision Processes

Markov Chains

def Paper.Section4.link₁ : Link MarkovChain

Equations

• Paper.Section4.link₁ = True.intro

def Paper.Section4.link₂ {α : Type u_1} {MC : MarkovChain α} : Link MC.Path

Equations

• ⋯ = True.intro

def Paper.Section4.link₃ {α : Type u_1} {MC : MarkovChain α} : Link MC.Path'

Written $\text{Path}^ω$ in the paper

Equations

• ⋯ = True.intro

def Paper.Section4.link₄ {α : Type u_1} {MC : MarkovChain α} : Link MarkovChain.Path'.pref

Equations

• ⋯ = True.intro

def Paper.Section4.link₅ {α : Type u_1} {MC : MarkovChain α} : Link MarkovChain.Path.Cyl

Equations

• ⋯ = True.intro

def Paper.Section4.link₆ {α : Type u_1} {MC : MarkovChain α} : Link MarkovChain.Pr

Equations

• ⋯ = True.intro

def Paper.Section4.thm₇ {α : Type u_1} {MC : MarkovChain α} : LinkThm (∀ (π : MC.Path), MarkovChain.Pr π.Cyl = ∏ i : Fin (π.length - 1), (MC.P π.states[i]) π.states[↑i + 1])

Equations

• ⋯ = True.intro

def Paper.Section4.link₈ {α : Type u_1} {MC : MarkovChain α} : Link MarkovChain.embed

Equations

• ⋯ = True.intro

Expected Costs of MDPs as Sums over Paths

def Paper.Section4.link₉ : Link MDP

Equations

• Paper.Section4.link₉ = True.intro

def Paper.Section4.link₁₀ {S : Type u_1} {A : Type u_2} {M : MDP S A} : Link M.succs

Equations

• ⋯ = True.intro

def Paper.Section4.link₁₁ {S : Type u_1} {A : Type u_2} {M : MDP S A} : Link M.act

Equations

• ⋯ = True.intro

def Paper.Section4.link₁₂ {S : Type u_1} {A : Type u_2} {M : MDP S A} : Link M.Path

Equations

• ⋯ = True.intro

def Paper.Section4.link₁₃ {S : Type u_1} {A : Type u_2} {M : MDP S A} : Link 𝔖[M]

Equations

• ⋯ = True.intro

def Paper.Section4.link₁₄ {S : Type u_1} {A : Type u_2} {M : MDP S A} : Link M.inducedMC'

Equations

• ⋯ = True.intro

def Paper.Section4.thm₁₅ {S : Type u_1} {A : Type u_2} {M : MDP S A} {π : M.Path} {𝒮✝ : 𝔖[M]} {h : MDP.Path.Prob 𝒮✝ π ≠ 0} : LinkThm (MarkovChain.Pr (π.toMC' h ⋯).Cyl = MDP.Path.Prob 𝒮✝ π)

Equations

• ⋯ = True.intro

Expected Costs of MDPs as Least Fixed Points

def Paper.Section4.link₁₆ {α : Type u_3} {β : Type u_4} [CompleteLattice β] : Link Pi.instCompleteLattice

Equations

• ⋯ = True.intro

noncomputable def MDP.ECost {S : Type u_1} {A : Type u_2} (M : MDP S A) (𝒮 : 𝔖[M]) (c : M.Costs) (s : S) : ENNReal

This definition is used in the paper, be in the formalization we use EC. See below.

Equations

• M.ECost 𝒮 c s = ⨆ (n : ℕ), ∑' (π : ↑Path[M,s,=n]), MDP.Path.Prob 𝒮 ↑π * MDP.Path.Cost c ↑π

def Paper.Section4.link₁₇ {S : Type u_1} {A : Type u_2} {M : MDP S A} : Link MDP.EC

Equations

• ⋯ = True.intro

def Paper.Section4.link₁₈ {S : Type u_1} {A : Type u_2} {M : MDP S A} : Link MDP.Φ

Equations

• ⋯ = True.intro

def Paper.Section4.thm₁₉ {S : Type u_1} {A : Type u_2} {M : MDP S A} {c : M.Costs} : LinkThm (OmegaCompletePartialOrder.ωScottContinuous ⇑(MDP.Φ Optimization.Angelic c))

Equations

• ⋯ = True.intro

def Paper.Section4.thm₂₀ {S : Type u_1} {A : Type u_2} [DecidableEq S] {M : MDP S A} {c : M.Costs} : LinkThm (⨆ (n : ℕ), ⨆ (𝒮 : 𝔖[M]), MDP.EC c 𝒮 n = OrderHom.lfp (MDP.Φ Optimization.Angelic c))

Equations

• ⋯ = True.intro

def Paper.Section4.thm₂₁ {S : Type u_1} {A : Type u_2} {M : MDP S A} [M.FiniteBranching] {c : M.Costs} : LinkThm (OmegaCompletePartialOrder.ωScottContinuous ⇑(MDP.Φ Optimization.Demonic c))

Equations

• ⋯ = True.intro

def Paper.Section4.thm₂₂ {S : Type u_1} {A : Type u_2} [DecidableEq S] {M : MDP S A} [M.FiniteBranching] {c : M.Costs} : LinkThm (⨆ (n : ℕ), ⨅ (𝒮 : 𝔖[M]), MDP.EC c 𝒮 n = OrderHom.lfp (MDP.Φ Optimization.Demonic c))

Equations

• ⋯ = True.intro

def Paper.Section4.link₂₃ {S : Type u_1} {A : Type u_2} {M : MDP S A} : Link 𝔏[M]

Equations

• ⋯ = True.intro

def Paper.Section4.link₂₄ {S : Type u_1} {A : Type u_2} {M : MDP S A} : Link MDP.Φℒ

Equations

• ⋯ = True.intro

def Paper.Section4.thm₂₅ {S : Type u_1} {A : Type u_2} {M : MDP S A} [M.FiniteBranching] {c : M.Costs} : LinkThm (MDP.lfp_Φℒ (MDP.optℒ c) c = OrderHom.lfp (MDP.Φ Optimization.Demonic c))

Equations

• ⋯ = True.intro

def Paper.Section4.thm₂₆ {S : Type u_1} {A : Type u_2} [DecidableEq S] {M : MDP S A} [M.FiniteBranching] {c : M.Costs} : LinkThm (⨅ (𝒮 : 𝔖[M]), ⨆ (n : ℕ), MDP.EC c 𝒮 n = OrderHom.lfp (MDP.Φ Optimization.Demonic c))

Equations

• ⋯ = True.intro

Section 5 – pGCL: probabilistic Guarded Command Language

Program States, pGCL Syntax, and Design Considerations

def Paper.Section5.link₁ {𝒱 : Type u_1} : Link pGCL.State

Equations

• ⋯ = True.intro

def Paper.Section5.link₂ : Link Substitution

Equations

• Paper.Section5.link₂ = True.intro

def Paper.Section5.link₃ {𝒱 : Type u_1} : Link pGCL

Equations

• ⋯ = True.intro

def Paper.Section5.link₄ {𝒱 : Type u_1} : Link pGCL.ProbExp

Equations

• ⋯ = True.intro

def Paper.Section5.link₅ : Link Conf

Equations

• Paper.Section5.link₅ = True.intro

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

Equations

• ⋯ = True.intro

Operational Semantics

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

Operational MDP

Equations

• ⋯ = True.intro

We split the cost functions into two parts, one for programs and one for terminations

def Paper.Section5.link₈ {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} : Link pGCL.cost_p

Cost of program for $\text{ct}$

Equations

• ⋯ = True.intro

def Paper.Section5.link₉ {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} : Link pGCL.cost_t

Cost of termination for $\text{ct}$

Equations

• ⋯ = True.intro

def Paper.Section5.link₁₀ {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} : Link pGCL.cost_p'

Cost of program for $\text{cp}$

Equations

• ⋯ = True.intro

def Paper.Section5.link₁₁ {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} : Link pGCL.cost_t'

Cost of termination for $\text{cp}$

Equations

• ⋯ = True.intro

def Paper.Section5.link₁₂ {𝒱 : 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

def Paper.Section5.thm₁₃ {𝒱 : 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 Γ} : LinkThm (∀ (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')))

Equations

• ⋯ = True.intro

Weakest Preexpectation Calculi

def Paper.Section5.link₁₄ : Link Iverson

Equations

• Paper.Section5.link₁₄ = True.intro

def Paper.Section5.link₁₅ {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} : Link pGCL.Ψ

Equations

• ⋯ = True.intro

def Paper.Section5.link₁₆ {𝒱 : Type u_1} [DecidableEq 𝒱] {Γ : 𝒱 → Type u_2} : Link pGCL.wp

Equations

• ⋯ = True.intro

def Paper.Section5.link₁₇ {𝒱 : Type u_1} [DecidableEq 𝒱] {Γ : 𝒱 → Type u_2} : Link pGCL.wlp

Equations

• ⋯ = True.intro

def Paper.Section5.link₁₈ {𝒱 : Type u_1} [DecidableEq 𝒱] {Γ : 𝒱 → Type u_2} : Link pGCL.cwp

Equations

• ⋯ = True.intro

Soundness

def Paper.Section5.link₁₉ {𝒱 : 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

def Paper.Section5.thm₂₀ {𝒱 : 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] : LinkThm (OrderHom.lfp (SmallStepSemantics.ξ O) = SmallStepSemantics.op O)

Equations

• ⋯ = True.intro

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

Equations

• ⋯ = True.intro

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

Equations

• ⋯ = True.intro

def Paper.Section5.thm₂₃ {𝒱 : Type u_1} [DecidableEq 𝒱] {Γ : 𝒱 → Type u_2} {O : Optimization} {C : pGCL Γ} : LinkThm (wfp[O]⟦@C⟧ = SmallStepSemantics.op O C)

Equations

• ⋯ = True.intro

def Paper.Section5.thm₂₄ {𝒱 : 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))

Equations

• ⋯ = True.intro

Quantitative Loop Invariants

def Paper.Section5.thm₂₅ {α : Type u_3} [CompleteLattice α] {Δ : α →o α} {f : α} : LinkThm (∀ (k : ℕ), Δ ((fun (x : α) => Δ x ⊓ f)^[k] f) ≤ f → OrderHom.lfp Δ ≤ f)

Equations

• ⋯ = True.intro

def Paper.Section5.thm₂₆ {α : Type u_3} [CompleteLattice α] {Δ : α →o α} {f : α} : LinkThm (∀ (k : ℕ), f ≤ Δ ((fun (x : α) => Δ x ⊔ f)^[k] f) → f ≤ OrderHom.gfp Δ)

Equations

• ⋯ = True.intro

def Paper.Section5.thm₂₇ {𝒱 : 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)

Equations

• ⋯ = True.intro

def Paper.Section5.thm₂₈ {𝒱 : 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 }⟧ φ)

Equations

• ⋯ = True.intro

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

Equations

• ⋯ = True.intro

def Paper.Section5.thm₃₀ {𝒱 : Type u_1} [DecidableEq 𝒱] {Γ : 𝒱 → Type u_2} {O : Optimization} {b : pGCL.BExpr Γ} {C : pGCL Γ} {φ I : pGCL.State Γ → ENNReal} {σ₀ : pGCL.State Γ} : LinkThm (∀ (k : ℕ), pGCL.IdleKInvariant wp[O]⟦@C⟧ b φ k I (~ C.mods) σ₀ → wp[O]⟦while @b { @C }⟧ φ σ₀ ≤ I σ₀)

Equations

• ⋯ = True.intro

def Paper.Section5.thm₃₁ {𝒱 : Type u_1} [DecidableEq 𝒱] {Γ : 𝒱 → Type u_2} {O : Optimization} {b : pGCL.BExpr Γ} {C : pGCL Γ} {φ I : pGCL.ProbExp Γ} {σ₀ : pGCL.State Γ} : LinkThm (∀ (k : ℕ), pGCL.IdleKCoinvariant wlp'[O]⟦@C⟧ b φ k I (~ C.mods) σ₀ → I σ₀ ≤ (wlp'[O]⟦while @b { @C }⟧ φ) σ₀)

Equations

• ⋯ = True.intro

Section 6 – Sound Encodings into an Intermediate Verification Language

The Intermediate Verification Language HeyVL

def Paper.Section6.link₁ : Link HeyLo

Equations

• Paper.Section6.link₁ = True.intro

def Paper.Section6.link₂ : Link HeyVL

Equations

• Paper.Section6.link₂ = True.intro

def Paper.Section6.link₃ : Link HNot

Written using ￢ (notice this is a different symbol than Boolean negation ¬)

Equations

• Paper.Section6.link₃ = True.intro

def Paper.Section6.link₄ : Link Compl

Written using xᶜ. We add ~x as custom syntax too to align with the paper

Equations

• Paper.Section6.link₄ = True.intro

def Paper.Section6.link₅ : Link HImp

Written using a ⇨ b and is Heyting implicaiton. In the paper this is b ↜ a (notice the flipped order of arguments).

Equations

• Paper.Section6.link₅ = True.intro

def Paper.Section6.link₆ : Link SDiff

Written using a \ b and is Heyting co-implicaiton. In the paper this is b ↜ a (notice the flipped order of arguments).

Equations

• Paper.Section6.link₆ = True.intro

def Paper.Section6.link₇ : Link BiheytingAlgebra

Equations

• Paper.Section6.link₇ = True.intro

def Paper.Section6.link₈ : Link HeyVL.vp

Equations

• Paper.Section6.link₈ = True.intro

def Paper.Section6.link₉ : Link HeyVL.Verifies

A HeyVL program C verifies if vp⟦C⟧ ⊤ = ⊤

Equations

• Paper.Section6.link₉ = True.intro

Case Study: Correctness of Encodings for pGCL

def Paper.Section6.thm₁₀ {C : spGCL} {O : Optimization} : LinkThm (Encoding → Globals → Globals × HeyVL)

Equations

• ⋯ = True.intro

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

Equations

• ⋯ = True.intro

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

Equations

• ⋯ = True.intro

def Paper.Section6.thm₁₃ {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⟧')

Equations

• ⋯ = True.intro