From 548d564c184687015dde1efb545c79038b8ea24e Mon Sep 17 00:00:00 2001 From: Sebastian Graf Date: Tue, 22 Jul 2025 13:50:16 +0200 Subject: [PATCH] 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 | 10 ++++++++++ src/Lean/Elab/Tactic/Do/VCGen.lean | 17 ++++++++++++----- src/Std/Do/SPred/DerivedLaws.lean | 2 -- src/Std/Tactic/Do/Syntax.lean | 16 ++++++++++++++++ tests/lean/run/doLogicTests.lean | 2 +- 5 files changed, 39 insertions(+), 8 deletions(-) diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean index 24c59e4bcf..18677bdef8 100644 --- a/src/Init/Tactics.lean +++ b/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`, diff --git a/src/Lean/Elab/Tactic/Do/VCGen.lean b/src/Lean/Elab/Tactic/Do/VCGen.lean index 5309c40305..1ab17cc1a5 100644 --- a/src/Lean/Elab/Tactic/Do/VCGen.lean +++ b/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 diff --git a/src/Std/Do/SPred/DerivedLaws.lean b/src/Std/Do/SPred/DerivedLaws.lean index 784553234e..e289157d80 100644 --- a/src/Std/Do/SPred/DerivedLaws.lean +++ b/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)) diff --git a/src/Std/Tactic/Do/Syntax.lean b/src/Std/Tactic/Do/Syntax.lean index dfcb23f2db..7869c4a253 100644 --- a/src/Std/Tactic/Do/Syntax.lean +++ b/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 diff --git a/tests/lean/run/doLogicTests.lean b/tests/lean/run/doLogicTests.lean index f0cea14a3b..8ce3e3d128 100644 --- a/tests/lean/run/doLogicTests.lean +++ b/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⌝⦄