From 6cf1c4a1be378abb1c738f89b2ad50e908c58a64 Mon Sep 17 00:00:00 2001
From: Sebastian Graf <sgraf1337@gmail.com>
Date: Fri, 27 Feb 2026 02:18:06 +0100
Subject: [PATCH] chore: simplify a proof in mvcgen test cases and remove
 duplicate (#12547)

---
 tests/elab/doLogicTests.lean   | 143 ---------------------------------
 tests/elab/mvcgenTutorial.lean |  30 +++----
 2 files changed, 12 insertions(+), 161 deletions(-)

diff --git a/tests/elab/doLogicTests.lean b/tests/elab/doLogicTests.lean
index 26e3f3c057..601948785e 100644
--- a/tests/elab/doLogicTests.lean
+++ b/tests/elab/doLogicTests.lean
@@ -533,149 +533,6 @@ example (p : Nat → Prop) [DecidablePred p] (n : Nat) :
 
 end Automated
 
-namespace Aeneas
-
-inductive Error where
-   | assertionFailure: Error
-   | integerOverflow: Error
-   | divisionByZero: Error
-   | arrayOutOfBounds: Error
-   | maximumSizeExceeded: Error
-   | panic: Error
-   | undef: Error
-
-open Error
-
-inductive Result (α : Type u) where
-  | ok (v: α): Result α
-  | fail (e: Error): Result α
-  | div
-
-instance : Monad Result where
-  pure x := .ok x
-  bind x f := match x with
-  | .ok v => f v
-  | .fail e => .fail e
-  | .div => .div
-
-instance : LawfulMonad Result :=
-  LawfulMonad.mk' _
-    (by dsimp only [Functor.map]; grind)
-    (by dsimp only [bind]; grind)
-    (by dsimp only [bind]; grind)
-
-abbrev _root_.Std.Do.PredTrans.pushResult (x : Result α) : PredTrans (.except Error .pure) α :=
-  match x with
-  | .ok v => PredTrans.pure v
-  | .fail e => PredTrans.throw e
-  | .div => PredTrans.const ⌜False⌝
-
-@[simp]
-theorem Result.apply_pushResult_pure {α} {a : α} {Q : PostCond α (.except Error .pure)} :
-  (PredTrans.pushResult (pure a)).apply Q = Q.1 a := by rfl
-
-@[simp]
-theorem Result.apply_pushResult_bind {α β} {x : Result α} {f : α → Result β} {Q : PostCond β (.except Error .pure)} :
-  (PredTrans.pushResult (do let a ← x; f a)).apply Q =
-    (PredTrans.pushResult x).apply (fun a => (PredTrans.pushResult (f a)).apply Q, Q.2) := by
-  simp only [PredTrans.pushResult, bind]
-  grind
-
-instance Result.instWP : WP Result (.except Error .pure) where
-  wp := PredTrans.pushResult
-
-instance Result.instWPMonad : WPMonad Result (.except Error .pure) where
-  wp_pure _ := by ext Q; simp [wp]
-  wp_bind x f := by ext Q; simp [wp]
-
-theorem Result.of_wp {α} {x : Result α} (P : Result α → Prop) :
-  (⊢ₛ wp⟦x⟧ post⟨fun a => ⌜P (.ok a)⌝, fun e => ⌜P (.fail e)⌝⟩) → P x := by
-    intro hspec
-    match x with
-    | .ok a => simpa [wp] using hspec
-    | .fail e => simpa [wp] using hspec
-    | .div => simp [wp] at hspec
-
-/-- Kinds of unsigned integers -/
-inductive UScalarTy where
-| Usize
-| U8
-| U16
-| U32
-| U64
-| U128
-
-def UScalarTy.numBits (ty : UScalarTy) : Nat :=
-  match ty with
-  | Usize => System.Platform.numBits
-  | U8 => 8
-  | U16 => 16
-  | U32 => 32
-  | U64 => 64
-  | U128 => 128
-
-/-- Signed integer -/
-structure UScalar (ty : UScalarTy) where
-  /- The internal representation is a bit-vector -/
-  bv : BitVec ty.numBits
-deriving Repr, BEq, DecidableEq
-
-def UScalar.val {ty} (x : UScalar ty) : Nat := x.bv.toNat
-
-def UScalar.ofNatCore {ty : UScalarTy} (x : Nat) (_ : x < 2^ty.numBits) : UScalar ty :=
-  { bv := BitVec.ofNat _ x }
-
-instance (ty : UScalarTy) : CoeOut (UScalar ty) Nat where
-  coe := λ v => v.val
-
-def UScalar.tryMk (ty : UScalarTy) (x : Nat) : Result (UScalar ty) :=
-  sorry
-
-def UScalar.add {ty : UScalarTy} (x y : UScalar ty) : Result (UScalar ty) :=
-  UScalar.tryMk ty (x.val + y.val)
-
-instance {ty} : HAdd (UScalar ty) (UScalar ty) (Result (UScalar ty)) where
-  hAdd x y := UScalar.add x y
-
-@[irreducible]
-def UScalar.max (ty : UScalarTy) : Nat := 2^ty.numBits-1
-
-theorem UScalar.add_spec {ty} {x y : UScalar ty}
-  (hmax : ↑x + ↑y ≤ UScalar.max ty) :
-  ∃ z, x + y = Result.ok z ∧ (↑z : Nat) = ↑x + ↑y := sorry
-
-abbrev U32 := UScalar .U32
-abbrev U32.max   : Nat := UScalar.max .U32
-
-theorem U32.add_spec {x y : U32} (hmax : x.val + y.val ≤ U32.max) :
-  ∃ z, x + y = Result.ok z ∧ (↑z : Nat) = ↑x + ↑y :=
-  UScalar.add_spec sorry -- (by scalar_tac)
-
-abbrev PCond (α : Type) := PostCond α (PostShape.except Error PostShape.pure)
-
-@[spec]
-theorem U32.add_spec' {x y : U32} {Q : PCond U32} (hmax : ↑x + ↑y ≤ U32.max):
-  ⦃Q.1 (UScalar.ofNatCore (↑x + ↑y) sorry)⦄ (x + y) ⦃Q⦄ := by
-    mintro h
-    have ⟨z, ⟨hxy, hz⟩⟩ := U32.add_spec hmax
-    simp [hxy, hz.symm, wp]
-    sorry -- show Q.1 z ↔ Q.1 (ofNatCore z.val ⋯)
-
-@[simp]
-theorem UScalar.ofNatCore_val_eq : (ofNatCore x h).val = x := sorry
-
-def mul2_add1 (x : U32) : Result U32 :=
-  do
-  let i ← x + x
-  i + (UScalar.ofNatCore 1 sorry : U32)
-
-theorem mul2_add1_spec' (x : U32) (h : 2 * x.val + 1 ≤ U32.max)
-  : ⦃Q.1 (UScalar.ofNatCore (2 * ↑x + (1 : Nat)) sorry)⦄ (mul2_add1 x) ⦃Q⦄ := by
-  mvcgen [mul2_add1]
-  all_goals simp_all +arith; try omega
-
-end Aeneas
-
 namespace VSTTE2010
 
 namespace MaxAndSum
diff --git a/tests/elab/mvcgenTutorial.lean b/tests/elab/mvcgenTutorial.lean
index f43ccd2ca7..deea2824d2 100644
--- a/tests/elab/mvcgenTutorial.lean
+++ b/tests/elab/mvcgenTutorial.lean
@@ -214,29 +214,23 @@ instance : LawfulMonad Result :=
     (by dsimp only [bind]; grind)
     (by dsimp only [bind]; grind)
 
-abbrev _root_.Std.Do.PredTrans.pushResult (x : Result α) : PredTrans (.except Error .pure) α :=
-  match x with
-  | .ok v => PredTrans.pure v
-  | .fail e => PredTrans.throw e
-  | .div => PredTrans.const ⌜False⌝
+instance Result.instWP : WP Result (.except Error .pure) where
+  wp
+    | .ok v => PredTrans.pure v
+    | .fail e => PredTrans.throw e
+    | .div => PredTrans.const ⌜False⌝
 
-@[simp]
-theorem Result.apply_pushResult_pure {α} {a : α} {Q : PostCond α (.except Error .pure)} :
-  (PredTrans.pushResult (pure a)).apply Q = Q.1 a := by rfl
+theorem Result.apply_wp_pure {α} {a : α} {Q : PostCond α (.except Error .pure)} :
+  wp⟦pure (f := Result) a⟧ Q = Q.1 a := by rfl
 
-@[simp]
-theorem Result.apply_pushResult_bind {α β} {x : Result α} {f : α → Result β} {Q : PostCond β (.except Error .pure)} :
-  (PredTrans.pushResult (do let a ← x; f a)).apply Q =
-    (PredTrans.pushResult x).apply (fun a => (PredTrans.pushResult (f a)).apply Q, Q.2) := by
-  simp only [PredTrans.pushResult, bind]
+theorem Result.apply_wp_bind {α β} {x : Result α} {f : α → Result β} {Q : PostCond β (.except Error .pure)} :
+  wp⟦do let a ← x; f a⟧ Q = wp⟦x⟧ (fun a => wp⟦f a⟧ Q, Q.2) := by
+  simp only [wp, bind]
   grind
 
-instance Result.instWP : WP Result (.except Error .pure) where
-  wp := PredTrans.pushResult
-
 instance Result.instWPMonad : WPMonad Result (.except Error .pure) where
-  wp_pure _ := by ext Q; simp [wp]
-  wp_bind x f := by ext Q; simp [wp]
+  wp_pure _ := by ext Q : 1; apply Result.apply_wp_pure
+  wp_bind x f := by ext Q : 1; apply Result.apply_wp_bind
 
 theorem Result.of_wp {α} {x : Result α} (P : Result α → Prop) :
   (⊢ₛ wp⟦x⟧ post⟨fun a => ⌜P (.ok a)⌝, fun e => ⌜P (.fail e)⌝⟩) → P x := by