Small step operational semantics for pGCL

Main definitions

• pGCL.SmallStep: The inductive definition of the probabilistic small step semantics of pGCL.

inductive pGCL.SmallStep {ϖ : Type u_1} [DecidableEq ϖ] : Conf ϖ → Act → ENNReal → Conf ϖ → Prop

Probabilistic small step operational semantics for pGCL

• bot {ϖ : Type u_1} [DecidableEq ϖ] : none ⤳[Act.N,1] none
• skip {ϖ : Type u_1} [DecidableEq ϖ] {σ : States ϖ} : ·⟨pGCL.skip,σ⟩ ⤳[Act.N,1] some (none, σ)
• sink {ϖ : Type u_1} [DecidableEq ϖ] {σ : States ϖ} : some (none, σ) ⤳[Act.N,1] none
• assign {ϖ : Type u_1} [DecidableEq ϖ] {x : ϖ} {e : Exp ϖ} {σ : States ϖ} : ·⟨x ::= e,σ⟩ ⤳[Act.N,1] ·⟨pGCL.skip,σ[x ↦ e σ]⟩
• prob {ϖ : Type u_1} [DecidableEq ϖ] {C : pGCL ϖ} {p : ProbExp ϖ} {σ : States ϖ} : ·⟨C ·[p] C,σ⟩ ⤳[Act.N,1] ·⟨C,σ⟩
• prob_L {ϖ : Type u_1} [DecidableEq ϖ] {C₁ C₂ : pGCL ϖ} {p : ProbExp ϖ} {σ : States ϖ} (h : ¬C₁ = C₂) (h' : 0 < ↑p σ) : ·⟨C₁ ·[p] C₂,σ⟩ ⤳[Act.N,↑p σ] ·⟨C₁,σ⟩
• prob_R {ϖ : Type u_1} [DecidableEq ϖ] {C₁ C₂ : pGCL ϖ} {p : ProbExp ϖ} {σ : States ϖ} (h : ¬C₁ = C₂) (h' : ↑p σ < 1) : ·⟨C₁ ·[p] C₂,σ⟩ ⤳[Act.N,1 - ↑p σ] ·⟨C₂,σ⟩
• nonDet_L {ϖ : Type u_1} [DecidableEq ϖ] {C₁ C₂ : pGCL ϖ} {σ : States ϖ} : ·⟨C₁ ·[] C₂,σ⟩ ⤳[Act.L,1] ·⟨C₁,σ⟩
• nonDet_R {ϖ : Type u_1} [DecidableEq ϖ] {C₁ C₂ : pGCL ϖ} {σ : States ϖ} : ·⟨C₁ ·[] C₂,σ⟩ ⤳[Act.R,1] ·⟨C₂,σ⟩
• tick {ϖ : Type u_1} [DecidableEq ϖ] {r : Exp ϖ} {σ : States ϖ} : ·⟨pGCL.tick r,σ⟩ ⤳[Act.N,1] ·⟨pGCL.skip,σ⟩
• seq_L {ϖ : Type u_1} [DecidableEq ϖ] {C₂ : pGCL ϖ} {σ : States ϖ} : ·⟨pGCL.skip ;; C₂,σ⟩ ⤳[Act.N,1] ·⟨C₂,σ⟩
• seq_R {ϖ : Type u_1} [DecidableEq ϖ] {C₁ : pGCL ϖ} {σ : States ϖ} {α : Act} {p : ENNReal} {C₁' : pGCL ϖ} {τ : States ϖ} {C₂ : pGCL ϖ} : (·⟨C₁,σ⟩ ⤳[α,p] ·⟨C₁',τ⟩) → ·⟨C₁ ;; C₂,σ⟩ ⤳[α,p] ·⟨C₁' ;; C₂,τ⟩
• loop {ϖ : Type u_1} [DecidableEq ϖ] {b : BExpr ϖ} {C : pGCL ϖ} {σ : States ϖ} : ¬b σ = true → ·⟨pGCL.loop b C,σ⟩ ⤳[Act.N,1] ·⟨pGCL.skip,σ⟩
• loop' {ϖ : Type u_1} [DecidableEq ϖ] {b : BExpr ϖ} {C : pGCL ϖ} {σ : States ϖ} : b σ = true → ·⟨pGCL.loop b C,σ⟩ ⤳[Act.N,1] ·⟨C ;; pGCL.loop b C,σ⟩

def pGCL.«term_⤳[_,_]_» : Lean.TrailingParserDescr

Probabilistic small step operational semantics for pGCL

Equations

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

@[simp]

theorem pGCL.SmallStep.p_pos {ϖ : Type u_1} [DecidableEq ϖ] {c : Conf ϖ} {α : Act} {p : ENNReal} {c' : Conf ϖ} (h : c ⤳[α,p] c') : 0 < p

@[simp]

theorem pGCL.SmallStep.p_ne_zero {ϖ : Type u_1} [DecidableEq ϖ] {c : Conf ϖ} {α : Act} {p : ENNReal} {c' : Conf ϖ} (h : c ⤳[α,p] c') : ¬p = 0

@[simp]

theorem pGCL.SmallStep.p_le_one {ϖ : Type u_1} [DecidableEq ϖ] {c : Conf ϖ} {α : Act} {p : ENNReal} {c' : Conf ϖ} (h : c ⤳[α,p] c') : p ≤ 1

@[simp]

theorem pGCL.SmallStep.skip_iff {ϖ : Type u_1} [DecidableEq ϖ] {c : Conf ϖ} {σ : States ϖ} {α : Act} {p : ENNReal} : (·⟨pGCL.skip,σ⟩ ⤳[α,p] c) ↔ p = 1 ∧ α = Act.N ∧ c = some (none, σ)

@[simp]

theorem pGCL.SmallStep.sink_iff {ϖ : Type u_1} [DecidableEq ϖ] {c : Conf ϖ} {σ : States ϖ} {α : Act} {p : ENNReal} : (some (none, σ) ⤳[α,p] c) ↔ p = 1 ∧ α = Act.N ∧ c = none

@[simp]

theorem pGCL.SmallStep.none_iff {ϖ : Type u_1} [DecidableEq ϖ] {c : Conf ϖ} {α : Act} {p : ENNReal} : (none ⤳[α,p] c) ↔ p = 1 ∧ α = Act.N ∧ c = none

@[simp]

theorem pGCL.SmallStep.to_bot {ϖ : Type u_1} [DecidableEq ϖ] {c : Conf ϖ} {α : Act} {p : ENNReal} : (c ⤳[α,p] none) ↔ ∃ (σ : States ϖ), p = 1 ∧ α = Act.N ∧ (c = some (none, σ) ∨ c = none)

@[simp]

theorem pGCL.SmallStep.to_sink {ϖ : Type u_1} [DecidableEq ϖ] {c : Conf ϖ} {σ : States ϖ} {α : Act} {p : ENNReal} : (c ⤳[α,p] some (none, σ)) ↔ p = 1 ∧ α = Act.N ∧ c = ·⟨pGCL.skip,σ⟩

@[simp]

theorem pGCL.SmallStep.assign_iff {ϖ : Type u_1} [DecidableEq ϖ] {σ : States ϖ} {x : ϖ} {e : Exp ϖ} {α : Act} {p : ENNReal} {c' : Conf ϖ} : (·⟨x ::= e,σ⟩ ⤳[α,p] c') ↔ p = 1 ∧ α = Act.N ∧ c' = ·⟨pGCL.skip,σ[x ↦ e σ]⟩

@[simp]

theorem pGCL.SmallStep.prob_iff {ϖ : Type u_1} [DecidableEq ϖ] {σ : States ϖ} {C₁ : pGCL ϖ} {p : ProbExp ϖ} {C₂ : pGCL ϖ} {α : Act} {p' : ENNReal} {c' : Conf ϖ} : (·⟨C₁ ·[p] C₂,σ⟩ ⤳[α,p'] c') ↔ α = Act.N ∧ if C₁ = C₂ then p' = 1 ∧ c' = ·⟨C₁,σ⟩ else p' = ↑p σ ∧ 0 < p' ∧ c' = ·⟨C₁,σ⟩ ∨ p' = 1 - ↑p σ ∧ 0 < p' ∧ c' = ·⟨C₂,σ⟩

@[simp]

theorem pGCL.SmallStep.nonDet_iff {ϖ : Type u_1} [DecidableEq ϖ] {σ : States ϖ} {C₁ C₂ : pGCL ϖ} {α : Act} {p' : ENNReal} {c' : Conf ϖ} : (·⟨C₁ ·[] C₂,σ⟩ ⤳[α,p'] c') ↔ p' = 1 ∧ (α = Act.L ∧ c' = ·⟨C₁,σ⟩ ∨ α = Act.R ∧ c' = ·⟨C₂,σ⟩)

@[simp]

theorem pGCL.SmallStep.tick_iff {ϖ : Type u_1} [DecidableEq ϖ] {σ : States ϖ} {r : Exp ϖ} {α : Act} {p : ENNReal} {c' : Conf ϖ} : (·⟨pGCL.tick r,σ⟩ ⤳[α,p] c') ↔ p = 1 ∧ α = Act.N ∧ c' = ·⟨pGCL.skip,σ⟩

@[simp]

theorem pGCL.SmallStep.seq_iff {ϖ : Type u_1} [DecidableEq ϖ] {σ : States ϖ} {C₁ C₂ : pGCL ϖ} {α : Act} {p : ENNReal} {c' : Conf ϖ} : (·⟨C₁ ;; C₂,σ⟩ ⤳[α,p] c') ↔ if C₁ = pGCL.skip then p = 1 ∧ α = Act.N ∧ c' = ·⟨C₂,σ⟩ else ∃ (C' : pGCL ϖ) (σ' : States ϖ), (·⟨C₁,σ⟩ ⤳[α,p] ·⟨C',σ'⟩) ∧ c' = ·⟨C' ;; C₂,σ'⟩

@[simp]

theorem pGCL.SmallStep.loop_iff {ϖ : Type u_1} [DecidableEq ϖ] {σ : States ϖ} {b : BExpr ϖ} {C : pGCL ϖ} {α : Act} {p : ENNReal} {c' : Conf ϖ} : (·⟨pGCL.loop b C,σ⟩ ⤳[α,p] c') ↔ p = 1 ∧ α = Act.N ∧ c' = if b σ = true then ·⟨C ;; pGCL.loop b C,σ⟩ else ·⟨pGCL.skip,σ⟩

def pGCL.SmallStep.act {ϖ : Type u_1} [DecidableEq ϖ] (c : Conf ϖ) : Set Act

Equations

• pGCL.SmallStep.act c = {α : pGCL.Act | ∃ (p : ENNReal) (c' : pGCL.Conf ϖ), c ⤳[α,p] c'}

noncomputable instance pGCL.SmallStep.instDecidableMemActSetAct {ϖ : Type u_1} [DecidableEq ϖ] {c : Conf ϖ} {α : Act} : Decidable (α ∈ act c)

Equations

• pGCL.SmallStep.instDecidableMemActSetAct = Classical.propDecidable (α ∈ pGCL.SmallStep.act c)

instance pGCL.SmallStep.instFiniteElemActAct {ϖ : Type u_1} [DecidableEq ϖ] {c : Conf ϖ} : Finite ↑(act c)

noncomputable instance pGCL.SmallStep.instFintypeElemActAct {ϖ : Type u_1} [DecidableEq ϖ] {c : Conf ϖ} : Fintype ↑(act c)

Equations

• pGCL.SmallStep.instFintypeElemActAct = Fintype.ofFinite ↑(pGCL.SmallStep.act c)

@[simp]

theorem pGCL.SmallStep.exists_succ_iff {ϖ : Type u_1} [DecidableEq ϖ] {σ : States ϖ} {α : Act} {p : ENNReal} {C : pGCL ϖ} (h : ¬C = pGCL.skip) : (∃ (c' : Conf ϖ), ·⟨C,σ⟩ ⤳[α,p] c') ↔ ∃ (C' : pGCL ϖ) (σ' : States ϖ), ·⟨C,σ⟩ ⤳[α,p] ·⟨C',σ'⟩

@[simp]

theorem pGCL.SmallStep.act_bot {ϖ : Type u_1} [DecidableEq ϖ] : act none = {Act.N}

@[simp]

theorem pGCL.SmallStep.act_sink {ϖ : Type u_1} [DecidableEq ϖ] {σ : States ϖ} : act (some (none, σ)) = {Act.N}

@[simp]

theorem pGCL.SmallStep.act_skip {ϖ : Type u_1} [DecidableEq ϖ] {σ : States ϖ} : act (·⟨pGCL.skip,σ⟩) = {Act.N}

@[simp]

theorem pGCL.SmallStep.act_assign {ϖ : Type u_1} [DecidableEq ϖ] {σ : States ϖ} {x : ϖ} {e : Exp ϖ} : act (·⟨x ::= e,σ⟩) = {Act.N}

@[simp]

theorem pGCL.SmallStep.act_seq {ϖ : Type u_1} [DecidableEq ϖ] {σ : States ϖ} {C₁ C₂ : pGCL ϖ} : act (·⟨C₁ ;; C₂,σ⟩) = act (·⟨C₁,σ⟩)

@[simp]

theorem pGCL.SmallStep.act_prob {ϖ : Type u_1} [DecidableEq ϖ] {σ : States ϖ} {C₁ : pGCL ϖ} {p : ProbExp ϖ} {C₂ : pGCL ϖ} : act (·⟨C₁ ·[p] C₂,σ⟩) = {Act.N}

@[simp]

theorem pGCL.SmallStep.act_nonDet {ϖ : Type u_1} [DecidableEq ϖ] {σ : States ϖ} {C₁ C₂ : pGCL ϖ} : act (·⟨C₁ ·[] C₂,σ⟩) = {Act.L, Act.R}

@[simp]

theorem pGCL.SmallStep.act_loop {ϖ : Type u_1} [DecidableEq ϖ] {σ : States ϖ} {b : BExpr ϖ} {C : pGCL ϖ} : act (·⟨pGCL.loop b C,σ⟩) = {Act.N}

@[simp]

theorem pGCL.SmallStep.act_tick {ϖ : Type u_1} [DecidableEq ϖ] {σ : States ϖ} {r : Exp ϖ} : act (·⟨pGCL.tick r,σ⟩) = {Act.N}

instance pGCL.SmallStep.act_nonempty {ϖ : Type u_1} [DecidableEq ϖ] (s : Conf ϖ) : Nonempty ↑(act s)

theorem pGCL.SmallStep.progress {ϖ : Type u_1} [DecidableEq ϖ] (s : Conf ϖ) : ∃ (p : ENNReal) (a : Act) (x : Conf ϖ), s ⤳[a,p] x

@[simp]

theorem pGCL.SmallStep.iInf_act_const {ϖ : Type u_1} [DecidableEq ϖ] {C : Conf ϖ} {x : ENNReal} : ⨅ α ∈ act C, x = x

noncomputable instance pGCL.SmallStep.instDecidable {ϖ : Type u_1} [DecidableEq ϖ] {c : Conf ϖ} {α : Act} {p : ENNReal} {c' : Conf ϖ} : Decidable (c ⤳[α,p] c')

Equations

• pGCL.SmallStep.instDecidable = Classical.propDecidable (c ⤳[α,p] c')

noncomputable instance pGCL.SmallStep.instDecidableExistsActENNReal {ϖ : Type u_1} [DecidableEq ϖ] {c c' : Conf ϖ} : Decidable (∃ (α : Act) (p : ENNReal), c ⤳[α,p] c')

Equations

• pGCL.SmallStep.instDecidableExistsActENNReal = Classical.propDecidable (∃ (α : pGCL.Act) (p : ENNReal), c ⤳[α,p] c')

@[simp]

theorem pGCL.SmallStep.tsum_p {ϖ : Type u_1} [DecidableEq ϖ] {c : Conf ϖ} {α : Act} {c' : Conf ϖ} : ∑' (p : { p : ENNReal // c ⤳[α,p] c' }), ↑p = ∑' (p : ENNReal), if c ⤳[α,p] c' then p else 0

def pGCL.SmallStep.succs {ϖ : Type u_1} [DecidableEq ϖ] (c : Conf ϖ) (α : Act) : Set (Conf ϖ)

Equations

• pGCL.SmallStep.succs c α = {c' : pGCL.Conf ϖ | ∃ (p : ENNReal), c ⤳[α,p] c'}

@[irreducible]

noncomputable def pGCL.SmallStep.succs_fin {ϖ : Type u_1} [DecidableEq ϖ] (c : Conf ϖ) (α : Act) : Finset (Conf ϖ)

Equations

• pGCL.SmallStep.succs_fin none pGCL.Act.N = {none}
• pGCL.SmallStep.succs_fin (some (none, snd)) pGCL.Act.N = {none}
• pGCL.SmallStep.succs_fin (·⟨pGCL.skip,σ⟩) pGCL.Act.N = {some (none, σ)}
• pGCL.SmallStep.succs_fin (·⟨pGCL.tick a,σ⟩) pGCL.Act.N = {·⟨pGCL.skip,σ⟩}
• pGCL.SmallStep.succs_fin (·⟨x ::= E,σ⟩) pGCL.Act.N = {·⟨pGCL.skip,σ[x ↦ E σ]⟩}
• pGCL.SmallStep.succs_fin (·⟨C₁ ·[p] C₂,σ⟩) pGCL.Act.N = if ↑p σ = 0 then {·⟨C₂,σ⟩} else if ↑p σ = 1 then {·⟨C₁,σ⟩} else {·⟨C₁,σ⟩, ·⟨C₂,σ⟩}
• pGCL.SmallStep.succs_fin (·⟨C₁ ·[] a,σ⟩) pGCL.Act.L = {·⟨C₁,σ⟩}
• pGCL.SmallStep.succs_fin (·⟨a ·[] C₂,σ⟩) pGCL.Act.R = {·⟨C₂,σ⟩}
• pGCL.SmallStep.succs_fin (·⟨pGCL.loop b C,σ⟩) pGCL.Act.N = if b σ = true then {·⟨C ;; pGCL.loop b C,σ⟩} else {·⟨pGCL.skip,σ⟩}
• pGCL.SmallStep.succs_fin (·⟨pGCL.skip ;; C₂,σ⟩) pGCL.Act.N = {·⟨C₂,σ⟩}
• pGCL.SmallStep.succs_fin (·⟨C₁ ;; C₂,σ⟩) α = Finset.map { toFun := C₂.after, inj' := ⋯ } (pGCL.SmallStep.succs_fin (·⟨C₁,σ⟩) α)
• pGCL.SmallStep.succs_fin c α = ∅

theorem pGCL.SmallStep.succs_eq_succs_fin {ϖ : Type u_1} [DecidableEq ϖ] {c : Conf ϖ} {α : Act} : succs c α = ↑(succs_fin c α)

theorem pGCL.SmallStep.sums_to_one {ϖ : Type u_1} [DecidableEq ϖ] {c : Conf ϖ} {α : Act} {p₀ : ENNReal} {c₀ : Conf ϖ} (h₀ : c ⤳[α,p₀] c₀) : ∑' (c' : Conf ϖ) (p : { p : ENNReal // c ⤳[α,p] c' }), ↑p = 1