Documentation

VCVio.OracleComp.ReachableWhen

Reachability with restricted oracle answers #

reachableWhen interprets an oracle program using a specified set of possible answers for each query. The public equations describe pure, query, bind, and monotone enlargement of answer sets.

source
def OracleComp.reachableWhen {ι : Type u} {spec : OracleSpec ι} {α : Type v} (o : QueryImpl spec Set) (mx : OracleComp spec α) :
Set α

Outputs reachable when a query may return any response selected by o.

Instances For
    source
    @[simp]
    theorem OracleComp.reachableWhen_pure {ι : Type u} {spec : OracleSpec ι} {α : Type v} (o : QueryImpl spec Set) (x : α) :
    reachableWhen o (pure x) = {x}
    source
    @[simp]
    theorem OracleComp.reachableWhen_liftM {ι : Type u} {spec : OracleSpec ι} {α : Type v} (o : QueryImpl spec Set) (q : OracleQuery spec α) :
    reachableWhen o (liftM q) = q.cont '' o q.input
    source
    theorem OracleComp.reachableWhen_query {ι : Type u} {spec : OracleSpec ι} (o : QueryImpl spec Set) (t : spec.Domain) :
    reachableWhen o (liftM (OracleSpec.query t)) = o t
    source
    @[simp]
    theorem OracleComp.reachableWhen_bind {ι : Type u} {spec : OracleSpec ι} {α β : Type v} (o : QueryImpl spec Set) (oa : OracleComp spec α) (ob : α → OracleComp spec β) :
    reachableWhen o (oa >>= ob) = ⋃ x ∈ reachableWhen o oa, reachableWhen o (ob x)
    source
    theorem OracleComp.reachableWhen_query_bind {ι : Type u} {spec : OracleSpec ι} {α : Type v} (o : QueryImpl spec Set) (t : spec.Domain) (next : spec.Range t → OracleComp spec α) :
    reachableWhen o (liftM (OracleSpec.query t) >>= next) = ⋃ direction ∈ o t, reachableWhen o (next direction)
    source
    theorem OracleComp.reachableWhen_mono {ι : Type u} {spec : OracleSpec ι} {α : Type v} {o₁ o₂ : QueryImpl spec Set} (h : ∀ (q : spec.Domain), o₁ q ⊆ o₂ q) (oa : OracleComp spec α) :
    reachableWhen o₁ oa ⊆ reachableWhen o₂ oa
    source
    theorem OracleComp.reachableWhen_univ_eq_support {ι : Type u} {spec : OracleSpec ι} {α : Type v} (oa : OracleComp spec α) :
    reachableWhen (fun (x : spec.Domain) => Set.univ) oa = support oa

    Admitting every typed response recovers the free tree's attachment support.

    source
    @[deprecated "VCVio retiring support API: use reachableWhen" (since := "2026-09-14")]
    def OracleComp.supportWhen {ι : Type u} {spec : OracleSpec ι} {α : Type v} (o : QueryImpl spec Set) (mx : OracleComp spec α) :
    Set α

    The SetM interpretation of possible outputs under a query-response assignment.

    Instances For
      source
      @[simp, deprecated "VCVio retiring support API: use reachableWhen_pure" (since := "2026-09-14")]
      theorem OracleComp.supportWhen_pure {ι : Type u} {spec : OracleSpec ι} {α : Type v} (o : QueryImpl spec Set) (x : α) :
      supportWhen o (pure x) = {x}
      source
      @[deprecated "VCVio retiring support API: use reachableWhen_query_bind" (since := "2026-09-14")]
      theorem OracleComp.supportWhen_query_bind {ι : Type u} {spec : OracleSpec ι} {α : Type v} (o : QueryImpl spec Set) (q : spec.Domain) (oa : spec.Range q → OracleComp spec α) :
      supportWhen o (liftM (OracleSpec.query q) >>= oa) = ⋃ x ∈ o q, supportWhen o (oa x)
      source
      @[simp, deprecated "VCVio retiring support API: use reachableWhen_bind" (since := "2026-09-14")]
      theorem OracleComp.supportWhen_bind {ι : Type u} {spec : OracleSpec ι} {α β : Type v} (o : QueryImpl spec Set) (oa : OracleComp spec α) (ob : α → OracleComp spec β) :
      supportWhen o (oa >>= ob) = ⋃ x ∈ supportWhen o oa, supportWhen o (ob x)

      Reachable outputs of a bind are the reachable outputs of the continuation over reachable outputs of the first computation.

      source
      @[deprecated "VCVio retiring support API: use reachableWhen_bind" (since := "2026-09-14")]
      theorem OracleComp.mem_supportWhen_bind_iff {ι : Type u} {spec : OracleSpec ι} {α β : Type v} (o : QueryImpl spec Set) (oa : OracleComp spec α) (ob : α → OracleComp spec β) (y : β) :
      y ∈ supportWhen o (oa >>= ob) ↔ ∃ x ∈ supportWhen o oa, y ∈ supportWhen o (ob x)

      Membership form of [OracleComp.supportWhen_bind].

      source
      @[deprecated "VCVio retiring support API: use reachableWhen_mono" (since := "2026-09-14")]
      theorem OracleComp.supportWhen_mono {ι : Type u} {spec : OracleSpec ι} {α : Type v} {o₁ o₂ : QueryImpl spec Set} (h : ∀ (q : spec.Domain), o₁ q ⊆ o₂ q) (oa : OracleComp spec α) :
      supportWhen o₁ oa ⊆ supportWhen o₂ oa

      Enlarging the set of possible oracle outputs only enlarges the reachable output set.

      source
      @[deprecated "VCVio retiring support API: use reachableWhen" (since := "2026-09-15")]
      theorem OracleComp.supportWhen_eq_reachableWhen {ι : Type u} {spec : OracleSpec ι} {α : Type v} (o : QueryImpl spec Set) (oa : OracleComp spec α) :
      supportWhen o oa = reachableWhen o oa

      The SetM interpretation agrees with operation-indexed reachability.