@[reducible, inline]

abbrev Globals : Type

Equations

• Globals = Finset HeyLo.Ident

def Globals.fresh (G : Globals) (α : HeyLo.Ty) : Globals × HeyLo.Ident

Equations

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

@[simp]

theorem Globals.fresh_type {ty : HeyLo.Ty} (G : Globals) : (G.fresh ty).2.type = ty

@[simp]

theorem Globals.fresh_update {ty : HeyLo.Ty} (G : Globals) : (G.fresh ty).1 = insert (G.fresh ty).2 G

@[simp]

theorem Globals.fresh_not_in {ty : HeyLo.Ty} (G : Globals) : (G.fresh ty).2 ∉ G

def Globals.«termLet_fresh_:_←__» : Lean.ParserDescr

Generate a fresh variables given some global.

This is a macro to ensure definitional equality of the generated idents type.

Equations

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

def HeyLo.fv {α : Ty} (C : HeyLo α) : Globals

Equations

• (HeyLo.Binary a S₁ S₂).fv = S₁.fv ∪ S₂.fv
• (HeyLo.Lit a).fv = ∅
• (HeyLo.Subst v e m).fv = {v} ∪ e.fv ∪ m.fv
• (HeyLo.Call a m).fv = m.fv
• (HeyLo.Quant a x m).fv = {x} ∪ m.fv
• (b.Ite l r).fv = b.fv ∪ l.fv ∪ r.fv
• (HeyLo.Var x α).fv = {{ name := x, type := α }}
• (HeyLo.Unary a m).fv = m.fv

def HeyLo.Distribution.fv {α : Ty} (D : Distribution α) : Globals

Equations

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

def spGCL.fv (C : spGCL) : Globals

Equations

• (S₁.seq S₂).fv = S₁.fv ∪ S₂.fv
• spGCL.skip.fv = ∅
• (spGCL.observe o).fv = o.fv
• (spGCL.tick r).fv = r.fv
• (spGCL.ite b S₁ S₂).fv = b.fv ∪ S₁.fv ∪ S₂.fv
• (spGCL.loop b c I).fv = b.fv ∪ c.fv ∪ I.fv
• (S₁.nonDet S₂).fv = S₁.fv ∪ S₂.fv
• (S₁.prob p S₂).fv = S₁.fv ∪ p.fv ∪ S₂.fv
• (spGCL.assign x e).fv = {x} ∪ e.fv

def HeyVL.fv (C : HeyVL) : Globals

Equations

• (S₁ ;; S₂).fv = S₁.fv ∪ S₂.fv
• HeyVL.Covalidate.fv = ∅
• (HeyVL.Cohavoc x).fv = {x}
• (HeyVL.Coassume x).fv = x.fv
• (HeyVL.Coassert x).fv = x.fv
• (l.IfSup r).fv = l.fv ∪ r.fv
• HeyVL.Validate.fv = ∅
• (HeyVL.Havoc x).fv = {x}
• (HeyVL.Assume x).fv = x.fv
• (HeyVL.Assert x).fv = x.fv
• (l.IfInf r).fv = l.fv ∪ r.fv
• (HeyVL.Reward x).fv = x.fv
• (HeyVL.Assign x e).fv = {x} ∪ e.fv

def spGCL.mods (C : spGCL) : Globals

Equations

• (S₁.seq S₂).mods = S₁.mods ∪ S₂.mods
• spGCL.skip.mods = ∅
• (spGCL.observe a).mods = ∅
• (spGCL.tick a).mods = ∅
• (spGCL.loop a a_1 c).mods = c.mods
• (spGCL.ite a S₁ S₂).mods = S₁.mods ∪ S₂.mods
• (S₁.nonDet S₂).mods = S₁.mods ∪ S₂.mods
• (S₁.prob a S₂).mods = S₁.mods ∪ S₂.mods
• (spGCL.assign x a).mods = {x}

def HeyVL.mods (C : HeyVL) : Globals

Equations

• (S₁ ;; S₂).mods = S₁.mods ∪ S₂.mods
• (l.IfSup r).mods = l.mods ∪ r.mods
• (l.IfInf r).mods = l.mods ∪ r.mods
• (HeyVL.Assign x μ).mods = {x}
• HeyVL.Covalidate.mods = ∅
• (HeyVL.Cohavoc x).mods = ∅
• (HeyVL.Coassume φ).mods = ∅
• (HeyVL.Coassert φ).mods = ∅
• HeyVL.Validate.mods = ∅
• (HeyVL.Havoc x).mods = ∅
• (HeyVL.Assume φ).mods = ∅
• (HeyVL.Assert φ).mods = ∅
• (HeyVL.Reward a).mods = ∅

def spGCL.invs (C : spGCL) : Finset (HeyLo HeyLo.Ty.ENNReal)

Equations

• (S₁.seq S₂).invs = S₁.invs ∪ S₂.invs
• spGCL.skip.invs = ∅
• (spGCL.observe a).invs = ∅
• (spGCL.tick a).invs = ∅
• (spGCL.loop a a_1 c).invs = insert a_1 c.invs
• (spGCL.ite a S₁ S₂).invs = S₁.invs ∪ S₂.invs
• (S₁.nonDet S₂).invs = S₁.invs ∪ S₂.invs
• (S₁.prob a S₂).invs = S₁.invs ∪ S₂.invs
• (spGCL.assign x a).invs = ∅

def spGCL.invsList_aux (C : spGCL) : List (HeyLo HeyLo.Ty.ENNReal)

Equations

• (S₁.seq S₂).invsList_aux = S₁.invsList_aux ++ S₂.invsList_aux
• spGCL.skip.invsList_aux = ∅
• (spGCL.observe a).invsList_aux = ∅
• (spGCL.tick a).invsList_aux = ∅
• (spGCL.loop a a_1 c).invsList_aux = a_1 :: c.invsList_aux
• (spGCL.ite a S₁ S₂).invsList_aux = S₁.invsList_aux ++ S₂.invsList_aux
• (S₁.nonDet S₂).invsList_aux = S₁.invsList_aux ++ S₂.invsList_aux
• (S₁.prob a S₂).invsList_aux = S₁.invsList_aux ++ S₂.invsList_aux
• (spGCL.assign x a).invsList_aux = ∅

def spGCL.invsList (C : spGCL) : List (HeyLo HeyLo.Ty.ENNReal)

Equations

• C.invsList = C.invsList_aux.dedup

@[simp]

theorem spGCL.mem_invsList_iff {C : spGCL} {I : HeyLo HeyLo.Ty.ENNReal} : I ∈ C.invsList ↔ I ∈ C.invs

@[simp]

theorem HeyVL.mods_subset_fv (C : HeyVL) : C.mods ⊆ C.fv

@[simp]

theorem HeyVL.Skip_fv : Skip.fv = ∅

@[simp]

theorem HeyVL.Havocs_fv {xs : List HeyLo.Ident} : (Havocs xs).fv = xs.toFinset

@[simp]

theorem HeyVL.Cohavocs_fv {xs : List HeyLo.Ident} : (Cohavocs xs).fv = xs.toFinset

@[simp]

theorem HeyLo.subst_fv {α : Ty} {x : Ident} (φ : HeyLo α) (y : HeyLo x.type) : φ[x ↦ y].fv = {x} ∪ φ.fv ∪ y.fv

@[simp]

theorem HeyLo.Distribution.toExpr_fv {μ : Distribution Ty.ENNReal} : μ.toExpr.fv = μ.fv

@[simp]

theorem HeyLo.fv_inf {X Y : HeyLo Ty.ENNReal} : (X ⊓ Y).fv = X.fv ∪ Y.fv