WIP

src/Init/Control/Option.lean

@@ -28,7 +28,7 @@ failure occurred.
 /--
 Executes an action that might fail in the underlying monad `m`, returning `none` in case of failure.
 -/
-@[always_inline, inline]
+@[always_inline, inline, expose]
 def OptionT.run {m : Type u → Type v} {α : Type u} (x : OptionT m α) : m (Option α) :=
   x
 
@@ -70,7 +70,7 @@ instance {m : Type u → Type v} [Pure m] : Inhabited (OptionT m α) where
 /--
 Recovers from failures. Typically used via the `<|>` operator.
 -/
-@[always_inline, inline] protected def orElse (x : OptionT m α) (y : Unit → OptionT m α) : OptionT m α := OptionT.mk do
+@[always_inline, inline, expose] protected def orElse (x : OptionT m α) (y : Unit → OptionT m α) : OptionT m α := OptionT.mk do
   match (← x) with
   | some a => pure (some a)
   | _      => y ()
@@ -78,7 +78,7 @@ Recovers from failures. Typically used via the `<|>` operator.
 /--
 A recoverable failure.
 -/
-@[always_inline, inline] protected def fail : OptionT m α := OptionT.mk do
+@[always_inline, inline, expose] protected def fail : OptionT m α := OptionT.mk do
   pure none
 
 instance : Alternative (OptionT m) where
@@ -91,7 +91,7 @@ Converts a computation from the underlying monad into one that could fail, even
 This function is typically implicitly accessed via a `MonadLiftT` instance as part of [automatic
 lifting](lean-manual://section/monad-lifting).
 -/
-@[always_inline, inline] protected def lift (x : m α) : OptionT m α := OptionT.mk do
+@[always_inline, inline, expose] protected def lift (x : m α) : OptionT m α := OptionT.mk do
   return some (← x)
 
 instance : MonadLift m (OptionT m) := ⟨OptionT.lift⟩
@@ -101,11 +101,11 @@ instance : MonadFunctor m (OptionT m) := ⟨fun f x => f x⟩
 /--
 Handles failures by treating them as exceptions of type `Unit`.
 -/
-@[always_inline, inline] protected def tryCatch (x : OptionT m α) (handle : Unit → OptionT m α) : OptionT m α := OptionT.mk do
-  let some a ← x | handle ()
+@[always_inline, inline, expose] protected def tryCatch (x : OptionT m α) (handle : PUnit → OptionT m α) : OptionT m α := OptionT.mk do
+  let some a ← x | handle ⟨⟩
   pure <| some a
 
-instance : MonadExceptOf Unit (OptionT m) where
+instance : MonadExceptOf PUnit (OptionT m) where
   throw    := fun _ => OptionT.fail
   tryCatch := OptionT.tryCatch
 

src/Init/Prelude.lean

@@ -3703,7 +3703,7 @@ When thinking about `f` as potential side effects, `*>` evaluates first the left
 argument for their side effects, discarding the value of the left argument and returning the value
 of the right argument.
 
-For most applications, `Applicative` or `Monad` should be used rather than `SeqLeft` itself.
+For most applications, `Applicative` or `Monad` should be used rather than `SeqRight` itself.
 -/
 class SeqRight (f : Type u → Type v) : Type (max (u+1) v) where
   /--

src/Lean/Meta/InferType.lean

@@ -129,6 +129,12 @@ private def inferProjType (structName : Name) (idx : Nat) (e : Expr) : MetaM Exp
 def throwTypeExpected {α} (type : Expr) : MetaM α :=
   throwError "type expected{indentExpr type}"
 
+/--
+If `type : sort` and `sort` reduces to `Sort u` for some `u`, then `getLevel type` returns `u`.
+
+If `sort` is an assignable MVar, then `getLevel type` produces a fresh level metavariable `?u`,
+assigns the MVar to `Sort ?u` and returns `?u`.
+-/
 def getLevel (type : Expr) : MetaM Level := do
   let typeType ← inferType type
   let typeType ← whnfD typeType

src/Std/Do/Triple/SpecLemmas.lean

@@ -165,6 +165,13 @@ theorem Spec.monadLift_ExceptT [Monad m] [WPMonad m ps] (x : m α) (Q : PostCond
     (wp⟦x⟧ (fun a => Q.1 a, Q.2.2))
     Q := by simp [Triple, SPred.entails.refl]
 
+@[spec]
+theorem Spec.monadLift_OptionT [Monad m] [WPMonad m ps] (x : m α) (Q : PostCond α (.except PUnit ps)) :
+  Triple (ps:=.except PUnit ps)
+    (MonadLift.monadLift x : OptionT m α)
+    (wp⟦x⟧ (fun a => Q.1 a, Q.2.2))
+    Q := by simp [Triple, SPred.entails.refl]
+
 /-! # `MonadLiftT` -/
 
 attribute [spec] liftM instMonadLiftTOfMonadLift instMonadLiftT
@@ -186,8 +193,16 @@ theorem Spec.monadMap_ExceptT [Monad m] [WP m ps]
     (f : ∀{β}, m β → m β) {α} (x : ExceptT ε m α) (Q : PostCond α (.except ε ps)) :
   Triple (ps:=.except ε ps)
     (MonadFunctor.monadMap (m:=m) f x)
-    (wp⟦f x.run⟧ (fun | .ok a => Q.1 a | .error e => Q.2.1 e, Q.2.2))
-    Q := by simp only [Triple, WP.monadMap_ExceptT]; rfl
+    (wp⟦f x.run⟧ (fun e => e.casesOn Q.2.1 Q.1, Q.2.2))
+    Q := by simp [Triple]
+
+@[spec]
+theorem Spec.monadMap_OptionT [Monad m] [WP m ps]
+    (f : ∀{β}, m β → m β) {α} (x : OptionT m α) (Q : PostCond α (.except PUnit ps)) :
+  Triple (ps:=.except PUnit ps)
+    (MonadFunctor.monadMap (m:=m) f x)
+    (wp⟦f x.run⟧ (fun o => o.casesOn (Q.2.1 ⟨⟩) Q.1, Q.2.2))
+    Q := by simp [Triple]
 
 /-! # `MonadFunctorT` -/
 
@@ -228,6 +243,14 @@ theorem Spec.liftWith_ExceptT [Monad m] [WPMonad m ps]
       (wp⟦f (fun x => x.run)⟧ (Q.1, Q.2.2))
       Q := by simp [Triple]
 
+@[spec]
+theorem Spec.liftWith_OptionT [Monad m] [WPMonad m ps]
+  (f : (∀{β}, OptionT m β → m (Option β)) → m α) :
+    Triple (ps := .except PUnit ps)
+      (MonadControl.liftWith (m:=m) f)
+      (wp⟦f (fun x => x.run)⟧ (Q.1, Q.2.2))
+      Q := by simp [Triple]
+
 @[spec]
 theorem Spec.restoreM_StateT [Monad m] [WPMonad m ps] (x : m (α × σ)) :
     Triple
@@ -246,8 +269,15 @@ theorem Spec.restoreM_ReaderT [Monad m] [WPMonad m ps] (x : m α) :
 theorem Spec.restoreM_ExceptT [Monad m] [WPMonad m ps] (x : m (Except ε α)) :
     Triple (ps := .except ε ps)
       (MonadControl.restoreM x : ExceptT ε m α)
-      (wp⟦x⟧ (fun | .ok a => Q.1 a | .error e => Q.2.1 e, Q.2.2))
-      Q := by simp [Triple]; rfl
+      (wp⟦x⟧ (fun e => e.casesOn Q.2.1 Q.1, Q.2.2))
+      Q := by simp [Triple]
+
+@[spec]
+theorem Spec.restoreM_OptionT [Monad m] [WPMonad m ps] (x : m (Option α)) :
+    Triple (ps := .except PUnit ps)
+      (MonadControl.restoreM x : OptionT m α)
+      (wp⟦x⟧ (fun e => e.casesOn (Q.2.1 ⟨⟩) Q.1, Q.2.2))
+      Q := by simp [Triple]
 
 /-! # `MonadControlT` -/
 
@@ -362,6 +392,46 @@ theorem Spec.orElse_Except (Q : PostCond α (.except ε .pure)) :
     Triple (OrElse.orElse x h : Except ε α) (spred(wp⟦x⟧ (Q.1, fun _ => wp⟦h ()⟧ Q, Q.2.2))) spred(Q) := by
   simp [Triple]
 
+/-! # `OptionT` -/
+
+@[spec]
+theorem Spec.run_OptionT [WP m ps] (x : OptionT m α) :
+  Triple (ps:=ps)
+    (x.run : m (Option α))
+    (wp⟦x⟧ (fun a => Q.1 (.some a), fun _ => Q.1 .none, Q.2))
+    Q := by simp [Triple]
+
+@[spec]
+theorem Spec.throw_OptionT [Monad m] [WPMonad m ps] :
+    Triple (MonadExceptOf.throw e : OptionT m α) (spred(Q.2.1 e)) spred(Q) := by
+  simp [Triple]
+
+@[spec]
+theorem Spec.tryCatch_OptionT [Monad m] [WPMonad m ps] (Q : PostCond α (.except PUnit ps)) :
+    Triple (MonadExceptOf.tryCatch x h : OptionT m α) (spred(wp⟦x⟧ (Q.1, fun e => wp⟦h e⟧ Q, Q.2.2))) spred(Q) := by
+  simp [Triple]
+
+@[spec]
+theorem Spec.orElse_OptionT [Monad m] [WPMonad m ps] (Q : PostCond α (.except PUnit ps)) :
+    Triple (OrElse.orElse x h : OptionT m α) (spred(wp⟦x⟧ (Q.1, fun _ => wp⟦h ()⟧ Q, Q.2.2))) spred(Q) := by
+  simp [Triple]
+
+/-! # `Option` -/
+
+@[spec]
+theorem Spec.throw_Option [Monad m] [WPMonad m ps] :
+  Triple (MonadExceptOf.throw e : Option α) (spred(Q.2.1 e)) spred(Q) := SPred.entails.rfl
+
+@[spec]
+theorem Spec.tryCatch_Option (Q : PostCond α (.except PUnit .pure)) :
+    Triple (MonadExceptOf.tryCatch x h : Option α) (spred(wp⟦x⟧ (Q.1, fun e => wp⟦h e⟧ Q, Q.2.2))) spred(Q) := by
+  simp [Triple]
+
+@[spec]
+theorem Spec.orElse_Option (Q : PostCond α (.except PUnit .pure)) :
+    Triple (OrElse.orElse x h : Option α) (spred(wp⟦x⟧ (Q.1, fun _ => wp⟦h ()⟧ Q, Q.2.2))) spred(Q) := by
+  simp [Triple]
+
 /-! # `EStateM` -/
 
 @[spec]
@@ -431,7 +501,19 @@ theorem Spec.throw_StateT [WP m ps] [Monad m] [MonadExceptOf ε m] (Q : PostCond
 theorem Spec.throw_ExceptT_lift [WP m ps] [MonadExceptOf ε m] (Q : PostCond α (.except ε' ps)) :
   Triple (ps:=.except ε' ps)
     (MonadExceptOf.throw e : ExceptT ε' m α)
-    (wp⟦MonadExceptOf.throw (ε:=ε) e : m (Except ε' α)⟧ (fun | .ok a => Q.1 a | .error e => Q.2.1 e, Q.2.2))
+    (wp⟦MonadExceptOf.throw (ε:=ε) e : m (Except ε' α)⟧ (fun e => e.casesOn Q.2.1 Q.1, Q.2.2))
+    Q := by
+  simp [Triple]
+  apply (wp _).mono
+  simp
+  intro x
+  split <;> rfl
+
+@[spec]
+theorem Spec.throw_Option_lift [WP m ps] [MonadExceptOf ε m] (Q : PostCond α (.except PUnit ps)) :
+  Triple (ps:=.except PUnit ps)
+    (MonadExceptOf.throw e : OptionT m α)
+    (wp⟦MonadExceptOf.throw (ε:=ε) e : m (Option α)⟧ (fun o => o.casesOn (Q.2.1 ⟨⟩) Q.1, Q.2.2))
     Q := by
   simp [Triple]
   apply (wp _).mono
@@ -452,7 +534,20 @@ theorem Spec.tryCatch_ExceptT_lift [WP m ps] [MonadExceptOf ε m] (Q : PostCond
     Triple
       (ps:=.except ε' ps)
       (MonadExceptOf.tryCatch x h : ExceptT ε' m α)
-      (wp⟦MonadExceptOf.tryCatch (ε:=ε) x h : m (Except ε' α)⟧ (fun | .ok a => Q.1 a | .error e => Q.2.1 e, Q.2.2))
+      (wp⟦MonadExceptOf.tryCatch (ε:=ε) x h : m (Except ε' α)⟧ (fun e => e.casesOn Q.2.1 Q.1, Q.2.2))
+      Q := by
+  simp only [Triple]
+  apply (wp _).mono
+  simp
+  intro x
+  split <;> rfl
+
+@[spec]
+theorem Spec.tryCatch_OptionT_lift [WP m ps] [MonadExceptOf ε m] (Q : PostCond α (.except PUnit ps)) :
+    Triple
+      (ps:=.except PUnit ps)
+      (MonadExceptOf.tryCatch x h : OptionT m α)
+      (wp⟦MonadExceptOf.tryCatch (ε:=ε) x h : m (Option α)⟧ (fun o => o.casesOn (Q.2.1 ⟨⟩) Q.1, Q.2.2))
       Q := by
   simp only [Triple]
   apply (wp _).mono

src/Std/Do/WP/SimpLemmas.lean

@@ -44,6 +44,13 @@ theorem ExceptT_run [WP m ps] (x : ExceptT ε m α) :
   congr
   (ext x; cases x) <;> rfl
 
+@[simp]
+theorem OptionT_run [WP m ps] (x : OptionT m α) :
+    wp⟦x.run⟧ Q = wp⟦x⟧ (fun a => Q.1 (.some a), fun _ => Q.1 .none, Q.2) := by
+  simp [wp, OptionT.run]
+  congr
+  (ext x; cases x) <;> rfl
+
 /-! ## `WPMonad` -/
 
 @[simp]
@@ -83,6 +90,11 @@ theorem monadLift_ExceptT [Monad m] [WPMonad m ps] (x : m α) (Q : PostCond α (
   wp⟦MonadLift.monadLift x : ExceptT ε m α⟧ Q = wp⟦x⟧ (fun a => Q.1 a, Q.2.2) := by
     simp [wp, MonadLift.monadLift, ExceptT.lift, ExceptT.mk]
 
+@[simp]
+theorem monadLift_OptionT [Monad m] [WPMonad m ps] (x : m α) (Q : PostCond α (.except PUnit ps)) :
+  wp⟦MonadLift.monadLift x : OptionT m α⟧ Q = wp⟦x⟧ (fun a => Q.1 a, Q.2.2) := by
+    simp [wp, MonadLift.monadLift, OptionT.lift, OptionT.mk]
+
 @[simp]
 theorem monadLift_trans [WP o ps] [MonadLift n o] [MonadLiftT m n] :
   wp⟦MonadLiftT.monadLift x : o α⟧ Q = wp⟦MonadLift.monadLift (m:=n) (MonadLiftT.monadLift (m:=m) x) : o α⟧ Q := rfl
@@ -101,6 +113,9 @@ theorem lift_StateT [WP m ps] [Monad m] (x : m α) :
 theorem lift_ExceptT [WP m ps] [Monad m] (x : m α) :
   wp⟦ExceptT.lift x : ExceptT ε m α⟧ Q = wp⟦MonadLift.monadLift x : ExceptT ε m α⟧ Q := rfl
 
+@[simp]
+theorem lift_OptionT [WP m ps] [Monad m] (x : m α) :
+  wp⟦OptionT.lift x : OptionT m α⟧ Q = wp⟦MonadLift.monadLift x : OptionT m α⟧ Q := rfl
 
 -- MonadReader
 
@@ -251,10 +266,17 @@ theorem monadMap_ReaderT [Monad m] [WP m ps]
 @[simp]
 theorem monadMap_ExceptT [Monad m] [WP m ps]
   (f : ∀{β}, m β → m β) {α} (x : ExceptT ε m α) (Q : PostCond α (.except ε ps)) :
-    wp⟦mmap (m:=m) f x⟧ Q = wp⟦f x.run⟧ (fun | .ok a => Q.1 a | .error e => Q.2.1 e, Q.2.2) := by
+    wp⟦mmap (m:=m) f x⟧ Q = wp⟦f x.run⟧ (fun e => e.casesOn Q.2.1 Q.1, Q.2.2) := by
   simp [wp, MonadFunctor.monadMap, ExceptT.run]
   congr; ext; split <;> rfl
 
+@[simp]
+theorem monadMap_OptionT [Monad m] [WP m ps]
+  (f : ∀{β}, m β → m β) {α} (x : OptionT m α) (Q : PostCond α (.except PUnit ps)) :
+    wp⟦mmap (m:=m) f x⟧ Q = wp⟦f x.run⟧ (fun o => o.casesOn (Q.2.1 ⟨⟩) Q.1, Q.2.2) := by
+  simp [wp, MonadFunctor.monadMap, OptionT.run]
+  congr; ext; split <;> rfl
+
 @[simp]
 theorem monadMap_trans [WP o ps] [MonadFunctor n o] [MonadFunctorT m n] :
   wp⟦MonadFunctorT.monadMap f x : o α⟧ Q = wp⟦MonadFunctor.monadMap (m:=n) (MonadFunctorT.monadMap (m:=m) f) x : o α⟧ Q := rfl
@@ -308,6 +330,13 @@ theorem liftWith_ExceptT [Monad m] [WPMonad m ps]
   -- For some reason, the spec for `liftM` does not apply.
   simp [wp, MonadControl.liftWith, ExceptT.run, liftM, monadLift, MonadLift.monadLift, ExceptT.lift, ExceptT.mk]
 
+@[simp]
+theorem liftWith_OptionT [Monad m] [WPMonad m ps]
+  (f : (∀{β}, OptionT m β → m (Option β)) → m α) :
+    wp⟦MonadControl.liftWith (m:=m) f⟧ Q = wp⟦f (fun x => x.run)⟧ (Q.1, Q.2.2) := by
+  -- For some reason, the spec for `liftM` does not apply.
+  simp [wp, MonadControl.liftWith, OptionT.run, liftM, monadLift, MonadLift.monadLift, OptionT.lift, OptionT.mk]
+
 @[simp]
 theorem liftWith_trans [WP o ps] [MonadControl n o] [MonadControlT m n]
   (f : (∀{β}, o β → m (stM m o β)) → m α) :
@@ -330,7 +359,15 @@ theorem restoreM_ReaderT [Monad m] [WPMonad m ps] (x : m α) :
 
 @[simp]
 theorem restoreM_ExceptT [Monad m] [WPMonad m ps] (x : m (Except ε α)) :
-    wp⟦MonadControl.restoreM (m:=m) x : ExceptT ε m α⟧ Q = wp⟦x⟧ (fun | .ok a => Q.1 a | .error e => Q.2.1 e, Q.2.2) := by
+    wp⟦MonadControl.restoreM (m:=m) x : ExceptT ε m α⟧ Q = wp⟦x⟧ (fun e => e.casesOn Q.2.1 Q.1, Q.2.2) := by
+  simp [wp, MonadControl.restoreM]
+  congr
+  ext
+  split <;> rfl
+
+@[simp]
+theorem restoreM_OptionT [Monad m] [WPMonad m ps] (x : m (Option α)) :
+    wp⟦MonadControl.restoreM (m:=m) x : OptionT m α⟧ Q = wp⟦x⟧ (fun o => o.casesOn (Q.2.1 ⟨⟩) Q.1, Q.2.2) := by
   simp [wp, MonadControl.restoreM]
   congr
   ext
@@ -385,6 +422,16 @@ theorem throw_ExceptT [Monad m] [WPMonad m ps] :
     wp⟦MonadExceptOf.throw e : ExceptT ε m α⟧ Q = Q.2.1 e := by
   simp [wp, MonadExceptOf.throw, ExceptT.mk]
 
+@[simp]
+theorem throw_Option :
+    wp⟦MonadExceptOf.throw e : Option α⟧ Q = Q.2.1 e := by
+  simp [wp, MonadExceptOf.throw, Id.run]
+
+@[simp]
+theorem throw_OptionT [Monad m] [WPMonad m ps] :
+    wp⟦MonadExceptOf.throw e : OptionT m α⟧ Q = Q.2.1 e := by
+  simp [wp, MonadExceptOf.throw, OptionT.fail, OptionT.mk]
+
 @[simp]
 theorem throw_EStateM :
     wp⟦MonadExceptOf.throw e : EStateM ε σ α⟧ Q = Q.2.1 e := by
@@ -402,12 +449,22 @@ theorem throw_StateT [WP m sh] [Monad m] [MonadExceptOf ε m] :
 -- for lifting throw
 @[simp]
 theorem throw_lift_ExceptT [WP m sh] [Monad m] [MonadExceptOf ε m] :
-    wp⟦MonadExceptOf.throw (ε:=ε) e : ExceptT ε' m α⟧ Q = wp⟦MonadExceptOf.throw (ε:=ε) e : m (Except ε' α)⟧ (fun | .ok a => Q.1 a | .error e => Q.2.1 e, Q.2.2) := by
+    wp⟦MonadExceptOf.throw (ε:=ε) e : ExceptT ε' m α⟧ Q = wp⟦MonadExceptOf.throw (ε:=ε) e : m (Except ε' α)⟧ (fun e => e.casesOn Q.2.1 Q.1, Q.2.2) := by
   simp only [wp, MonadExceptOf.throw, PredTrans.pushExcept_apply]
   congr
   ext x
   split <;> rfl
 
+-- The following lemma is structurally different to StateT and others because of weird definitions
+-- for lifting throw
+@[simp]
+theorem throw_lift_OptionT [WP m sh] [Monad m] [MonadExceptOf ε m] :
+    wp⟦MonadExceptOf.throw (ε:=ε) e : OptionT m α⟧ Q = wp⟦MonadExceptOf.throw (ε:=ε) e : m (Option α)⟧ (fun o => o.casesOn (Q.2.1 ⟨⟩) Q.1, Q.2.2) := by
+  simp only [wp, MonadExceptOf.throw, PredTrans.pushOption_apply]
+  congr
+  ext x
+  split <;> rfl
+
 @[simp]
 theorem tryCatch_MonadExcept [MonadExceptOf ε m] [WP m ps] :
   wp⟦tryCatch x h : m α⟧ Q = wp⟦MonadExceptOf.tryCatch x h : m α⟧ Q := rfl
@@ -429,7 +486,22 @@ theorem tryCatch_ExceptT [Monad m] [WPMonad m ps] :
   simp only [wp, MonadExceptOf.tryCatch, ExceptT.tryCatch, ExceptT.mk, bind, PredTrans.pushExcept_apply]
   congr
   ext x
-  split <;> simp
+  cases x <;> simp
+
+@[simp]
+theorem tryCatch_Option :
+    wp⟦MonadExceptOf.tryCatch x h : Option α⟧ Q = wp⟦x⟧ (Q.1, fun e => wp⟦h e⟧ Q, Q.2.2) := by
+  simp only [wp, PredTrans.pure, Id.run, MonadExceptOf.tryCatch, Option.tryCatch,
+    PredTrans.pushOption_apply]
+  cases x <;> simp
+
+@[simp]
+theorem tryCatch_OptionT [Monad m] [WPMonad m ps] :
+    wp⟦MonadExceptOf.tryCatch x h : OptionT m α⟧ Q = wp⟦x⟧ (Q.1, fun e => wp⟦h e⟧ Q, Q.2.2) := by
+  simp only [wp, MonadExceptOf.tryCatch, OptionT.tryCatch, OptionT.mk, bind, PredTrans.pushOption_apply]
+  congr
+  ext x
+  cases x <;> simp
 
 open EStateM.Backtrackable in
 @[simp]
@@ -451,12 +523,20 @@ theorem tryCatch_StateT [WP m sh] [Monad m] [MonadExceptOf ε m] :
 
 @[simp]
 theorem tryCatch_lift_ExceptT [WP m sh] [Monad m] [MonadExceptOf ε m] :
-    wp⟦MonadExceptOf.tryCatch (ε:=ε) x h : ExceptT ε' m α⟧ Q = wp⟦MonadExceptOf.tryCatch (ε:=ε) x h : m (Except ε' α)⟧ (fun | .ok a => Q.1 a | .error e => Q.2.1 e, Q.2.2) := by
+    wp⟦MonadExceptOf.tryCatch (ε:=ε) x h : ExceptT ε' m α⟧ Q = wp⟦MonadExceptOf.tryCatch (ε:=ε) x h : m (Except ε' α)⟧ (fun e => e.casesOn Q.2.1 Q.1, Q.2.2) := by
   simp only [wp, MonadExceptOf.tryCatch, tryCatchThe, PredTrans.pushExcept_apply, ExceptT.mk]
   congr
   ext x
   split <;> rfl
 
+@[simp]
+theorem tryCatch_lift_OptionT [WP m sh] [Monad m] [MonadExceptOf ε m] :
+    wp⟦MonadExceptOf.tryCatch (ε:=ε) x h : OptionT m α⟧ Q = wp⟦MonadExceptOf.tryCatch (ε:=ε) x h : m (Option α)⟧ (fun o => o.casesOn (Q.2.1 ⟨⟩) Q.1, Q.2.2) := by
+  simp only [wp, MonadExceptOf.tryCatch, tryCatchThe, PredTrans.pushOption_apply, OptionT.mk]
+  congr
+  ext x
+  split <;> rfl
+
 /-
 example :
   wp (m:= ReaderT Char (StateT Bool (ExceptT Nat Id))) (do set true; throw 42; set false; get) =
@@ -495,4 +575,17 @@ theorem orElse_ExceptT [Monad m] [WPMonad m ps] :
     wp⟦OrElse.orElse x h : ExceptT ε m α⟧ Q = wp⟦x⟧ (Q.1, fun _ => wp⟦h ()⟧ Q, Q.2.2) := by
   simp [OrElse.orElse, MonadExcept.orElse]
 
+@[simp]
+theorem orElse_Option  :
+    wp⟦OrElse.orElse x h : Option α⟧ Q = wp⟦x⟧ (Q.1, fun _ => wp⟦h ()⟧ Q, Q.2.2) := by
+  cases x <;> simp [OrElse.orElse, Option.orElse, wp, Id.run]
+
+@[simp]
+theorem orElse_OptionT [Monad m] [WPMonad m ps] :
+    wp⟦OrElse.orElse x h : OptionT m α⟧ Q = wp⟦x⟧ (Q.1, fun _ => wp⟦h ()⟧ Q, Q.2.2) := by
+  simp [OrElse.orElse, Alternative.orElse, OptionT.orElse, OptionT.mk, wp]
+  congr
+  ext x
+  cases x <;> simp
+
 end OrElse

tests/lean/run/newassertions.lean

@@ -0,0 +1,108 @@
+import Std
+
+variable {ps : Type u}
+
+class TransShape (ps : Type u) where
+  Assertion : Type u
+  ExceptConds : Type u
+
+open TransShape (Assertion ExceptConds)
+
+abbrev PostCond (α : Type u) (ps : Type u) [TransShape ps] :=
+  (α → Assertion ps) ×' ExceptConds ps
+
+class TransShape.Entails (ps : Type u) extends TransShape ps where
+  assertionEntails : Assertion → Assertion → Prop
+  exceptCondsEntails : ExceptConds → ExceptConds → Prop
+
+abbrev TransShape.Entails.postCondEntails [TransShape.Entails ps]
+  (p q : PostCond α ps) : Prop :=
+  (∀ a, assertionEntails (p.1 a) (q.1 a)) ∧ exceptCondsEntails p.2 q.2
+
+infixr:25 " ⊢ₛ " => TransShape.Entails.assertionEntails
+infixr:25 " ⊢ₑ " => TransShape.Entails.exceptCondsEntails
+infixr:25 " ⊢ₚ " => TransShape.Entails.postCondEntails
+
+class TransShape.EntailsPre (ps : Type u) extends TransShape.Entails ps where
+  assertionPreorder : @Std.IsPreorder Assertion ⟨assertionEntails⟩
+  exceptCondsPreorder : @Std.IsPreorder ExceptConds ⟨exceptCondsEntails⟩
+
+theorem TransShape.EntailsPre.postCondPreorder [TransShape.EntailsPre ps]
+  : @Std.IsPreorder (PostCond α ps) ⟨TransShape.Entails.postCondEntails⟩ :=
+  let : LE (PostCond α ps) := ⟨TransShape.Entails.postCondEntails⟩
+  let ap := assertionPreorder (ps := ps)
+  let ep := exceptCondsPreorder (ps := ps)
+  { le_refl x := by
+      constructor
+      · intro a; apply ap.le_refl
+      · apply ep.le_refl
+  , le_trans := by
+      intro x y z hxy hyz
+      constructor
+      · intro a; apply ap.le_trans _ _ _ (hxy.1 a) (hyz.1 a)
+      · apply ep.le_trans _ _ _ (hxy.2) (hyz.2)
+  }
+
+/-- The stronger the postcondition, the stronger the transformed precondition. -/
+def PredTrans.Monotonic [TransShape.Entails ps] (t : PostCond α ps → Assertion ps) : Prop :=
+  ∀ Q₁ Q₂, (Q₁ ⊢ₚ Q₂) → (t Q₁) ⊢ₛ (t Q₂)
+
+/--
+  The type of predicate transformers for a given `ps : TransShape` and return type `α : Type`.
+  A predicate transformer `x : PredTrans ps α` is a function that takes a postcondition
+  `Q : PostCond α ps` and returns a precondition `x.apply Q : Assertion ps`.
+ -/
+@[ext]
+structure PredTrans (ps : Type u) [TransShape.Entails ps] (α : Type u) : Type u where
+  /-- Apply the predicate transformer to a postcondition. -/
+  apply : PostCond α ps → Assertion ps
+  mono : PredTrans.Monotonic apply
+  /-- The predicate transformer is conjunctive: `t (Q₁ ∧ₚ Q₂) ⊣⊢ₛ t Q₁ ∧ t Q₂`.
+  So the stronger the postcondition, the stronger the resulting precondition. -/
+  -- conjunctive : PredTrans.Conjunctive apply
+
+structure Prop' : Type u
+structure PMF' (α : Type u) : Type u
+structure Arg' (σ : Type u) (ps : Type u) : Type u
+structure Except' (ε : Type u) (ps : Type u) : Type u
+
+instance : TransShape Prop' where
+  Assertion := ULift Prop
+  ExceptConds := PUnit
+
+instance [inst : TransShape ps'] : TransShape (Arg' σ ps') where
+  Assertion := σ → Assertion ps'
+  ExceptConds := inst.ExceptConds
+
+instance [inst : TransShape ps'] : TransShape (Except' ε ps') where
+  Assertion := inst.Assertion
+  ExceptConds := (ε → inst.Assertion) ×' inst.ExceptConds
+
+example : Assertion (Arg' σ (Except' ε Prop')) :=
+  fun s => ULift.up True
+example : PostCond α (Arg' σ Prop') :=
+  ⟨fun r s => ULift.up True, ⟨⟩⟩
+example : PostCond α (Arg' σ (Except' ε Prop')) :=
+  ⟨fun r s => ULift.up True, fun e => ULift.up False, ⟨⟩⟩
+example : PostCond α (Except' ε (Arg' σ (Except' ε Prop'))) :=
+  ⟨fun r s => ULift.up True, fun e s => ULift.up False, fun e => ULift.up False, ⟨⟩⟩
+
+class WP (m : Type u → Type v) (ps : outParam (Type u)) extends TransShape ps where
+  wp : ∀ {α}, m α → PredTrans ps α
+
+instance : WP Id Prop' := sorry
+instance [WP m ps] : WP (StateT σ m) (Arg' σ ps) := sorry
+instance [WP m ps] : WP (ExceptT ε m) (Except' ε ps) := sorry
+instance : WP (EStateM ε σ) (Except' ε (Arg' σ Prop')) := sorry
+
+def Triple [WP m ps] (x : m α) (P Q : α → Assertion ps) := True
+
+theorem spec {α : Type} {ps} [WP m ps] (prog : m α) (P : α → Assertion ps) :
+  Triple prog P P := sorry
+
+#guard_msgs (error) in
+#check (spec _ (fun p s => p.1 = p.2 ∧ s = 4)
+        : @Triple (MProd (Option Nat) Nat) (Arg' Nat Prop') _ _ _ _ _)
+
+#check ∀ ε σ α s (prog : EStateM ε σ α) (P : σ → Prop),
+    Triple prog (fun s' => s' = s) P → P s

tests/lean/run/unfoldingStuckOnMVar.lean

@@ -0,0 +1,87 @@
+/-!
+# Definitional equality on a definition the unfolding of which is stuck on an MVar
+-/
+
+namespace One
+
+def Pred (σs : List Type) := match σs with
+  | [] => Prop
+  | σ::σs => σ → Pred σs
+
+def Blah (x : Nat) := x
+
+def trp {α : Type} {σs : List Type} (P Q : α → Pred σs) : Prop := sorry
+
+theorem spec {α : Type} {σs : List Type} {a : α} (P : α → Pred σs) :
+  trp P P := sorry
+
+/--
+info: spec fun p s =>
+  p.fst = some p.snd ∧ s = 4 : trp (fun p s => p.fst = some p.snd ∧ s = 4) fun p s => p.fst = some p.snd ∧ s = 4
+-/
+#guard_msgs in
+#check (spec (σs := [Nat]) (fun p s => p.1 = p.2 ∧ s = 4)
+        : @trp (MProd (Option Nat) Nat) [Nat] _ _)
+
+/-!
+This used to have a failure on `(fun p s => p.1 = p.2 ∧ s = 4)` because the definitional equality
+  ?m.547 p → Prop =?= Pred ?m.504
+used to return `false` instead of being stuck on `?m.504`.
+-/
+set_option trace.Meta.isDefEq.stuckMVar true in
+/--
+error: Application type mismatch: The argument
+  fun p s => ?m.11 = ?m.13 ∧ s = 4
+has type
+  (p : ?m.5) → ?m.19 p → Prop
+but is expected to have type
+  ?m.5 → Pred ?m.6
+in the application
+  spec fun p s => ?m.11 = ?m.13 ∧ s = 4
+-/
+#guard_msgs (error) in
+#check (spec (fun p s => p.1 = p.2 ∧ s = 4)
+        : @trp (MProd (Option Nat) Nat) [Nat] _ _)
+
+end One
+
+namespace I8766
+
+
+class WP (m : Type → Type) (l : outParam Type) where
+
+instance [WP m l] : WP (StateT σ m) (σ → l) where
+instance : WP (EStateM ε σ) (σ → Prop) where
+
+def Triple [WP m l] (x : m α) (P Q : l) := True
+
+/-!
+Similarly to the above, reduction of `SPred ?m.1250` is stuck on `?m.1250`.
+It will eventually be solved once `WP (EStateM ε σ) [σ]` has been synthesized.
+-/
+set_option trace.Meta.isDefEq.stuckMVar true in
+#guard_msgs (error) in
+#check ∀ ε σ α s (prog : EStateM ε σ α) (P : σ → Prop),
+    Triple prog (fun s' => s' = s) P → P s
+
+end I8766
+
+namespace I87662
+
+
+class WP (m : Type → Type) (l : outParam Type) where
+
+instance [WP m l] : WP (StateT σ m) (σ → l) where
+instance : WP (EStateM ε σ) (σ → Prop) where
+
+def Triple [WP m l] (x : m α) (P Q : l) := True
+
+/-!
+Similarly to the above, reduction of `SPred ?m.1250` is stuck on `?m.1250`.
+It will eventually be solved once `WP (EStateM ε σ) [σ]` has been synthesized.
+-/
+set_option trace.Meta.isDefEq.stuckMVar true in
+#check ∀ ε σ α s (prog : EStateM ε σ α) (P : σ → Prop),
+    Triple prog (fun s' => s' = s) P → P s
+
+end I8766