theorem pGCL.wlp'_apply_eq_wlp_apply {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {O : Optimization} {X : ProbExp Γ} {σ : State Γ} {C : pGCL Γ} : (wlp'[O]⟦@C⟧ X) σ = wlp[O]⟦@C⟧ (⇑X) σ

def pGCL.State.EQ {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} (V : Set 𝒱) (σ₀ : State Γ) : Set (State Γ)

Equations

• pGCL.State.EQ V σ₀ = {σ : pGCL.State Γ | ∀ v ∈ V, σ v = σ₀ v}

def pGCL.IdleInvariant {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} (g : (State Γ → ENNReal) →o State Γ → ENNReal) (b : BExpr Γ) (φ I : State Γ → ENNReal) (V : Set 𝒱) (σ₀ : State Γ) : Prop

An Idle invariant is Park invariant that holds for states with a set of fixed variables.

Equations

• pGCL.IdleInvariant g b φ I V σ₀ = ∀ σ ∈ pGCL.State.EQ V σ₀, ((Ψ[g] b) φ) I σ ≤ I σ

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

Idle induction is Park induction, but the engine is running (i.e. an initial state is given), and as a consequence only states that vary over the modified variables need to be considered for the inductive invariant.

def pGCL.IdleCoinvariant {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} (g : (State Γ → ENNReal) →o State Γ → ENNReal) (b : BExpr Γ) (φ I : State Γ → ENNReal) (V : Set 𝒱) (σ₀ : State Γ) : Prop

An Idle coinvariant is Park coinvariant that holds for states with a set of fixed variables.

Equations

• pGCL.IdleCoinvariant g b φ I V σ₀ = ∀ σ ∈ pGCL.State.EQ V σ₀, I σ ≤ ((Ψ[g] b) φ) I σ

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

Idle coinduction is Park coinduction, but the engine is running (i.e. an initial state is given), and as a consequence only states that vary over the modified variables need to be considered for the coinductive invariant.

def pGCL.IdleKInvariant {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} (g : (State Γ → ENNReal) →o State Γ → ENNReal) (b : BExpr Γ) (φ : State Γ → ENNReal) (k : ℕ) (I : State Γ → ENNReal) (V : Set 𝒱) (σ₀ : State Γ) : Prop

A Idle k-invariant.

Equations

• pGCL.IdleKInvariant g b φ k I V σ₀ = ∀ σ ∈ pGCL.State.EQ V σ₀, ((Ψ[g] b) φ) ((fun (x : pGCL.State Γ → ENNReal) => ((Ψ[g] b) φ) x ⊓ I)^[k] I) σ ≤ I σ

theorem pGCL.IdleKInduction {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {O : Optimization} {b : BExpr Γ} {C : pGCL Γ} {φ I : State Γ → ENNReal} (k : ℕ) {σ₀ : State Γ} (h : IdleKInvariant wp[O]⟦@C⟧ b φ k I (~ C.mods) σ₀) : wp[O]⟦while @b { @C }⟧ φ σ₀ ≤ I σ₀

Idle k-induction.

def pGCL.IdleKCoinvariant {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} (g : ProbExp Γ →o ProbExp Γ) (b : BExpr Γ) (φ : ProbExp Γ) (k : ℕ) (I : ProbExp Γ) (V : Set 𝒱) (σ₀ : State Γ) : Prop

A Idle k-coinvariant.

Equations

• pGCL.IdleKCoinvariant g b φ k I V σ₀ = ∀ σ ∈ pGCL.State.EQ V σ₀, I σ ≤ (((pΨ[g] b) φ) ((fun (x : pGCL.ProbExp Γ) => ((pΨ[g] b) φ) x ⊔ I)^[k] I)) σ

theorem pGCL.IdleKCoinduction {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {O : Optimization} {b : BExpr Γ} {C : pGCL Γ} {φ I : ProbExp Γ} (k : ℕ) {σ₀ : State Γ} (h : IdleKCoinvariant wlp'[O]⟦@C⟧ b φ k I (~ C.mods) σ₀) : I σ₀ ≤ (wlp'[O]⟦while @b { @C }⟧ φ) σ₀

Idle k-coinduction.

def pGCL.IdleKCoinvariant'' {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} (g : (State Γ → ENNReal) →o State Γ → ENNReal) (b : BExpr Γ) (φ : State Γ → ENNReal) (k : ℕ) (I : State Γ → ENNReal) (V : Set 𝒱) (σ₀ : State Γ) : Prop

A Idle k-coinvariant.

Equations

• pGCL.IdleKCoinvariant'' g b φ k I V σ₀ = ∀ σ ∈ pGCL.State.EQ V σ₀, I σ ≤ ((Ψ[g] b) φ) ((fun (x : pGCL.State Γ → ENNReal) => ((Ψ[g] b) φ) x ⊔ I)^[k] I) σ

def pGCL.IdleKCoinvariant''.toIdleKCoinvariant {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {O : Optimization} {b : BExpr Γ} {φ : State Γ → ENNReal} {k : ℕ} {I : State Γ → ENNReal} {σ₀ : State Γ} {C : pGCL Γ} (h : IdleKCoinvariant'' wlp[O]⟦@C⟧ b φ k I (~ C.mods) σ₀) (hI : I ≤ 1) (hφ : φ ≤ 1) : IdleKCoinvariant wlp'[O]⟦@C⟧ b ⟨φ, hφ⟩ k ⟨I, hI⟩ (~ C.mods) σ₀

Equations

• ⋯ = ⋯

theorem pGCL.IdleKCoinduction'' {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {O : Optimization} {b : BExpr Γ} {C : pGCL Γ} {φ I : State Γ → ENNReal} (k : ℕ) {σ₀ : State Γ} (h : IdleKCoinvariant'' wlp[O]⟦@C⟧ b φ k I (~ C.mods) σ₀) (hI : I ≤ 1) (hφ : φ ≤ 1) : I σ₀ ≤ wlp[O]⟦while @b { @C }⟧ φ σ₀

Idle k-coinduction.