PGCL.Fix

source

theorem OrderHom.le_gfp_prob {𝒱✝ : Type u_1} {Γ : 𝒱✝ → Type u_2} {x : pGCL.State Γ → ENNReal} {f : pGCL.ProbExp Γ →o pGCL.ProbExp Γ} (h₁ : x ≤ 1) (h₂ : x ≤ ⇑(f ⟨x, h₁⟩)) :

x ≤ ⇑(gfp f)

source

theorem OrderHom.le_gfp_of_iter_prob {𝒱✝ : Type u_1} {Γ : 𝒱✝ → Type u_2} {x : pGCL.State Γ → ENNReal} {f : pGCL.ProbExp Γ →o pGCL.ProbExp Γ} (k : ℕ) (h₁ : x ≤ 1) (h₂ : x ≤ ⇑(f ((fun (x_1 : pGCL.ProbExp Γ) => f x_1 ⊔ ⟨x, h₁⟩)^[k] ⟨x, h₁⟩))) :

x ≤ ⇑(gfp f)

source

def pGCL.Exp.substs_mono {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {X₁ X₂ : State Γ → ENNReal} {xs : List ((v : 𝒱) × (State Γ → Γ v))} (h : X₁ ≤ X₂) :

X₁[..xs] ≤ X₂[..xs]

Equations

⋯ = ⋯

Instances For

source

theorem pGCL.Exp.himp_mono {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} {a₁ a₂ b₁ b₂ : State Γ → ENNReal} (ha : a₂ ≤ a₁) (hb : b₁ ≤ b₂) :

a₁ ⇨ b₁ ≤ a₂ ⇨ b₂

source

theorem pGCL.Exp.hnot_mono {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} {a₁ a₂ : State Γ → ENNReal} (ha : a₂ ≤ a₁) :

￢a₁ ≤ ￢a₂

source

theorem pGCL.Exp.compl_mono {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} {a₁ a₂ : State Γ → ENNReal} (ha : a₂ ≤ a₁) :

~ a₁ ≤ ~ a₂

source

theorem pGCL.Exp.validate_mono {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} {a₁ a₂ : State Γ → ENNReal} (ha : a₁ ≤ a₂) :

▵ a₁ ≤ ▵ a₂

source

theorem pGCL.Exp.covalidate_mono {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} {a₁ a₂ : State Γ → ENNReal} (ha : a₁ ≤ a₂) :

▿ a₁ ≤ ▿ a₂

source

theorem pGCL.ENNReal.hnot_mono {a₁ a₂ : ENNReal} (ha : a₂ ≤ a₁) :

￢a₁ ≤ ￢a₂

source

theorem pGCL.ENNReal.covalidate_mono {a₁ a₂ : ENNReal} (ha : a₁ ≤ a₂) :

▿ a₁ ≤ ▿ a₂

source

@[simp]

theorem pGCL.Exp.zero_himp {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} {a : State Γ → ENNReal} :

0 ⇨ a = ⊤

source

theorem pGCL.State.subst_comm {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {σ : State Γ} {x₁ x₂ : 𝒱} {v₁ : Γ x₁} {v₂ : Γ x₂} (h : x₁ ≠ x₂) :

σ[x₁ ↦ v₁][x₂ ↦ v₂] = σ[x₂ ↦ v₂][x₁ ↦ v₁]

source

@[simp]

theorem pGCL.Exp.top_subst {𝒱 : Type u_1} {Γ : 𝒱 → Type u_3} [DecidableEq 𝒱] (xs : List ((v : 𝒱) × (State Γ → Γ v))) :

⊤[..xs] = ⊤

source

@[simp]

theorem pGCL.Exp.iver_subst {𝒱 : Type u_1} {Γ : 𝒱 → Type u_3} [DecidableEq 𝒱] {b : BExpr Γ} (xs : List ((v : 𝒱) × (State Γ → Γ v))) :

i[b][..xs] = i[b[..xs]]

source

@[simp]

theorem pGCL.Exp.not_subst {𝒱 : Type u_1} {Γ : 𝒱 → Type u_3} [DecidableEq 𝒱] {b : BExpr Γ} (xs : List ((v : 𝒱) × (State Γ → Γ v))) :

(~ b)[..xs] = ~ b[..xs]

source

@[simp]

theorem pGCL.Exp.hnot_subst {𝒱 : Type u_1} {Γ : 𝒱 → Type u_3} [DecidableEq 𝒱] {a : State Γ → ENNReal} (xs : List ((v : 𝒱) × (State Γ → Γ v))) :

(￢a)[..xs] = ￢a[..xs]

source

@[simp]

theorem pGCL.Exp.validate_subst {𝒱 : Type u_1} {Γ : 𝒱 → Type u_3} [DecidableEq 𝒱] {a : State Γ → ENNReal} (xs : List ((v : 𝒱) × (State Γ → Γ v))) :

(▵ a)[..xs] = ▵ a[..xs]

source

@[simp]

theorem pGCL.Exp.covalidate_subst {𝒱 : Type u_1} {Γ : 𝒱 → Type u_3} [DecidableEq 𝒱] {a : State Γ → ENNReal} (xs : List ((v : 𝒱) × (State Γ → Γ v))) :

(▿ a)[..xs] = ▿ a[..xs]

source

@[simp]

theorem pGCL.BExpr.eq_self {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} {a : State Γ → ENNReal} :

pgcl_bexp {@a = @a} = ↑(true = true)

source

@[simp]

theorem pGCL.BExpr.eq_of_ne {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} {a b : State Γ → ENNReal} (h : ∀ (σ : State Γ), a σ ≠ b σ) :

pgcl_bexp {@a = @b} = ↑(false = true)

source

@[simp]

theorem pGCL.BExpr.iver_coe_bool {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} {a : Prop} :

i[↑a] = ↑i[a]

source

@[simp]

theorem pGCL.BExpr.not_coe_bool {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} {a : Prop} :

~ ↑a = ↑¬a

source

noncomputable def pGCL.State.cofix {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} (σ₀ : State Γ) {S : Set 𝒱} (σ : State fun (x : ↑(~ S)) => Γ ↑x) :

State Γ

Equations

σ₀.cofix σ v = if h : v ∈ S then σ₀ v else σ ⟨v, h⟩

Instances For

source

@[simp]

theorem pGCL.State.cofix_apply_mem {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} {v : 𝒱} {S : Set 𝒱} (h : v ∈ S) (σ₀ : State Γ) (σ' : State fun (x : ↑(~ S)) => Γ ↑x) :

σ₀.cofix σ' v = σ₀ v

source

noncomputable def pGCL.Exp.fix {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} {α : Sort u_3} (X : State Γ → α) (S : Set 𝒱) (σ₀ : State Γ) :

(State fun (x : ↑(~ S)) => Γ ↑x) → α

Equations

pGCL.Exp.fix X S σ₀ σ = X (σ₀.cofix σ)

Instances For

source

@[simp]

theorem pGCL.Exp.fix_empty {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} {α : Sort u_3} {σ₀ : State Γ} {σ : State fun (x : ↑(~ ∅)) => Γ ↑x} (φ : State Γ → α) :

fix φ ∅ σ₀ σ = φ fun (x : 𝒱) => σ ⟨x, ⋯⟩

source

@[simp]

theorem pGCL.Exp.fix_compl_empty {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} {α : Sort u_3} {σ₀ : State Γ} {σ : State fun (x : ↑(~ ~ ∅)) => Γ ↑x} (φ : State Γ → α) :

fix φ (~ ∅) σ₀ σ = φ σ₀

source

@[simp]

theorem pGCL.Exp.fix_compl_empty_eq {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} {α : Sort u_3} (φ ψ : State Γ → α) :

fix φ (~ ∅) = fix ψ (~ ∅) ↔ φ = ψ

source

noncomputable def pGCL.ProbExp.fix {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} (X : ProbExp Γ) (S : Set 𝒱) (σ₀ : State Γ) :

ProbExp fun (x : ↑(~ S)) => Γ ↑x

Equations

X.fix S σ₀ = ⟨pGCL.Exp.fix (⇑X) S σ₀, ⋯⟩

Instances For

source

@[simp]

theorem pGCL.ProbExp.fix_apply {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} {S : Set 𝒱} {σ₀ : State Γ} {σ : State fun (x : ↑(~ S)) => Γ ↑x} {φ : ProbExp Γ} :

(φ.fix S σ₀) σ = φ (σ₀.cofix σ)

source

def pGCL.mods {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} :

pGCL Γ → Set 𝒱

Equations

pgcl {skip }.mods = ∅
pgcl {@x_1 := @a}.mods = {x_1}
pgcl {@C₁ ; @C₂}.mods = C₁.mods ∪ C₂.mods
pgcl {{ @C₁ } [@a] { @C₂ }}.mods = C₁.mods ∪ C₂.mods
pgcl {{ @C₁ } [] { @C₂ }}.mods = C₁.mods ∪ C₂.mods
pgcl {while @a { @C' }}.mods = C'.mods
pgcl {tick(@a)}.mods = ∅
pgcl {observe(@a)}.mods = ∅

Instances For

source

noncomputable def pGCL.fix {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} (C : pGCL Γ) (S : Set 𝒱) (σ₀ : State Γ) :

pGCL fun (x : ↑(~ S)) => Γ ↑x

Equations

pgcl {skip }.fix S σ₀ = pgcl {skip }
pgcl {@x_1 := @a}.fix S σ₀ = if hx : x_1 ∈ ~ S then pgcl {@⟨x_1, hx⟩ := @(pGCL.Exp.fix a S σ₀)} else pgcl {skip }
pgcl {@C₁ ; @C₂}.fix S σ₀ = pgcl {@(C₁.fix S σ₀) ; @(C₂.fix S σ₀)}
pgcl {{ @C₁ } [@a] { @C₂ }}.fix S σ₀ = pgcl {{ @(C₁.fix S σ₀) } [@(a.fix S σ₀)] { @(C₂.fix S σ₀) }}
pgcl {{ @C₁ } [] { @C₂ }}.fix S σ₀ = pgcl {{ @(C₁.fix S σ₀) } [] { @(C₂.fix S σ₀) }}
pgcl {while @a { @C' }}.fix S σ₀ = pgcl {while @(pGCL.Exp.fix a S σ₀) { @(C'.fix S σ₀) }}
pgcl {tick(@a)}.fix S σ₀ = pgcl {tick(@(pGCL.Exp.fix a S σ₀))}
pgcl {observe(@a)}.fix S σ₀ = pgcl {observe(@(pGCL.Exp.fix a S σ₀))}

Instances For

source

@[simp]

theorem pGCL.Exp.fix_apply {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} {α : Sort u_3} {S : Set 𝒱} {σ₀ : State Γ} {σ : State fun (x : ↑(~ S)) => Γ ↑x} {φ : State Γ → α} :

fix φ S σ₀ σ = φ (σ₀.cofix σ)

source

@[simp]

theorem pGCL.Exp.zero_fix {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} :

fix 0 = 0

source

@[simp]

theorem pGCL.Exp.top_fix {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} :

fix ⊤ = ⊤

source

@[simp]

theorem pGCL.Exp.iSup_fix {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} {α : Sort u_3} {S : Set 𝒱} {σ₀ : State Γ} {σ : State fun (x : ↑(~ S)) => Γ ↑x} {X : α → State Γ → ENNReal} :

fix (⨆ (n : α), X n) S σ₀ σ = ⨆ (n : α), fix (X n) S σ₀ σ

source

@[simp]

theorem pGCL.Exp.iInf_fix {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} {α : Sort u_3} {S : Set 𝒱} {σ₀ : State Γ} {σ : State fun (x : ↑(~ S)) => Γ ↑x} {X : α → State Γ → ENNReal} :

fix (⨅ (n : α), X n) S σ₀ σ = ⨅ (n : α), fix (X n) S σ₀ σ

source

@[simp]

theorem pGCL.Exp.subst_fix {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {α : Type u_3} {σ : State Γ} {φ : State Γ → α} {x : 𝒱} {e : State Γ → Γ x} {S : Set 𝒱} (hx : x ∉ S) :

fix (φ[x ↦ e]) S σ = (fix φ S σ)[⟨x, hx⟩ ↦ fix e S σ]

source

theorem pGCL.wp_le_of_fix {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {O : Optimization} {σ₀ : State Γ} (C : pGCL Γ) (φ : State Γ → ENNReal) (S : Set 𝒱) (X : State Γ → ENNReal) :

Exp.fix (wp[O]⟦@C⟧ φ) S σ₀ ≤ Exp.fix X S σ₀ → wp[O]⟦@C⟧ φ σ₀ ≤ X σ₀

source

theorem pGCL.le_wlp_of_fix {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {σ₀ : State Γ} {O : Optimization} (C : pGCL Γ) (φ : State Γ → ENNReal) (S : Set 𝒱) (X : State Γ → ENNReal) :

Exp.fix X S σ₀ ≤ Exp.fix (wlp[O]⟦@C⟧ φ) S σ₀ → X σ₀ ≤ wlp[O]⟦@C⟧ φ σ₀

source

theorem pGCL.le_wlp'_of_fix {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {σ₀ : State Γ} {O : Optimization} (C : pGCL Γ) (φ : ProbExp Γ) (S : Set 𝒱) (X : ProbExp Γ) :

X.fix S σ₀ ≤ (wlp'[O]⟦@C⟧ φ).fix S σ₀ → X σ₀ ≤ (wlp'[O]⟦@C⟧ φ) σ₀

source

theorem pGCL.wp_fix {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {O : Optimization} {σ₀ : State Γ} (C : pGCL Γ) (φ : State Γ → ENNReal) (S : Set 𝒱) (hS : C.mods ⊆ ~ S) :

Exp.fix (wp[O]⟦@C⟧ φ) S σ₀ = wp[O]⟦@(C.fix S σ₀)⟧ (Exp.fix φ S σ₀)

source

theorem pGCL.wlp_fix {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {O : Optimization} {σ₀ : State Γ} (C : pGCL Γ) (φ : State Γ → ENNReal) (S : Set 𝒱) (hS : C.mods ⊆ ~ S) :

Exp.fix (wlp[O]⟦@C⟧ φ) S σ₀ = wlp[O]⟦@(C.fix S σ₀)⟧ (Exp.fix φ S σ₀)

source

theorem pGCL.wlp'_fix_apply {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {O : Optimization} {σ₀ : State Γ} (C : pGCL Γ) (φ : ProbExp Γ) (S : Set 𝒱) (hS : C.mods ⊆ ~ S) (σ : State fun (x : ↑(~ S)) => Γ ↑x) :

Exp.fix (⇑(wlp'[O]⟦@C⟧ φ)) S σ₀ σ = (wlp'[O]⟦@(C.fix S σ₀)⟧ ⟨Exp.fix (⇑φ) S σ₀, ⋯⟩) σ

source

theorem pGCL.wlp'_fix_apply' {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {O : Optimization} {σ₀ : State Γ} (C : pGCL Γ) (φ : State Γ → ENNReal) (hφ : φ ≤ 1) (S : Set 𝒱) (hS : C.mods ⊆ ~ S) (σ : State fun (x : ↑(~ S)) => Γ ↑x) :

Exp.fix (⇑(wlp'[O]⟦@C⟧ ⟨φ, hφ⟩)) S σ₀ σ = (wlp'[O]⟦@(C.fix S σ₀)⟧ ⟨Exp.fix φ S σ₀, ⋯⟩) σ

source

theorem pGCL.wlp'_fix {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {O : Optimization} {σ₀ : State Γ} (C : pGCL Γ) (φ : ProbExp Γ) (S : Set 𝒱) (hS : C.mods ⊆ ~ S) :

(wlp'[O]⟦@C⟧ φ).fix S σ₀ = wlp'[O]⟦@(C.fix S σ₀)⟧ (φ.fix S σ₀)