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.

Equations

• spec.QueryCache = ((t : spec.Domain) → Option (spec.Range t))

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

Equations

• OracleSpec.QueryCache.instEmptyCollection = { emptyCollection := fun (x : spec.Domain) => none }

@[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.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• OracleSpec.QueryCache.instOrderBot = { bot := ∅, bot_le := ⋯ }

@[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.

Equations

• cache.isCached t = (cache t).isSome

@[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.

Equations

• cache.toSet ⟨t, r⟩ = (cache t = some r)

@[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

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

Equations

• cache.cacheQuery t u = Function.update cache t (some u)

@[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.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₁.

Equations

• cache.fst t = cache (Sum.inl t)

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

Equations

• cache.snd t = cache (Sum.inr t)

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

Equations

• cache.inl (Sum.inl t) = cache t
• cache.inl (Sum.inr val) = none

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

Equations

• cache.inr (Sum.inl t) = none
• cache.inr (Sum.inr val) = cache val

@[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 = ∅

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

Equations

• OracleSpec.QueryCache.instCoeSumHAdd = { coe := OracleSpec.QueryCache.inl }

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

Equations

• OracleSpec.QueryCache.instCoeSumHAdd_1 = { coe := OracleSpec.QueryCache.inr }

@[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

Equations

• OracleSpec.QueryCount ι = (ι → ℕ)

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

Pointwise addition as the Monoid operation used for WriterT.

Equations

• OracleSpec.QueryCount.instMonoid = { mul := fun (qc qc' : OracleSpec.QueryCount ι) => qc + qc', mul_assoc := ⋯, one := 0, one_mul := ⋯, mul_one := ⋯, npow_zero := ⋯, npow_succ := ⋯ }

@[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 ι

Equations

• OracleSpec.QueryCount.single i = Function.update 0 i 1

@[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.

Equations

• spec.QueryLog = List ((t : spec.Domain) × spec.Range t)

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

Query log with a single entry.

Equations

• OracleSpec.QueryLog.singleton t u = [⟨t, u⟩]

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.

Equations

• log.logQuery t u = log ++ OracleSpec.QueryLog.singleton t u

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

Equations

• OracleSpec.QueryLog.instDecidableEqOfDecidableEq = inferInstanceAs (DecidableEq (List ((t : spec.Domain) × spec.Range t)))

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

Equations

• One or more equations did not get rendered due to their size.

@[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.

Equations

• log.countQ p = (log.getQ p).length

@[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.

Equations

• log.wasQueried t = decide ((log.getQ fun (x : spec.Domain) => x = t) ≠ [])

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

Equations

• log.fst = List.filterMap (fun (x : (t : (spec₁ + spec₂).Domain) × (spec₁ + spec₂).Range t) => match x with | ⟨Sum.inl t, u⟩ => some ⟨t, u⟩ | x => none) log

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

Equations

• log.snd = List.filterMap (fun (x : (t : (spec₁ + spec₂).Domain) × (spec₁ + spec₂).Range t) => match x with | ⟨Sum.inr t, u⟩ => some ⟨t, u⟩ | x => none) log

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.

Equations

• log.inl = List.map (fun (x : (t : spec₁.Domain) × spec₁.Range t) => match x with | ⟨t, u⟩ => ⟨Sum.inl t, u⟩) log

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.

Equations

• log.inr = List.map (fun (x : (t : spec₂.Domain) × spec₂.Range t) => match x with | ⟨t, u⟩ => ⟨Sum.inr t, u⟩) log

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

Equations

• OracleSpec.QueryLog.instCoeSumHAdd = { coe := OracleSpec.QueryLog.inl }

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

Equations

• OracleSpec.QueryLog.instCoeSumHAdd_1 = { coe := OracleSpec.QueryLog.inr }

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

Equations

• spec.QuerySeed = ((i : ι) → List (spec.Range i))

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

Equations

• OracleSpec.QuerySeed.instEmptyCollection = { emptyCollection := fun (x : ι) => [] }

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.

Equations

• seed.update i xs = Function.update seed i xs

@[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.

Equations

• seed.addValues us = Function.update seed i (seed i ++ us)

@[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.

Equations

• seed.prependValues us = Function.update seed i (us ++ seed 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

Equations

• seed.addValue i u = seed.addValues [u]

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.

Equations

• seed.takeAtIndex i n = Function.update seed i (List.take n (seed 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.

Equations

• seed.pop i = match seed i with | [] => none | u :: us => some (u, Function.update seed i us)

@[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.

Equations

• OracleSpec.QuerySeed.ofList xs j = if h : i = j then h ▸ xs else []

@[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))