inductive Encoding : Type

• wlp : Encoding
• wp : Encoding

def spGCL.enc (C : spGCL) (O : Optimization) (E : Encoding) : Globals → Globals × HeyVL

Equations

• One or more equations did not get rendered due to their size.
• spgcl {skip}.enc O E G = (G, heyvl {skip})
• spgcl {x := @e}.enc O E G = (G, heyvl {x :≈ @(HeyLo.Distribution.pure e)})
• spgcl {@C₁ ; @C₂}.enc O E G = match C₂.enc O E G with | (G, C₂) => match C₁.enc O E G with | (G, C₁) => (G, heyvl {@C₁ ; @C₂})
• spgcl {if @b then @C₁ else @C₂ end}.enc O E G = match C₁.enc O E G with | (G, C₁) => match C₂.enc O E G with | (G, C₂) => (G, heyvl {if (@b) {@C₁} else {@C₂}})
• spgcl {tick(@r)}.enc O Encoding.wp G = (G, heyvl {reward(@r)})
• spgcl {tick(@r)}.enc O Encoding.wlp G = (G, heyvl {reward(0 * @r)})
• spgcl {observe(@r)}.enc O E G = (G, heyvl {assert(@r.embed)})

@[simp]

theorem spGCL.enc_G_mono {G : Globals} {O : Optimization} {E : Encoding} {C : spGCL} : G ⊆ (C.enc O E G).1

@[simp]

theorem spGCL.fv_HeyVL_subset {O : Optimization} {E : Encoding} {G : Globals} {C : spGCL} : (C.enc O E G).2.fv = C.fv ∪ (C.enc O E G).1 \ G

@[simp]

theorem spGCL.enc_mods {O : Optimization} {E : Encoding} {G : Globals} (C : spGCL) : C.mods ⊆ (C.enc O E G).2.mods

def spGCL.vp (C : spGCL) (O : Optimization) (E : Encoding) (φ : HeyLo HeyLo.Ty.ENNReal) : HeyLo HeyLo.Ty.ENNReal

Equations

• C.vp O E φ = vp⟦@(C.enc O E (C.fv ∪ φ.fv)).2⟧ φ

theorem spGCL.enc_prob_vp {p : HeyLo HeyLo.Ty.ENNReal} {O : Optimization} {E : Encoding} {φ : HeyLo HeyLo.Ty.ENNReal} {C₁ C₂ : spGCL} {G : Globals} (hG : spgcl {{ @C₁ } [@p] { @C₂ }}.fv ∪ φ.fv ⊆ G) : ⟦@(vp⟦@(spgcl {{ @C₁ } [@p] { @C₂ }}.enc O E G).2⟧ φ)⟧' = (⟦@p⟧' ⊓ 1) * ⟦@(vp⟦@(C₁.enc O E G).2⟧ φ)⟧' + (1 - ⟦@p⟧' ⊓ 1) * ⟦@(vp⟦@(C₂.enc O E (C₁.enc O E G).1).2⟧ φ)⟧'

theorem spGCL.wp_le_vp {O : Optimization} {φ : HeyLo HeyLo.Ty.ENNReal} {C : spGCL} : wp[O]⟦@C.pGCL⟧ ⟦@φ⟧' ≤ ⟦@(C.vp O Encoding.wp φ)⟧'

@[simp]

theorem pGCL.wlp_le_one {𝒱 : Type u_2} {O : Optimization} [DecidableEq 𝒱] {Γ : 𝒱 → Type u_1} {C : pGCL Γ} {φ : State Γ → ENNReal} : wlp[O]⟦@C⟧ φ ≤ 1

theorem spGCL.vp_le_wlp {O : Optimization} {φ : HeyLo HeyLo.Ty.ENNReal} {C : spGCL} (hφ : ⟦@φ⟧' ≤ 1) (hI : ∀ I ∈ C.invs, ⟦@I⟧' ≤ 1) : ⟦@(C.vp O Encoding.wlp φ)⟧' ≤ wlp[O]⟦@C.pGCL⟧ ⟦@φ⟧'