Lemmas About the Distribution Semantics of Failure Operations

This file collects various lemmas about the operations associated to Alternative, like guard, orElse, tryM?, etc.

@[simp]

theorem OracleComp.evalDist_orElse {ι : Type u} {spec : OracleSpec ι} {α : Type v} [h : spec.FiniteRange] (oa oa' : OracleComp spec α) : (oa <|> oa').evalDist = (oa.evalDist <|> oa'.evalDist)

@[simp]

theorem OracleComp.probFailure_orElse {ι : Type u} {spec : OracleSpec ι} {α : Type u} [h : spec.FiniteRange] (oa oa' : OracleComp spec α) : [⊥|oa <|> oa'] = [⊥|oa] * [⊥|oa']

@[simp]

theorem OracleComp.support_orElse {ι : Type u} {spec : OracleSpec ι} {α : Type u} (oa oa' : OracleComp spec α) [Decidable oa.neverFails] : (oa <|> oa').support = if oa.neverFails then oa.support else oa.support ∪ oa'.support