fix: Use fullApproxDefEq in mspec to fix a bug reported by Rish (#9041)

This PR makes `mspec` detect more viable assignments by `rfl` instead of
generating a VC.

---------

Co-authored-by: Sebastian Graf <sg@lean-fro.org>
Co-authored-by: Rishikesh Vaishnav <rishhvaishnav@gmail.com>

src/Lean/Elab/Tactic/Do/Spec.lean

@@ -168,14 +168,17 @@ def mSpec (goal : MGoal) (elabSpecAtWP : Expr → n (SpecTheorem × List MVarId)
     unless (← withAssignableSyntheticOpaque <| isDefEq wp wp') do
       Term.throwTypeMismatchError none wp wp' spec
 
+    let P ← instantiateMVarsIfMVarApp P
+    let Q ← instantiateMVarsIfMVarApp Q
+
     let P := P.betaRev excessArgs
     let spec := spec.betaRev excessArgs
 
-    -- often P or Q are schematic (i.e. an MVar app). Try to solve by rfl.
-    let P ← instantiateMVarsIfMVarApp P
-    let Q ← instantiateMVarsIfMVarApp Q
-    let HPRfl ← withDefault <| withAssignableSyntheticOpaque <| isDefEqGuarded P goal.hyps
-    let QQ'Rfl ← withDefault <| withAssignableSyntheticOpaque <| isDefEqGuarded Q Q'
+    -- Often P or Q are schematic (i.e. an MVar app). Try to solve by rfl.
+    -- We do `fullApproxDefEq` here so that `constApprox` is active; this is useful in
+    -- `need_const_approx` of `doLogicTests.lean`.
+    let (HPRfl, QQ'Rfl) ← withDefault <| withAssignableSyntheticOpaque <| fullApproxDefEq <| do
+      return (← isDefEqGuarded P goal.hyps, ← isDefEqGuarded Q Q')
 
     -- Discharge the validity proof for the spec if not rfl
     let mut prePrf : Expr → Expr := id

src/Lean/Elab/Tactic/Do/Syntax.lean

@@ -11,20 +11,28 @@ import Std.Do.Triple.Basic
 
 namespace Std.Do.Syntax
 
-open Lean Parser Meta Elab Term
+open Lean Parser Meta Elab Term PrettyPrinter Delaborator
 
-@[builtin_term_parser] def «totalPostCond» := leading_parser:maxPrec
+@[builtin_term_parser] meta def «totalPostCond» := leading_parser:maxPrec
   ppAllowUngrouped >> "⇓" >> basicFun
 
 @[inherit_doc PostCond.total, builtin_doc, builtin_term_elab totalPostCond]
-private def elabTotalPostCond : TermElab
+private meta def elabTotalPostCond : TermElab
   | `(totalPostCond| ⇓ $xs* => $e), ty? => do
     elabTerm (← `(PostCond.total (by exact (fun $xs* => spred($e))))) ty?
      -- NB: Postponement through by exact
   | _, _ => throwUnsupportedSyntax
 
+@[builtin_delab app.Std.Do.PostCond.total]
+private meta def unexpandPostCondTotal : Delab := do
+  match ← SubExpr.withAppArg <| delab with
+  | `(fun $xs* => $e) =>
+    let t ← `(totalPostCond| ⇓ $xs* => $(← SPred.Notation.unpack e))
+    return ⟨t.raw⟩
+  | t => `($(mkIdent ``PostCond.total):term $t)
+
 @[inherit_doc Triple, builtin_doc, builtin_term_elab triple]
-private def elabTriple : TermElab
+private meta def elabTriple : TermElab
   | `(⦃$P⦄ $x ⦃$Q⦄), _ => do
     -- In a simple world, this would just be a macro expanding to
     -- `Triple $x spred($P) spred($Q)`.

src/Std/Do/PostCond.lean

@@ -197,12 +197,6 @@ abbrev PostCond.total (p : α → Assertion ps) : PostCond α ps :=
 -- The syntax `⇓ a b c => p` is defined as a builtin term parser in `Lean.Elab.Tactic.Do.Syntax`
 -- because the `basicFun` parser is not available in `Init`.
 
--- TODO: Uncomment after stage0 update
--- @[app_unexpander PostCond.total]
--- private def unexpandPostCondTotal : Lean.PrettyPrinter.Unexpander
---   | `($_ fun $xs* => $e) => do `(⇓ $xs* => $(← SPred.Notation.unpack e))
---   | _ => throw ()
-
 /-- A postcondition expressing partial correctness. -/
 abbrev PostCond.partial (p : α → Assertion ps) : PostCond α ps :=
   (p, FailConds.true)

src/Std/Do/Triple/Basic.lean

@@ -36,7 +36,7 @@ def Triple [WP m ps] {α} (x : m α) (P : Assertion ps) (Q : PostCond α ps) : P
 scoped syntax:lead (name := triple) "⦃" term "⦄ " term:lead " ⦃" term "⦄" : term
 
 @[app_unexpander Triple]
-private def unexpandTriple : Lean.PrettyPrinter.Unexpander
+private meta def unexpandTriple : Lean.PrettyPrinter.Unexpander
   | `($_ $x $P $Q) => do
     `(⦃$(← SPred.Notation.unpack P)⦄ $x ⦃$Q⦄)
   | _ => throw ()

tests/lean/run/doLogicTests.lean

@@ -522,7 +522,7 @@ theorem sum_loop_spec :
   ⦃True⦄
   sum_loop
   ⦃⇓r => r < 30⦄ := by
-  -- cf. `Toy.sum_loop_spec`
+  -- cf. `ByHand.sum_loop_spec`
   mintro -
   mvcgen [sum_loop]
   case inv => exact (⇓ (r, xs) => (∀ x, x ∈ xs.suff → x ≤ 5) ∧ r + xs.suff.length * 5 ≤ 25)
@@ -828,3 +828,38 @@ theorem max_and_sum_spec (xs : Array Nat) :
 end MaxAndSum
 
 end VSTTE2010
+
+namespace RishsConstApproxBug
+
+@[spec]
+theorem Spec.get_StateT' [Monad m] [WPMonad m psm] :
+  ⦃fun s => Q.1 s s⦄ (MonadState.get : StateT σ m σ) ⦃Q⦄ := Spec.get_StateT
+
+@[inline] def test : StateM Unit Unit := do
+  let _ ← get
+  if True then
+    pure ()
+
+/--
+error: unsolved goals
+⊢ ∀ (s : Unit), True → ⦃fun s => True⦄ pure () ⦃⇓ x => ⌜True⌝⦄
+
+⊢ ∀ (s : Unit), ¬True → ⦃fun s => True⦄ pure PUnit.unit ⦃⇓ x => ⌜True⌝⦄
+-/
+#guard_msgs in
+theorem need_const_approx :
+   ⦃fun x => x = ()⦄
+   test
+   ⦃⇓ _ => ⌜True⌝⦄ := by
+  unfold test
+  mintro _
+  mspec
+  mspec
+
+theorem need_const_approx' :
+   ⦃fun x => x = ()⦄
+   test
+   ⦃⇓ _ => ⌜True⌝⦄ := by
+  mvcgen [test]
+
+end RishsConstApproxBug