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 NeverFailWhen.
def
OracleComp.allWhen
{ι : Type u}
{spec : OracleSpec ι}
{α : Type v}
(Q : spec.Domain → Prop)
(P : {α : Type v} → α → Prop)
(possible_outputs : (x : spec.Domain) → Set (spec.Range x))
(oa : OracleComp spec α)
:
Given that oracle outputs are bounded by possible_outputs, all query inputs in the
computation satisfy Q and all pure values satisfy P.
Equations
Instances For
def
OracleComp.someWhen
{ι : Type u}
{spec : OracleSpec ι}
{α : Type v}
(Q : spec.Domain → Prop)
(P : {α : Type v} → α → Prop)
(possible_outputs : (x : spec.Domain) → Set (spec.Range x))
(oa : OracleComp spec α)
:
Given that oracle outputs are bounded by possible_outputs, some query input in the
computation satisfies Q or some pure value satisfyies P.