From 33b45132a49ac4e1ef458c290c254fce892d3d40 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Sun, 9 Feb 2025 09:11:28 -0800
Subject: [PATCH] feat: `bv_decide` hint (#7009)

This PR ensures users get an error message saying which module to import
when they try to use `bv_decide`.
---
 src/Init/Tactics.lean               | 51 +++++++++++++++++++++++++++++
 src/Std/Tactic/BVDecide/Syntax.lean | 36 ++------------------
 2 files changed, 54 insertions(+), 33 deletions(-)

diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean
index 96468f9cd7..e56de8cada 100644
--- a/src/Init/Tactics.lean
+++ b/src/Init/Tactics.lean
@@ -1608,6 +1608,57 @@ accessible name. If no local declarations require renaming, the original goal is
 -/
 syntax (name := exposeNames) "expose_names" : tactic
 
+/--
+Close fixed-width `BitVec` and `Bool` goals by obtaining a proof from an external SAT solver and
+verifying it inside Lean. The solvable goals are currently limited to
+- the Lean equivalent of [`QF_BV`](https://smt-lib.org/logics-all.shtml#QF_BV)
+- automatically splitting up `structure`s that contain information about `BitVec` or `Bool`
+```lean
+example : ∀ (a b : BitVec 64), (a &&& b) + (a ^^^ b) = a ||| b := by
+  intros
+  bv_decide
+```
+
+If `bv_decide` encounters an unknown definition it will be treated like an unconstrained `BitVec`
+variable. Sometimes this enables solving goals despite not understanding the definition because
+the precise properties of the definition do not matter in the specific proof.
+
+If `bv_decide` fails to close a goal it provides a counter-example, containing assignments for all
+terms that were considered as variables.
+
+In order to avoid calling a SAT solver every time, the proof can be cached with `bv_decide?`.
+
+If solving your problem relies inherently on using associativity or commutativity, consider enabling
+the `bv.ac_nf` option.
+
+
+Note: `bv_decide` uses `ofReduceBool` and thus trusts the correctness of the code generator.
+
+Note: include `import Std.Tactic.BVDecide`
+-/
+macro (name := bvDecideMacro) (priority:=low) "bv_decide" optConfig : tactic =>
+  Macro.throwError "to use `bv_decide`, please include `import Std.Tactic.BVDecide`"
+
+
+/--
+Suggest a proof script for a `bv_decide` tactic call. Useful for caching LRAT proofs.
+
+Note: include `import Std.Tactic.BVDecide`
+-/
+macro (name := bvTraceMacro) (priority:=low) "bv_decide?" optConfig : tactic =>
+  Macro.throwError "to use `bv_decide?`, please include `import Std.Tactic.BVDecide`"
+
+
+/--
+Run the normalization procedure of `bv_decide` only. Sometimes this is enough to solve basic
+`BitVec` goals already.
+
+Note: include `import Std.Tactic.BVDecide`
+-/
+macro (name := bvNormalizeMacro) (priority:=low) "bv_normalize" optConfig : tactic =>
+  Macro.throwError "to use `bv_normalize`, please include `import Std.Tactic.BVDecide`"
+
+
 end Tactic
 
 namespace Attr
diff --git a/src/Std/Tactic/BVDecide/Syntax.lean b/src/Std/Tactic/BVDecide/Syntax.lean
index dff66a4c8b..7dbb45ce85 100644
--- a/src/Std/Tactic/BVDecide/Syntax.lean
+++ b/src/Std/Tactic/BVDecide/Syntax.lean
@@ -79,44 +79,14 @@ bv_check "proof.lrat"
 -/
 syntax (name := bvCheck) "bv_check " optConfig str : tactic
 
-/--
-Close fixed-width `BitVec` and `Bool` goals by obtaining a proof from an external SAT solver and
-verifying it inside Lean. The solvable goals are currently limited to
-- the Lean equivalent of [`QF_BV`](https://smt-lib.org/logics-all.shtml#QF_BV)
-- automatically splitting up `structure`s that contain information about `BitVec` or `Bool`
-```lean
-example : ∀ (a b : BitVec 64), (a &&& b) + (a ^^^ b) = a ||| b := by
-  intros
-  bv_decide
-```
-
-If `bv_decide` encounters an unknown definition it will be treated like an unconstrained `BitVec`
-variable. Sometimes this enables solving goals despite not understanding the definition because
-the precise properties of the definition do not matter in the specific proof.
-
-If `bv_decide` fails to close a goal it provides a counter-example, containing assignments for all
-terms that were considered as variables.
-
-In order to avoid calling a SAT solver every time, the proof can be cached with `bv_decide?`.
-
-If solving your problem relies inherently on using associativity or commutativity, consider enabling
-the `bv.ac_nf` option.
-
-
-Note: `bv_decide` uses `ofReduceBool` and thus trusts the correctness of the code generator.
--/
+@[inherit_doc bvDecideMacro]
 syntax (name := bvDecide) "bv_decide" optConfig : tactic
 
 
-/--
-Suggest a proof script for a `bv_decide` tactic call. Useful for caching LRAT proofs.
--/
+@[inherit_doc bvTraceMacro]
 syntax (name := bvTrace) "bv_decide?" optConfig : tactic
 
-/--
-Run the normalization procedure of `bv_decide` only. Sometimes this is enough to solve basic
-`BitVec` goals already.
--/
+@[inherit_doc bvNormalizeMacro]
 syntax (name := bvNormalize) "bv_normalize" optConfig : tactic
 
 end Tactic