Output Distribution of Computations

This file defines the MonadLiftT-based probability and support semantics for OracleComp.

class OracleSpec.IsProbabilitySpec {ι : Type u_1} (spec : OracleSpec ι) : Type (max u_1 u_2)

A per-query distribution on an OracleSpec. Each query index t : ι is assigned a PMF (spec t) for its responses. This is the abstract data needed to lift OracleComp spec into PMF; uniformity is not assumed — see IsUniformSpec for the uniform-sampling specialization.

Specs that should opt into uniform sampling are best registered via IsUniformSpec, which extends this class and additionally carries Fintype / Inhabited on each range plus a propositional witness that toPMF is the canonical uniform distribution.

• toPMF (t : ι) : PMF (spec t)

  The distribution of responses to query t.

class OracleSpec.IsUniformSpec {ι : Type u_1} (spec : OracleSpec ι) extends spec.IsProbabilitySpec : Type (max u_1 u_2)

An OracleSpec whose responses are uniformly sampled from finite, inhabited ranges. Bundles spec.Fintype, spec.Inhabited, and IsProbabilitySpec spec together with a Prop witness that the per-query distribution agrees with PMF.uniformOfFintype. Use this as the canonical input to lemmas that mention Fintype.card (spec.Range _) or PMF.uniformOfFintype in their statements.

• toPMF (t : ι) : PMF (spec t)
• fintype : spec.Fintype

  Every response set is finite.

• inhabited : spec.Inhabited

  Every response set is inhabited.

• toPMF_eq_uniform (t : ι) : IsProbabilitySpec.toPMF t = PMF.uniformOfFintype (spec.Range t)

  The per-query distribution is the uniform distribution on the response set.

@[reducible]

noncomputable def OracleSpec.IsUniformSpec.ofFintypeInhabited {ι : Type u} (spec : OracleSpec ι) [hF : spec.Fintype] [hI : spec.Inhabited] : spec.IsUniformSpec

Bridge from [spec.Fintype] [spec.Inhabited] to IsUniformSpec spec. Deliberately not an instance — IsUniformSpec must be opted into per spec so that uniform-sampling semantics never attach silently to a spec whose author didn't intend a probabilistic interpretation. Use this helper when declaring IsUniformSpec for a concrete spec.

@[implicit_reducible]

noncomputable instance OracleSpec.instIsUniformSpecNatUnifSpec : unifSpec.IsUniformSpec

@[implicit_reducible]

noncomputable instance OracleSpec.instIsUniformSpecUnitCoinSpec : coinSpec.IsUniformSpec

@[implicit_reducible]

noncomputable instance OracleSpec.instIsUniformSpecAdd {ι : Type u_1} {ι' : Type u_2} (spec : OracleSpec ι) (spec' : OracleSpec ι') [spec.IsUniformSpec] [spec'.IsUniformSpec] : (spec + spec').IsUniformSpec

Propagate IsUniformSpec through +: each summand's uniformity is preserved on its branch. IsProbabilitySpec (spec + spec') is derived via the extends chain.

@[deprecated OracleSpec.IsUniformSpec (since := "2026-05-20")]

def OracleSpec.IsProbSpec {ι : Type u_1} (spec : OracleSpec ι) : Type (max u_1 u_2)

Successor to the legacy empty marker OracleSpec.IsProbSpec. The replacement IsUniformSpec bundles Fintype, Inhabited, IsProbabilitySpec, and a uniformity witness.

@[implicit_reducible]

noncomputable instance OracleComp.instMonadLiftTPMF {ι : Type u_1} {spec : OracleSpec ι} [spec.IsProbabilitySpec] : MonadLiftT (OracleComp spec) PMF

Embed OracleComp into PMF by interpreting each query via the per-query distribution provided by IsProbabilitySpec.

instance OracleComp.instLawfulMonadLiftTPMF {ι : Type u_1} {spec : OracleSpec ι} [spec.IsProbabilitySpec] : LawfulMonadLiftT (OracleComp spec) PMF

@[implicit_reducible]

instance OracleComp.instMonadLiftTSetM {ι : Type u_1} {spec : OracleSpec ι} : MonadLiftT (OracleComp spec) SetM

Direct MonadLiftT (OracleComp spec) SetM: the syntactic / operational support of mx, computed by folding queries to Set.univ. Independent of any probability structure on spec — works for arbitrary specs without Fintype or Inhabited. The bridge to the probability side is EvalDistCompatible below, supplied only when [IsUniformSpec spec].

Note: This is the only MonadLiftT (OracleComp spec) SetM instance Lean will find. The generic MonadLiftT SPMF SetM is declared as MonadLiftT (not MonadLift), so monadLiftTrans cannot chain OracleComp → SPMF → SetM.

instance OracleComp.instLawfulMonadLiftTSetM {ι : Type u_2} {spec : OracleSpec ι} : LawfulMonadLiftT (OracleComp spec) SetM

theorem OracleComp.evalDist_eq_simulateQ {ι : Type u_1} {spec : OracleSpec ι} {α : Type w} [spec.IsProbabilitySpec] (mx : OracleComp spec α) : 𝒟[mx] = liftM (simulateQ OracleSpec.IsProbabilitySpec.toPMF mx)

theorem OracleComp.evalDist_liftM_toPMF {ι : Type u_1} {spec : OracleSpec ι} {α : Type w} [spec.IsProbabilitySpec] (q : OracleQuery spec α) : 𝒟[liftM q] = liftM (PMF.map q.cont (OracleSpec.IsProbabilitySpec.toPMF q.input))

Abstract distribution of a single lifted query under IsProbabilitySpec: the per-query distribution toPMF is pushed forward through the query's continuation. Uniform-content sibling: evalDist_liftM.

theorem OracleComp.evalDist_query_toPMF {ι : Type u_1} {spec : OracleSpec ι} [spec.IsProbabilitySpec] (t : spec.Domain) : 𝒟[liftM (OracleSpec.query t)] = liftM (OracleSpec.IsProbabilitySpec.toPMF t)

liftM (query t) : OracleComp spec _ evaluates to the per-query distribution IsProbabilitySpec.toPMF t, lifted to SPMF.

@[simp]

theorem OracleComp.support_liftM {ι : Type u_1} {spec : OracleSpec ι} {α : Type w} (q : OracleQuery spec α) : support (liftM q) = Set.range q.cont

theorem OracleComp.support_query {ι : Type u_1} {spec : OracleSpec ι} (t : spec.Domain) : support (liftM (OracleSpec.query t)) = Set.univ

theorem OracleComp.mem_support_liftM_iff {ι : Type u_1} {spec : OracleSpec ι} {α : Type w} (q : OracleQuery spec α) (u : α) : u ∈ support (liftM q) ↔ ∃ (t : spec.Range q.input), q.cont t = u

theorem OracleComp.mem_support_query {ι : Type u_1} {spec : OracleSpec ι} (t : spec.Domain) (u : spec.Range t) : u ∈ support (liftM (OracleSpec.query t))

theorem OracleComp.support_liftM_query {ι : Type u_1} {spec : OracleSpec ι} (t : spec.Domain) : support (liftM (OracleSpec.query t)) = Set.univ

Alias of OracleComp.support_query.

theorem OracleComp.bind_congr_of_forall_mem_support {ι : Type u_1} {spec : OracleSpec ι} {α β : Type w} (mx : OracleComp spec α) {f g : α → OracleComp spec β} (h : ∀ x ∈ support mx, f x = g x) : mx >>= f = mx >>= g

Support-aware bind congruence: if two continuations agree on all elements in the support of mx, the resulting bind computations are equal.

@[simp]

theorem OracleComp.support_finite {ι : Type u_1} {spec : OracleSpec ι} {α : Type w} [spec.Fintype] (mx : OracleComp spec α) : (support mx).Finite

@[implicit_reducible]

instance OracleComp.instHasEvalFinset {ι : Type u_1} {spec : OracleSpec ι} [spec.Fintype] : HasEvalFinset (OracleComp spec)

Finite version of support for when oracles have a finite set of possible outputs. NOTE: we can't use simulateQ because Finset lacks a Monad instance.

@[simp]

theorem OracleComp.finSupport_liftM {ι : Type u_1} {spec : OracleSpec ι} {α : Type w} [spec.Fintype] [DecidableEq α] (q : OracleQuery spec α) : finSupport (liftM q) = Finset.image q.cont Finset.univ

theorem OracleComp.finSupport_query {ι : Type u_1} {spec : OracleSpec ι} [spec.Fintype] [spec.DecidableEq] (t : spec.Domain) : finSupport (liftM (OracleSpec.query t)) = Finset.univ

theorem OracleComp.mem_finSupport_liftM_iff {ι : Type u_1} {spec : OracleSpec ι} {α : Type w} [spec.Fintype] [DecidableEq α] (q : OracleQuery spec α) (x : α) : x ∈ finSupport (liftM q) ↔ ∃ (t : spec.Range q.input), q.cont t = x

theorem OracleComp.mem_finSupport_query {ι : Type u_1} {spec : OracleSpec ι} [spec.Fintype] [spec.DecidableEq] (t : spec.Domain) (u : spec.Range t) : u ∈ finSupport (liftM (OracleSpec.query t))

@[simp]

theorem OracleComp.evalDist_liftM {ι : Type u_1} {spec : OracleSpec ι} {α : Type w} [spec.IsUniformSpec] (q : OracleQuery spec α) : 𝒟[liftM q] = liftM (PMF.map q.cont (PMF.uniformOfFintype (spec.Range q.input)))

@[simp]

theorem OracleComp.evalDist_query {ι : Type u_1} {spec : OracleSpec ι} [spec.IsUniformSpec] (t : spec.Domain) : 𝒟[liftM (OracleSpec.query t)] = liftM (PMF.uniformOfFintype (spec.Range t))

@[simp]

theorem OracleComp.probOutput_liftM_eq_div {ι : Type u_1} {spec : OracleSpec ι} {α : Type w} [spec.IsUniformSpec] (q : OracleQuery spec α) (x : α) : Pr[= x | liftM q] = (∑' (u : spec.Range q.input), Pr[= x | pure (q.cont u)]) / ↑(Fintype.card (spec.Range q.input))

@[simp]

theorem OracleComp.probOutput_query {ι : Type u_1} {spec : OracleSpec ι} [spec.IsUniformSpec] (t : spec.Domain) (u : spec.Range t) : Pr[= u | liftM (OracleSpec.query t)] = (↑(Fintype.card (spec.Range t)))⁻¹

theorem OracleComp.probEvent_liftM_eq_div {ι : Type u_1} {spec : OracleSpec ι} {α : Type w} [spec.IsUniformSpec] (q : OracleQuery spec α) (p : α → Prop) : probEvent (liftM q) p = (∑' (u : spec.Range q.input), probEvent (pure (q.cont u)) p) / ↑(Fintype.card (spec.Range q.input))

theorem OracleComp.probOutput_query_eq_div {ι : Type u_1} {spec : OracleSpec ι} [spec.IsUniformSpec] (t : spec.Domain) (u : spec.Range t) : Pr[= u | liftM (OracleSpec.query t)] = 1 / ↑(Fintype.card (spec.Range t))

@[simp]

theorem OracleComp.probEvent_query {ι : Type u_1} {spec : OracleSpec ι} [spec.IsUniformSpec] (t : spec.Domain) (p : spec.Range t → Prop) [DecidablePred p] : probEvent (liftM (OracleSpec.query t)) p = ↑{x : spec.Range t | p x}.card / ↑(Fintype.card (spec.Range t))

instance OracleComp.instEvalDistCompatible {ι : Type u_2} {spec : OracleSpec ι} [spec.IsUniformSpec] : EvalDistCompatible (OracleComp spec)

OracleComp spec admits the bridge between its direct support semantics and the SPMF.support of its evalDist.

@[simp]

theorem OracleComp.mem_support_evalDist_iff {ι : Type u_1} {spec : OracleSpec ι} {α : Type w} [spec.IsUniformSpec] (oa : OracleComp spec α) (x : α) : some x ∈ (OptionT.run 𝒟[oa]).support ↔ x ∈ support oa

An output has non-zero probability in evalDist iff it is in computation support.

theorem OracleComp.mem_support_of_mem_support_evalDist {ι : Type u_1} {spec : OracleSpec ι} {α : Type w} [spec.IsUniformSpec] (oa : OracleComp spec α) (x : α) : some x ∈ (OptionT.run 𝒟[oa]).support → x ∈ support oa

Alias of the forward direction of OracleComp.mem_support_evalDist_iff.

---

An output has non-zero probability in evalDist iff it is in computation support.

theorem OracleComp.mem_support_evalDist {ι : Type u_1} {spec : OracleSpec ι} {α : Type w} [spec.IsUniformSpec] (oa : OracleComp spec α) (x : α) : x ∈ support oa → some x ∈ (OptionT.run 𝒟[oa]).support

Alias of the reverse direction of OracleComp.mem_support_evalDist_iff.

---

An output has non-zero probability in evalDist iff it is in computation support.

@[simp]

theorem OracleComp.mem_support_evalDist_iff' {ι : Type u_1} {spec : OracleSpec ι} {α : Type w} [spec.IsUniformSpec] (oa : OracleComp spec α) (x : α) [DecidableEq α] : some x ∈ (OptionT.run 𝒟[oa]).support ↔ x ∈ finSupport oa

Finite-support variant of mem_support_evalDist_iff.

theorem OracleComp.mem_finSupport_of_mem_support_evalDist {ι : Type u_1} {spec : OracleSpec ι} {α : Type w} [spec.IsUniformSpec] (oa : OracleComp spec α) (x : α) [DecidableEq α] : some x ∈ (OptionT.run 𝒟[oa]).support → x ∈ finSupport oa

Alias of the forward direction of OracleComp.mem_support_evalDist_iff'.

---

Finite-support variant of mem_support_evalDist_iff.

theorem OracleComp.mem_support_evalDist' {ι : Type u_1} {spec : OracleSpec ι} {α : Type w} [spec.IsUniformSpec] (oa : OracleComp spec α) (x : α) [DecidableEq α] : x ∈ finSupport oa → some x ∈ (OptionT.run 𝒟[oa]).support

Alias of the reverse direction of OracleComp.mem_support_evalDist_iff'.

---

Finite-support variant of mem_support_evalDist_iff.

@[simp]

theorem OracleComp.probFailure_eq_zero_iff {ι : Type u_1} {spec : OracleSpec ι} {α : Type w} [spec.IsProbabilitySpec] (oa : OracleComp spec α) : Pr[⊥ | oa] = 0 ↔ NeverFail oa

@[simp]

theorem OracleComp.probFailure_pos_iff {ι : Type u_1} {spec : OracleSpec ι} {α : Type w} [spec.IsProbabilitySpec] (oa : OracleComp spec α) : 0 < Pr[⊥ | oa] ↔ ¬NeverFail oa

theorem OracleComp.noFailure_of_probFailure_eq_zero {ι : Type u_1} {spec : OracleSpec ι} {α : Type w} [spec.IsProbabilitySpec] {oa : OracleComp spec α} (h : Pr[⊥ | oa] = 0) : NeverFail oa

theorem OracleComp.not_noFailure_of_probFailure_pos {ι : Type u_1} {spec : OracleSpec ι} {α : Type w} [spec.IsProbabilitySpec] {oa : OracleComp spec α} (h : 0 < Pr[⊥ | oa]) : ¬NeverFail oa

theorem OracleComp.evalDist_query_bind {ι : Type u_1} {spec : OracleSpec ι} {α : Type w} [spec.IsUniformSpec] (t : spec.Domain) (ou : spec.Range t → OracleComp spec α) : 𝒟[liftM (OracleSpec.query t) >>= ou] = OptionT.lift (PMF.uniformOfFintype (spec.Range t)) >>= evalDist ∘ ou

theorem OracleComp.probOutput_congr {ι : Type u_1} {ι' : Type u_2} {spec : OracleSpec ι} {spec' : OracleSpec ι'} {α : Type w} [spec.IsUniformSpec] [spec'.IsProbabilitySpec] {x y : α} {oa : OracleComp spec α} {oa' : OracleComp spec' α} (h1 : x = y) (h2 : 𝒟[oa] = 𝒟[oa']) : Pr[= x | oa] = Pr[= y | oa']

theorem OracleComp.probEvent_congr' {ι : Type u_1} {ι' : Type u_2} {spec : OracleSpec ι} {spec' : OracleSpec ι'} {α : Type w} [spec.IsUniformSpec] [spec'.IsProbabilitySpec] {p q : α → Prop} {oa : OracleComp spec α} {oa' : OracleComp spec' α} (h1 : ∀ x ∈ support oa, p x ↔ q x) (h2 : 𝒟[oa] = 𝒟[oa']) : probEvent oa p = probEvent oa' q

theorem OracleComp.evalDist_ext_probEvent {ι : Type u_1} {ι' : Type u_2} {spec : OracleSpec ι} {spec' : OracleSpec ι'} {α : Type w} [spec.IsUniformSpec] [spec'.IsProbabilitySpec] {oa : OracleComp spec α} {oa' : OracleComp spec' α} (h : ∀ (x : α), Pr[= x | oa] = Pr[= x | oa']) : OptionT.run 𝒟[oa] = OptionT.run 𝒟[oa']

theorem OracleComp.probFailure_eq_sub_probEvent' {ι : Type u_1} {spec : OracleSpec ι} {α : Type w} [spec.IsUniformSpec] (oa : OracleComp spec α) : Pr[⊥ | oa] = 1 - probEvent oa fun (x : α) => True

@[simp]

theorem OracleComp.probOutput_guard {ι : Type u_1} {spec : OracleSpec ι} [spec.IsProbabilitySpec] {p : Prop} [Decidable p] : Pr[= () | guard p] = if p then 1 else 0

@[simp]

theorem OracleComp.probFailure_guard {ι : Type u_1} {spec : OracleSpec ι} [spec.IsProbabilitySpec] {p : Prop} [Decidable p] : Pr[⊥ | guard p] = if p then 0 else 1

theorem OracleComp.probOutput_eq_sub_probFailure_of_unit {ι : Type u_1} {spec : OracleSpec ι} [spec.IsProbabilitySpec] {oa : OracleComp spec PUnit.{1}} : Pr[= () | oa] = 1 - Pr[⊥ | oa]

theorem OracleComp.probOutput_guard_eq_sub_probOutput_guard_not {ι : Type u_1} {spec : OracleSpec ι} [spec.IsProbabilitySpec] {α : Type} {oa : OracleComp spec α} [NeverFail oa] {p : α → Prop} [DecidablePred p] : Pr[= () | do let a ← liftM oa guard (p a)] = 1 - Pr[= () | do let a ← liftM oa guard ¬p a]

theorem OracleComp.evalDist_simulateQ_eq_evalDist {ι : Type u_1} {ι' : Type u_2} {spec : OracleSpec ι} {spec' : OracleSpec ι'} {α : Type w} [spec.IsProbabilitySpec] [spec'.IsProbabilitySpec] (so : QueryImpl spec' (OracleComp spec)) (h : ∀ (t : spec'.Domain), 𝒟[so t] = 𝒟[liftM (OracleSpec.query t)]) (oa : OracleComp spec' α) : 𝒟[simulateQ so oa] = 𝒟[oa]

If an oracle implementation preserves the distribution of each source query, then simulateQ preserves the distribution of every source computation.

def OracleComp.supportWhen {ι : Type u_1} {spec : OracleSpec ι} {α : Type w} (o : QueryImpl spec Set) (mx : OracleComp spec α) : Set α

The possible outputs of mx when queries can output values in the specified sets. NOTE: currently proofs using this should reduce to simulateQ. A full API would be better

@[simp]

theorem OracleComp.supportWhen_pure {ι : Type u_1} {spec : OracleSpec ι} {α : Type w} (o : QueryImpl spec Set) (x : α) : supportWhen o (pure x) = {x}

@[simp]

theorem OracleComp.supportWhen_query_bind {ι : Type u_1} {spec : OracleSpec ι} {α : Type w} (o : QueryImpl spec Set) (q : spec.Domain) (oa : spec.Range q → OracleComp spec α) : supportWhen o (liftM (OracleSpec.query q) >>= oa) = ⋃ x ∈ o q, supportWhen o (oa x)

@[simp]

theorem OracleComp.supportWhen_bind {ι : Type u_1} {spec : OracleSpec ι} {α β : Type w} (o : QueryImpl spec Set) (oa : OracleComp spec α) (ob : α → OracleComp spec β) : supportWhen o (oa >>= ob) = ⋃ x ∈ supportWhen o oa, supportWhen o (ob x)

Reachable outputs of a bind are the reachable outputs of the continuation over reachable outputs of the first computation.

theorem OracleComp.mem_supportWhen_bind_iff {ι : Type u_1} {spec : OracleSpec ι} {α β : Type w} (o : QueryImpl spec Set) (oa : OracleComp spec α) (ob : α → OracleComp spec β) (y : β) : y ∈ supportWhen o (oa >>= ob) ↔ ∃ x ∈ supportWhen o oa, y ∈ supportWhen o (ob x)

Membership form of [OracleComp.supportWhen_bind].

theorem OracleComp.supportWhen_mono {ι : Type u_1} {spec : OracleSpec ι} {α : Type w} {o₁ o₂ : QueryImpl spec Set} (h : ∀ (q : spec.Domain), o₁ q ⊆ o₂ q) (oa : OracleComp spec α) : supportWhen o₁ oa ⊆ supportWhen o₂ oa

Enlarging the set of possible oracle outputs only enlarges the reachable output set.

@[reducible]

noncomputable def OracleComp.evalDistWhen {ι : Type u_1} {spec : OracleSpec ι} {α : Type w} (d : QueryImpl spec SPMF) (mx : OracleComp spec α) : SPMF α

The output distribution of mx when queries follow the specified distribution.