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 α)

@[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 α) : replicate 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.Fintype] [spec.Inhabited] : 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.Fintype] [spec.Inhabited] (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.Fintype] [spec.Inhabited] (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 : ℕ) [spec.Fintype] [spec.Inhabited] : 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.Fintype] [spec.Inhabited] [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))⁻¹