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} {spec : OracleSpec ι} {α : Type v} (n : ℕ) (oa : OracleComp spec α) : OracleComp spec (List α)

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

Equations

• OracleComp.replicate n oa = mapM (fun (x : Unit) => oa) (List.replicate n ())

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

Equations

• OracleComp.replicateTR n oa = mapM (fun (x : Unit) => oa) (List.replicateTR n ())

@[simp]

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

@[simp]

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

@[simp]

theorem OracleComp.replicate_succ {ι : Type u} {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} {spec : OracleSpec ι} {α : Type v} (n : ℕ) (x : α) : replicate n (pure x) = pure (List.replicate n x)

@[simp]

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

@[simp]

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

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

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

@[simp]

theorem OracleComp.probEvent_all_replicate {ι : Type u} {spec : OracleSpec ι} {α : Type v} [spec.FiniteRange] (oa : OracleComp spec α) (n : ℕ) (p : α → Bool) : [fun (xs : List α) => xs.all p = true|replicate n oa] = [fun (x : α) => p x = true|oa] ^ n

theorem OracleComp.support_eq_setOf_probOutput_eq_zero {ι : Type u} {spec : OracleSpec ι} {α : Type v} [spec.FiniteRange] (oa : OracleComp spec α) : oa.support = {x : α | [=x|oa] ≠ 0}

@[simp]

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

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

theorem OracleComp.support_replicate' {ι : Type u} {spec : OracleSpec ι} {α : Type v} [spec.FiniteRange] [DecidableEq α] (oa : OracleComp spec α) (n : ℕ) : (replicate n oa).support = {xs : List α | xs.length = n ∧ (xs.all fun (x : α) => decide (x ∈ oa.support)) = true}

Version of support_replicate using List.all instead of quantifiers. Requires decidable equality on the output type of the computation.

@[simp]

theorem OracleComp.mem_finSupport_replicate {ι : Type u} {spec : OracleSpec ι} {α : Type v} [spec.FiniteRange] [spec.DecidableEq] [DecidableEq α] (oa : OracleComp spec α) (n : ℕ) (xs : List α) : xs ∈ (replicate n oa).finSupport ↔ xs.length = n ∧ (xs.all fun (x : α) => decide (x ∈ oa.finSupport)) = true