Traversing Possible Paths of a Computation

This file defines structural predicates for checking whether all or some reachable paths of an OracleComp satisfy predicates on query nodes and final outputs, relative to a chosen set of possible oracle outputs.

It also connects those structural predicates to the denotational set supportWhen, so proofs can move cleanly between the syntax-level traversal view and the reachable-output view.

def OracleComp.allPathsSatisfy {ι : Type u} {spec : OracleSpec ι} {α : Type v} (queryPred : spec.Domain → Prop) (outputPred : α → Prop) (possibleOutputs : (x : spec.Domain) → Set (spec.Range x)) (oa : OracleComp spec α) : Prop

Given that oracle outputs are bounded by possibleOutputs, every reachable query input in the computation satisfies queryPred, and every reachable pure output satisfies outputPred.

def OracleComp.somePathSatisfies {ι : Type u} {spec : OracleSpec ι} {α : Type v} (queryPred : spec.Domain → Prop) (outputPred : α → Prop) (possibleOutputs : (x : spec.Domain) → Set (spec.Range x)) (oa : OracleComp spec α) : Prop

Given that oracle outputs are bounded by possibleOutputs, some reachable query input in the computation satisfies queryPred, or some reachable pure output satisfies outputPred.

def OracleComp.allOutputsSatisfyWhen {ι : Type u} {spec : OracleSpec ι} {α : Type v} (outputPred : α → Prop) (possibleOutputs : (x : spec.Domain) → Set (spec.Range x)) (oa : OracleComp spec α) : Prop

Output-only view of [OracleComp.allPathsSatisfy]: every output reachable under possibleOutputs satisfies outputPred.

def OracleComp.someOutputSatisfiesWhen {ι : Type u} {spec : OracleSpec ι} {α : Type v} (outputPred : α → Prop) (possibleOutputs : (x : spec.Domain) → Set (spec.Range x)) (oa : OracleComp spec α) : Prop

Output-only view of [OracleComp.somePathSatisfies]: some output reachable under possibleOutputs satisfies outputPred.

@[simp]

theorem OracleComp.allPathsSatisfy_pure {ι : Type u} {spec : OracleSpec ι} {α : Type v} {queryPred : spec.Domain → Prop} {outputPred : α → Prop} {possibleOutputs : (x : spec.Domain) → Set (spec.Range x)} (x : α) : allPathsSatisfy queryPred outputPred possibleOutputs (pure x) = outputPred x

@[simp]

theorem OracleComp.somePathSatisfies_pure {ι : Type u} {spec : OracleSpec ι} {α : Type v} {queryPred : spec.Domain → Prop} {outputPred : α → Prop} {possibleOutputs : (x : spec.Domain) → Set (spec.Range x)} (x : α) : somePathSatisfies queryPred outputPred possibleOutputs (pure x) = outputPred x

@[simp]

theorem OracleComp.allPathsSatisfy_query_bind {ι : Type u} {spec : OracleSpec ι} {α : Type v} {queryPred : spec.Domain → Prop} {outputPred : α → Prop} {possibleOutputs : (x : spec.Domain) → Set (spec.Range x)} (q : spec.Domain) (oa : spec.Range q → OracleComp spec α) : allPathsSatisfy queryPred outputPred possibleOutputs (liftM (OracleSpec.query q) >>= oa) ↔ queryPred q ∧ ∀ x ∈ possibleOutputs q, allPathsSatisfy queryPred outputPred possibleOutputs (oa x)

@[simp]

theorem OracleComp.somePathSatisfies_query_bind {ι : Type u} {spec : OracleSpec ι} {α : Type v} {queryPred : spec.Domain → Prop} {outputPred : α → Prop} {possibleOutputs : (x : spec.Domain) → Set (spec.Range x)} (q : spec.Domain) (oa : spec.Range q → OracleComp spec α) : somePathSatisfies queryPred outputPred possibleOutputs (liftM (OracleSpec.query q) >>= oa) ↔ queryPred q ∨ ∃ x ∈ possibleOutputs q, somePathSatisfies queryPred outputPred possibleOutputs (oa x)

theorem OracleComp.allOutputsSatisfyWhen_iff_supportWhen {ι : Type u} {spec : OracleSpec ι} {α : Type v} (outputPred : α → Prop) (possibleOutputs : (x : spec.Domain) → Set (spec.Range x)) (oa : OracleComp spec α) : allOutputsSatisfyWhen outputPred possibleOutputs oa ↔ ∀ x ∈ supportWhen possibleOutputs oa, outputPred x

theorem OracleComp.someOutputSatisfiesWhen_iff_supportWhen {ι : Type u} {spec : OracleSpec ι} {α : Type v} (outputPred : α → Prop) (possibleOutputs : (x : spec.Domain) → Set (spec.Range x)) (oa : OracleComp spec α) : someOutputSatisfiesWhen outputPred possibleOutputs oa ↔ ∃ x ∈ supportWhen possibleOutputs oa, outputPred x

@[simp]

theorem OracleComp.allPathsSatisfy_bind_iff {ι : Type u} {spec : OracleSpec ι} {α β : Type v} (queryPred : spec.Domain → Prop) (outputPred : β → Prop) (possibleOutputs : (x : spec.Domain) → Set (spec.Range x)) (oa : OracleComp spec α) (ob : α → OracleComp spec β) : allPathsSatisfy queryPred outputPred possibleOutputs (oa >>= ob) ↔ allPathsSatisfy queryPred (fun (x : α) => allPathsSatisfy queryPred outputPred possibleOutputs (ob x)) possibleOutputs oa

A bind satisfies a universal path property exactly when every path of the first computation leads to a continuation that also satisfies that path property.

@[simp]

theorem OracleComp.somePathSatisfies_bind_iff {ι : Type u} {spec : OracleSpec ι} {α β : Type v} (queryPred : spec.Domain → Prop) (outputPred : β → Prop) (possibleOutputs : (x : spec.Domain) → Set (spec.Range x)) (oa : OracleComp spec α) (ob : α → OracleComp spec β) : somePathSatisfies queryPred outputPred possibleOutputs (oa >>= ob) ↔ somePathSatisfies queryPred (fun (x : α) => somePathSatisfies queryPred outputPred possibleOutputs (ob x)) possibleOutputs oa

A bind satisfies an existential path property exactly when either the first computation already satisfies it on some path, or one reachable continuation does.

@[simp]

theorem OracleComp.allOutputsSatisfyWhen_bind_iff {ι : Type u} {spec : OracleSpec ι} {α β : Type v} (outputPred : β → Prop) (possibleOutputs : (x : spec.Domain) → Set (spec.Range x)) (oa : OracleComp spec α) (ob : α → OracleComp spec β) : allOutputsSatisfyWhen outputPred possibleOutputs (oa >>= ob) ↔ allOutputsSatisfyWhen (fun (x : α) => allOutputsSatisfyWhen outputPred possibleOutputs (ob x)) possibleOutputs oa

Output-only specialization of [OracleComp.allPathsSatisfy_bind_iff].

@[simp]

theorem OracleComp.someOutputSatisfiesWhen_bind_iff {ι : Type u} {spec : OracleSpec ι} {α β : Type v} (outputPred : β → Prop) (possibleOutputs : (x : spec.Domain) → Set (spec.Range x)) (oa : OracleComp spec α) (ob : α → OracleComp spec β) : someOutputSatisfiesWhen outputPred possibleOutputs (oa >>= ob) ↔ someOutputSatisfiesWhen (fun (x : α) => someOutputSatisfiesWhen outputPred possibleOutputs (ob x)) possibleOutputs oa

Output-only specialization of [OracleComp.somePathSatisfies_bind_iff].

theorem OracleComp.allOutputsSatisfyWhen_bind_iff_supportWhen {ι : Type u} {spec : OracleSpec ι} {α β : Type v} (outputPred : β → Prop) (possibleOutputs : (x : spec.Domain) → Set (spec.Range x)) (oa : OracleComp spec α) (ob : α → OracleComp spec β) : allOutputsSatisfyWhen outputPred possibleOutputs (oa >>= ob) ↔ ∀ x ∈ supportWhen possibleOutputs oa, allOutputsSatisfyWhen outputPred possibleOutputs (ob x)

Output-only bind rule phrased directly in terms of reachable intermediate outputs.

theorem OracleComp.someOutputSatisfiesWhen_bind_iff_supportWhen {ι : Type u} {spec : OracleSpec ι} {α β : Type v} (outputPred : β → Prop) (possibleOutputs : (x : spec.Domain) → Set (spec.Range x)) (oa : OracleComp spec α) (ob : α → OracleComp spec β) : someOutputSatisfiesWhen outputPred possibleOutputs (oa >>= ob) ↔ ∃ x ∈ supportWhen possibleOutputs oa, someOutputSatisfiesWhen outputPred possibleOutputs (ob x)

Existential output bind rule phrased directly in terms of reachable intermediate outputs.