def HeyVL.Verifies (C : HeyVL) : Prop

A HeyVL program C verifies if vp⟦C⟧ ⊤ = ⊤

Equations

• C.Verifies = (⟦@(vp⟦@C⟧ ⊤)⟧' = ⊤)

structure Conditions (E : Encoding) : Type

• original : spGCL
• O : Optimization
• post : HeyLo HeyLo.Ty.ENNReal
• pre : HeyLo HeyLo.Ty.ENNReal

def pgclEncoding.quot : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.pgclEncoding : Category

Equations

• Lean.Parser.Category.pgclEncoding = { }

def pgclEncoding_ : Lean.ParserDescr

Equations

• pgclEncoding_ = Lean.ParserDescr.node `pgclEncoding_ 1022 (Lean.ParserDescr.const `ident)

def «termPgclEncoding[_]» : Lean.ParserDescr

Equations

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

def «termVc[_,_]{_}_{_}» : Lean.ParserDescr

Equations

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

theorem HeyVL.vp_sem_eq {φ ψ : HeyLo HeyLo.Ty.ENNReal} (S : HeyVL) (h : ⟦@φ⟧' = ⟦@ψ⟧') : ⟦@(vp⟦@S⟧ φ)⟧' = ⟦@(vp⟦@S⟧ ψ)⟧'

theorem Conditions.wlp_valid {E : Encoding} (C : Conditions E) (h₁ : ⟦@C.post⟧' ≤ 1) (hI : ∀ I ∈ C.original.invs, ⟦@I⟧' ≤ 1) (h : heyvl {assume(@C.pre) ; @(C.original.enc C.O Encoding.wlp (C.original.fv ∪ C.post.fv)).2 ; assert(@C.post)}.Verifies) : ⟦@C.pre⟧' ≤ wlp[C.O]⟦@C.original.pGCL⟧ ⟦@C.post⟧'

def Conditions.sound {E : Encoding} (C : Conditions E) : Prop

Equations

• C_2.sound = (wp[C_2.O]⟦@C_2.original.pGCL⟧ ⟦@C_2.post⟧' ≤ ⟦@C_2.pre⟧')
• C_2.sound = (⟦@C_2.pre⟧' ≤ wlp[C_2.O]⟦@C_2.original.pGCL⟧ ⟦@C_2.post⟧')

@[simp]

theorem ENNReal.compl_compl_le {a b : ENNReal} : ~ ~ a ≤ b ↔ a = 0 ∨ b = ⊤

@[simp]

theorem Nat.log2_div_2 (n : ℕ) : (n / 2).log2 = n.log2 - 1

theorem Nat.log2_le_succ {n : ℕ} : n.log2 ≤ (n + 1).log2

theorem Nat.log2_mono {n m : ℕ} (h : n ≤ m) : n.log2 ≤ m.log2

@[simp]

theorem ENNReal.two_inv_mul_two : 2⁻¹ * 2 = 1

@[simp]

theorem ENNReal.two_mul_two_inv : 2 * 2⁻¹ = 1

@[simp]

theorem ENNReal.two_inv_mul_two_id (q : ENNReal) : 2⁻¹ * q * 2 = q

def tacticCbv_le : Lean.ParserDescr

Equations

• tacticCbv_le = Lean.ParserDescr.node `tacticCbv_le 1024 (Lean.ParserDescr.nonReservedSymbol "cbv_le" false)

def tacticVc_simp : Lean.ParserDescr

Equations

• tacticVc_simp = Lean.ParserDescr.node `tacticVc_simp 1024 (Lean.ParserDescr.nonReservedSymbol "vc_simp" false)

@[simp]

theorem Set.mem_fun_exists {α : Type u_1} {β : Type u_2} {a : α} {q : β → α} : (a ∈ fun (x : α) => ∃ (y : β), q y = x) ↔ ∃ (y : β), q y = a