Discrete compatibility laws for oracle-signature inclusions #
The signature inclusion and operational API is public through SubSpec.Basic. This module adds
uniform discrete probability compatibility equations.
theorem
OracleSpec.LawfulSubSpec.evalSPMF_liftM_query
{ι : Type u}
{τ : Type v}
{spec : OracleSpec ι}
{superSpec : OracleSpec τ}
[h : spec ⊂ₒ superSpec]
[spec.LawfulSubSpec superSpec]
[(t : τ) → Fintype (superSpec.Range t)]
[∀ (t : τ), Nonempty (superSpec.Range t)]
(t : spec.Domain)
[Fintype (spec.Range t)]
[Nonempty (spec.Range t)]
:
PMF.map (liftM (OracleSpec.query t)).cont (PMF.uniformOfFintype (superSpec.Range (liftM (OracleSpec.query t)).input)) = PMF.uniformOfFintype (spec.Range t)
Pushing the uniform distribution on superSpec.Range through the lens's
backward fiber recovers the uniform distribution on spec.Range. Load-bearing
for evalSPMF_liftComp below.
theorem
OracleComp.evalSPMF_liftComp
{ι : Type u}
{τ : Type v}
{spec : OracleSpec ι}
{superSpec : OracleSpec τ}
{α : Type w}
[spec.IsUniformSpec]
[superSpec.IsUniformSpec]
[h : spec ⊂ₒ superSpec]
[spec.LawfulSubSpec superSpec]
(mx : OracleComp spec α)
:
theorem
OracleComp.probOutput_liftComp
{ι : Type u}
{τ : Type v}
{spec : OracleSpec ι}
{superSpec : OracleSpec τ}
{α : Type w}
[spec.IsUniformSpec]
[superSpec.IsUniformSpec]
[h : spec ⊂ₒ superSpec]
[spec.LawfulSubSpec superSpec]
(mx : OracleComp spec α)
(x : α)
:
theorem
OracleComp.probEvent_liftComp
{ι : Type u}
{τ : Type v}
{spec : OracleSpec ι}
{superSpec : OracleSpec τ}
{α : Type w}
[spec.IsUniformSpec]
[superSpec.IsUniformSpec]
[h : spec ⊂ₒ superSpec]
[spec.LawfulSubSpec superSpec]
(mx : OracleComp spec α)
(p : α → Prop)
:
theorem
OracleComp.probFailure_liftComp
{ι : Type u}
{τ : Type v}
{spec : OracleSpec ι}
{superSpec : OracleSpec τ}
{α : Type w}
[spec.IsUniformSpec]
[superSpec.IsUniformSpec]
[h : spec ⊂ₒ superSpec]
(mx : OracleComp spec α)
: