From 13c23877d46eb02468ee409e28b130aa53c15426 Mon Sep 17 00:00:00 2001 From: Sebastian Graf Date: Fri, 19 Sep 2025 10:21:04 +0200 Subject: [PATCH] fix: reduce through `let`s in `mvcgen` main loop (#10453) This PR makes `mvcgen` reduce through `let`s, so that it progresses over `(have t := 42; fun _ => foo t) 23` by reduction to `have t := 42; foo t` and then introducing `t`. --- src/Lean/Elab/Tactic/Do/VCGen/Basic.lean | 4 ++++ tests/lean/run/mvcgenTutorial.lean | 5 +++++ 2 files changed, 9 insertions(+) diff --git a/src/Lean/Elab/Tactic/Do/VCGen/Basic.lean b/src/Lean/Elab/Tactic/Do/VCGen/Basic.lean index f43faa43f0..031f9be542 100644 --- a/src/Lean/Elab/Tactic/Do/VCGen/Basic.lean +++ b/src/Lean/Elab/Tactic/Do/VCGen/Basic.lean @@ -181,6 +181,10 @@ partial def reduceProjBeta? (e : Expr) : MetaM (Option Expr) := let e' := mkAppRev f' rargs go (some e') e'.getAppFn e'.getAppRevArgs | none => pure lastReduction + | .letE x ty val body nondep => + match ← go none body rargs with + | none => pure lastReduction + | some body' => pure (some (.letE x ty val body' nondep)) | _ => pure lastReduction def mkSpecContext (optConfig : Syntax) (lemmas : Syntax) (ignoreStarArg := false) : TacticM Context := do diff --git a/tests/lean/run/mvcgenTutorial.lean b/tests/lean/run/mvcgenTutorial.lean index e2991f2de5..4588f7665b 100644 --- a/tests/lean/run/mvcgenTutorial.lean +++ b/tests/lean/run/mvcgenTutorial.lean @@ -115,6 +115,11 @@ def mkFreshN (n : Nat) : AppM (List Nat) := do acc := acc.push n return acc.toList +theorem mkFreshN_spec_noncompositional (n : Nat) : ⦃⌜True⌝⦄ mkFreshN n ⦃⇓ r => ⌜r.Nodup⌝⦄ := by + mvcgen [mkFreshN, mkFresh, liftCounterM] + case inv1 => exact ⇓⟨xs, acc⟩ _ state => ⌜(∀ n ∈ acc, n < state.counter) ∧ acc.toList.Nodup⌝ + all_goals mleave; grind + @[spec] theorem mkFresh_spec [Monad m] [WPMonad m ps] (c : Nat) : ⦃fun state => ⌜state.counter = c⌝⦄ mkFresh (m := m) ⦃⇓ r state => ⌜r = c ∧ c < state.counter⌝⦄ := by