Documentation

VCVio.OracleComp.Traversal

Traversing Possible Paths of a Computation. #

This file defines functions alwaysWhen and someWhen that allow for traversing a computation's structure to check some given predicates on each node, using a set of possible outputs for that traversal. These definitions are Prop not Bool and should usually only be used in proofs, not in defining an actual computaion.

The file also contains many special cases of these functions like neverFailsWhen.

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

All the given predicates hold on a computation when queries respond with elements of possible_outputs q for every query q

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    def OracleComp.someWhen {ι : Type u} {spec : OracleSpec ι} {α : Type v} (Q : {α : Type v} → spec.OracleQuery αProp) (F : Prop) (possible_outputs : {α : Type v} → spec.OracleQuery αSet α) (oa : OracleComp spec α) :

    One of the given predicates hold on a computation when queries respond with elements of possible_outputs q for every query q

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      @[simp]
      theorem OracleComp.allWhen_pure {ι : Type u} {spec : OracleSpec ι} {α : Type v} (Q : {α : Type v} → spec.OracleQuery αProp) (F : Prop) (possible_outputs : {α : Type v} → spec.OracleQuery αSet α) (x : α) :
      allWhen (fun {α : Type v} => Q) F (fun {α : Type v} => possible_outputs) (pure x)
      @[simp]
      theorem OracleComp.someWhen_pure {ι : Type u} {spec : OracleSpec ι} {α : Type v} (Q : {α : Type v} → spec.OracleQuery αProp) (F : Prop) (possible_outputs : {α : Type v} → spec.OracleQuery αSet α) (x : α) :
      someWhen (fun {α : Type v} => Q) F (fun {α : Type v} => possible_outputs) (pure x)
      @[simp]
      theorem OracleComp.allWhen_failure_iff {ι : Type u} {spec : OracleSpec ι} {α : Type v} (Q : {α : Type v} → spec.OracleQuery αProp) (F : Prop) (possible_outputs : {α : Type v} → spec.OracleQuery αSet α) :
      allWhen (fun {α : Type v} => Q) F (fun {α : Type v} => possible_outputs) failure F
      @[simp]
      theorem OracleComp.allWhen_query_iff {ι : Type u} {spec : OracleSpec ι} {α : Type v} (Q : {α : Type v} → spec.OracleQuery αProp) (F : Prop) (possible_outputs : {α : Type v} → spec.OracleQuery αSet α) (q : spec.OracleQuery α) :
      allWhen (fun {α : Type v} => Q) F (fun {α : Type v} => possible_outputs) (liftM q) Q q
      @[simp]
      theorem OracleComp.allWhen_query_bind {ι : Type u} {spec : OracleSpec ι} {α β : Type v} (Q : {α : Type v} → spec.OracleQuery αProp) (F : Prop) (possible_outputs : {α : Type v} → spec.OracleQuery αSet α) (q : spec.OracleQuery α) (oa : αOracleComp spec β) :
      allWhen (fun {α : Type v} => Q) F (fun {α : Type v} => possible_outputs) (liftM q >>= oa) Q q xpossible_outputs q, allWhen (fun {α : Type v} => Q) F (fun {α : Type v} => possible_outputs) (oa x)
      @[simp]
      theorem OracleComp.allWhen_bind_iff {ι : Type u} {spec : OracleSpec ι} {α β : Type v} (Q : {α : Type v} → spec.OracleQuery αProp) (F : Prop) (possible_outputs : {α : Type v} → spec.OracleQuery αSet α) (oa : OracleComp spec α) (ob : αOracleComp spec β) :
      allWhen (fun {α : Type v} => Q) F (fun {α : Type v} => possible_outputs) (oa >>= ob) allWhen (fun {α : Type v} => Q) F (fun {α : Type v} => possible_outputs) oa xoa.supportWhen fun {α : Type v} => possible_outputs, allWhen (fun {α : Type v} => Q) F (fun {α : Type v} => possible_outputs) (ob x)
      def OracleComp.neverFailsWhen {ι : Type u} {spec : OracleSpec ι} {α : Type v} (oa : OracleComp spec α) (possible_outputs : {α : Type v} → spec.OracleQuery αSet α) :

      oa never fails if when responses to queries q are in possible_outputs q.

      Equations
      Instances For
        @[reducible, inline]
        def OracleComp.neverFails {ι : Type u} {spec : OracleSpec ι} {α : Type v} (oa : OracleComp spec α) :

        oa never fails even when queries can output any possible value.

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

          oa might fail when responses to queries q are in possible_outputs q

          Equations
          Instances For
            @[reducible, inline]
            def OracleComp.mayFail {ι : Type u} {spec : OracleSpec ι} {α : Type v} (oa : OracleComp spec α) :

            oa might fail if queries can output any possible value.

            Equations
            Instances For
              theorem OracleComp.neverFailsWhen_simulate {ι : Type u} {spec : OracleSpec ι} {α : Type v} {ι' : Type u_1} {spec' : OracleSpec ι'} (oa : OracleComp spec α) (possible_outputs : {α : Type v} → spec.OracleQuery αSet α) (h : oa.neverFailsWhen fun {α : Type v} => possible_outputs) (so : QueryImpl spec (OracleComp spec')) (h' : ∀ {α : Type v} (q : spec.OracleQuery α), (so.impl q).support possible_outputs q) (hso : ∀ {α : Type v} (q : spec.OracleQuery α), (so.impl q).neverFails) :
              theorem OracleComp.neverFails_eq_oracleComp_construct {ι : Type u} {spec : OracleSpec ι} {α : Type v} (oa : OracleComp spec α) :
              oa.neverFails = OracleComp.construct (fun (x : α) => True) (fun {β : Type v} (x : spec.OracleQuery β) (x : βOracleComp spec α) (r : βProp) => ∀ (x : β), r x) False oa
              theorem OracleComp.neverFails_eq_freeMonad_construct {ι : Type u} {spec : OracleSpec ι} {α : Type v} (oa : OracleComp spec α) :
              oa.neverFails = FreeMonad.construct (fun (t : Option α) => Option.rec False (fun (x : α) => True) t) (fun {β : Type v} (x : spec.OracleQuery β) (x : βFreeMonad spec.OracleQuery (Option α)) (r : βProp) => ∀ (x : β), r x) oa
              @[simp]
              theorem OracleComp.neverFails_pure {ι : Type u} {spec : OracleSpec ι} {α : Type v} (x : α) :
              @[simp]
              theorem OracleComp.neverFails_query {ι : Type u} {spec : OracleSpec ι} {α : Type v} (q : spec.OracleQuery α) :
              @[simp]
              theorem OracleComp.neverFails_query_bind_iff {ι : Type u} {spec : OracleSpec ι} {α β : Type v} {q : spec.OracleQuery α} {oa : αOracleComp spec β} :
              (liftM q >>= oa).neverFails ∀ (x : α), (oa x).neverFails
              theorem OracleComp.neverFails_query_bind {ι : Type u} {spec : OracleSpec ι} {α β : Type v} {q : spec.OracleQuery α} {oa : αOracleComp spec β} :
              (liftM q >>= oa).neverFails∀ (x : α), (oa x).neverFails

              Alias of the forward direction of OracleComp.neverFails_query_bind_iff.

              @[simp]
              @[simp]
              theorem OracleComp.neverFails_bind_iff {ι : Type u} {spec : OracleSpec ι} {α β : Type v} (oa : OracleComp spec α) (ob : αOracleComp spec β) :
              (oa >>= ob).neverFails oa.neverFails xoa.support, (ob x).neverFails
              theorem OracleComp.neverFails_bind {ι : Type u} {spec : OracleSpec ι} {α β : Type v} (oa : OracleComp spec α) (ob : αOracleComp spec β) :
              (oa >>= ob).neverFailsoa.neverFails xoa.support, (ob x).neverFails

              Alias of the forward direction of OracleComp.neverFails_bind_iff.

              @[simp]
              theorem OracleComp.neverFails_map_iff {ι : Type u} {spec : OracleSpec ι} {α β : Type v} (oa : OracleComp spec α) (f : αβ) :
              Equations
              • One or more equations did not get rendered due to their size.
              @[simp]
              theorem OracleComp.neverFails_guard {ι : Type u} {spec : OracleSpec ι} {α : Type v} (p : Prop) [Decidable p] (oa : OracleComp spec α) (h : oa.neverFails) :