From 4fb7ea2ba00bfe4f137de282457020c5f868504e Mon Sep 17 00:00:00 2001
From: Sebastian Graf <sgraf1337@gmail.com>
Date: Fri, 12 Jun 2026 19:16:25 +0000
Subject: [PATCH] feat: add Triple.observe

---
 src/Std/Do/Triple/Basic.lean | 17 ++++++++
 tests/elab/doLogicTests.lean | 80 ++++++++++++++++++++++++++++++++++++
 2 files changed, 97 insertions(+)

diff --git a/src/Std/Do/Triple/Basic.lean b/src/Std/Do/Triple/Basic.lean
index 46c17edbf548..52256c056bc8 100644
--- a/src/Std/Do/Triple/Basic.lean
+++ b/src/Std/Do/Triple/Basic.lean
@@ -110,4 +110,21 @@ for `Q₁`, then `mp x h₁ h₂` is a proof for `Q₂` about `x`.
 theorem mp [WP m ps] (x : m α) (h₁ : Triple x P₁ Q₁) (h₂ : Triple x P₂ (Q₁ →ₚ Q₂)) : Triple x spred(P₁ ∧ P₂) (Q₁ ∧ₚ Q₂) :=
   Triple.iff.mpr <| SPred.and_mono (Triple.iff.mp h₁) (Triple.iff.mp h₂) |>.trans ((wp x).conjunctive Q₁ (Q₁ →ₚ Q₂)).mpr |>.trans ((wp x).mono _ _ PostCond.and_imp)
 
+/--
+Observes a fact `Q` about the state by running a stateless program `obs`, then carries `Q` into the
+proof of `prog`. A triple for `prog` follows from a triple for `obs` that assumes the postcondition
+`Q` of the specification `h` and establishes the goal `wp⟦prog⟧ Post`. This requires `obs` to be
+*stateless*: the premise `hp` states that its successful runs leave the state unchanged.
+-/
+theorem observe [WP m ps] {α β : Type u} {obs : m α} {prog : m β}
+    {Pre : Assertion ps} {Q : PostCond α ps} {Post : PostCond β ps}
+    (hp : ∀ C : Assertion ps, wp⟦obs⟧ (PostCond.noThrow fun _ => C) ⊢ₛ C)
+    (h : Triple obs Pre Q)
+    (hgoal : Triple obs Pre (Q →ₚ PostCond.noThrow fun _ => wp⟦prog⟧ Post)) :
+    Triple prog Pre Post :=
+  Triple.of_entails_wp <|
+    (Triple.entails_wp_of_pre_post (Triple.mp obs h hgoal) SPred.and_self.mpr
+      (PostCond.entails.mk (fun _ => SPred.and_elim_r) (ExceptConds.and_elim_right _ _))).trans
+    (hp (wp⟦prog⟧ Post))
+
 end Triple
diff --git a/tests/elab/doLogicTests.lean b/tests/elab/doLogicTests.lean
index 10d4cbadd460..19d2069dac6f 100644
--- a/tests/elab/doLogicTests.lean
+++ b/tests/elab/doLogicTests.lean
@@ -829,3 +829,83 @@ theorem foldM_eq_sum (xs : Array Nat) {m ps} [Monad m] [LawfulMonad m]
   mvcgen
   case inv1 => exact ⇓⟨cur, n⟩ => ⌜n = cur.prefix.sum⌝
   all_goals grind
+
+/-! ### The partial correctness trick
+
+Specifications are written in the object language as boolean monadic predicates. A triple
+hypothesis is consumed by observing its program via `Triple.observe`
+and stepping through it with `mvcgen`. -/
+
+namespace PartialCorrectnessTrick
+
+inductive RustError where
+  | rustPanic
+  | integerOverflow
+
+abbrev RustM := Except RustError
+
+/-- A boolean monadic predicate holds when it returns `true` without throwing. -/
+abbrev RustM.holds (p : RustM Bool) : Prop := ⦃⌜True⌝⦄ p ⦃⇓ r => ⌜r⌝⦄
+
+/-- Running an `Except` program and discarding its result preserves any goal. -/
+theorem wp_const (p : RustM α) (C : Assertion (.except RustError .pure)) :
+    wp⟦p⟧ (⇓ _ => C) ⊢ₛ C := by
+  cases p with
+  | ok a => exact SPred.entails.refl _
+  | error e => exact SPred.false_elim
+
+namespace Unfoldable
+
+def panicAdd (x y : Nat) : RustM Nat := do
+  if (x + y) ≤ 100 then pure (x + y) else Except.error .integerOverflow
+
+def pre (x : Nat) : RustM Bool := do
+  if x ≤ 10 then
+    pure ((← panicAdd x 10) == 15)
+  else
+    pure false
+
+def f (x : Nat) : RustM Nat := do
+  panicAdd x 5
+
+def post (x : Nat) (res : Nat) : RustM Bool := do
+  pure (res == 10)
+
+example (x : Nat) :
+    (pre x).holds → ⦃⌜True⌝⦄ f x ⦃⇓ res => ⌜(post x res).holds⌝⦄ := by
+  intro h
+  apply Triple.observe (wp_const (pre x)) h
+  mvcgen [pre, panicAdd] <;> try grind
+  intro hx
+  mvcgen [f, post, panicAdd] <;> try grind
+  mvcgen [post] <;> grind
+
+end Unfoldable
+
+namespace Opaque
+
+opaque g : Nat → RustM Nat
+
+def pre (x : Nat) : RustM Bool := do pure (x == (← g 0))
+
+def f (x : Nat) : RustM Nat := pure (x + 1)
+
+def post (x : Nat) (res : Nat) : RustM Bool := do pure (res - 1 == (← g 0))
+
+/-- Partial-correctness self-specification: if `p` succeeds with `r`, then `p = .ok r`. -/
+theorem self_spec (p : RustM α) : ⦃⌜True⌝⦄ p ⦃⇓? r => ⌜p = .ok r⌝⦄ := by
+  cases p with
+  | ok a => exact Triple.pure a (by simp)
+  | error e => apply Triple.of_entails_wp; intro _; exact True.intro
+
+example (x : Nat) :
+    (pre x).holds → ⦃⌜True⌝⦄ f x ⦃⇓ res => ⌜(post x res).holds⌝⦄ := by
+  intro h
+  apply Triple.observe (wp_const (pre x)) h
+  have hg := self_spec (g 0)
+  mvcgen [pre, hg, f] <;> try grind
+  simp
+
+end Opaque
+
+end PartialCorrectnessTrick