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

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

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

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

@[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 ∧ ∀ x ∈ possible_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 ∧ ∀ x ∈ oa.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 α) : Prop

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

@[reducible, inline]

def OracleComp.neverFails {ι : Type u} {spec : OracleSpec ι} {α : Type v} (oa : OracleComp spec α) : Prop

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

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

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

@[reducible, inline]

def OracleComp.mayFail {ι : Type u} {spec : OracleSpec ι} {α : Type v} (oa : OracleComp spec α) : Prop

oa might fail if queries can output any possible value.

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) : (simulateQ so oa).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 : α) : (pure x).neverFails

@[simp]

theorem OracleComp.neverFails_query {ι : Type u} {spec : OracleSpec ι} {α : Type v} (q : spec.OracleQuery α) : (liftM q).neverFails

@[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]

theorem OracleComp.not_neverFails_failure {ι : Type u} {spec : OracleSpec ι} {α : Type v} : ¬failure.neverFails

@[simp]

theorem OracleComp.neverFails_bind_iff {ι : Type u} {spec : OracleSpec ι} {α β : Type v} (oa : OracleComp spec α) (ob : α → OracleComp spec β) : (oa >>= ob).neverFails ↔ oa.neverFails ∧ ∀ x ∈ oa.support, (ob x).neverFails

theorem OracleComp.neverFails_bind {ι : Type u} {spec : OracleSpec ι} {α β : Type v} (oa : OracleComp spec α) (ob : α → OracleComp spec β) : (oa >>= ob).neverFails → oa.neverFails ∧ ∀ x ∈ oa.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 : α → β) : (f <$> oa).neverFails ↔ oa.neverFails

instance OracleComp.instDecidablePredNeverFailsOfFiniteRange {ι : Type u} {spec : OracleSpec ι} {α : Type v} [spec.FiniteRange] : DecidablePred neverFails

@[simp]

theorem OracleComp.neverFails_guard {ι : Type u} {spec : OracleSpec ι} {α : Type v} (p : Prop) [Decidable p] (oa : OracleComp spec α) (h : oa.neverFails) : (if p then oa else failure).neverFails ↔ p