test: use Sym.simp to unfold in VCGen benchmarks (#12593)

This PR improves the Sym VCGen such that we can use Sym.simp to unfold
definitions in the benchmark driver. To do so, it adds support for
zeta-reduction in the VCGen and ensures that proof terms are maximally
shared before being sent to the kernel.

tests/bench/mvcgen/sym/lib/Driver.lean

@@ -20,26 +20,16 @@ def timeItMs (k : MetaM α) : MetaM (α × UInt64) := do
 /-- Helper function for executing a tactic `k` for solving `$(goal) n`. -/
 def driver (goal : Name) (unfold : List Name) (n : Nat) (discharge : MetaM (TSyntax `tactic)) (k : MVarId → MetaM (List MVarId)) : MetaM Unit := do
   let mvar ← mkFreshExprMVar (mkApp (mkConst goal) (mkNatLit n))
-  -- The following code uses `Sym.simp`, but it balloons in the kernel. TODO: Investigate with new semantic
-  -- foundations. Use regular simp for now.
-  let useSymSimpForUnfolding := false
-  let (mvarId, _unfoldMs) ← timeItMs do
-    if useSymSimpForUnfolding then SymM.run do
-        let mvarId ← preprocessMVar mvar.mvarId!
-        let eqnss ← unfold.toArray
-          |>.push goal
-          |>.mapM fun n => getEqnsFor? n
-        let thms := eqnss.flatMap (fun o => o.getD #[])
-        match (← Sym.simpGoal mvarId (← Sym.mkMethods thms)) with
-        | .goal mvarId => return mvarId
-        | .noProgress => throwError "SIMP NO PROGRESS on {mvarId}!"
-        | .closed => throwError "SIMP CLOSED!"
-    else
-      let lemmas ← unfold.toArray |>.push goal |>.mapM fun n => `(simpLemma| $(Lean.mkIdent n):term)
-      let unfold := Syntax.TSepArray.ofElems (sep := ",") lemmas
-      let ([mvarId], _) ← Lean.Elab.runTactic mvar.mvarId! (← `(tactic| simp only [$unfold,*])).raw {} {}
-        | throwError "FAILED!"
-      return mvarId
+  let (mvarId, _unfoldMs) ← timeItMs do SymM.run do
+    let mvarId ← preprocessMVar mvar.mvarId!
+    let eqnss ← unfold.toArray
+      |>.push goal
+      |>.mapM fun n => getEqnsFor? n
+    let thms := eqnss.flatMap (fun o => o.getD #[])
+    match (← Sym.simpGoal mvarId (← Sym.mkMethods thms)) with
+    | .goal mvarId => return mvarId
+    | .noProgress => throwError "No progress when simping {mvarId}!"
+    | .closed => throwError "Simp closed goal {mvarId}"
   -- IO.println s!"time spent unfolding: {_unfoldMs} ms"
   let (mvarIds, ms) ← timeItMs do k mvarId
   let discharge ← discharge
@@ -51,6 +41,9 @@ def driver (goal : Name) (unfold : List Name) (n : Nat) (discharge : MetaM (TSyn
         let ([], _) ← Lean.Elab.runTactic mvarId discharge.raw {} {}
           | throwError "{dischargePp} failed to solve {mvarId}"
   let (expr, instMs) ← timeItMs (instantiateMVars mvar)
+  -- Emulate the shareCommonPreDefs step before sending the term to the kernel.
+  -- If we don't do this, kernel checking time balloons.
+  let expr ← SymM.run (shareCommon expr)
   let (_, kernelMs) ← timeItMs (checkWithKernel expr)
   let mut msg := s!"goal_{n}: {ms} ms"
   if let some dischargeMs := dischargeMs? then

tests/bench/mvcgen/sym/lib/VCGen.lean

@@ -478,6 +478,37 @@ inductive SolveResult where
   /-- Successfully discharged the goal. These are the subgoals. -/
   | goals (subgoals : List MVarId)
 
+open Sym Sym.Internal
+-- The following function is vendored until it is made public:
+/-- `mkAppRevRangeS f b e args == mkAppRev f (revArgs.extract b e)` -/
+meta def mkAppRevRangeS [Monad m] [Internal.MonadShareCommon m] (f : Expr) (beginIdx endIdx : Nat) (revArgs : Array Expr) : m Expr :=
+  loop revArgs beginIdx f endIdx
+where
+  loop (revArgs : Array Expr) (start : Nat) (b : Expr) (i : Nat) : m Expr := do
+  if i ≤ start then
+    return b
+  else
+    let i := i - 1
+    loop revArgs start (← mkAppS b revArgs[i]!) i
+
+open Sym Sym.Internal
+meta def mkAppRevS [Monad m] [Internal.MonadShareCommon m] (f : Expr) (revArgs : Array Expr) : m Expr :=
+  mkAppRevRangeS f 0 revArgs.size revArgs
+
+open Sym Sym.Internal
+meta def mkAppRangeS [Monad m] [Internal.MonadShareCommon m] (f : Expr) (beginIdx endIdx : Nat) (args : Array Expr) : m Expr :=
+  loop args endIdx f beginIdx
+where
+  loop (args : Array Expr) (end' : Nat) (b : Expr) (i : Nat) : m Expr := do
+  if end' ≤ i then
+    return b
+  else
+    loop args end' (← mkAppS b args[i]!) (i + 1)
+
+open Sym Sym.Internal
+meta def mkAppNS [Monad m] [Internal.MonadShareCommon m] (f : Expr) (args : Array Expr) : m Expr :=
+  mkAppRangeS f 0 args.size args
+
 /--
 The main VC generation function.
 Looks at a goal of the form `P ⊢ₛ T`. Then
@@ -517,6 +548,16 @@ meta def solve (goal : MVarId) : VCGenM SolveResult := goal.withContext do
   let f := e.getAppFn
   withTraceNode `Elab.Tactic.Do.vcgen (msg := fun _ => return m!"Program: {e}") do
 
+  -- 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 [goal]
+
   -- Hard-code match splitting for `ite` for now.
   if f.isAppOf ``ite then
     let some info ← Lean.Elab.Tactic.Do.getSplitInfo? e | return .noStrategyForProgram e