Repeated oracle computations

replicate runs a computation a specified number of times, retaining its outputs in order. replicateTR gives the equivalent tail-recursive traversal.

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)