@[simp]

theorem HeyLo.ofNat_ident (n : String) : OfNat.ofNat 0 = 0

@[simp]

theorem HeyLo.ofNat_sem {σ : pGCL.State Ty.Γ} (n : ℕ) : ⟦@(OfNat.ofNat n)⟧' σ = n

@[simp]

theorem HeyLo.nat_zero_sem : ⟦0⟧' = 0

@[simp]

theorem HeyLo.nat_one_sem : ⟦1⟧' = 1

@[simp]

theorem HeyLo.sem_zero : ⟦0⟧' = 0

@[simp]

theorem HeyLo.sem_one : ⟦1⟧' = 1

@[simp]

theorem HeyLo.sem_var {a : String} {t : Ty} {σ : pGCL.State Ty.Γ} : ⟦@(Var a t)⟧' σ = σ { name := a, type := t }

@[simp]

theorem HeyLo.sem_binop {α : Ty} {A B : HeyLo α} {a✝ : Ty} {op : BinOp α a✝} : ⟦@(Binary op A B)⟧' = op.sem ⟦@A⟧' ⟦@B⟧'

@[simp]

theorem HeyLo.sem_unop {α : Ty} {A : HeyLo α} {a✝ : Ty} {op : UnOp α a✝} : ⟦@(Unary op A)⟧' = op.sem ⟦@A⟧'

@[simp]

theorem HeyLo.sem_eq {α : Ty} {A B : HeyLo α} : (⟦@A = @B⟧') = fun (σ : pGCL.State Ty.Γ) => ⟦@A⟧' σ = ⟦@B⟧' σ

@[simp]

theorem HeyLo.sem_add_apply {A B : HeyLo Ty.ENNReal} : ⟦@A + @B⟧' = ⟦@A⟧' + ⟦@B⟧'

@[simp]

theorem HeyLo.sem_sub_apply {A B : HeyLo Ty.ENNReal} : ⟦@A - @B⟧' = ⟦@A⟧' - ⟦@B⟧'

@[simp]

theorem HeyLo.sem_mul_apply {A B : HeyLo Ty.ENNReal} : ⟦@A * @B⟧' = ⟦@A⟧' * ⟦@B⟧'

@[simp]

theorem HeyLo.sem_inf_apply {A B : HeyLo Ty.ENNReal} : ⟦@(A ⊓ B)⟧' = ⟦@A⟧' ⊓ ⟦@B⟧'

@[simp]

theorem HeyLo.sem_sup_apply {A B : HeyLo Ty.ENNReal} : ⟦@(A ⊔ B)⟧' = ⟦@A⟧' ⊔ ⟦@B⟧'

@[simp]

theorem HeyLo.sem_lit_apply {a✝ : Ty} {l : Literal a✝} : ⟦@(Lit l)⟧' = l.sem

@[simp]

theorem HeyLo.sem_validate {A : HeyLo Ty.ENNReal} : ⟦@(▵ A)⟧' = ▵ ⟦@A⟧'

@[simp]

theorem HeyLo.sem_covalidate {A : HeyLo Ty.ENNReal} : ⟦@(▿ A)⟧' = ▿ ⟦@A⟧'

@[simp]

theorem HeyLo.sem_hnot_apply {A : HeyLo Ty.ENNReal} : ⟦@(￢A)⟧' = ￢⟦@A⟧'

@[simp]

theorem HeyLo.sem_compl {A : HeyLo Ty.ENNReal} : ⟦@(~ A)⟧' = ~ ⟦@A⟧'

@[simp]

theorem HeyLo.sem_himp_apply {A B : HeyLo Ty.ENNReal} : ⟦@(A ⇨ B)⟧' = ⟦@A⟧' ⇨ ⟦@B⟧'

@[simp]

theorem HeyLo.sem_sdiff_apply {A B : HeyLo Ty.ENNReal} : ⟦@(A \ B)⟧' = ⟦@A⟧' \ ⟦@B⟧'

@[simp]

theorem HeyLo.sem_subst_apply' {A : HeyLo Ty.ENNReal} {xs : List ((v : Ident) × HeyLo v.type)} : ⟦@(A[..xs])⟧' = ⟦@A⟧'[..List.map (fun (x : (v : Ident) × HeyLo v.type) => ⟨x.fst, ⟦@x.snd⟧'⟩) xs]

@[simp]

theorem HeyLo.sem_subst_apply {x : Ident} {P : HeyLo Ty.Bool} {X : HeyLo x.type} {σ : pGCL.State Ty.Γ} : ⟦@(P[x ↦ X])⟧' σ = ⟦@P⟧' (σ[x ↦ ⟦@X⟧' σ])

@[simp]

theorem HeyLo.sem_iver {P : HeyLo Ty.Bool} : ⟦@P.iver⟧' = i[⟦@P⟧']

@[simp]

theorem HeyLo.sem_embed {P : HeyLo Ty.Bool} : ⟦@P.embed⟧' = i[⟦@P⟧'] * ⊤

@[simp]

theorem HeyLo.sem_not_apply {P : HeyLo Ty.Bool} : ⟦@P.not⟧' = ￢⟦@P⟧'

@[simp]

theorem HeyLo.substs_inf {xs : List ((a : Ident) × (pGCL.State Ty.Γ → Ty.Γ a))} {A B : HeyLo Ty.ENNReal} : ⟦@(A ⊓ B)⟧'[..xs] = ⟦@A⟧'[..xs] ⊓ ⟦@B⟧'[..xs]

@[simp]

theorem Distribution.map_toExpr_apply {σ : pGCL.State HeyLo.Ty.Γ} (x : HeyLo.Ident) (μ : HeyLo.Distribution x.type) (f : HeyLo x.type → HeyLo HeyLo.Ty.ENNReal) : ⟦@(μ.map f).toExpr⟧' σ = (Array.map (fun (x_1 : HeyLo HeyLo.Ty.ENNReal × HeyLo x.type) => match x_1 with | (a, b) => ⟦@a⟧' σ * ⟦@(f b)⟧' σ) μ.values).sum

@[simp]

theorem HeyLo.Var_sem_subst {n : String} {t : Ty} {x : Ident} {v : pGCL.State Ty.Γ → Ty.Γ x} : ⟦@(Var n t)⟧'[x ↦ v] = if h : x = { name := n, type := t } then cast ⋯ v else fun (x : pGCL.State Ty.Γ) => x { name := n, type := t }

def Substitution.applied (σ : pGCL.State fun (x : HeyLo.Ident) => x.type.lit) (xs : List ((v : HeyLo.Ident) × (pGCL.State HeyLo.Ty.Γ → v.type.lit))) : pGCL.State fun (x : HeyLo.Ident) => x.type.lit

Equations

• Substitution.applied σ [] = σ
• Substitution.applied σ (x :: xs_2) = Substitution.applied (σ[x.fst ↦ x.snd σ]) xs_2

theorem BExpr.subst_applied {b : pGCL.BExpr fun (x : HeyLo.Ident) => x.type.lit} {xs : List ((v : HeyLo.Ident) × (pGCL.State HeyLo.Ty.Γ → v.type.lit))} : b[..xs] = fun (σ : pGCL.State fun (x : HeyLo.Ident) => x.type.lit) => b (Substitution.applied σ xs)

theorem BExpr.subst_apply {σ : pGCL.State fun (x : HeyLo.Ident) => x.type.lit} {b : pGCL.BExpr fun (x : HeyLo.Ident) => x.type.lit} {xs : List ((v : HeyLo.Ident) × (pGCL.State HeyLo.Ty.Γ → v.type.lit))} : (b[..xs]) σ = b (Substitution.applied σ xs)

theorem Exp.subst_applied {α : Type u_1} {b : pGCL.State HeyLo.Ty.Γ → α} {xs : List ((v : HeyLo.Ident) × (pGCL.State HeyLo.Ty.Γ → v.type.lit))} : b[..xs] = fun (σ : pGCL.State fun (x : HeyLo.Ident) => x.type.lit) => b (Substitution.applied σ xs)

theorem Exp.subst_apply {α : Type u_1} {σ : pGCL.State HeyLo.Ty.Γ} {b : pGCL.State HeyLo.Ty.Γ → α} {xs : List ((v : HeyLo.Ident) × (pGCL.State HeyLo.Ty.Γ → v.type.lit))} : (b[..xs]) σ = b (Substitution.applied σ xs)

structure HeyVL.Subs (Vars : List HeyLo.Ident) (hn : Vars.Nodup) : Type

• values : List ((x : HeyLo.Ident) × x.type.lit)
• prop : Vars.length = self.values.length
• prop' (i : Fin Vars.length) : self.values[i].fst = Vars[i]

@[implicit_reducible]

instance instInhabitedSubs {xs : List HeyLo.Ident} {hn : xs.Nodup} : Inhabited (HeyVL.Subs xs hn)

Equations

• instInhabitedSubs = { default := { values := List.map (fun (x : HeyLo.Ident) => ⟨x, default⟩) xs, prop := ⋯, prop' := ⋯ } }

@[simp]

theorem HeyVL.Subs.values_nil {hn : [].Nodup} (S : Subs [] hn) : S.values = []

def HeyVL.Subs.cons {xs : List HeyLo.Ident} {hn : xs.Nodup} (S : Subs xs hn) (x : HeyLo.Ident) (v : x.type.lit) (hv : x ∉ xs) : Subs (x :: xs) ⋯

Equations

• S.cons x v hv = { values := ⟨x, v⟩ :: S.values, prop := ⋯, prop' := ⋯ }

def HeyVL.Subs.tail {x : HeyLo.Ident} {xs : List HeyLo.Ident} {hn : (x :: xs).Nodup} (S : Subs (x :: xs) hn) : x.type.lit × Subs xs ⋯

Equations

• S.tail = (cast ⋯ S.values[0].snd, { values := S.values.tail, prop := ⋯, prop' := ⋯ })

theorem HeyVL.Subs.tail_bij {x : HeyLo.Ident} {xs : List HeyLo.Ident} {hn : (x :: xs).Nodup} : Function.Bijective tail

@[simp]

theorem HeyVL.Subs.values_length {xs : List HeyLo.Ident} {hn : xs.Nodup} (S : Subs xs hn) : S.values.length = xs.length

def HeyVL.Subs.help {xs : List HeyLo.Ident} {hn : xs.Nodup} (S : Subs xs hn) : List ((v : HeyLo.Ident) × (pGCL.State HeyLo.Ty.Γ → v.type.lit))

Equations

• S.help = List.map (fun (a : (x : HeyLo.Ident) × x.type.lit) => ⟨a.fst, fun (x : pGCL.State HeyLo.Ty.Γ) => a.snd⟩) S.values

def HeyVL.Subs.help' {xs : List HeyLo.Ident} {hn : xs.Nodup} (S : Subs xs hn) : List ((v : HeyLo.Ident) × v.type.lit)

Equations

• S.help' = S.values

@[simp]

theorem HeyVL.Subs.help_length {xs : List HeyLo.Ident} {hn : xs.Nodup} (S : Subs xs hn) : S.help.length = xs.length

@[simp]

theorem HeyVL.Subs.help_cons {x : HeyLo.Ident} {xs : List HeyLo.Ident} {hn : (x :: xs).Nodup} (S : Subs (x :: xs) hn) : S.help = ⟨x, fun (x_1 : pGCL.State HeyLo.Ty.Γ) => S.tail.1⟩ :: S.tail.2.help

@[simp]

theorem HeyVL.Subs.help'_cons {x : HeyLo.Ident} {xs : List HeyLo.Ident} {hn : (x :: xs).Nodup} (S : Subs (x :: xs) hn) : S.help' = ⟨x, S.tail.1⟩ :: S.tail.2.help'

def HeyVL.Subs.get {xs : List HeyLo.Ident} {hn : xs.Nodup} (S : Subs xs hn) (x : HeyLo.Ident) (hx : x ∈ xs) : x.type.lit

Equations

• S.get x hx = cast ⋯ S.values[List.findIdx (fun (x_1 : HeyLo.Ident) => decide (x_1 = x)) xs].snd

@[simp]

theorem HeyVL.Subs.tail_get {x : HeyLo.Ident} {xs : List HeyLo.Ident} {hn : (x :: xs).Nodup} (S : Subs (x :: xs) hn) (y : HeyLo.Ident) (hy : y ∈ xs) : S.tail.2.get y hy = S.get y ⋯

theorem HeyVL.Subs.tail_1_eq_get {x : HeyLo.Ident} {xs : List HeyLo.Ident} {hn : (x :: xs).Nodup} (S : Subs (x :: xs) hn) : S.tail.1 = S.get x ⋯

@[simp]

theorem HeyVL.Subs.subst_help'_apply {xs : List HeyLo.Ident} {hn : xs.Nodup} {y : HeyLo.Ident} (S : Subs xs hn) (σ : pGCL.State fun (x : HeyLo.Ident) => x.type.lit) : (σ[..S.help']) y = if h : y ∈ xs then S.get y h else σ y

@[simp]

theorem Exp.substs_help_apply {α : Type u_1} {xs : List HeyLo.Ident} {hxs : xs.Nodup} {σ : pGCL.State HeyLo.Ty.Γ} (m : pGCL.State HeyLo.Ty.Γ → α) (Ξ : HeyVL.Subs xs hxs) : (m[..Ξ.help]) σ = m (σ[..Ξ.help'])

@[simp]

theorem BExpr.substs_help_apply {xs : List HeyLo.Ident} {hxs : xs.Nodup} {σ : pGCL.State fun (x : HeyLo.Ident) => x.type.lit} (m : pGCL.BExpr fun (x : HeyLo.Ident) => x.type.lit) (Ξ : HeyVL.Subs xs hxs) : (m[..Ξ.help]) σ = m (σ[..Ξ.help'])

theorem HeyLo.sem_substs_apply {α : Ty} {xs : List ((a : Ident) × (pGCL.State Ty.Γ → Ty.Γ a))} {σ : pGCL.State Ty.Γ} (m : HeyLo α) : (⟦@m⟧'[..xs]) σ = ⟦@m⟧' (Substitution.applied σ xs)

theorem HeyLo.sem_substs_apply' {α : Ty} {xs : List Ident} {hxs : xs.Nodup} {σ : pGCL.State Ty.Γ} (m : HeyLo α) (Ξ : HeyVL.Subs xs hxs) : (⟦@m⟧'[..Ξ.help]) σ = ⟦@m⟧' (σ[..Ξ.help'])

theorem Substitution.applied_subst {x : HeyLo.Ident} (σ : pGCL.State fun (x : HeyLo.Ident) => x.type.lit) (xs : List ((v : HeyLo.Ident) × (pGCL.State HeyLo.Ty.Γ → v.type.lit))) (v : pGCL.State HeyLo.Ty.Γ → x.type.lit) : (applied σ xs)[x ↦ v (applied σ xs)] = applied σ (xs ++ [⟨x, v⟩])

def HeyVL.Subs.of (xs : List HeyLo.Ident) (hn : xs.Nodup) (σ : pGCL.State fun (x : HeyLo.Ident) => x.type.lit) : Subs xs hn

Equations

• HeyVL.Subs.of xs hn σ = { values := List.map (fun (x : HeyLo.Ident) => ⟨x, σ x⟩) xs, prop := ⋯, prop' := ⋯ }

@[simp]

theorem HeyVL.Subs.of_get (xs : List HeyLo.Ident) (hn : xs.Nodup) (σ : pGCL.State fun (x : HeyLo.Ident) => x.type.lit) {y : HeyLo.Ident} {hy : y ∈ xs} : (of xs hn σ).get y hy = σ y

@[simp]

theorem HeyLo.sem_indep {α : Ty} {φ : HeyLo α} {x : Ident} (h : x ∉ φ.fv) : Substitution.IsIndepPair ⟦@φ⟧' x

@[simp]

theorem HeyVL.vp_havocs {xs : List HeyLo.Ident} {φ : HeyLo HeyLo.Ty.ENNReal} {hn : xs.Nodup} (h : xs.Nodup) : ⟦@(vp⟦@(Havocs xs)⟧ φ)⟧' = ⨅ (vs : Subs xs hn), ⟦@φ⟧'[..vs.help]

@[simp]

theorem HeyVL.vp_cohavocs {xs : List HeyLo.Ident} {φ : HeyLo HeyLo.Ty.ENNReal} {hn : xs.Nodup} (h : xs.Nodup) : ⟦@(vp⟦@(Cohavocs xs)⟧ φ)⟧' = ⨆ (vs : Subs xs hn), ⟦@φ⟧'[..vs.help]

@[simp]

theorem HeyVL.if_vp_sem {b : HeyLo HeyLo.Ty.Bool} {S₁ S₂ : HeyVL} {φ : HeyLo HeyLo.Ty.ENNReal} : ⟦@(vp⟦if (@b) {@S₁} else {@S₂}⟧ φ)⟧' = i[⟦@b⟧'] * ⟦@(vp⟦@S₁⟧ φ)⟧' + i[⟦@b.not⟧'] * ⟦@(vp⟦@S₂⟧ φ)⟧'

@[simp]

theorem spGCL.pGCL_mods (C : spGCL) : C.pGCL.mods = ↑C.mods