Probability Distributions on Potentially Failing Computations

This file lifts MonadLiftT _ SetM and MonadLiftT _ SPMF semantics through the OptionT monad transformer.

dt: should add more instances and connecting lemmas

@[implicit_reducible]

noncomputable instance OptionT.instMonadLiftTSetM {m : Type u → Type v} [Monad m] [MonadLiftT m SetM] : MonadLiftT (OptionT m) SetM

Standalone MonadLiftT (OptionT m) SetM instance under the weaker [MonadLiftT m SetM] assumption. Keeping this standalone means support on OptionT m works without requiring a full MonadLiftT m SPMF lift — only MonadLiftT m SetM is needed.

We declare a MonadLiftT (rather than MonadLift) so the instance has no semiOutParam arguments to synthesize — OptionT m's m cannot be recovered from the SetM codomain.

instance OptionT.instLawfulMonadLiftTSetM {m : Type u → Type v} [Monad m] [MonadLiftT m SetM] [LawfulMonadLiftT m SetM] : LawfulMonadLiftT (OptionT m) SetM

theorem OptionT.support_def {m : Type u → Type v} [Monad m] {α : Type u} [MonadLiftT m SetM] (mx : OptionT m α) : support mx = some ⁻¹' support mx.run

@[simp]

theorem OptionT.mem_support_iff {m : Type u → Type v} [Monad m] {α : Type u} [MonadLiftT m SetM] (mx : OptionT m α) (x : α) : x ∈ support mx ↔ some x ∈ support mx.run

@[simp]

theorem OptionT.support_liftM {m : Type u → Type v} [Monad m] {α : Type u} [MonadLiftT m SetM] [LawfulMonadLiftT m SetM] (mx : m α) : support (liftM mx) = support mx

@[simp]

theorem OptionT.support_lift {m : Type u → Type v} [Monad m] {α : Type u} [MonadLiftT m SetM] [LawfulMonadLiftT m SetM] (mx : m α) : support (OptionT.lift mx) = support mx

@[implicit_reducible]

noncomputable instance OptionT.instHasEvalFinset (m : Type u → Type v) [Monad m] [MonadLiftT m SetM] [HasEvalFinset m] : HasEvalFinset (OptionT m)

Lift a HasEvalFinset instance to OptionT. by just taking preimage under some.

theorem OptionT.finSupport_def {m : Type u → Type v} [Monad m] {α : Type u} [MonadLiftT m SetM] [HasEvalFinset m] [DecidableEq α] (mx : OptionT m α) : finSupport mx = (finSupport mx.run).preimage some ⋯

@[simp]

theorem OptionT.mem_finSupport_iff {m : Type u → Type v} [Monad m] {α : Type u} [MonadLiftT m SetM] [HasEvalFinset m] [DecidableEq α] (mx : OptionT m α) (x : α) : x ∈ finSupport mx ↔ some x ∈ finSupport mx.run

@[simp]

theorem OptionT.finSupport_liftM {m : Type u → Type v} [Monad m] {α : Type u} [MonadLiftT m SetM] [HasEvalFinset m] [LawfulMonadLiftT m SetM] [LawfulMonad m] [DecidableEq α] (mx : m α) : finSupport (liftM mx) = finSupport mx

@[simp]

theorem OptionT.finSupport_lift {m : Type u → Type v} [Monad m] {α : Type u} [MonadLiftT m SetM] [HasEvalFinset m] [LawfulMonadLiftT m SetM] [LawfulMonad m] [DecidableEq α] (mx : m α) : finSupport (OptionT.lift mx) = finSupport mx

@[implicit_reducible]

noncomputable instance OptionT.instMonadLiftTSPMF (m : Type u → Type v) [Monad m] [MonadLiftT m SPMF] [LawfulMonadLiftT m SPMF] : MonadLiftT (OptionT m) SPMF

Lift a MonadLiftT m SPMF instance to MonadLiftT (OptionT m) SPMF. Failure in OptionT contributes to the failure mass of the resulting SPMF.

instance OptionT.instLawfulMonadLiftTSPMF (m : Type u → Type v) [Monad m] [MonadLiftT m SPMF] [LawfulMonadLiftT m SPMF] : LawfulMonadLiftT (OptionT m) SPMF

instance OptionT.instLawfulFailure (m : Type u → Type v) [Monad m] [MonadLiftT m SetM] [LawfulMonadLiftT m SetM] [MonadLiftT m SPMF] [LawfulMonadLiftT m SPMF] : HasEvalSet.LawfulFailure (OptionT m)

instance OptionT.instEvalDistCompatible (m : Type u → Type v) [Monad m] [MonadLiftT m SetM] [LawfulMonadLiftT m SetM] [MonadLiftT m SPMF] [LawfulMonadLiftT m SPMF] [EvalDistCompatible m] : EvalDistCompatible (OptionT m)

The SetM-lift of OptionT m (preimage of support mx.run under some) agrees with the SPMF-lift (the OptionT.mapM' bind into SPMF) on outputs, given EvalDistCompatible m.

theorem OptionT.evalDist_eq {m : Type u → Type v} [Monad m] {α : Type u} [MonadLiftT m SPMF] [LawfulMonadLiftT m SPMF] (mx : OptionT m α) : 𝒟[mx] = (fun {α : Type u} (x : OptionT m α) => (OptionT.mapM' (MonadHom.ofLift m SPMF)).toFun α x) mx

theorem OptionT.probOutput_eq {m : Type u → Type v} [Monad m] {α : Type u} [MonadLiftT m SPMF] [LawfulMonadLiftT m SPMF] (mx : OptionT m α) (x : α) : Pr[= x | mx] = Pr[= some x | mx.run]

theorem OptionT.probEvent_eq {m : Type u → Type v} [Monad m] {α : Type u} [MonadLiftT m SPMF] [LawfulMonadLiftT m SPMF] (mx : OptionT m α) (p : α → Prop) [DecidablePred p] : probEvent mx p + Pr[= none | mx.run] = probEvent mx.run fun (x : Option α) => Option.all (fun (b : α) => decide (p b)) x = true

theorem OptionT.probFailure_eq {m : Type u → Type v} [Monad m] {α : Type u} [MonadLiftT m SPMF] [LawfulMonadLiftT m SPMF] (mx : OptionT m α) : Pr[⊥ | mx] = Pr[⊥ | mx.run] + Pr[= none | mx.run]

@[simp]

theorem OptionT.probOutput_liftM {m : Type u → Type v} [Monad m] {α : Type u} [MonadLiftT m SPMF] [LawfulMonadLiftT m SPMF] [LawfulMonad m] (mx : m α) (x : α) : Pr[= x | liftM mx] = Pr[= x | mx]

@[simp]

theorem OptionT.probOutput_lift {m : Type u → Type v} [Monad m] {α : Type u} [MonadLiftT m SPMF] [LawfulMonadLiftT m SPMF] [LawfulMonad m] (mx : m α) (x : α) : Pr[= x | OptionT.lift mx] = Pr[= x | mx]

@[simp]

theorem OptionT.probEvent_liftM {m : Type u → Type v} [Monad m] {α : Type u} [MonadLiftT m SPMF] [LawfulMonadLiftT m SPMF] [LawfulMonad m] (mx : m α) (p : α → Prop) : probEvent (liftM mx) p = probEvent mx p

@[simp]

theorem OptionT.probEvent_lift {m : Type u → Type v} [Monad m] {α : Type u} [MonadLiftT m SPMF] [LawfulMonadLiftT m SPMF] [LawfulMonad m] (mx : m α) (p : α → Prop) : probEvent (OptionT.lift mx) p = probEvent mx p

@[simp]

theorem OptionT.probFailure_liftM {m : Type u → Type v} [Monad m] {α : Type u} [MonadLiftT m SPMF] [LawfulMonadLiftT m SPMF] [LawfulMonad m] (mx : m α) : Pr[⊥ | liftM mx] = Pr[⊥ | mx]

@[simp]

theorem OptionT.probFailure_lift {m : Type u → Type v} [Monad m] {α : Type u} [MonadLiftT m SPMF] [LawfulMonadLiftT m SPMF] [LawfulMonad m] (mx : m α) : Pr[⊥ | OptionT.lift mx] = Pr[⊥ | mx]