From 9d9f5dee884f3442247e7dbb03384191fc8efd88 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Fri, 20 Jun 2025 12:00:25 -0700
Subject: [PATCH] test: Use synthetic tactic to generate aux lemmas

---
 Test/Common.lean | 20 ++++++++++++++++++++
 Test/Serial.lean | 25 ++++++++++++-------------
 2 files changed, 32 insertions(+), 13 deletions(-)

diff --git a/Test/Common.lean b/Test/Common.lean
index 8bea339..34ce07b 100644
--- a/Test/Common.lean
+++ b/Test/Common.lean
@@ -183,6 +183,26 @@ def buildGoal (nameType: List (String × String)) (target: String) (userName?: O
     })).toArray
   }
 
+namespace Tactic
+
+/-- Create an aux lemma and assigns it to `mvarId`, which is circuitous, but
+exercises the aux lemma generator. -/
+def assignWithAuxLemma (type value : Expr) : Elab.Tactic.TacticM Unit := do
+  let type ← instantiateMVars type
+  let value ← instantiateMVars value
+  if type.hasExprMVar then
+    throwError "Type has expression mvar"
+  if value.hasExprMVar then
+    throwError "value has expression mvar"
+  let goal ← Elab.Tactic.getMainGoal
+  goal.withContext do
+  let name ← Meta.mkAuxLemma [] type value
+  unless ← Meta.isDefEq type (← goal.getType) do
+    throwError "Type provided is incorrect"
+  goal.assign (.const name [])
+
+end Tactic
+
 end Test
 
 end Pantograph
diff --git a/Test/Serial.lean b/Test/Serial.lean
index 9fb8601..b37cc95 100644
--- a/Test/Serial.lean
+++ b/Test/Serial.lean
@@ -74,22 +74,21 @@ def test_goal_state_simple : TestM Unit := do
 
 def test_pickling_env_extensions : TestM Unit := do
   let coreSrc : Core.State := { env := ← getEnv }
+  let p := mkIdent `p
+  let h := mkIdent `h
   let ((), _) ← runCoreM coreSrc $ transformTestT runTermElabMInCore do
-    let .ok e ← elabTerm (← `(term|2 ≤ 5)) .none | unreachable!
+    let .ok e ← elabTerm (← `(term|(2: Nat) ≤ 3 ∧ (3: Nat) ≤ 5)) .none | unreachable!
     let state ← GoalState.create e
-    let .success state _ ← state.tacticOn' 0 (← `(tactic|apply Nat.le_trans)) | unreachable!
-    let .success state' _ ← state.tacticOn' 2 (← `(tactic|exact 3)) | unreachable!
-    let state := state'.immediateResume state
-    let .success state1 _ ← state.tacticOn' 1 (← `(tactic|simp)) | unreachable!
-    let parentExpr := state1.parentExpr?.get!
-    IO.println s!"{parentExpr}"
-    checkTrue "has aux lemma" $ parentExpr.getUsedConstants.any λ name => name.isAuxLemma
+    let .success state _ ← state.tacticOn' 0 (← `(tactic|apply And.intro)) | unreachable!
 
-    let state1 := state1.immediateResume state
-    let .success stateT _ ← state.tacticOn' 0 (← `(tactic|simp)) | unreachable!
-    let rootExpr:= stateT.rootExpr?.get!
-    IO.println s!"root is {rootExpr}"
-    checkTrue "has aux lemma" $ rootExpr.getUsedConstants.any λ name => name.isAuxLemma
+    let goal := state.goals[0]!
+    let (type, value) ← goal.withContext do
+      let .ok type ← elabTerm (← `(term|(2: Nat) ≤ 3)) (.some $ .sort 0) | unreachable!
+      let .ok value ← elabTerm (← `(term|sorry)) (.some type) | unreachable!
+      pure (type, value)
+    let .success state1 _ ← state.tryTacticM goal (Tactic.assignWithAuxLemma type value) | unreachable!
+    let parentExpr := state1.parentExpr?.get!
+    checkTrue "has aux lemma" $ parentExpr.getUsedConstants.any λ name => name.isAuxLemma
   return ()
 
 structure Test where