Structures For Tracking a Computation's Oracle Queries

This file defines types like QueryLog and QueryCache for use with simulation oracles and implementation transformers defined in the same directory.

def OracleSpec.QueryCache {ι : Type u} (spec : OracleSpec ι) : Type (max u v)

Type to represent a cache of queries to oracles in spec. Defined to be a function from (indexed) inputs to an optional output.

@[implicit_reducible]

instance OracleSpec.QueryCache.instEmptyCollection {ι : Type u} {spec : OracleSpec ι} : EmptyCollection spec.QueryCache

@[simp]

theorem OracleSpec.QueryCache.empty_apply {ι : Type u} {spec : OracleSpec ι} (t : spec.Domain) : ∅ t = none

theorem OracleSpec.QueryCache.ext {ι : Type u} {spec : OracleSpec ι} {c₁ c₂ : spec.QueryCache} (h : ∀ (t : spec.Domain), c₁ t = c₂ t) : c₁ = c₂

theorem OracleSpec.QueryCache.ext_iff {ι : Type u} {spec : OracleSpec ι} {c₁ c₂ : spec.QueryCache} : c₁ = c₂ ↔ ∀ (t : spec.Domain), c₁ t = c₂ t

Partial Order

A QueryCache carries a natural partial order where c₁ ≤ c₂ means every cached entry in c₁ also appears (with the same value) in c₂. The empty cache is the bottom element.

@[implicit_reducible]

instance OracleSpec.QueryCache.instPartialOrder {ι : Type u} {spec : OracleSpec ι} : PartialOrder spec.QueryCache

@[implicit_reducible]

instance OracleSpec.QueryCache.instOrderBot {ι : Type u} {spec : OracleSpec ι} : OrderBot spec.QueryCache

@[simp]

theorem OracleSpec.QueryCache.bot_eq_empty {ι : Type u} {spec : OracleSpec ι} : ⊥ = ∅

theorem OracleSpec.QueryCache.le_def {ι : Type u} {spec : OracleSpec ι} {c₁ c₂ : spec.QueryCache} : c₁ ≤ c₂ ↔ ∀ ⦃t : ι⦄ ⦃u : spec.Range t⦄, c₁ t = some u → c₂ t = some u

Query membership

def OracleSpec.QueryCache.isCached {ι : Type u} {spec : OracleSpec ι} (cache : spec.QueryCache) (t : spec.Domain) : Bool

Check whether a query t has a cached response.

@[simp]

theorem OracleSpec.QueryCache.isCached_empty {ι : Type u} {spec : OracleSpec ι} (t : spec.Domain) : ∅.isCached t = false

Conversion to a set of query-response pairs

def OracleSpec.QueryCache.toSet {ι : Type u} {spec : OracleSpec ι} (cache : spec.QueryCache) : Set ((t : spec.Domain) × spec.Range t)

The set of all (query, response) pairs stored in the cache.

@[simp]

theorem OracleSpec.QueryCache.mem_toSet {ι : Type u} {spec : OracleSpec ι} {cache : spec.QueryCache} {t : spec.Domain} {r : spec.Range t} : ⟨t, r⟩ ∈ cache.toSet ↔ cache t = some r

@[simp]

theorem OracleSpec.QueryCache.toSet_empty {ι : Type u} {spec : OracleSpec ι} : ∅.toSet = ∅

theorem OracleSpec.QueryCache.toSet_mono {ι : Type u} {spec : OracleSpec ι} {c₁ c₂ : spec.QueryCache} (h : c₁ ≤ c₂) : c₁.toSet ⊆ c₂.toSet

noncomputable def OracleSpec.QueryCache.enncard {ι : Type u} {spec : OracleSpec ι} (cache : spec.QueryCache) : ENNReal

Number of live entries in a query cache, as an ℝ≥0∞ resource.

@[simp]

theorem OracleSpec.QueryCache.enncard_empty {ι : Type u} {spec : OracleSpec ι} : ∅.enncard = 0

Cache update

def OracleSpec.QueryCache.cacheQuery {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (cache : spec.QueryCache) (t : spec.Domain) (u : spec.Range t) : spec.QueryCache

Add an index + input pair to the cache by updating the function (wrapper around Function.update).

@[simp]

theorem OracleSpec.QueryCache.cacheQuery_self {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (cache : spec.QueryCache) (t : spec.Domain) (u : spec.Range t) : cache.cacheQuery t u t = some u

@[simp]

theorem OracleSpec.QueryCache.cacheQuery_of_ne {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (cache : spec.QueryCache) {t' t : spec.Domain} (u : spec.Range t) (h : t' ≠ t) : cache.cacheQuery t u t' = cache t'

theorem OracleSpec.QueryCache.toSet_cacheQuery_subset_insert {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (cache : spec.QueryCache) (t : spec.Domain) (u : spec.Range t) : (cache.cacheQuery t u).toSet ⊆ insert ⟨t, u⟩ cache.toSet

theorem OracleSpec.QueryCache.toSet_encard_cacheQuery_le {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (cache : spec.QueryCache) (t : spec.Domain) (u : spec.Range t) : (cache.cacheQuery t u).toSet.encard ≤ cache.toSet.encard + 1

theorem OracleSpec.QueryCache.enncard_cacheQuery_le {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (cache : spec.QueryCache) (t : spec.Domain) (u : spec.Range t) : (cache.cacheQuery t u).enncard ≤ cache.enncard + 1

theorem OracleSpec.QueryCache.le_cacheQuery {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (cache : spec.QueryCache) {t : spec.Domain} {u : spec.Range t} (h : cache t = none) : cache ≤ cache.cacheQuery t u

theorem OracleSpec.QueryCache.cacheQuery_mono {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] {c₁ c₂ : spec.QueryCache} (h : c₁ ≤ c₂) (t : spec.Domain) (u : spec.Range t) : c₁.cacheQuery t u ≤ c₂.cacheQuery t u

@[simp]

theorem OracleSpec.QueryCache.isCached_cacheQuery_self {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (cache : spec.QueryCache) (t : spec.Domain) (u : spec.Range t) : (cache.cacheQuery t u).isCached t = true

@[simp]

theorem OracleSpec.QueryCache.isCached_cacheQuery_of_ne {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (cache : spec.QueryCache) {t' t : spec.Domain} (u : spec.Range t) (h : t' ≠ t) : (cache.cacheQuery t u).isCached t' = cache.isCached t'

Sum spec projections

def OracleSpec.QueryCache.fst {ι₁ : Type u_1} {ι₂ : Type u_2} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} (cache : (spec₁ + spec₂).QueryCache) : spec₁.QueryCache

Project a cache for spec₁ + spec₂ onto spec₁.

def OracleSpec.QueryCache.snd {ι₁ : Type u_1} {ι₂ : Type u_2} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} (cache : (spec₁ + spec₂).QueryCache) : spec₂.QueryCache

Project a cache for spec₁ + spec₂ onto spec₂.

def OracleSpec.QueryCache.inl {ι₁ : Type u_1} {ι₂ : Type u_2} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} (cache : spec₁.QueryCache) : (spec₁ + spec₂).QueryCache

Embed a cache for spec₁ into one for spec₁ + spec₂.

def OracleSpec.QueryCache.inr {ι₁ : Type u_1} {ι₂ : Type u_2} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} (cache : spec₂.QueryCache) : (spec₁ + spec₂).QueryCache

Embed a cache for spec₂ into one for spec₁ + spec₂.

@[simp]

theorem OracleSpec.QueryCache.fst_apply {ι₁ : Type u_1} {ι₂ : Type u_2} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} (cache : (spec₁ + spec₂).QueryCache) (t : ι₁) : cache.fst t = cache (Sum.inl t)

@[simp]

theorem OracleSpec.QueryCache.snd_apply {ι₁ : Type u_1} {ι₂ : Type u_2} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} (cache : (spec₁ + spec₂).QueryCache) (t : ι₂) : cache.snd t = cache (Sum.inr t)

@[simp]

theorem OracleSpec.QueryCache.inl_apply_inl {ι₁ : Type u_1} {ι₂ : Type u_2} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} (cache : spec₁.QueryCache) (t : ι₁) : cache.inl (Sum.inl t) = cache t

@[simp]

theorem OracleSpec.QueryCache.inl_apply_inr {ι₁ : Type u_1} {ι₂ : Type u_2} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} (cache : spec₁.QueryCache) (t : ι₂) : cache.inl (Sum.inr t) = none

@[simp]

theorem OracleSpec.QueryCache.inr_apply_inl {ι₁ : Type u_1} {ι₂ : Type u_2} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} (cache : spec₂.QueryCache) (t : ι₁) : cache.inr (Sum.inl t) = none

@[simp]

theorem OracleSpec.QueryCache.inr_apply_inr {ι₁ : Type u_1} {ι₂ : Type u_2} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} (cache : spec₂.QueryCache) (t : ι₂) : cache.inr (Sum.inr t) = cache t

@[simp]

theorem OracleSpec.QueryCache.fst_inl {ι₁ : Type u_1} {ι₂ : Type u_2} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} (cache : spec₁.QueryCache) : cache.inl.fst = cache

@[simp]

theorem OracleSpec.QueryCache.snd_inr {ι₁ : Type u_1} {ι₂ : Type u_2} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} (cache : spec₂.QueryCache) : cache.inr.snd = cache

@[simp]

theorem OracleSpec.QueryCache.fst_inr {ι₁ : Type u_1} {ι₂ : Type u_2} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} (cache : spec₂.QueryCache) : cache.inr.fst = ∅

@[simp]

theorem OracleSpec.QueryCache.snd_inl {ι₁ : Type u_1} {ι₂ : Type u_2} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} (cache : spec₁.QueryCache) : cache.inl.snd = ∅

@[simp]

theorem OracleSpec.QueryCache.fst_empty {ι₁ : Type u_1} {ι₂ : Type u_2} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} : ∅.fst = ∅

@[simp]

theorem OracleSpec.QueryCache.snd_empty {ι₁ : Type u_1} {ι₂ : Type u_2} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} : ∅.snd = ∅

@[implicit_reducible]

instance OracleSpec.QueryCache.instCoeSumHAdd {ι₁ : Type u_1} {ι₂ : Type u_2} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} : Coe spec₁.QueryCache (spec₁ + spec₂).QueryCache

@[implicit_reducible]

instance OracleSpec.QueryCache.instCoeSumHAdd_1 {ι₁ : Type u_1} {ι₂ : Type u_2} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} : Coe spec₂.QueryCache (spec₁ + spec₂).QueryCache

@[reducible]

def OracleSpec.QueryCount (ι : Type u_1) : Type u_1

Simple wrapper in order to introduce the Monoid structure for countingOracle. Marked as reducible and can generally be treated as just a function. idx gives the "index" for a given input.

A QueryCount ι is a commutative monoid under pointwise addition; it is exactly the trace-monoid value type used by QueryImpl.withCost, which attaches a WriterT (QueryCount ι) m writer effect via the generic QueryImpl.withTraceBefore primitive in VCVio/OracleComp/QueryTracking/Tracing.lean.

@[implicit_reducible]

instance OracleSpec.QueryCount.instMonoid {ι : Type u} : Monoid (QueryCount ι)

Pointwise addition as the Monoid operation used for WriterT.

@[simp]

theorem OracleSpec.QueryCount.monoid_mul_def {ι : Type u} (qc qc' : QueryCount ι) : qc * qc' = qc + qc'

@[simp]

theorem OracleSpec.QueryCount.monoid_one_def {ι : Type u} : OfNat.ofNat 1 = 0

def OracleSpec.QueryCount.single {ι : Type u} [DecidableEq ι] (i : ι) : QueryCount ι

@[simp]

theorem OracleSpec.QueryCount.single_le_iff_pos {ι : Type u} [DecidableEq ι] (i : ι) (qc : QueryCount ι) : single i ≤ qc ↔ 0 < qc i

@[reducible]

def OracleSpec.QueryLog {ι : Type u} (spec : OracleSpec ι) : Type (max u v)

Log of queries represented by a list of dependent product's tagging the oracle's index. (t : spec.Domain) × (spec.Range t) is slightly more restricted as it doesn't keep track of query ordering between different oracles.

A QueryLog spec is morally a free monoid on Idx spec.toPFunctor, with identity [] and product (++). By Mathlib reducibility this is exactly FreeMonoid (Idx spec.toPFunctor) = TraceList spec.toPFunctor, so a trace-valued boundary description such as BoundaryAction.emit (in VCVio/Interaction/UC/OpenProcess.lean) and a per-call QueryLog-valued writer share the same underlying free-monoid carrier.

We do not declare a global Monoid (QueryLog spec) instance: doing so would conflict with the [EmptyCollection ω] [Append ω] → Monad (WriterT ω M) instance Mathlib already provides for WriterT (QueryLog spec) M, which the existing WriterTBridge/mvcgen proof infrastructure relies on. The QueryImpl.withTrace/withLogging API instead uses the Append-based Monad (WriterT _ _) directly via QueryImpl.withTraceAppend.

def OracleSpec.QueryLog.singleton {ι : Type u} {spec : OracleSpec ι} (t : spec.Domain) (u : spec.Range t) : spec.QueryLog

Query log with a single entry.

def OracleSpec.QueryLog.logQuery {ι : Type u} {spec : OracleSpec ι} (log : spec.QueryLog) (t : spec.Domain) (u : spec.Range t) : spec.QueryLog

Update a query log by adding a new element to the appropriate list. Note that this requires decidable equality on the indexing set.

@[implicit_reducible]

instance OracleSpec.QueryLog.instDecidableEqOfDecidableEq {ι : Type u} {spec : OracleSpec ι} [spec.DecidableEq] : DecidableEq spec.QueryLog

def OracleSpec.QueryLog.getQ {ι : Type u} {spec : OracleSpec ι} (log : spec.QueryLog) (p : spec.Domain → Prop) [DecidablePred p] : List ((t : spec.Domain) × spec.Range t)

Get all the queries with inputs satisfying p

@[simp]

theorem OracleSpec.QueryLog.getQ_nil {ι : Type u} {spec : OracleSpec ι} (p : spec.Domain → Prop) [DecidablePred p] : getQ [] p = []

@[simp]

theorem OracleSpec.QueryLog.getQ_cons {ι : Type u} {spec : OracleSpec ι} (entry : (t : spec.Domain) × spec.Range t) (log : spec.QueryLog) (p : spec.Domain → Prop) [DecidablePred p] : getQ (entry :: log) p = if p entry.fst then entry :: log.getQ p else log.getQ p

@[simp]

theorem OracleSpec.QueryLog.getQ_singleton {ι : Type u} {spec : OracleSpec ι} (t : spec.Domain) (u : spec.Range t) (p : spec.Domain → Prop) [DecidablePred p] : (singleton t u).getQ p = if p t then [⟨t, u⟩] else []

@[simp]

theorem OracleSpec.QueryLog.getQ_append {ι : Type u} {spec : OracleSpec ι} (log log' : spec.QueryLog) (p : spec.Domain → Prop) [DecidablePred p] : (log ++ log').getQ p = log.getQ p ++ log'.getQ p

def OracleSpec.QueryLog.countQ {ι : Type u} {spec : OracleSpec ι} (log : spec.QueryLog) (p : spec.Domain → Prop) [DecidablePred p] : ℕ

Count the number of queries with inputs satisfying p.

@[simp]

theorem OracleSpec.QueryLog.countQ_singleton {ι : Type u} {spec : OracleSpec ι} (t : spec.Domain) (u : spec.Range t) (p : spec.Domain → Prop) [DecidablePred p] : (singleton t u).countQ p = if p t then 1 else 0

@[simp]

theorem OracleSpec.QueryLog.countQ_append {ι : Type u} {spec : OracleSpec ι} (log log' : spec.QueryLog) (p : spec.Domain → Prop) [DecidablePred p] : (log ++ log').countQ p = log.countQ p + log'.countQ p

def OracleSpec.QueryLog.wasQueried {ι : Type u} {spec : OracleSpec ι} [spec.DecidableEq] (log : spec.QueryLog) (t : spec.Domain) : Bool

Check if an element was ever queried in a log of queries. Relies on decidable equality of the domain types of oracles.

theorem OracleSpec.QueryLog.getQ_ne_nil_iff_mem_map_fst {ι : Type u} {spec : OracleSpec ι} [spec.DecidableEq] (log : spec.QueryLog) (t : spec.Domain) : (log.getQ fun (x : spec.Domain) => x = t) ≠ [] ↔ t ∈ List.map (fun (e : (t : spec.Domain) × spec.Range t) => e.fst) log

theorem OracleSpec.QueryLog.wasQueried_eq_decide_mem_map_fst {ι : Type u} {spec : OracleSpec ι} [spec.DecidableEq] (log : spec.QueryLog) (t : spec.Domain) : log.wasQueried t = decide (t ∈ List.map (fun (e : (t : spec.Domain) × spec.Range t) => e.fst) log)

def OracleSpec.QueryLog.fst {ι₁ : Type u_1} {ι₂ : Type u_2} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} (log : (spec₁ + spec₂).QueryLog) : spec₁.QueryLog

Get only the portion of the log for queries in spec₁.

def OracleSpec.QueryLog.snd {ι₁ : Type u_1} {ι₂ : Type u_2} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} (log : (spec₁ + spec₂).QueryLog) : spec₂.QueryLog

Get only the portion of the log for queries in spec₂.

def OracleSpec.QueryLog.inl {ι₁ : Type u_1} {ι₂ : Type u_2} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} (log : spec₁.QueryLog) : (spec₁ + spec₂).QueryLog

View a log for spec₁ as one for spec₁ ++ₒ spec₂ by inclusion.

def OracleSpec.QueryLog.inr {ι₁ : Type u_1} {ι₂ : Type u_2} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} (log : spec₂.QueryLog) : (spec₁ + spec₂).QueryLog

View a log for spec₂ as one for spec₁ ++ₒ spec₂ by inclusion.

@[implicit_reducible]

instance OracleSpec.QueryLog.instCoeSumHAdd {ι₁ : Type u_1} {ι₂ : Type u_2} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} : Coe spec₁.QueryLog (spec₁ + spec₂).QueryLog

@[implicit_reducible]

instance OracleSpec.QueryLog.instCoeSumHAdd_1 {ι₁ : Type u_1} {ι₂ : Type u_2} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} : Coe spec₂.QueryLog (spec₁ + spec₂).QueryLog

def OracleSpec.QuerySeed {ι : Type u} (spec : OracleSpec ι) : Type (max u v)

A store of pre-generated seed values for oracle queries, indexed by oracle. Maps each oracle index i to a list of outputs List (spec.Range i).

@[implicit_reducible]

instance OracleSpec.QuerySeed.instEmptyCollection {ι : Type u} {spec : OracleSpec ι} : EmptyCollection spec.QuerySeed

theorem OracleSpec.QuerySeed.ext {ι : Type u} {spec : OracleSpec ι} {seed₁ seed₂ : spec.QuerySeed} (h : ∀ (i : ι), seed₁ i = seed₂ i) : seed₁ = seed₂

theorem OracleSpec.QuerySeed.ext_iff {ι : Type u} {spec : OracleSpec ι} {seed₁ seed₂ : spec.QuerySeed} : seed₁ = seed₂ ↔ ∀ (i : ι), seed₁ i = seed₂ i

@[simp]

theorem OracleSpec.QuerySeed.empty_apply {ι : Type u} {spec : OracleSpec ι} (i : ι) : ∅ i = []

def OracleSpec.QuerySeed.update {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (seed : spec.QuerySeed) (i : ι) (xs : List (spec.Range i)) : spec.QuerySeed

Replace the seed values at index i.

@[simp]

theorem OracleSpec.QuerySeed.update_self {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (seed : spec.QuerySeed) (i : ι) (xs : List (spec.Range i)) : seed.update i xs i = xs

@[simp]

theorem OracleSpec.QuerySeed.update_of_ne {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (seed : spec.QuerySeed) (i : ι) (xs : List (spec.Range i)) (j : ι) (hj : j ≠ i) : seed.update i xs j = seed j

def OracleSpec.QuerySeed.addValues {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (seed : spec.QuerySeed) {i : ι} (us : List (spec.Range i)) : spec.QuerySeed

Append a list of values to the seed at index i.

@[simp]

theorem OracleSpec.QuerySeed.addValues_self {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (seed : spec.QuerySeed) {i : ι} (us : List (spec.Range i)) : seed.addValues us i = seed i ++ us

@[simp]

theorem OracleSpec.QuerySeed.addValues_of_ne {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (seed : spec.QuerySeed) {i : ι} (us : List (spec.Range i)) {j : ι} (hj : j ≠ i) : seed.addValues us j = seed j

@[simp]

theorem OracleSpec.QuerySeed.addValues_nil {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (seed : spec.QuerySeed) (i : ι) : seed.addValues [] = seed

theorem OracleSpec.QuerySeed.addValues_cons {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (seed : spec.QuerySeed) {i : ι} (u : spec.Range i) (us : List (spec.Range i)) : seed.addValues (u :: us) = (seed.addValues [u]).addValues us

def OracleSpec.QuerySeed.prependValues {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (seed : spec.QuerySeed) {i : ι} (us : List (spec.Range i)) : spec.QuerySeed

Prepend a list of values to the seed at index i.

@[simp]

theorem OracleSpec.QuerySeed.prependValues_self {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (seed : spec.QuerySeed) {i : ι} (us : List (spec.Range i)) : seed.prependValues us i = us ++ seed i

@[simp]

theorem OracleSpec.QuerySeed.prependValues_singleton {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (seed : spec.QuerySeed) {i : ι} (u : spec.Range i) : seed.prependValues [u] i = u :: seed i

@[simp]

theorem OracleSpec.QuerySeed.prependValues_of_ne {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (seed : spec.QuerySeed) {i : ι} (us : List (spec.Range i)) {j : ι} (hj : j ≠ i) : seed.prependValues us j = seed j

@[simp]

theorem OracleSpec.QuerySeed.prependValues_nil {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (seed : spec.QuerySeed) (i : ι) : seed.prependValues [] = seed

theorem OracleSpec.QuerySeed.prependValues_take_drop {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (seed : spec.QuerySeed) (i : ι) (n : ℕ) : prependValues (Function.update seed i (List.drop n (seed i))) (List.take n (seed i)) = seed

theorem OracleSpec.QuerySeed.eq_of_prependValues_eq {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (seed rest : spec.QuerySeed) {i : ι} (xs : List (spec.Range i)) {n : ℕ} (hlen : xs.length = n) (h : rest.prependValues xs = seed) : xs = List.take n (seed i) ∧ rest = Function.update seed i (List.drop n (seed i))

theorem OracleSpec.QuerySeed.eq_of_prependValues_singleton_eq {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (seed rest : spec.QuerySeed) {i : ι} (u : spec.Range i) (h : rest.prependValues [u] = seed) : u :: rest i = seed i ∧ rest = Function.update seed i (seed i).tail

@[reducible, inline]

abbrev OracleSpec.QuerySeed.addValue {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (seed : spec.QuerySeed) (i : ι) (u : spec.Range i) : spec.QuerySeed

def OracleSpec.QuerySeed.takeAtIndex {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (seed : spec.QuerySeed) (i : ι) (n : ℕ) : spec.QuerySeed

Take only the first n values of the seed at index i.

@[simp]

theorem OracleSpec.QuerySeed.takeAtIndex_apply_self {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (seed : spec.QuerySeed) (i : ι) (n : ℕ) : seed.takeAtIndex i n i = List.take n (seed i)

@[simp]

theorem OracleSpec.QuerySeed.takeAtIndex_apply_of_ne {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (seed : spec.QuerySeed) (i : ι) (n : ℕ) (j : ι) (hj : j ≠ i) : seed.takeAtIndex i n j = seed j

@[simp]

theorem OracleSpec.QuerySeed.takeAtIndex_length {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (seed : spec.QuerySeed) (i : ι) : seed.takeAtIndex i (seed i).length = seed

theorem OracleSpec.QuerySeed.takeAtIndex_addValues_drop {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (seed : spec.QuerySeed) (i : ι) (n : ℕ) : (seed.takeAtIndex i n).addValues (List.drop n (seed i)) = seed

def OracleSpec.QuerySeed.pop {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (seed : spec.QuerySeed) (i : ι) : Option (spec.Range i × spec.QuerySeed)

Pop one value from index i, returning the consumed value and updated seed when nonempty.

@[simp]

theorem OracleSpec.QuerySeed.pop_eq_none_iff {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (seed : spec.QuerySeed) (i : ι) : seed.pop i = none ↔ seed i = []

@[simp]

theorem OracleSpec.QuerySeed.pop_eq_some_of_cons {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (seed : spec.QuerySeed) (i : ι) (u : spec.Range i) (us : List (spec.Range i)) (h : seed i = u :: us) : seed.pop i = some (u, Function.update seed i us)

theorem OracleSpec.QuerySeed.cons_of_pop_eq_some {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (seed : spec.QuerySeed) (i : ι) (u : spec.Range i) (rest : spec.QuerySeed) (h : seed.pop i = some (u, rest)) : u :: rest i = seed i

theorem OracleSpec.QuerySeed.rest_eq_update_tail_of_pop_eq_some {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (seed : spec.QuerySeed) (i : ι) (u : spec.Range i) (rest : spec.QuerySeed) (h : seed.pop i = some (u, rest)) : rest = Function.update seed i (seed i).tail

def OracleSpec.QuerySeed.ofList {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] {i : ι} (xs : List (spec.Range i)) : spec.QuerySeed

Construct a query seed from a list at a single index.

@[simp]

theorem OracleSpec.QuerySeed.ofList_apply_self {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] {i : ι} (xs : List (spec.Range i)) : ofList xs i = xs

@[simp]

theorem OracleSpec.QuerySeed.ofList_apply_of_ne {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] {i j : ι} (xs : List (spec.Range i)) (hj : j ≠ i) : ofList xs j = []

theorem OracleSpec.QuerySeed.eq_addValues_iff {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (seed seed' : spec.QuerySeed) {i : ι} (xs : List (spec.Range i)) : seed = seed'.addValues xs ↔ seed' i ++ xs = seed i ∧ ∀ (j : ι), j ≠ i → seed' j = seed j

theorem OracleSpec.QuerySeed.addValues_eq_iff {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (seed seed' : spec.QuerySeed) {i : ι} (xs : List (spec.Range i)) : seed.addValues xs = seed' ↔ seed i ++ xs = seed' i ∧ ∀ (j : ι), j ≠ i → seed j = seed' j

@[simp]

theorem OracleSpec.QuerySeed.pop_prependValues_singleton {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (s' : spec.QuerySeed) (i : ι) (u : spec.Range i) : (s'.prependValues [u]).pop i = some (u, s')

theorem OracleSpec.QuerySeed.prependValues_singleton_injective {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (i : ι) : Function.Injective fun (p : spec.Range i × spec.QuerySeed) => p.2.prependValues [p.1]

theorem OracleSpec.QuerySeed.eq_prependValues_of_pop_eq_some {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] {seed : spec.QuerySeed} {i : ι} {u : spec.Range i} {rest : spec.QuerySeed} (h : seed.pop i = some (u, rest)) : rest.prependValues [u] = seed

theorem OracleSpec.QuerySeed.pop_takeAtIndex_prependValues_of_ne {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (s' : spec.QuerySeed) (i₀ : ι) (k : ℕ) {t : ι} (u₀ : spec.Range t) (hti : t ≠ i₀) : ((s'.prependValues [u₀]).takeAtIndex i₀ k).pop t = some (u₀, s'.takeAtIndex i₀ k)

theorem OracleSpec.QuerySeed.pop_takeAtIndex_prependValues_self {ι : Type u} {spec : OracleSpec ι} [DecidableEq ι] (s' : spec.QuerySeed) (i₀ : ι) (u₀ : spec.Range i₀) {k : ℕ} (hk : 0 < k) : ((s'.prependValues [u₀]).takeAtIndex i₀ k).pop i₀ = some (u₀, s'.takeAtIndex i₀ (k - 1))