Support of a Computation

This file defines a function OracleComp.support : OracleComp spec α → Set α that gives the set of possible outputs of a computation, assuming all oracle outputs are possible.

If the final output type has decidable equality we can also define a function OracleComp.finSupport : OracleComp spec α → Finset α with the same property. This relies on decidable equality instances in OracleSpec as well, and the definition would need to be adjusted if those were moved into a seperate typeclass.

We avoid using (evalDist oa).support as the definition of the support, as this forces noncomputability due to the use of real numbers, and also makes defining finSupport harder.

def OracleComp.supportWhen {ι : Type u} {spec : OracleSpec ι} {α : Type v} (oa : OracleComp spec α) (possible_outputs : {α : Type v} → spec.OracleQuery α → Set α) : Set α

Possible outputs of the computation oa given a set of possible outputs for each query.

Equations

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

def OracleComp.support {ι : Type u} {spec : OracleSpec ι} {α : Type v} (oa : OracleComp spec α) : Set α

The support of a computation oa is the set of all possible output values, assuming that all output values of the oracles are possible. This is naturally compatible with evalDist where the oracles respond uniformly.

Equations

• oa.support = oa.supportWhen fun {α : Type ?u.5} (x : spec.OracleQuery α) => Set.univ

theorem OracleComp.support_def {ι : Type u} {spec : OracleSpec ι} {α : Type v} (oa : OracleComp spec α) : oa.support = oa.supportWhen fun {α : Type v} (x : spec.OracleQuery α) => Set.univ

def OracleComp.finSupportWhen {ι : Type u} {spec : OracleSpec ι} {α : Type v} [DecidableEq α] (oa : OracleComp spec α) (possible_outputs : {α : Type v} → spec.OracleQuery α → Finset α) : Finset α

Given a DecidableEq instance on the return typ of a computation oa, and a finite set possible_outputs q for any possible oracle query q, construct a finite set of all possible outputs of the computation oa assuming that at each query only the possible outputs are returned.

Equations

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

def OracleComp.finSupport {ι : Type u} {spec : OracleSpec ι} {α : Type v} [(i : ι) → Fintype (spec.range i)] [DecidableEq α] (oa : OracleComp spec α) : Finset α

Case of finSupportWhen where each oracle has a finite type as output and we assume any possible output of oracle queries.

Equations

• oa.finSupport = oa.finSupportWhen fun {α : Type ?u.13} (x : spec.OracleQuery α) => match α, x with | .(spec.range i), OracleSpec.query i t => Finset.univ

theorem OracleComp.finSupport_def {ι : Type u} {spec : OracleSpec ι} {α : Type v} [(i : ι) → Fintype (spec.range i)] [DecidableEq α] (oa : OracleComp spec α) : oa.finSupport = oa.finSupportWhen fun {α : Type v} (x : spec.OracleQuery α) => match α, x with | .(spec.range i), OracleSpec.query i t => Finset.univ

@[simp]

theorem OracleComp.supportWhen_pure {ι : Type u} {spec : OracleSpec ι} {α : Type v} (poss : {α : Type v} → spec.OracleQuery α → Set α) (x : α) : ((pure x).supportWhen fun {α : Type v} => poss) = {x}

@[simp]

theorem OracleComp.support_pure {ι : Type u} {spec : OracleSpec ι} {α : Type v} (x : α) : (pure x).support = {x}

@[simp]

theorem OracleComp.finSupportWhen_pure {ι : Type u} {spec : OracleSpec ι} {α : Type v} (fin_poss : {α : Type v} → spec.OracleQuery α → Finset α) [DecidableEq α] (x : α) : ((pure x).finSupportWhen fun {α : Type v} => fin_poss) = {x}

@[simp]

theorem OracleComp.finSupport_pure {ι : Type u} {spec : OracleSpec ι} {α : Type v} [spec.FiniteRange] [DecidableEq α] (x : α) : (pure x).finSupport = {x}

@[simp]

theorem OracleComp.supportWhen_failure {ι : Type u} {spec : OracleSpec ι} {α : Type v} (poss : {α : Type v} → spec.OracleQuery α → Set α) : (failure.supportWhen fun {α : Type v} => poss) = ∅

@[simp]

theorem OracleComp.support_failure {ι : Type u} {spec : OracleSpec ι} {α : Type v} : failure.support = ∅

@[simp]

theorem OracleComp.finSupportWhen_failure {ι : Type u} {spec : OracleSpec ι} {α : Type v} (fin_poss : {α : Type v} → spec.OracleQuery α → Finset α) [DecidableEq α] : (failure.finSupportWhen fun {α : Type v} => fin_poss) = ∅

@[simp]

theorem OracleComp.finSupport_failure {ι : Type u} {spec : OracleSpec ι} {α : Type v} [spec.FiniteRange] [DecidableEq α] : failure.finSupport = ∅

@[simp]

theorem OracleComp.supportWhen_query {ι : Type u} {spec : OracleSpec ι} {α : Type v} (poss : {α : Type v} → spec.OracleQuery α → Set α) (q : spec.OracleQuery α) : ((liftM q).supportWhen fun {α : Type v} => poss) = poss q

@[simp]

theorem OracleComp.support_query {ι : Type u} {spec : OracleSpec ι} {α : Type v} (q : spec.OracleQuery α) : (liftM q).support = Set.univ

@[simp]

theorem OracleComp.finSupportWhen_query {ι : Type u} {spec : OracleSpec ι} {α : Type v} (fin_poss : {α : Type v} → spec.OracleQuery α → Finset α) [DecidableEq α] (q : spec.OracleQuery α) : ((liftM q).finSupportWhen fun {α : Type v} => fin_poss) = fin_poss q

theorem OracleComp.finSupport_query {ι : Type u} {spec : OracleSpec ι} {α : Type v} [spec.FiniteRange] [DecidableEq α] (q : spec.OracleQuery α) : (liftM q).finSupport = match α, q with | .(spec.range i), OracleSpec.query i t => Finset.univ

@[simp]

theorem OracleComp.supportWhen_query_bind {ι : Type u} {spec : OracleSpec ι} {α β : Type v} (poss : {α : Type v} → spec.OracleQuery α → Set α) (q : spec.OracleQuery α) (ob : α → OracleComp spec β) : ((liftM q >>= ob).supportWhen fun {α : Type v} => poss) = ⋃ x ∈ poss q, (ob x).supportWhen fun {α : Type v} => poss

@[simp]

theorem OracleComp.support_query_bind {ι : Type u} {spec : OracleSpec ι} {α β : Type v} (q : spec.OracleQuery α) (ob : α → OracleComp spec β) : (liftM q >>= ob).support = ⋃ (x : α), (ob x).support

@[simp]

theorem OracleComp.finSupportWhen_query_bind {ι : Type u} {spec : OracleSpec ι} {α β : Type v} (fin_poss : {α : Type v} → spec.OracleQuery α → Finset α) [DecidableEq β] (q : spec.OracleQuery α) (ob : α → OracleComp spec β) : ((liftM q >>= ob).finSupportWhen fun {α : Type v} => fin_poss) = (fin_poss q).biUnion fun (x : α) => (ob x).finSupportWhen fun {α : Type v} => fin_poss

@[simp]

theorem OracleComp.finSupport_query_bind {ι : Type u} {spec : OracleSpec ι} {α β : Type v} [spec.FiniteRange] [Fintype α] [DecidableEq β] (q : spec.OracleQuery α) (ob : α → OracleComp spec β) : (liftM q >>= ob).finSupport = Finset.univ.biUnion fun (x : α) => (ob x).finSupport

@[simp]

theorem OracleComp.supportWhen_bind {ι : Type u} {spec : OracleSpec ι} {α β : Type v} (poss : {α : Type v} → spec.OracleQuery α → Set α) (oa : OracleComp spec α) (ob : α → OracleComp spec β) : ((oa >>= ob).supportWhen fun {α : Type v} => poss) = ⋃ x ∈ oa.supportWhen fun {α : Type v} => poss, (ob x).supportWhen fun {α : Type v} => poss

@[simp]

theorem OracleComp.support_bind {ι : Type u} {spec : OracleSpec ι} {α β : Type v} (oa : OracleComp spec α) (ob : α → OracleComp spec β) : (oa >>= ob).support = ⋃ x ∈ oa.support, (ob x).support

@[simp]

theorem OracleComp.finSupportWhen_bind {ι : Type u} {spec : OracleSpec ι} {α β : Type v} (fin_poss : {α : Type v} → spec.OracleQuery α → Finset α) (oa : OracleComp spec α) (ob : α → OracleComp spec β) [DecidableEq α] [DecidableEq β] : ((oa >>= ob).finSupportWhen fun {α : Type v} => fin_poss) = (oa.finSupportWhen fun {α : Type v} => fin_poss).biUnion fun (x : α) => (ob x).finSupportWhen fun {α : Type v} => fin_poss

@[simp]

theorem OracleComp.finSupport_bind {ι : Type u} {spec : OracleSpec ι} {α β : Type v} (oa : OracleComp spec α) (ob : α → OracleComp spec β) [hα : DecidableEq α] [hβ : DecidableEq β] [spec.FiniteRange] : (oa >>= ob).finSupport = oa.finSupport.biUnion fun (x : α) => (ob x).finSupport

theorem OracleComp.mem_support_bind_iff {ι : Type u} {spec : OracleSpec ι} {α β : Type v} (oa : OracleComp spec α) (ob : α → OracleComp spec β) (y : β) : y ∈ (oa >>= ob).support ↔ ∃ x ∈ oa.support, y ∈ (ob x).support

theorem OracleComp.mem_finSupport_bind_iff {ι : Type u} {spec : OracleSpec ι} {α β : Type v} [spec.FiniteRange] (oa : OracleComp spec α) (ob : α → OracleComp spec β) [hoa : DecidableEq α] [hob : DecidableEq β] (y : β) : y ∈ (oa >>= ob).finSupport ↔ ∃ x ∈ oa.finSupport, y ∈ (ob x).finSupport

instance OracleComp.supportWhen_finite {ι : Type u} {spec : OracleSpec ι} {α : Type v} (poss : {α : Type v} → spec.OracleQuery α → Set α) [spec.FiniteRange] (oa : OracleComp spec α) : Finite ↑(oa.supportWhen fun {α : Type v} => poss)

The support of a computation is finite if oracles have finite ranges.

instance OracleComp.support_finite {ι : Type u} {spec : OracleSpec ι} {α : Type v} [spec.FiniteRange] (oa : OracleComp spec α) : Finite ↑oa.support

The support of a computation is finite when viewed as a type.

instance OracleComp.support_fintype {ι : Type u} {spec : OracleSpec ι} {α : Type v} [spec.FiniteRange] [DecidableEq α] (oa : OracleComp spec α) : Fintype ↑oa.support

With a DecidableEq instance we can show that the support is actually a Fintype, rather than just Finite as in support_finite.

Equations

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

@[simp]

theorem OracleComp.coe_finSupport {ι : Type u} {spec : OracleSpec ι} {α : Type v} [spec.FiniteRange] [DecidableEq α] (oa : OracleComp spec α) : ↑oa.finSupport = oa.support

finSupport when viewed as a Set gives the regular support of the computation.

theorem OracleComp.finSupport_eq_iff_support_eq_coe {ι : Type u} {spec : OracleSpec ι} {α : Type v} [spec.FiniteRange] [DecidableEq α] (oa : OracleComp spec α) (s : Finset α) : oa.finSupport = s ↔ oa.support = ↑s

theorem OracleComp.eq_finSupport_iff_coe_eq_support {ι : Type u} {spec : OracleSpec ι} {α : Type v} [spec.FiniteRange] [DecidableEq α] (oa : OracleComp spec α) (s : Finset α) : s = oa.finSupport ↔ ↑s = oa.support

theorem OracleComp.finSupport_subset_iff_support_subset_coe {ι : Type u} {spec : OracleSpec ι} {α : Type v} [spec.FiniteRange] [DecidableEq α] (oa : OracleComp spec α) (s : Finset α) : oa.finSupport ⊆ s ↔ oa.support ⊆ ↑s

theorem OracleComp.subset_finSupport_iff_coe_subset_support {ι : Type u} {spec : OracleSpec ι} {α : Type v} [spec.FiniteRange] [DecidableEq α] (oa : OracleComp spec α) (s : Finset α) : s ⊆ oa.finSupport ↔ ↑s ⊆ oa.support

theorem OracleComp.mem_finSupport_iff_mem_support {ι : Type u} {spec : OracleSpec ι} {α : Type v} [spec.FiniteRange] [DecidableEq α] (oa : OracleComp spec α) (x : α) : x ∈ oa.finSupport ↔ x ∈ oa.support

theorem OracleComp.mem_finSupport_of_mem_support {ι : Type u} {spec : OracleSpec ι} {α : Type v} [spec.FiniteRange] [DecidableEq α] (oa : OracleComp spec α) {x : α} (hx : x ∈ oa.support) : x ∈ oa.finSupport

theorem OracleComp.mem_support_of_mem_finSupport {ι : Type u} {spec : OracleSpec ι} {α : Type v} [spec.FiniteRange] [DecidableEq α] (oa : OracleComp spec α) {x : α} (hx : x ∈ oa.finSupport) : x ∈ oa.support

instance OracleComp.decidablePred_mem_support {ι : Type u} {spec : OracleSpec ι} {α : Type v} [spec.FiniteRange] [hα : DecidableEq α] (oa : OracleComp spec α) : DecidablePred fun (x : α) => x ∈ oa.support

If the output type of a computation has DecidableEq then membership in the support of a computation is also decidable as a predicate. NOTE: will need to be restricted if we allow infinite oracle codomains.

Equations

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

instance OracleComp.decidablePred_mem_finSupport {ι : Type u} {spec : OracleSpec ι} {α : Type v} [spec.DecidableEq] [spec.FiniteRange] [DecidableEq α] (oa : OracleComp spec α) : DecidablePred fun (x : α) => x ∈ oa.finSupport

Membership in finSupport is a decidable predicate if it's defined.

Equations

• oa.decidablePred_mem_finSupport = ⋯.mpr oa.decidablePred_mem_support

@[simp]

theorem OracleComp.support_eqRec {ι : Type u} {spec : OracleSpec ι} {α β : Type v} (oa : OracleComp spec α) (h : α = β) : (h ▸ oa).support = ⋯ ▸ oa.support

@[simp]

theorem OracleComp.finSupport_eqRec {ι : Type u} {spec : OracleSpec ι} {α β : Type v} [spec.DecidableEq] [spec.FiniteRange] [hα : DecidableEq α] [hβ : DecidableEq β] (oa : OracleComp spec α) (h : α = β) : (h ▸ oa).finSupport = ⋯ ▸ oa.finSupport

theorem OracleComp.mem_support_eqRec_iff {ι : Type u} {spec : OracleSpec ι} {α β : Type v} (oa : OracleComp spec α) (h : α = β) (y : β) : y ∈ (h ▸ oa).support ↔ ⋯ ▸ y ∈ oa.support

@[simp]

theorem OracleComp.support_map {ι : Type u} {spec : OracleSpec ι} {α β : Type v} (oa : OracleComp spec α) (f : α → β) : (f <$> oa).support = f '' oa.support

@[simp]

theorem OracleComp.fin_support_map {ι : Type u} {spec : OracleSpec ι} {α β : Type v} [spec.DecidableEq] [spec.FiniteRange] [DecidableEq α] [DecidableEq β] (oa : OracleComp spec α) (f : α → β) : (f <$> oa).finSupport = Finset.image f oa.finSupport

theorem OracleComp.mem_support_map {ι : Type u} {spec : OracleSpec ι} {α β : Type v} {oa : OracleComp spec α} {x : α} (hx : x ∈ oa.support) (f : α → β) : f x ∈ (f <$> oa).support

@[simp]

theorem OracleComp.support_ite {ι : Type u} {spec : OracleSpec ι} {α : Type v} (p : Prop) [Decidable p] (oa oa' : OracleComp spec α) : (if p then oa else oa').support = if p then oa.support else oa'.support

@[simp]

theorem OracleComp.finSupport_ite {ι : Type u} {spec : OracleSpec ι} {α : Type v} [spec.DecidableEq] [spec.FiniteRange] [DecidableEq α] (p : Prop) [Decidable p] (oa oa' : OracleComp spec α) : (if p then oa else oa').finSupport = if p then oa.finSupport else oa'.finSupport

@[simp]

theorem OracleComp.support_coin : coin.support = {true, false}

@[simp]

theorem OracleComp.finSupport_coin : coin.finSupport = {true, false}

@[simp]

theorem OracleComp.support_uniformFin (n : ℕ) : support $[0..n] = Set.univ

@[simp]

theorem OracleComp.finSupport_uniformFin (n : ℕ) : finSupport $[0..n] = Finset.univ