Ergonomic Notation and Convenience Layer for Program Logic #
This file extends VCVio.ProgramLogic.NotationCore with the heavier quantitative
bridge lemmas that depend on the full eRHL development.
theorem
OracleComp.ProgramLogic.GameEquiv.of_relTriple'
{ι₁ : Type u}
{spec₁ : OracleSpec ι₁}
[spec₁.Fintype]
[spec₁.Inhabited]
{α : Type}
{g₁ g₂ : OracleComp spec₁ α}
(h : Relational.RelTriple' g₁ g₂ (Relational.EqRel α))
:
GameEquiv g₁ g₂
Game equivalence from exact pRHL equality coupling.
theorem
OracleComp.ProgramLogic.GameEquiv.of_approxRelTriple_zero
{ι₁ : Type u}
{spec₁ : OracleSpec ι₁}
[spec₁.Fintype]
[spec₁.Inhabited]
{α : Type}
{g₁ g₂ : OracleComp spec₁ α}
(h : Relational.ApproxRelTriple 0 g₁ g₂ (Relational.EqRel α))
:
GameEquiv g₁ g₂
Game equivalence from zero-error approximate coupling.