PGCL.WeakestPre

source

theorem OrderHom.lfp_ωScottContinuous {α : Type u_1} {ι : Type u_2} [CompleteLattice α] [CompleteLattice ι] {f : ι →o α →o α} (hf' : OmegaCompletePartialOrder.ωScottContinuous ⇑f) (hf : ∀ (i : ι), OmegaCompletePartialOrder.ωScottContinuous ⇑(f i)) :

OmegaCompletePartialOrder.ωScottContinuous fun (X : ι) => lfp (f X)

source

theorem OrderHom.lfp_iSup {α : Type u_1} [CompleteLattice α] {f : ℕ →o α →o α} (hf : ∀ (i : ℕ), OmegaCompletePartialOrder.ωScottContinuous ⇑(f i)) :

lfp (⨆ (i : ℕ), f i) = ⨆ (i : ℕ), lfp (f i)

source

noncomputable def pGCL.Ψ {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} (g : (State Γ → ENNReal) →o State Γ → ENNReal) (φ : BExpr Γ) :

(State Γ → ENNReal) →o (State Γ → ENNReal) →o State Γ → ENNReal

Equations

Ψ[g] φ = { toFun := fun (f : pGCL.State Γ → ENNReal) => { toFun := fun (X : pGCL.State Γ → ENNReal) => i[φ] * g X + i[~ φ] * f, monotone' := ⋯ }, monotone' := ⋯ }

Instances For

source

def pGCL.«termΨ[_]» :

Lean.ParserDescr

Equations

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

Instances For

source

noncomputable def pGCL.wp {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] (O : Optimization) :

pGCL Γ → (State Γ → ENNReal) →o State Γ → ENNReal

Equations

wp[O]⟦skip ⟧ = { toFun := fun (X : pGCL.State Γ → ENNReal) => X, monotone' := ⋯ }
wp[O]⟦@x_1 := @A⟧ = { toFun := fun (X : pGCL.State Γ → ENNReal) => X[x_1 ↦ A], monotone' := ⋯ }
wp[O]⟦@C₁ ; @C₂⟧ = { toFun := fun (X : pGCL.State Γ → ENNReal) => wp[O]⟦@C₁⟧ (wp[O]⟦@C₂⟧ X), monotone' := ⋯ }
wp[O]⟦{ @C₁ } [@p] { @C₂ }⟧ = { toFun := fun (X : pGCL.State Γ → ENNReal) => ⇑p * wp[O]⟦@C₁⟧ X + (1 - ⇑p) * wp[O]⟦@C₂⟧ X, monotone' := ⋯ }
wp[O]⟦{ @C₁ } [] { @C₂ }⟧ = { toFun := O.opt ⇑wp[O]⟦@C₁⟧ ⇑wp[O]⟦@C₂⟧, monotone' := ⋯ }
wp[O]⟦while @b { @C' }⟧ = { toFun := fun (X : pGCL.State Γ → ENNReal) => OrderHom.lfp ((Ψ[wp[O]⟦@C'⟧] b) X), monotone' := ⋯ }
wp[O]⟦tick(@e)⟧ = { toFun := fun (x : pGCL.State Γ → ENNReal) => e + x, monotone' := ⋯ }
wp[O]⟦observe(@b)⟧ = { toFun := fun (x : pGCL.State Γ → ENNReal) => i[b] * x, monotone' := ⋯ }

Instances For

source

def pGCL.«termWp[_]⟦_⟧» :

Lean.ParserDescr

Equations

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

Instances For

source

def pGCL.wpUnexpander :

Lean.PrettyPrinter.Unexpander

Equations

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

Instances For

source

theorem pGCL.wp_loop {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {O : Optimization} {f : State Γ → ENNReal} (φ : BExpr Γ) (C' : pGCL Γ) :

wp[O]⟦while @φ { @C' }⟧ f = OrderHom.lfp ((Ψ[wp[O]⟦@C'⟧] φ) f)

source

theorem pGCL.wp_fp {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {O : Optimization} {f : State Γ → ENNReal} (φ : BExpr Γ) (C' : pGCL Γ) :

((Ψ[wp[O]⟦@C'⟧] φ) f) (wp[O]⟦while @φ { @C' }⟧ f) = wp[O]⟦while @φ { @C' }⟧ f

source

@[simp]

theorem pGCL.wp.skip_apply {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {O : Optimization} {X : State Γ → ENNReal} :

(wp[O]⟦skip ⟧) X = X

source

@[simp]

theorem pGCL.wp.assign_apply {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {O : Optimization} {x : 𝒱} {X : State Γ → ENNReal} {A : State Γ → Γ x} :

(wp[O]⟦@x := @A⟧) X = X[x ↦ A]

source

@[simp]

theorem pGCL.wp.seq_apply {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {O : Optimization} {C₁ : pGCL Γ} {X : State Γ → ENNReal} {C₂ : pGCL Γ} :

(wp[O]⟦@C₁ ; @C₂⟧) X = wp[O]⟦@C₁⟧ (wp[O]⟦@C₂⟧ X)

source

@[simp]

theorem pGCL.wp.prob_apply {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {O : Optimization} {C₁ : pGCL Γ} {X : State Γ → ENNReal} {p : ProbExp Γ} {C₂ : pGCL Γ} :

wp[O]⟦{ @C₁ } [@p] { @C₂ }⟧ X = ⇑p * wp[O]⟦@C₁⟧ X + (1 - ⇑p) * wp[O]⟦@C₂⟧ X

source

@[simp]

theorem pGCL.wp.nonDet_apply {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {O : Optimization} {C₁ : pGCL Γ} {X : State Γ → ENNReal} {C₂ : pGCL Γ} :

wp[O]⟦{ @C₁ } [] { @C₂ }⟧ X = O.opt (wp[O]⟦@C₁⟧ X) (wp[O]⟦@C₂⟧ X)

source

@[simp]

theorem pGCL.wp.tick_apply {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {O : Optimization} {e X : State Γ → ENNReal} :

wp[O]⟦tick(@e)⟧ X = e + X

source

@[simp]

theorem pGCL.wp.observe_apply {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {O : Optimization} {b : BExpr Γ} {X : State Γ → ENNReal} :

wp[O]⟦observe(@b)⟧ X = i[b] * X

source

theorem pGCL.wp_le_wp {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {O : Optimization} {σ : State Γ} {C : pGCL Γ} {a b : State Γ → ENNReal} (h : a ≤ b) :