diff --git a/tests/bench/mvcgen/sym/cases/Cases.lean b/tests/bench/mvcgen/sym/cases/Cases.lean index daa1c76683..d304df1af8 100644 --- a/tests/bench/mvcgen/sym/cases/Cases.lean +++ b/tests/bench/mvcgen/sym/cases/Cases.lean @@ -3,7 +3,7 @@ import Cases.AddSubCancelDeep import Cases.AddSubCancelSimp import Cases.DiteSplit import Cases.GetThrowSet +import Cases.MatchIota import Cases.MatchSplit -import Cases.MatchSplitState import Cases.PurePrecond import Cases.ReaderState diff --git a/tests/bench/mvcgen/sym/cases/Cases/MatchSplitState.lean b/tests/bench/mvcgen/sym/cases/Cases/MatchIota.lean similarity index 63% rename from tests/bench/mvcgen/sym/cases/Cases/MatchSplitState.lean rename to tests/bench/mvcgen/sym/cases/Cases/MatchIota.lean index 66384168cf..9fbfd1abe1 100644 --- a/tests/bench/mvcgen/sym/cases/Cases/MatchSplitState.lean +++ b/tests/bench/mvcgen/sym/cases/Cases/MatchIota.lean @@ -3,7 +3,7 @@ import VCGen open Lean Meta Elab Tactic Sym Std Do SpecAttr -namespace MatchSplitState +namespace MatchIota set_option mvcgen.warning false @@ -24,18 +24,17 @@ theorem Spec.get_M : ⦃fun s => Q.1 s s⦄ get (m := M) ⦃Q⦄ := by mvcgen -/-- Matches on state `s` — the discriminant IS the excess state arg. -/ -def step : M Unit := do +def step (v : Nat) : M Unit := do let s ← get - match s with - | 0 => throw "s is zero" - | n+1 => set n + match v with + | 0 => throw "v is zero" + | n+1 => set (s + n + 1); let s ← get; set (s - n) def loop (n : Nat) : M Unit := do match n with | 0 => pure () - | n+1 => step; loop n + | n+1 => step n; loop n -def Goal (n : Nat) : Prop := ⦃fun s => ⌜s = n⌝⦄ loop n ⦃⇓_ s => ⌜s = 0⌝⦄ +def Goal (n : Nat) : Prop := ⦃fun s => ⌜s = 0⌝⦄ loop n ⦃⇓_ s => ⌜s = n⌝⦄ -end MatchSplitState +end MatchIota diff --git a/tests/bench/mvcgen/sym/cases/Cases/MatchSplit.lean b/tests/bench/mvcgen/sym/cases/Cases/MatchSplit.lean index 5a873ab2b4..7cac619f40 100644 --- a/tests/bench/mvcgen/sym/cases/Cases/MatchSplit.lean +++ b/tests/bench/mvcgen/sym/cases/Cases/MatchSplit.lean @@ -24,17 +24,18 @@ theorem Spec.get_M : ⦃fun s => Q.1 s s⦄ get (m := M) ⦃Q⦄ := by mvcgen -def step (v : Nat) : M Unit := do +/-- Matches on state `s` — the discriminant IS the excess state arg. -/ +def step : M Unit := do let s ← get - match v with - | 0 => throw "v is zero" - | n+1 => set (s + n + 1); let s ← get; set (s - n) + match s with + | 0 => throw "s is zero" + | n+1 => set n def loop (n : Nat) : M Unit := do match n with | 0 => pure () - | n+1 => step n; loop n + | n+1 => step; loop n -def Goal (n : Nat) : Prop := ⦃fun s => ⌜s = 0⌝⦄ loop n ⦃⇓_ s => ⌜s = n⌝⦄ +def Goal (n : Nat) : Prop := ⦃fun s => ⌜s = n⌝⦄ loop n ⦃⇓_ s => ⌜s = 0⌝⦄ end MatchSplit diff --git a/tests/bench/mvcgen/sym/lib/VCGen.lean b/tests/bench/mvcgen/sym/lib/VCGen.lean index 218472cdf1..c616ed5ca9 100644 --- a/tests/bench/mvcgen/sym/lib/VCGen.lean +++ b/tests/bench/mvcgen/sym/lib/VCGen.lean @@ -838,18 +838,24 @@ meta def solve (item : WorkItem) : VCGenM SolveResult := item.mvarId.withContext let f := e.getAppFn withTraceNode `Elab.Tactic.Do.vcgen (msg := fun _ => return m!"Program: {e}") do + -- Replace the program in the goal with `e'` (which must be definitionally equal). + let replaceProgDefEq (e' : Expr) : VCGenM MVarId := do + let wp ← Sym.Internal.mkAppS₅ wpConst m ps instWP α e' + let T ← mkAppNS head (args.set! 2 wp) + let target ← mkAppS₃ ent σs H T + goal.replaceTargetDefEq target + -- Zeta let-expressions if let .letE _x _ty val body _nonDep := f then let body' ← Sym.instantiateRevBetaS body #[val] let e' ← mkAppRevS body' e.getAppRevArgs - let wp ← Sym.Internal.mkAppS₅ wpConst m ps instWP α e' - let T ← mkAppNS head (args.set! 2 wp) - let target ← mkAppS₃ ent σs H T - let goal ← goal.replaceTargetDefEq target - return .goals [item.withMVarId goal] + return .goals [item.withMVarId (← replaceProgDefEq e')] -- Split ite/dite/match if let some info ← liftMetaM <| Lean.Elab.Tactic.Do.getSplitInfo? e then + -- Try iota reduction first (reduces matcher/recursor with concrete discriminant) + if let some e' ← liftMetaM <| reduceRecMatcher? e then + return .goals [item.withMVarId (← replaceProgDefEq (← shareCommonInc e'))] -- Internalize pending hypotheses before forking let item ← internalizePending item let rule ← mkBackwardRuleFromSplitInfoCached info m σs ps instWP excessArgs diff --git a/tests/bench/mvcgen/sym/test_vcgen.lean b/tests/bench/mvcgen/sym/test_vcgen.lean index 301e31ed57..c189bbf8f8 100644 --- a/tests/bench/mvcgen/sym/test_vcgen.lean +++ b/tests/bench/mvcgen/sym/test_vcgen.lean @@ -19,8 +19,8 @@ Each case exercises a different aspect of the VC generation: - `PurePrecond`: Pure hypotheses `⌜φ⌝` in preconditions - `ReaderState`: `ReaderT`/`StateM` combination - `DiteSplit`: Dependent if-then-else (`if h : cond then ...`) -- `MatchSplit`: Pattern matching in monadic programs -- `MatchSplitState`: Match on state variable (discriminant = excess state arg) +- `MatchIota`: Pattern matching with concrete discriminants (iota-reduced, no split) +- `MatchSplit`: Pattern matching with symbolic discriminant (state), exercising match split -/ open Lean Parser Meta Elab Tactic Sym Std Do SpecAttr @@ -57,8 +57,8 @@ open ReaderState in open DiteSplit in #eval runBenchUsingTactic ``Goal [``loop, ``step] `(tactic| mvcgen') `(tactic| sorry) [10] -open MatchSplit in +open MatchIota in #eval runBenchUsingTactic ``Goal [``loop, ``step] `(tactic| mvcgen') `(tactic| sorry) [10] -open MatchSplitState in +open MatchSplit in #eval runBenchUsingTactic ``Goal [``loop, ``step] `(tactic| mvcgen') `(tactic| grind) [10] diff --git a/tests/bench/mvcgen/sym/vcgen_match_split.lean b/tests/bench/mvcgen/sym/vcgen_match_split.lean index 2ff6170430..e0da99dad2 100644 --- a/tests/bench/mvcgen/sym/vcgen_match_split.lean +++ b/tests/bench/mvcgen/sym/vcgen_match_split.lean @@ -3,11 +3,11 @@ Copyright (c) 2026 Lean FRO LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Sebastian Graf -/ -import Cases.MatchSplit +import Cases.MatchIota import Driver open Lean Parser Meta Elab Tactic Sym Std Do SpecAttr -open MatchSplit +open MatchIota set_option maxRecDepth 10000 set_option maxHeartbeats 10000000