Running a Computation Multiple Times

This file defines a function replicate oa n that runs the computation oa a total of n times, returning the result as a list of length n.

Note that while the executions are independent, they may no longer be after calling simulate.

def OracleComp.replicate {ι : Type u_1} {spec : OracleSpec ι} {α : Type v} (n : ℕ) (oa : OracleComp spec α) : OracleComp spec (List α)

Run the computation oa repeatedly n times to get a list of n results.

def OracleComp.replicateTR {ι : Type u_1} {spec : OracleSpec ι} {α : Type v} (n : ℕ) (oa : OracleComp spec α) : OracleComp spec (List α)

Tail-recursive variant of replicate, running oa for each entry of a length-n list built by List.replicateTR. Agrees with replicate via replicateTR_eq_replicate.

@[simp]

theorem OracleComp.replicate_zero {ι : Type u_2} {spec : OracleSpec ι} {α : Type v} (oa : OracleComp spec α) : replicate 0 oa = pure []

@[simp]

theorem OracleComp.replicateTR_zero {ι : Type u_2} {spec : OracleSpec ι} {α : Type v} (oa : OracleComp spec α) : replicateTR 0 oa = pure []

@[simp]

theorem OracleComp.replicate_succ_bind {ι : Type u_2} {spec : OracleSpec ι} {α : Type v} (oa : OracleComp spec α) (n : ℕ) : replicate (n + 1) oa = do let x ← oa let xs ← replicate n oa pure (x :: xs)

Bind-style unfolding of replicate, convenient for program-logic proofs.

@[simp]

theorem OracleComp.replicateTR_eq_replicate {ι : Type u_2} {spec : OracleSpec ι} {α : Type v} (oa : OracleComp spec α) (n : ℕ) : replicateTR n oa = replicate n oa

The tail-recursive replicateTR agrees with the recursive replicate. The @[simp] annotation lets every later proof about replicateTR reduce to the recursive form automatically.

theorem OracleComp.replicate_succ {ι : Type u_2} {spec : OracleSpec ι} {α : Type v} (oa : OracleComp spec α) (n : ℕ) : replicate (n + 1) oa = List.cons <$> oa <*> replicate n oa

@[simp]

theorem OracleComp.replicate_pure {ι : Type u_2} {spec : OracleSpec ι} {α : Type v} (n : ℕ) (x : α) : replicate n (pure x) = pure (List.replicate n x)

theorem OracleComp.probFailure_replicate {ι : Type u_1} {spec : OracleSpec ι} {α : Type v} (oa : OracleComp spec α) (n : ℕ) [spec.IsUniformSpec] : Pr[⊥ | replicate n oa] = 1 - (1 - Pr[⊥ | oa]) ^ n

@[simp]

theorem OracleComp.probOutput_replicate {ι : Type u_1} {spec : OracleSpec ι} {α : Type v} (oa : OracleComp spec α) (n : ℕ) [spec.IsUniformSpec] (xs : List α) : Pr[= xs | replicate n oa] = if xs.length = n then (List.map (fun (x : α) => Pr[= x | oa]) xs).prod else 0

The probability of getting a list from replicate is the product of the chances of getting each of the individual elements.

theorem OracleComp.probEvent_replicate_of_probEvent_cons {ι : Type u_1} {spec : OracleSpec ι} {α : Type v} (oa : OracleComp spec α) (n : ℕ) [spec.IsUniformSpec] (p : List α → Prop) (hp : p []) (q : α → Prop) (hq : ∀ (x : α) (xs : List α), p (x :: xs) ↔ q x ∧ p xs) : probEvent (replicate n oa) p = probEvent oa q ^ n

@[simp]

theorem OracleComp.support_replicate {ι : Type u_1} {spec : OracleSpec ι} {α : Type v} (oa : OracleComp spec α) (n : ℕ) : support (replicate n oa) = {xs : List α | xs.length = n ∧ ∀ x ∈ xs, x ∈ support oa}

Possible outputs of replicate n oa are lists of length n where each element in the list is a possible output of oa.

@[simp]

theorem OracleComp.mem_finSupport_replicate {ι : Type u_1} {spec : OracleSpec ι} {α : Type v} (oa : OracleComp spec α) (n : ℕ) [spec.IsUniformSpec] [spec.DecidableEq] [DecidableEq α] (xs : List α) : xs ∈ finSupport (replicate n oa) ↔ xs.length = n ∧ ∀ x ∈ xs, x ∈ finSupport oa

theorem OracleComp.probOutput_replicate_uniformSample {α : Type} [Fintype α] [SampleableType α] {n : ℕ} {xs : List α} (hlen : xs.length = n) : Pr[= xs | replicate n ($ᵗ α)] = (↑(Fintype.card α ^ n))⁻¹

SimulateQ distributivity

theorem OracleComp.simulateQ_replicate {ι : Type u_2} {spec : OracleSpec ι} {α : Type v} (oa : OracleComp spec α) (n : ℕ) {r : Type v → Type u_1} [Monad r] [LawfulMonad r] (impl : QueryImpl spec r) : simulateQ impl (replicate n oa) = List.mapM (fun (x : Unit) => simulateQ impl oa) (List.replicate n ())

simulateQ distributes over replicate: simulating a replicated computation equals running the simulated body n times via monadic recursion.

theorem OracleComp.support_ofFn_mapM_index {ι α : Type} {spec : OracleSpec ι} {L : ℕ} (f : Fin L → OracleComp spec α) {v : Vector α L} (hv : v ∈ support (Vector.mapM f (Vector.ofFn id))) (i : Fin L) : v[i] ∈ support (f i)

Index-extraction for (Vector.ofFn id).mapM over an OracleComp: any element in the support of the monadic mapM has each component lying in the support of the corresponding inner computation.