Documentation

PGCL.WeakestPre

def pGCL.wp.lfp {α : Type u_2} [CompleteLattice α] (f : α → α) :

α

A version of OrderHom.lfp that does not require f the Monotone upfront.

Equations

pGCL.wp.lfp f = sInf {a : α | f a ≤ a}

Instances For

theorem pGCL.wp.lfp.monotone {α : Type u_2} [CompleteLattice α] :

Monotone wp.lfp

@[simp]

theorem pGCL.wp.lfp.wp_lfp_eq_lfp {α : Type u_2} [CompleteLattice α] (f : α → α) (h : Monotone f) :

wp.lfp f = OrderHom.lfp { toFun := f, monotone' := h }

@[simp]

theorem pGCL.wp.lfp.wp_lfp_eq_lfp_OrderHom {α : Type u_2} [CompleteLattice α] (f : α →o α) :

wp.lfp ⇑f = OrderHom.lfp f

noncomputable def pGCL.wp {ϖ : Type u_1} [DecidableEq ϖ] (C : pGCL ϖ) (X : Exp ϖ) :

Exp ϖ

Equations

pGCL.skip.wp X = X
(x ::= A).wp X = fun (σ : pGCL.States ϖ) => X (σ[x ↦ A σ])
(C₁ ;; C₂).wp X = C₁.wp (C₂.wp X)
(C₁ ·[p] C₂).wp X = p.pick (C₁.wp X) (C₂.wp X)
(C₁ ·[] C₂).wp X = C₁.wp X ⊓ C₂.wp X
(pGCL.loop b C').wp X = pGCL.wp.lfp fun (x : pGCL.Exp ϖ) => b.probOf * C'.wp x + b.not.probOf * X
(pGCL.tick e).wp X = e + X

Instances For

@[simp]

theorem pGCL.wp.skip {ϖ : Type u_1} [DecidableEq ϖ] :

pGCL.skip.wp = fun (x : Exp ϖ) => x

@[simp]

theorem pGCL.wp.assign {ϖ : Type u_1} [DecidableEq ϖ] {x : ϖ} {A : Exp ϖ} :

(x ::= A).wp = fun (X : Exp ϖ) (σ : States ϖ) => X (σ[x ↦ A σ])

@[simp]

theorem pGCL.wp.seq {ϖ : Type u_1} [DecidableEq ϖ] {C₁ C₂ : pGCL ϖ} :

(C₁ ;; C₂).wp = C₁.wp ∘ C₂.wp

@[simp]

theorem pGCL.wp.prob {ϖ : Type u_1} [DecidableEq ϖ] {C₁ : pGCL ϖ} {p : ProbExp ϖ} {C₂ : pGCL ϖ} :

(C₁ ·[p] C₂).wp = fun (X : Exp ϖ) => p.pick (C₁.wp X) (C₂.wp X)

@[simp]

theorem pGCL.wp.nonDet {ϖ : Type u_1} [DecidableEq ϖ] {C₁ C₂ : pGCL ϖ} :

(C₁ ·[] C₂).wp = C₁.wp ⊓ C₂.wp

@[simp]

theorem pGCL.wp.tick {ϖ : Type u_1} [DecidableEq ϖ] {e : Exp ϖ} :

(pGCL.tick e).wp = fun (X : Exp ϖ) => e + X

@[simp]

theorem pGCL.wp.monotone {ϖ : Type u_1} [DecidableEq ϖ] (C : pGCL ϖ) :

noncomputable def pGCL.wp_loop_f {ϖ : Type u_1} [DecidableEq ϖ] (b : BExpr ϖ) (C' : pGCL ϖ) (X : Exp ϖ) :

Exp ϖ →o Exp ϖ

Equations

pGCL.wp_loop_f b C' X = { toFun := fun (Y : pGCL.Exp ϖ) => b.probOf * C'.wp Y + b.not.probOf * X, monotone' := ⋯ }

Instances For

theorem pGCL.wp_loop {ϖ : Type u_1} [DecidableEq ϖ] {b : BExpr ϖ} {C' : pGCL ϖ} :

(loop b C').wp = fun (X : Exp ϖ) => OrderHom.lfp (wp_loop_f b C' X)

theorem pGCL.wp_loop_fp {ϖ : Type u_1} [DecidableEq ϖ] (b : BExpr ϖ) (C : pGCL ϖ) :

(loop b C).wp = fun (X : Exp ϖ) => b.probOf * (C ;; loop b C).wp X + b.not.probOf * X