From 017a1f2b940ca696f2ac12bb471a5c819ffcff76 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Mon, 3 Mar 2025 22:27:53 +0100
Subject: [PATCH] fix: bv_decide structures pass instantiate mvars (#7309)

This PR fixes a bug where bv_decide's new structure support would
sometimes not case split on all available structure fvars as their type
was an mvar.
---
 .../Frontend/Normalize/Structures.lean        |  2 +-
 .../Frontend/Normalize/TypeAnalysis.lean      |  3 +++
 tests/bv_relation.lean                        | 24 +++++++++++++++++++
 3 files changed, 28 insertions(+), 1 deletion(-)
 create mode 100644 tests/bv_relation.lean

diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Structures.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Structures.lean
index 770ef4e32e..4e6994d83d 100644
--- a/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Structures.lean
+++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Structures.lean
@@ -64,7 +64,7 @@ partial def structuresPass : Pass where
       if decl.isLet || decl.isImplementationDetail then
         return false
       else
-        let some const := decl.type.getAppFn.constName? | return false
+        let some const := (← instantiateMVars decl.type).getAppFn.constName? | return false
         return interesting.contains const
     match goals with
     | [goal] => postprocess goal interesting
diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/TypeAnalysis.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/TypeAnalysis.lean
index ab25db8904..9c868efc9b 100644
--- a/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/TypeAnalysis.lean
+++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/TypeAnalysis.lean
@@ -22,6 +22,9 @@ partial def typeAnalysisPass : Pass where
   name := `typeAnalysis
   run' goal := do
     checkContext goal
+    let analysis ← PreProcessM.getTypeAnalysis
+    trace[Meta.Tactic.bv] m!"Type analysis found structures: {analysis.interestingStructures.toList}"
+    trace[Meta.Tactic.bv] m!"Type analysis found enums: {analysis.interestingEnums.toList}"
     return goal
 where
   checkContext (goal : MVarId) : PreProcessM Unit := do
diff --git a/tests/bv_relation.lean b/tests/bv_relation.lean
new file mode 100644
index 0000000000..3bb750402b
--- /dev/null
+++ b/tests/bv_relation.lean
@@ -0,0 +1,24 @@
+import Std.Tactic.BVDecide
+
+structure State where
+  x : BitVec 8
+  y : BitVec 8
+  z : BitVec 8
+
+inductive Transfer : State → State → Prop
+  | step : Transfer ⟨x, y, z⟩ ⟨y, z, x⟩
+
+@[simp]
+theorem Transfer.iff_x : Transfer s1 s2 ↔ (s2.x = s1.y ∧ s2.y = s1.z ∧ s2.z = s1.x) := by
+  constructor
+  · intro h
+    cases h
+    simp
+  · intro h
+    cases s1 <;> cases s2 <;> simp_all [Transfer.step]
+
+def P (s : State) : Prop := s.x > 3
+
+example : ∀ s1 s2 s3 s4, P s1 ∧ Transfer s1 s2 ∧ P s2 ∧ Transfer s2 s3 ∧ P s3 ∧ Transfer s3 s4 → P s4  := by
+  simp [P]
+  bv_decide