From 7459304e98cedfa25f7e1e1774a7bbe84ae65c00 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Thu, 6 Nov 2025 10:22:36 +0100
Subject: [PATCH] refactor: bv_decide: remove `verifyEnum` et. al (#11068)

This PR removes the `verifyEnum` functions from the bv_decide frontend.
These functions looked at the implementation of matchers to see if they
really do the matching that they claim to do. This breaks that
abstraction barrier, and should not be necessary, as only functions with
a `MatcherInfo` env entry are considered here, which should all play
nicely.
---
 .../Frontend/Normalize/TypeAnalysis.lean      | 63 +------------------
 1 file changed, 2 insertions(+), 61 deletions(-)

diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/TypeAnalysis.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/TypeAnalysis.lean
index 92b8403e68..d411d57324 100644
--- a/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/TypeAnalysis.lean
+++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/TypeAnalysis.lean
@@ -71,7 +71,7 @@ def isSupportedMatch (declName : Name) : MetaM (Option MatchKind) := do
       Where we have as many arms as constructors but the last arm is a default.
       -/
 
-      if let some kind ← trySimpleEnum defnInfo inductiveInfo xs numCtors motive then
+      if let some kind ← trySimpleEnum inductiveInfo xs numCtors motive then
         return kind
 
     if xs.size > 2 then
@@ -97,12 +97,11 @@ def isSupportedMatch (declName : Name) : MetaM (Option MatchKind) := do
 
       if !defaultOk then return none
 
-      if !(← verifyEnumWithDefault defnInfo inductiveInfo handledCtors) then return none
       return some <| .enumWithDefault inductiveInfo handledCtors
     else
       return none
 where
-  trySimpleEnum (defnInfo : DefinitionVal) (inductiveInfo : InductiveVal) (xs : Array Expr)
+  trySimpleEnum (inductiveInfo : InductiveVal) (xs : Array Expr)
       (numCtors : Nat) (motive : Expr) : MetaM (Option MatchKind) := do
     -- Check that all parameters are `h_n EnumInductive.ctor`
     let mut handledCtors := Array.mkEmpty numCtors
@@ -113,66 +112,8 @@ where
       let .ctorInfo ctorInfo ← getConstInfo c | return none
       handledCtors := handledCtors.push ctorInfo
 
-    if !(← verifySimpleEnum defnInfo inductiveInfo handledCtors) then return none
-
     return some <| .simpleEnum inductiveInfo handledCtors
 
-  verifySimpleCasesOnApp (inductiveInfo : InductiveVal) (fn : Expr) (args : Array Expr)
-      (params : Array Expr) : MetaM Bool := do
-    -- Body is an application of `EnumInductive.casesOn`
-    if !fn.isConstOf (mkCasesOnName inductiveInfo.name) then return false
-    if args.size != inductiveInfo.numCtors + 2 then return false
-    -- first argument is `(fun x => motive x)`
-    let firstArgOk ← lambdaTelescope args[0]! fun args body => do
-      if args.size != 1 then return false
-      let arg := args[0]!
-      let .app fn arg' := body | return false
-      return fn == params[0]! && arg == arg'
-
-    if !firstArgOk then return false
-
-    -- second argument is discr
-    return args[1]! == params[1]!
-
-  verifySimpleEnum (defnInfo : DefinitionVal) (inductiveInfo : InductiveVal)
-      (ctors : Array ConstructorVal) : MetaM Bool := do
-    lambdaTelescope defnInfo.value fun params body =>
-      body.withApp fun fn args => do
-        if !(← verifySimpleCasesOnApp inductiveInfo fn args params) then return false
-
-        -- remaining arguments are of the form `(h_n Unit.unit)`
-        for i in *...inductiveInfo.numCtors do
-          let .app fn (.const ``Unit.unit []) := args[i + 2]! | return false
-          let some (_, .app _ (.const relevantCtor ..)) := (← inferType fn).arrow? | unreachable!
-          let some ctorIdx := ctors.findIdx? (·.name == relevantCtor) | unreachable!
-          if fn != params[ctorIdx + 2]! then return false
-
-        return true
-
-  verifyEnumWithDefault (defnInfo : DefinitionVal) (inductiveInfo : InductiveVal)
-      (ctors : Array ConstructorVal) : MetaM Bool := do
-    lambdaTelescope defnInfo.value fun params body =>
-      body.withApp fun fn args => do
-        if !(← verifySimpleCasesOnApp inductiveInfo fn args params) then return false
-
-        /-
-        Remaining arguments are of the form:
-        - `(h_n Unit.unit)` if the constructor is handled explicitly
-        - `(h_n InductiveEnum.ctor)` if the constructor is handled as part of the default case
-        -/
-        for i in *...inductiveInfo.numCtors do
-          let .app fn (.const argName ..) := args[i + 2]! | return false
-          if argName == ``Unit.unit then
-            let some (_, .app _ (.const relevantCtor ..)) := (← inferType fn).arrow? | unreachable!
-            let some ctorIdx := ctors.findIdx? (·.name == relevantCtor) | unreachable!
-            if fn != params[ctorIdx + 2]! then return false
-          else
-            let .ctorInfo ctorInfo ← getConstInfo argName | return false
-            if ctorInfo.cidx != i then return false
-            if fn != params[params.size - 1]! then return false
-
-        return true
-
 def builtinTypes : Array Name :=
   #[``BitVec, ``Bool,
     ``UInt8, ``UInt16, ``UInt32, ``UInt64, ``USize,