Documentation

VCVio.OracleComp.Constructions.Replicate

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.

source
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.

Equations
    Instances For
      source
      def OracleComp.replicateTR {ι : Type u_1} {spec : OracleSpec ι} {α : Type v} (n : ℕ) (oa : OracleComp spec α) :
      OracleComp spec (List α)
      Equations
        Instances For
          source
          @[simp]
          theorem OracleComp.replicate_zero {ι : Type u_2} {spec : OracleSpec ι} {α : Type v} (oa : OracleComp spec α) :
          replicate 0 oa = pure []
          source
          @[simp]
          theorem OracleComp.replicateTR_zero {ι : Type u_2} {spec : OracleSpec ι} {α : Type v} (oa : OracleComp spec α) :
          replicate 0 oa = pure []
          source
          @[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.

          source
          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
          source
          @[simp]
          theorem OracleComp.replicate_pure {ι : Type u_2} {spec : OracleSpec ι} {α : Type v} (n : ℕ) (x : α) :
          replicate n (pure x) = pure (List.replicate n x)
          source
          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
          source
          @[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.

          source
          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) :
          Pr[p | replicate n oa] = Pr[q | oa] ^ n
          source
          @[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.

          source
          @[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
          source
          theorem OracleComp.probOutput_replicate_uniformSample {α : Type} [Fintype α] [SampleableType α] {n : ℕ} {xs : List α} (hlen : xs.length = n) :
          Pr[=xs | replicate n ($ᵗα)] = (↑(Fintype.card α ^ n))⁻¹