fix: Handle let/have in mintro (#9365)

src/Lean/Elab/Tactic/Do/ProofMode/Intro.lean

@@ -11,20 +11,29 @@ namespace Lean.Elab.Tactic.Do.ProofMode
 open Std.Do SPred.Tactic
 open Lean Elab Tactic Meta
 
-partial def mIntro [Monad m] [MonadControlT MetaM m] (goal : MGoal) (ident : TSyntax ``binderIdent) (k : MGoal → m (α × Expr)) : m (α × Expr) :=
-  controlAt MetaM fun map => do
-  let some (σs, H, T) := goal.target.app3? ``SPred.imp | throwError "Target not an implication {goal.target}"
-  let (name, ref) ← getFreshHypName ident
-  let uniq ← mkFreshId
+partial def mIntro [Monad m] [MonadControlT MetaM m] [MonadLiftT MetaM m] (goal : MGoal) (ident : TSyntax ``binderIdent) (k : MGoal → m (α × Expr)) : m (α × Expr) := do
+  if let some (σs, H, T) := goal.target.app3? ``SPred.imp then
+  let (name, ref) ← liftMetaM <| getFreshHypName ident
+  let uniq ← liftMetaM mkFreshId
   let hyp := Hyp.mk name uniq H
   addHypInfo ref σs hyp (isBinder := true)
   let Q := goal.hyps
   let H := hyp.toExpr
   let (P, hand) := mkAnd goal.u goal.σs goal.hyps H
-  map do
-    let (a, prf) ← k { goal with hyps := P, target := T }
-    let prf := mkApp7 (mkConst ``Intro.intro [goal.u]) σs P Q H T hand prf
-    return (a, prf)
+  let (a, prf) ← k { goal with hyps := P, target := T }
+  let prf := mkApp7 (mkConst ``Intro.intro [goal.u]) σs P Q H T hand prf
+  return (a, prf)
+  else if let .letE name type val body _nondep := goal.target then
+    let name ← match ident with
+    | `(binderIdent| $name:ident) => pure name.getId
+    | `(binderIdent| $_) => liftMetaM <| mkFreshUserName name
+    -- Even if `_nondep = true` we want to retain the value of the let binding for the proof.
+    withLetDecl name type val (nondep := false) fun val => do
+      let (a, prf) ← k { goal with target := body.instantiate1 val }
+      let prf ← liftMetaM <| mkLetFVars #[val] prf
+      return (a, prf)
+  else
+    liftMetaM <| throwError "Target not an implication or let-binding {goal.target}"
 
 -- This is regular MVar.intro, but it takes care not to leave the proof mode by preserving metadata
 partial def mIntroForall [Monad m] [MonadControlT MetaM m] [MonadLiftT MetaM m] (goal : MGoal) (ident : TSyntax ``binderIdent) (k : MGoal → m (α × Expr)) : m (α × Expr) :=

src/Std/Do/Triple/SpecLemmas.lean

@@ -176,7 +176,7 @@ theorem Spec.set_StateT [Monad m] [WPMonad m psm] :
 
 @[spec]
 theorem Spec.modifyGet_StateT [Monad m] [WPMonad m ps] :
-  ⦃fun s => Q.1 (f s).1 (f s).2⦄ (MonadStateOf.modifyGet f : StateT σ m α) ⦃Q⦄ := by
+  ⦃fun s => let t := f s; Q.1 t.1 t.2⦄ (MonadStateOf.modifyGet f : StateT σ m α) ⦃Q⦄ := by
     simp [Triple]
 
 /-! # `ExceptT` -/
@@ -221,7 +221,7 @@ theorem Spec.set_EStateM :
 
 @[spec]
 theorem Spec.modifyGet_EStateM :
-    ⦃fun s => Q.1 (f s).1 (f s).2⦄ (MonadStateOf.modifyGet f : EStateM ε σ α) ⦃Q⦄ := SPred.entails.rfl
+    ⦃fun s => let t := f s; Q.1 t.1 t.2⦄ (MonadStateOf.modifyGet f : EStateM ε σ α) ⦃Q⦄ := SPred.entails.rfl
 
 @[spec]
 theorem Spec.throw_EStateM :

tests/lean/run/9365.lean

@@ -0,0 +1,23 @@
+import Std.Tactic.Do
+
+open Std.Do
+
+set_option mvcgen.warning false
+
+abbrev SM := StateM (Array Nat)
+
+abbrev gns : SVal ((Array Nat)::[]) (Array Nat) := fun s => SVal.pure s
+
+noncomputable def setZeroHead : StateM (Array Nat) Unit := do
+  modify fun _ => #[0, 1, 2, 3, 4, 5]
+
+theorem setZeroHead_spec :
+   ⦃⌜True⌝⦄
+   setZeroHead
+   ⦃⇓ _ => ⌜∃ ns', (#gns).toList = 0 :: ns'⌝⦄ := by
+  mvcgen [setZeroHead]
+  -- We want `mintro`duce the tuple `t` here in order for us not having to repeat its
+  -- definition in t.2.toList.tail below
+  mintro t
+  simp
+  exists t.2.toList.tail