From 6a8d7cc17ce51d8b0619cf67d1a44707d1f00a3f Mon Sep 17 00:00:00 2001
From: Cameron Zwarich <cameron@lean-fro.org>
Date: Sun, 7 Sep 2025 16:42:52 -0700
Subject: [PATCH] chore: remove `instWPMonad` instance and test that relies
 upon it (#10293)

The proof of the instWPMonad instance relies on the equality of any two
terms of type `IO.RealWorld`, which is only a side effect of the current
transparent definition. Ignoring the questions around the utility of
proving things about programs in `IO`, the semantic validity of this
instance in the intended model of the IO monad is also unclear.

I tried a few things to axiomatize this instance so it could be put into
the test file to preserve the one test section that relies on it, but I
was unsuccessful; everything I attempted caused errors.
---
 src/Std/Do/WP/IO.lean            |  7 -----
 tests/lean/run/doLogicTests.lean | 47 --------------------------------
 2 files changed, 54 deletions(-)

diff --git a/src/Std/Do/WP/IO.lean b/src/Std/Do/WP/IO.lean
index 18b27fd4c5..a0ddda8404 100644
--- a/src/Std/Do/WP/IO.lean
+++ b/src/Std/Do/WP/IO.lean
@@ -41,10 +41,3 @@ scoped instance instWP : WP (EIO ε) (.except ε .pure) where
     }
 
 instance instLawfulMonad : LawfulMonad (EIO ε) := inferInstanceAs (LawfulMonad (EStateM ε IO.RealWorld))
-
-scoped instance instWPMonad : WPMonad (EIO ε) (.except ε .pure) where
-  wp_pure a := by simp only [wp, pure, EStateM.pure, PredTrans.pure]
-  wp_bind x f := by
-    ext Q : 2
-    simp only [wp, bind, EStateM.bind, PredTrans.bind]
-    cases (x ()) <;> rfl
diff --git a/tests/lean/run/doLogicTests.lean b/tests/lean/run/doLogicTests.lean
index bcf520c084..3c3aa9fe17 100644
--- a/tests/lean/run/doLogicTests.lean
+++ b/tests/lean/run/doLogicTests.lean
@@ -292,53 +292,6 @@ theorem fib_correct {n} : (fib_impl n).run = fib_spec n := by
 
 end fib
 
-section KimsBabySteps
-
-/-- Add `n` random even numbers to `k`. -/
-def addRandomEvens (n : Nat) (k : Nat) : IO Nat := do
-  let mut r := k
-  for _ in List.range n do
-    r := r + 2 * (← IO.rand 0 37)
-  pure r
-
-def program (n : Nat) (k : Nat) : IO Nat := do
-  let r₁ ← addRandomEvens n k
-  let r₂ ← addRandomEvens n k
-  return r₁ + r₂
-
-open scoped Std.Do.IO.Bare
-
-axiom IO.rand_spec {n : Nat} : ⦃⌜True⌝⦄ (IO.rand 0 n : IO Nat) ⦃⇓r => ⌜r < n⌝⦄
-
-/-- The result has the same parity as the input. -/
-theorem addRandomEvens_spec (n k) : ⦃⌜True⌝⦄ (addRandomEvens n k) ⦃⇓r => ⌜r % 2 = k % 2⌝⦄ := by
-  unfold addRandomEvens
-  mintro -
-  mspec Spec.forIn_list_const_inv
-  intro n r
-  mintro ⌜h⌝
-  mspec IO.rand_spec
-  simp_all
-
-attribute [local spec] addRandomEvens_spec
-
-/-- Since we're adding even numbers to our number twice, and summing,
-the entire result is even. -/
-theorem program_spec (n k) : ⦃⌜True⌝⦄ program n k ⦃⇓r => ⌜r % 2 = 0⌝⦄ := by
-  unfold program
-  mintro -
-  mspec (addRandomEvens_spec n k)
-  mrename_i h
-  mpure h
-  mspec /- registered spec is taken -/
-  mrename_i h
-  mpure h
-  mspec
-  mpure_intro
-  grind
-
-end KimsBabySteps
-
 section WeNeedAProofMode
 
 abbrev M := StateT Nat (StateT Char (StateT Bool (StateT String Id)))