Traversing Possible Paths of a Computation.

This file defines functions allWhen 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 computation.

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 α) : Prop

Given that oracle outputs are bounded by possible_outputs, all query inputs in the computation satisfy Q and all pure values satisfy P.

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 α) : Prop

Given that oracle outputs are bounded by possible_outputs, some query input in the computation satisfies Q or some pure value satisfyies P.

@[simp]

theorem OracleComp.allWhen_pure {ι : Type u} {spec : OracleSpec ι} {α : Type v} (x : α) (Q : spec.Domain → Prop) (P : {α : Type v} → α → Prop) (possible_outputs : (x : spec.Domain) → Set (spec.Range x)) : allWhen Q (fun {α : Type v} => P) possible_outputs (pure x) = P x

@[simp]

theorem OracleComp.someWhen_pure {ι : Type u} {spec : OracleSpec ι} {α : Type v} (x : α) (Q : spec.Domain → Prop) (P : {α : Type v} → α → Prop) (possible_outputs : (x : spec.Domain) → Set (spec.Range x)) : someWhen Q (fun {α : Type v} => P) possible_outputs (pure x) = P x

@[simp]

theorem OracleComp.allWhen_query_bind {ι : Type u} {spec : OracleSpec ι} {α : Type v} {Q : spec.Domain → Prop} {P : {α : Type v} → α → Prop} {possible_outputs : (x : spec.Domain) → Set (spec.Range x)} (q : spec.Domain) (oa : spec.Range q → OracleComp spec α) : allWhen Q (fun {α : Type v} => P) possible_outputs (liftM (query q) >>= oa) ↔ Q q ∧ ∀ x ∈ possible_outputs q, allWhen Q (fun {α : Type v} => P) possible_outputs (oa x)