Samplers.lean
Shared uniform samplers for ReductionDsl reductions
Trusted in part. The theorems of Computational/ use every definition in this file except unifSamplers0, which is checked by Lean; the ones they use are part of what you must read to trust the result. See Computational/.
Coin-only uniform sampler templates attached to target interfaces via Iface., providing uniform bits ($ᵗ Bool, cost 1), bounded indices in {0, …, N - 1} (cost bits N + 1), and uniform values on designated sampleable base sorts f : B → S. at declared block costs w (at least each sort's block size).
@[expose] public sectionnamespace ReductionDslopen OracleCompdef sampleIndex
Uniform index in {0, …, N - 1}, returning 0 when N = 0.
def sampleIndex (N : ℕ) : ProbComp ℕ :=
if h : 0 < N then
letI : NeZero N := ⟨Nat.ne_of_gt h⟩
do let x ← $ᵗ (Fin N); return x.val
else return 0inductive UniformSamplerTag
Tags for coin-only uniform samplers: a bit, an index < N, or a sampleable base sort in B.
inductive UniformSamplerTag (B : Type) where
| bool
| index (N : ℕ)
| base (b : B)def unifSamplers
Shared uniform samplers over S for bits (cost 1), indices < N (cost bits N + 1), and base sorts f : B → S. at declared block costs w : B → ℕ.
@[reducible] def unifSamplers {S : Sig} {B : Type} (f : B → S.Base) (w : B → ℕ)
[∀ b, SampleableType (S.den (f b))] : Samplers S where
Samp := UniformSamplerTag B
sDom := fun _ => .unit
sTy := fun
| .bool => .bool
| .index _ => .nat
| .base b => .base (f b)
samp := fun s _ => match s with
| .bool => $ᵗ Bool
| .index N => sampleIndex N
| .base b => $ᵗ (S.den (f b))
sCost := fun
| .bool => 1
| .index N => bits N + 1
| .base b => w b1 declaration not shown (lines 66–71): theorems, which Lean checks, or definitions that no headline statement uses
ReductionDsl.
end ReductionDsl