Qualitative Prop-valued Hoare triples for OracleComp

This file registers the qualitative Prop-valued unary monad algebra for OracleComp spec. The carrier is Prop with its standard complete-lattice structure (≤ is implication), and μ (oa : OracleComp spec Prop) is the almost-sure assertion allOutputsSatisfy id oa = ∀ x ∈ support oa, x.

The induced MAlgOrdered.wp is the support-based weakest precondition: wp oa post ↔ allOutputsSatisfy post oa = ∀ x ∈ support oa, post x.

This is the qualitative companion of the quantitative MAlgOrdered (OracleComp spec) ℝ≥0∞ in VCVio/ProgramLogic/Unary/HoareTriple.lean. Together they let MAlgRelOrdered.Anchored (in ToMathlib/Control/Monad/RelationalAlgebra.lean) state its anchoring axioms uniformly across the qualitative and quantitative settings.

@[implicit_reducible]

instance OracleComp.ProgramLogic.PropLogic.instMAlgOrdered {ι : Type u} {spec : OracleSpec ι} : MAlgOrdered (OracleComp spec) Prop

The qualitative Prop-valued unary monad algebra for OracleComp.

μ is the almost-sure assertion allOutputsSatisfy id; the induced wp is the support-based weakest precondition; Triple pre oa post is pre → allOutputsSatisfy post oa.

theorem OracleComp.ProgramLogic.PropLogic.wp_iff_forall_support {ι : Type u} {spec : OracleSpec ι} {α : Type} (oa : OracleComp spec α) (post : α → Prop) : MAlgOrdered.wp oa post ↔ ∀ x ∈ support oa, post x

Support-based characterization of the Prop-valued WP for OracleComp.