feat: Introduce mleave tactic that leaves the SPred proof mode (#9363) (#9454)

This PR introduces tactic `mleave` that leaves the `SPred` proof mode by
eta expanding through its abstractions and applying some mild
simplifications. This is useful to apply automation such as `grind`
afterwards.

Relates to #9363.

src/Init/Tactics.lean

@@ -2045,6 +2045,16 @@ macro (name := mstopMacro) (priority:=low) "mstop" : tactic =>
   Macro.throwError "to use `mstop`, please include `import Std.Tactic.Do`"
 
 
+/--
+Leaves the stateful proof mode of `Std.Do.SPred`, tries to eta-expand through all definitions
+related to the logic of the `Std.Do.SPred` and gently simplifies the resulting pure Lean
+proposition. This is often the right thing to do after `mvcgen` in order for automation to prove
+the goal.
+-/
+macro (name := mleaveMacro) (priority:=low) "mleave" : tactic =>
+  Macro.throwError "to use `mleave`, please include `import Std.Tactic.Do`"
+
+
 /--
 Like `rcases`, but operating on stateful `Std.Do.SPred` goals.
 Example: Given a goal `h : (P ∧ (Q ∨ R) ∧ (Q → R)) ⊢ₛ R`,

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

@@ -386,19 +386,20 @@ def genVCs (goal : MVarId) (ctx : Context) (fuel : Fuel) : TacticM (Array MVarId
   mvar.withContext do
   let (prf, vcs) ← step ctx (fuel := fuel) goal (← mvar.getTag)
   mvar.assign prf
-  replaceMainGoal vcs.toList
   return vcs
 
 @[builtin_tactic Lean.Parser.Tactic.mvcgenStep]
 def elabMVCGenStep : Tactic := fun stx => withMainContext do
   let ctx ← mkSpecContext stx[1] stx[3]
   let n := if stx[2].isNone then 1 else stx[2][0].toNat
-  discard <| genVCs (← getMainGoal) ctx (fuel := .limited n)
+  let vcs ← genVCs (← getMainGoal) ctx (fuel := .limited n)
+  replaceMainGoal vcs.toList
 
 @[builtin_tactic Lean.Parser.Tactic.mvcgenNoTrivial]
 def elabMVCGenNoTrivial : Tactic := fun stx => withMainContext do
   let ctx ← mkSpecContext stx[0] stx[1]
-  discard <| genVCs (← getMainGoal) ctx (fuel := .unlimited)
+  let vcs ← genVCs (← getMainGoal) ctx (fuel := .unlimited)
+  replaceMainGoal vcs.toList
 
 @[builtin_tactic Lean.Parser.Tactic.mvcgen]
 def elabMVCGen : Tactic := fun stx => withMainContext do
@@ -409,5 +410,11 @@ def elabMVCGen : Tactic := fun stx => withMainContext do
   -- but optConfig is not a leading_parser, and neither is the syntax for `lemmas`
   let ctx ← mkSpecContext stx[1] stx[2]
   let vcs ← genVCs (← getMainGoal) ctx (fuel := .unlimited)
-  let tac ← `(tactic| try ((try apply $(mkIdent ``Std.Do.SPred.Tactic.Pure.intro)); trivial))
-  for vc in vcs do discard <| runTactic vc tac
+  let tac ← `(tactic| (try (try apply $(mkIdent ``Std.Do.SPred.Tactic.Pure.intro)); trivial))
+  let mut s := {}
+  let mut newVCs := #[]
+  for vc in vcs do
+    let (vcs, s') ← runTactic vc tac (s := s)
+    s := s'
+    newVCs := newVCs ++ vcs
+  replaceMainGoal newVCs.toList

src/Std/Do/SPred/DerivedLaws.lean

@@ -161,8 +161,6 @@ theorem and_right_comm : (P ∧ Q) ∧ R ⊣⊢ₛ (P ∧ R) ∧ Q := and_assoc.
 
 theorem entails_pure_intro (P Q : Prop) (h : P → Q) : entails ⌜P⌝ (σs := σs) ⌜Q⌝ := pure_elim' fun hp => pure_intro (h hp)
 
-@[simp] theorem entails_elim_nil (P Q : SPred []) : entails P Q ↔ P.down → Q.down := iff_of_eq rfl
-theorem entails_elim_cons {σ : Type u} (P Q : SPred (σ::σs)) : P ⊢ₛ Q ↔ ∀ s, (P s ⊢ₛ Q s) := by simp only [entails]
 @[simp] theorem entails_pure_elim_cons {σ : Type u} [Inhabited σ] (P Q : Prop) : entails ⌜P⌝ (σs := σ::σs) ⌜Q⌝ ↔ entails ⌜P⌝ (σs := σs) ⌜Q⌝:= by simp [entails]
 @[simp] theorem entails_true_intro (P Q : SPred σs) : ⊢ₛ P → Q ↔ P ⊢ₛ Q := Iff.intro (fun h => (and_intro true_intro .rfl).trans (imp_elim h)) (fun h => imp_intro (and_elim_r.trans h))
 

src/Std/Tactic/Do/Syntax.lean

@@ -90,6 +90,22 @@ syntax (name := mstart) "mstart" : tactic
 @[inherit_doc Lean.Parser.Tactic.mstopMacro]
 syntax (name := mstop) "mstop" : tactic
 
+@[inherit_doc Lean.Parser.Tactic.mleaveMacro]
+macro (name := mleave) "mleave" : tactic =>
+  `(tactic| (try simp only [
+              $(mkIdent ``Std.Do.SPred.entails_cons):term,
+              $(mkIdent ``Std.Do.SPred.entails_nil):term,
+              $(mkIdent ``Std.Do.SPred.and_cons):term,
+              $(mkIdent ``Std.Do.SPred.and_nil):term,
+              $(mkIdent ``Std.Do.SVal.curry_cons):term,
+              $(mkIdent ``Std.Do.SVal.curry_nil):term,
+              $(mkIdent ``Std.Do.SVal.uncurry_cons):term,
+              $(mkIdent ``Std.Do.SVal.uncurry_nil):term,
+              $(mkIdent ``Std.Do.SVal.getThe_here):term,
+              $(mkIdent ``Std.Do.SVal.getThe_there):term,
+              $(mkIdent ``and_imp):term,
+              $(mkIdent ``true_implies):term]))
+
 declare_syntax_cat mcasesPat
 syntax mcasesPatAlts := sepBy1(mcasesPat, " | ")
 syntax binderIdent : mcasesPat

tests/lean/run/doLogicTests.lean

@@ -508,7 +508,7 @@ theorem add_unfold [Monad m] [WPMonad m sh] :
 
 theorem mkFreshPair_triple : ⦃⌜True⌝⦄ mkFreshPair ⦃⇓ (a, b) => ⌜a ≠ b⌝⦄ := by
   mvcgen [mkFreshPair]
-  simp_all [SPred.entails_elim_cons]
+  simp_all [SPred.entails_cons]
 
 theorem sum_loop_spec :
   ⦃⌜True⌝⦄