From 0bcac0d46cc76fd7410e0abec06dcda33fddf4d7 Mon Sep 17 00:00:00 2001
From: Sebastian Graf <sgraf1337@gmail.com>
Date: Mon, 26 Jan 2026 13:50:23 +0100
Subject: [PATCH] feat: add `Option.of_wp_eq` and `Except.of_wp_eq` (#12161)

This PR adds `Option.of_wp_eq` and `Except.of_wp_eq`, similar to the
existing `Except.of_wp`. `Except.of_wp` is deprecated because applying
it requires prior generalization, at which point it is more convenient
to use `Except.of_wp_eq`.
---
 src/Std/Do/WP/Basic.lean | 31 ++++++++++++++++++++++++++++++-
 1 file changed, 30 insertions(+), 1 deletion(-)

diff --git a/src/Std/Do/WP/Basic.lean b/src/Std/Do/WP/Basic.lean
index 65e6dae286..efb6b18032 100644
--- a/src/Std/Do/WP/Basic.lean
+++ b/src/Std/Do/WP/Basic.lean
@@ -143,12 +143,27 @@ you want to use `mvcgen` to reason about `prog`.
 theorem ReaderM.of_wp_run_eq {α} {x : α} {prog : ReaderM ρ α} (h : ReaderT.run prog r = x) (P : α → Prop) :
   (⊢ₛ wp⟦prog⟧ (⇓ a _ => ⌜P a⌝) r) → P x := h ▸ (· True.intro)
 
+/--
+Adequacy lemma for `Except`.
+Useful if you want to prove a property about a complex expression `prog : Except ε α` that you have
+generalized to a variable `x` and you want to use `mvcgen` to reason about `prog`.
+-/
+theorem Except.of_wp_eq {ε α : Type u} {x prog : Except ε α} (h : prog = x) (P : Except ε α → Prop) :
+    (⊢ₛ wp⟦prog⟧ post⟨fun a => ⌜P (.ok a)⌝, fun e => ⌜P (.error e)⌝⟩) → P x := by
+  subst h
+  intro hspec
+  simp only [wp, PredTrans.pushExcept_apply, PredTrans.pure_apply] at hspec
+  split at hspec
+  case h_1 a s' heq => rw[← heq] at hspec; exact hspec True.intro
+  case h_2 e s' heq => rw[← heq] at hspec; exact hspec True.intro
+
 /--
 Adequacy lemma for `Except`.
 Useful if you want to prove a property about an expression `prog : Except ε α` and you want to use
 `mvcgen` to reason about `prog`.
 -/
-theorem Except.of_wp {α} {prog : Except ε α} (P : Except ε α → Prop) :
+@[deprecated Except.of_wp_eq (since := "2026-01-26")]
+theorem Except.of_wp {ε α : Type u} {prog : Except ε α} (P : Except ε α → Prop) :
     (⊢ₛ wp⟦prog⟧ post⟨fun a => ⌜P (.ok a)⌝, fun e => ⌜P (.error e)⌝⟩) → P prog := by
   intro hspec
   simp only [wp, PredTrans.pushExcept_apply, PredTrans.pure_apply] at hspec
@@ -156,6 +171,20 @@ theorem Except.of_wp {α} {prog : Except ε α} (P : Except ε α → Prop) :
   case h_1 a s' heq => rw[← heq] at hspec; exact hspec True.intro
   case h_2 e s' heq => rw[← heq] at hspec; exact hspec True.intro
 
+/--
+Adequacy lemma for `Option`.
+Useful if you want to prove a property about a complex expression `prog : Option α` that you have
+generalized to a variable `x` and you want to use `mvcgen` to reason about `prog`.
+-/
+theorem Option.of_wp_eq {α : Type u} {x prog : Option α} (h : prog = x) (P : Option α → Prop) :
+    (⊢ₛ wp⟦prog⟧ post⟨fun a => ⌜P (some a)⌝, fun _ => ⌜P none⌝⟩) → P x := by
+  subst h
+  intro hspec
+  simp only [wp, PredTrans.pushOption_apply, PredTrans.pure_apply] at hspec
+  split at hspec
+  case h_1 a s' heq => rw[← heq] at hspec; exact hspec True.intro
+  case h_2   s' heq => rw[← heq] at hspec; exact hspec True.intro
+
 /--
 Adequacy lemma for `EStateM.run`.
 Useful if you want to prove a property about an expression `x` defined as `EStateM.run prog s` and