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

Equations

• pΨ[g] φ = { toFun := fun (f : pGCL.ProbExp Γ) => { toFun := fun (X : pGCL.ProbExp Γ) => p[φ] * g X + (1 - p[φ]) * f, monotone' := ⋯ }, monotone' := ⋯ }

def pGCL.«termPΨ[_]» : Lean.ParserDescr

Equations

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

theorem pGCL.pΨ_eq_Ψ {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} {g : ProbExp Γ →o ProbExp Γ} {g' : (State Γ → ENNReal) →o State Γ → ENNReal} {φ : BExpr Γ} {x y : ProbExp Γ} (hg : ∀ (X : ProbExp Γ) (σ : State Γ), (g X) σ = g' (⇑X) σ) : ⇑(((pΨ[g] φ) x) y) = ((Ψ[g'] φ) ⇑x) ⇑y

theorem pGCL.pΨ_apply {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} {φ : BExpr Γ} {f : ProbExp Γ} {g : ProbExp Γ →o ProbExp Γ} : (pΨ[g] φ) f = { toFun := fun (X : ProbExp Γ) => p[φ] * g X + (1 - p[φ]) * f, monotone' := ⋯ }

theorem pGCL.pΨ_apply₂ {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} {φ : BExpr Γ} {f X : ProbExp Γ} {g : ProbExp Γ →o ProbExp Γ} : ((pΨ[g] φ) f) X = p[φ] * g X + (1 - p[φ]) * f

theorem pGCL.ProbExp.ωScottContinuous_dual_iff' {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} {f : ProbExp Γ →o ProbExp Γ} : OmegaCompletePartialOrder.ωScottContinuous ⇑(OrderHom.dual f) ↔ ∀ (c : ℕ → ProbExp Γ), Antitone c → f (⨅ (i : ℕ), c i) = ⨅ (i : ℕ), f (c i)

theorem pGCL.pΨ.continuous {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} {b : BExpr Γ} {X : ProbExp Γ} {g : ProbExp Γ →o ProbExp Γ} (hg : OmegaCompletePartialOrder.ωScottContinuous ⇑(OrderHom.dual g)) : OmegaCompletePartialOrder.ωScottContinuous ⇑(OrderHom.dual ((pΨ[g] b) X))

theorem pGCL.pΨ.continuous' {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} {b : BExpr Γ} {X : ProbExp Γ} {g : ProbExp Γ →o ProbExp Γ} (hg : OmegaCompletePartialOrder.ωScottContinuous ⇑g) : OmegaCompletePartialOrder.ωScottContinuous ⇑((pΨ[g] b) X)

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

Equations

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

def pGCL.«termWfp'[_]⟦_⟧» : Lean.ParserDescr

Equations

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

def pGCL.wfp'Unexpander : Lean.PrettyPrinter.Unexpander

Equations

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

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

Equations

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

def pGCL.«termWfp[_]⟦_⟧» : Lean.ParserDescr

Equations

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

def pGCL.wfpUnexpander : Lean.PrettyPrinter.Unexpander

Equations

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

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

theorem pGCL.wfp_loop {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {O : Optimization} {f : State Γ → ENNReal} (φ : BExpr Γ) (C' : pGCL Γ) : wfp[O]⟦while @φ { @C' }⟧ f = OrderHom.lfp ((Ψ[wfp[O]⟦@C'⟧] φ) f)

theorem pGCL.wfp_fp {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {O : Optimization} {f : State Γ → ENNReal} (φ : BExpr Γ) (C' : pGCL Γ) : ((Ψ[wfp[O]⟦@C'⟧] φ) f) (wfp[O]⟦while @φ { @C' }⟧ f) = wfp[O]⟦while @φ { @C' }⟧ f

theorem pGCL.wfp'_loop {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {O : Optimization} {f : ProbExp Γ} (φ : BExpr Γ) (C' : pGCL Γ) : ⇑(wfp'[O]⟦while @φ { @C' }⟧ f) = OrderHom.lfp ((Ψ[wfp[O]⟦@C'⟧] φ) ⇑f)

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

Equations

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

def pGCL.«termWlp'[_]⟦_⟧» : Lean.ParserDescr

Equations

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

def pGCL.wlp'Unexpander : Lean.PrettyPrinter.Unexpander

Equations

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

noncomputable def pGCL.lΨ {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] (O : Optimization) (b : BExpr Γ) (C' : pGCL Γ) (f : ProbExp Γ) : ProbExp Γ →o ProbExp Γ

Equations

• pGCL.lΨ O b C' f = { toFun := fun (Y : pGCL.ProbExp Γ) => p[b] * wlp'[O]⟦@C'⟧ Y + (1 - p[b]) * f, monotone' := ⋯ }

theorem pGCL.wlp'_loop {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {O : Optimization} {f : ProbExp Γ} (φ : BExpr Γ) (C' : pGCL Γ) : wlp'[O]⟦while @φ { @C' }⟧ f = OrderHom.gfp (lΨ O φ C' f)

@[simp]

theorem pGCL.wlp'.skip_apply {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {X : ProbExp Γ} {O : Optimization} : (wlp'[O]⟦skip⟧) X = X

@[simp]

theorem pGCL.wlp'.assign_apply {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {X : ProbExp Γ} {O : Optimization} {x : 𝒱} {A : State Γ → Γ x} : (wlp'[O]⟦@x := @A⟧) X = X[x ↦ A]

@[simp]

theorem pGCL.wlp'.seq_apply {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {X : ProbExp Γ} {O : Optimization} {C₁ C₂ : pGCL Γ} : (wlp'[O]⟦@C₁ ; @C₂⟧) X = wlp'[O]⟦@C₁⟧ (wlp'[O]⟦@C₂⟧ X)

@[simp]

theorem pGCL.wlp'.prob_apply {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {X : ProbExp Γ} {O : Optimization} {C₁ : pGCL Γ} {p : ProbExp Γ} {C₂ : pGCL Γ} : wlp'[O]⟦{ @C₁ } [@p] { @C₂ }⟧ X = p * wlp'[O]⟦@C₁⟧ X + (1 - p) * wlp'[O]⟦@C₂⟧ X

@[simp]

theorem pGCL.wlp'.nonDet_apply {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {X : ProbExp Γ} {O : Optimization} {C₁ C₂ : pGCL Γ} : wlp'[O]⟦{ @C₁ } [] { @C₂ }⟧ X = O.opt (wlp'[O]⟦@C₁⟧ X) (wlp'[O]⟦@C₂⟧ X)

@[simp]

theorem pGCL.wlp'.tick_apply {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {X : ProbExp Γ} {O : Optimization} {e : State Γ → ENNReal} : wlp'[O]⟦tick(@e)⟧ X = X

@[simp]

theorem pGCL.wlp'.observe_apply {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {X : ProbExp Γ} {O : Optimization} {b : State Γ → Prop} : wlp'[O]⟦observe(@b)⟧ X = p[b] * X

noncomputable def pGCL.wlp {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] (O : Optimization) (C : pGCL Γ) : (State Γ → ENNReal) →o State Γ → ENNReal

Equations

• wlp[O]⟦@C⟧ = { toFun := fun (X : pGCL.State Γ → ENNReal) => ⇑(wlp'[O]⟦@C⟧ (pGCL.ProbExp.ofExp X)), monotone' := ⋯ }

def pGCL.«termWlp[_]⟦_⟧» : Lean.ParserDescr

Equations

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

def pGCL.wlpUnexpander : Lean.PrettyPrinter.Unexpander

Equations

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

@[simp]

theorem pGCL.wlp.skip_apply {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {X : State Γ → ENNReal} {O : Optimization} : (wlp[O]⟦skip⟧) X = X ⊓ 1

@[simp]

theorem pGCL.wlp.assign_apply {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {X : State Γ → ENNReal} {O : Optimization} {x : 𝒱} {A : State Γ → Γ x} : (wlp[O]⟦@x := @A⟧) X = (X ⊓ 1)[x ↦ A]

@[simp]

theorem pGCL.wlp.seq_apply {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {X : State Γ → ENNReal} {O : Optimization} {C₁ C₂ : pGCL Γ} : (wlp[O]⟦@C₁ ; @C₂⟧) X = wlp[O]⟦@C₁⟧ (wlp[O]⟦@C₂⟧ X ⊓ 1)

@[simp]

theorem pGCL.wlp.prob_apply {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {X : State Γ → ENNReal} {O : Optimization} {C₁ : pGCL Γ} {p : ProbExp Γ} {C₂ : pGCL Γ} : wlp[O]⟦{ @C₁ } [@p] { @C₂ }⟧ X = ⇑p * wlp[O]⟦@C₁⟧ X + (1 - ⇑p) * wlp[O]⟦@C₂⟧ X

@[simp]

theorem pGCL.wlp.nonDet_apply {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {X : State Γ → ENNReal} {O : Optimization} {C₁ C₂ : pGCL Γ} : wlp[O]⟦{ @C₁ } [] { @C₂ }⟧ X = O.opt (wlp[O]⟦@C₁⟧ X) (wlp[O]⟦@C₂⟧ X)

@[simp]

theorem pGCL.wlp.tick_apply {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {X : State Γ → ENNReal} {O : Optimization} {e : State Γ → ENNReal} : wlp[O]⟦tick(@e)⟧ X = X ⊓ 1

@[simp]

theorem pGCL.wlp.observe_apply {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {X : State Γ → ENNReal} {O : Optimization} {b : State Γ → Prop} : wlp[O]⟦observe(@b)⟧ X = ⇑p[b] * (X ⊓ 1)

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

theorem pGCL.wlp'_sound {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {O : Optimization} (C : pGCL Γ) : wlp'[O]⟦@C⟧ = ~ wfp'[O.dual]⟦@C⟧

def pGCL.wfp.continuous {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {O : Optimization} (C : pGCL Γ) : OmegaCompletePartialOrder.ωScottContinuous ⇑wfp[O]⟦@C⟧

Equations

• ⋯ = ⋯

def pGCL.wfp'.continuous {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {O : Optimization} (C : pGCL Γ) : OmegaCompletePartialOrder.ωScottContinuous ⇑wfp'[O]⟦@C⟧

Equations

• ⋯ = ⋯

theorem pGCL.ωScottContinuous_dual_prob_iff {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} {f : ProbExp Γ →o ProbExp Γ} : OmegaCompletePartialOrder.ωScottContinuous ⇑(OrderHom.dual f) ↔ ∀ (c : ℕ → ProbExp Γ), Antitone c → f (⨅ (i : ℕ), c i) = ⨅ (i : ℕ), f (c i)

def pGCL.wlp'.continuous_aux {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {O : Optimization} (C : pGCL Γ) (h : ∀ (X : ProbExp Γ), wlp'[O]⟦@C⟧ X = 1 - wfp'[O.dual]⟦@C⟧ (1 - X)) : OmegaCompletePartialOrder.ωScottContinuous ⇑(OrderHom.dual wlp'[O]⟦@C⟧)

Equations

• ⋯ = ⋯

def pGCL.wlp'.continuous {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {O : Optimization} (C : pGCL Γ) : OmegaCompletePartialOrder.ωScottContinuous ⇑(OrderHom.dual wlp'[O]⟦@C⟧)

Equations

• ⋯ = ⋯

@[simp]

def pGCL.wlp.continuous {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {O : Optimization} (C : pGCL Γ) : OmegaCompletePartialOrder.ωScottContinuous ⇑(OrderHom.dual wlp[O]⟦@C⟧)

Equations

• ⋯ = ⋯

@[simp]

def pGCL.Ψ.wlp_continuous {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {O : Optimization} {φ : BExpr Γ} {f : State Γ → ENNReal} {C' : pGCL Γ} : OmegaCompletePartialOrder.ωScottContinuous ⇑(OrderHom.dual ((Ψ[wlp[O]⟦@C'⟧] φ) f))

Equations

• ⋯ = ⋯

theorem pGCL.wlp_loop_eq_gfp {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {O : Optimization} {f : State Γ → ENNReal} (φ : BExpr Γ) (C' : pGCL Γ) : wlp[O]⟦while @φ { @C' }⟧ f = ⇑(OrderHom.gfp ((pΨ[wlp'[O]⟦@C'⟧] φ) (ProbExp.ofExp f)))

theorem pGCL.wlp_loop_eq_iter {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {O : Optimization} {f : State Γ → ENNReal} (φ : BExpr Γ) (C' : pGCL Γ) : wlp[O]⟦while @φ { @C' }⟧ f = ⨅ (n : ℕ), (⇑((Ψ[wlp[O]⟦@C'⟧] φ) (f ⊓ 1)))^[n] 1