Ensure that auxiliary declarations on different branches have different names (#224)

Author: JLimperg

Aesop/Tree/AddRapp.lean

@@ -155,6 +155,18 @@ def makeInitialGoal (goal : Subgoal) (mvars : UnorderedArraySet MVarId)
 unsafe def addRappUnsafe (r : AddRapp) : TreeM RappRef := do
   let originalSubgoals := r.goals
 
+  -- We update the rapp's `auxDeclNGen` to ensure that tactics on different
+  -- branches of the search tree generate different names for auxiliary
+  -- declarations.
+  let auxDeclNGen ←
+    match ← (← r.parent.get).parentRapp? with
+    | none =>
+      let (child, parent) := (← getDeclNGen).mkChild
+      setDeclNGen parent
+      pure child
+    | some parentRapp => parentRapp.getChildAuxDeclNameGenerator
+  let metaState := { r.postState with core.auxDeclNGen := auxDeclNGen }
+
   let rref : RappRef ← IO.mkRef $ Rapp.mk {
     id := ← getAndIncrementNextRappId
     parent := r.parent
@@ -165,7 +177,7 @@ unsafe def addRappUnsafe (r : AddRapp) : TreeM RappRef := do
     scriptSteps? := r.scriptSteps?
     originalSubgoals := originalSubgoals.map (·.mvarId)
     successProbability := r.successProbability
-    metaState := r.postState
+    metaState
     introducedMVars := {} -- will be filled in later
     assignedMVars   := {} -- will be filled in later
   }

Aesop/Tree/Data.lean

@@ -906,3 +906,17 @@ def provenGoal? (c : MVarCluster) : BaseIO (Option GoalRef) :=
   c.goals.findM? λ gref => return (← gref.get).state.isProven
 
 end MVarCluster
+
+
+namespace RappRef
+
+/-- Get a `DeclNameGenerator` for auxiliary declarations that can be used by
+children of this rapp. Successive calls to this function return
+`DeclNameGenerators` that are guaranteed to generate distinct names. -/
+def getChildAuxDeclNameGenerator (r : RappRef) : BaseIO DeclNameGenerator := do
+  r.modifyGet λ r =>
+    let (child, parent) := r.metaState.core.auxDeclNGen.mkChild
+    let r := r.setMetaState $ { r.metaState with core.auxDeclNGen := parent }
+    (child, r)
+
+end RappRef

Aesop/Tree/ExtractProof.lean

@@ -34,8 +34,11 @@ When we assign a metavariable `m`, we must take some care:
   assignments, since they may additionally contain delayed-assigned
   metavariables which depend on the unassigned metavariables.
 
-We also replay env modifications in a similar fashion. We assume that rules only
-add declarations to the environment.
+We also replay environment modifications -- e.g., auxiliary declarations added
+by a tactic -- in a similar fashion. To do this, we use
+`Environment.replayConsts`, so newly added constants are sent to the kernel
+again and environment extensions get a chance to replay their changes with
+`replay?`.
 
 If the root goal is not proven, we extract the goals after safe rule
 applications. This means we proceed as above, but stop as soon as we reach the
@@ -51,11 +54,8 @@ local macro "throwPRError " s:interpolatedStr(term) : term =>
 
 -- ## Copying Declarations
 
-
 private def copyEnvModifications (oldEnv newEnv : Environment) : CoreM Unit := do
-  let env ← getEnv
-  let env ← env.replayConsts oldEnv newEnv
-  setEnv env
+  setEnv $ ← (← getEnv).replayConsts oldEnv newEnv (skipExisting := true)
 
 -- ## Copying Metavariables
 
@@ -104,7 +104,7 @@ private def visitGoal (parentEnv : Environment) (g : Goal) :
   | NormalizationState.normal postNormGoal postState _ =>
     copyEnvModifications parentEnv postState.core.env
     copyExprMVar postState g.preNormGoal
-    return (postNormGoal, g.children, ← getEnv)
+    return (postNormGoal, g.children, postState.core.env)
   | NormalizationState.provenByNormalization postState _ =>
     copyEnvModifications parentEnv postState.core.env
     copyExprMVar postState g.preNormGoal

AesopTest/AuxDecl.lean

@@ -0,0 +1,32 @@
+/-
+Copyright (c) 2025 Jannis Limperg. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jannis Limperg
+-/
+
+import Aesop
+
+/-
+This test case checks whether tactics that make use of auxiliary declarations,
+such as `omega` and `bv_decide`, work with Aesop. Auxiliary declarations are
+problematic because we can't allows tactics on different branches of the search
+tree to add auxiliary declarations with the same name.
+-/
+
+theorem foo (m n : Nat) : n + m = m + n ∧ m + n = n + m := by
+  fail_if_success aesop (config := { terminal := true })
+  aesop (add safe (by omega))
+
+local instance [Add α] [Add β] : Add (α × β) :=
+  ⟨λ (a, b) (a', b') => (a + a', b + b')⟩
+
+theorem bar
+    (fst snd fst_1 snd_1 fst_2 snd_2 w w_1 w_2 w_3 : BitVec 128)
+    (left : w_1.uaddOverflow w_3 = true)
+    (left_1 : w.uaddOverflow w_2 = true)
+    (right : (w_1 + w_3).uaddOverflow 1#128 = true) :
+    (fst_2, snd_2) = (fst, snd) + (fst_1, snd_1) := by
+  aesop (add safe (by bv_decide))
+
+theorem baz (a b : BitVec 1) : (a = 0 ∨ a = 1) ∧ (b = 0 ∨ b = 1) := by
+  aesop (add safe 1000 (by bv_decide))