chore: remove cbv at from sym => mode and fix the transparency level for projections (#14030)

This PR removes the hypothesis rewriting functionality of `cbv`
(introduced using `cbv at` syntax) in the `Sym` mode. Additionally, this
PR fixes the transparency level when dealing with projections in `cbv`.

Author: wkrozowski

src/Init/Grind/Interactive.lean

@@ -347,15 +347,11 @@ It reduces terms by unfolding definitions using their defining equations and
 applying matcher equations. The unfolding is propositional, so `cbv` also works
 with functions defined via well-founded recursion or partial fixpoints.
 
-`cbv` reduces the goal type (and optionally hypothesis types) using call-by-value
-evaluation. For equation goals (`lhs = rhs`), `cbv` automatically attempts `refl`
-after reduction to close the goal.
+`cbv` reduces the goal target using call-by-value evaluation. For equation goals
+(`lhs = rhs`), `cbv` automatically attempts `refl` after reduction to close the goal.
 
-`cbv` supports the standard `at` location syntax:
-- `cbv` — reduce the goal target
-- `cbv at h` — reduce hypothesis `h`
-- `cbv at h |-` — reduce hypothesis `h` and the goal target
-- `cbv at *` — reduce all non-dependent propositional hypotheses and the goal target
+Unlike the standalone `cbv` tactic, this variant does not support the `at` location
+syntax: in `sym =>` mode it only reduces the goal target.
 
 `cbv` is not a finishing tactic in general: it may leave a new (simpler) goal.
 
@@ -365,6 +361,6 @@ generator.
 
 This is a variant of `cbv` that only works in `sym =>` mode.
 -/
-syntax (name := symCbv) "cbv" (location)? : grind
+syntax (name := symCbv) "cbv" : grind
 end Grind
 end Lean.Parser.Tactic

src/Lean/Elab/Tactic/Grind/Sym.lean

@@ -295,22 +295,11 @@ def elabDSimpVariant (variantName : Name) (args : DSimpArgs) : GrindTacticM (Sym
       goal.mvarId.assign mvarNew
       replaceMainGoal [{ goal with mvarId := mvarNew.mvarId! }]
 
-/-- Resolve the hypothesis identifiers of a `cbv at` location to `FVarId`s. -/
-private def resolveLocFVarIds (hyps : Array Syntax) : GrindTacticM (Array FVarId) := do
-  let lctx ← getLCtx
-  hyps.mapM fun hyp => do
-    let some decl := lctx.findFromUserName? hyp.getId
-      | throwError "unknown hypothesis `{hyp}`"
-    return decl.fvarId
-
-@[builtin_grind_tactic Parser.Tactic.Grind.symCbv] def evalSymCbv : GrindTactic := fun stx => withMainContext do
+@[builtin_grind_tactic Parser.Tactic.Grind.symCbv] def evalSymCbv : GrindTactic := fun _ => withMainContext do
   ensureSym
   let goal ← getMainGoal
-  let (fvarIds, simplifyTarget) ← match expandOptLocation stx[1] with
-    | .targets hyps simplifyTarget => pure (← resolveLocFVarIds hyps, simplifyTarget)
-    | .wildcard => pure (← goal.mvarId.getNondepPropHyps, true)
   let result ← liftGrindM <|
-    Lean.Meta.Tactic.Cbv.cbvGoalCore goal.mvarId simplifyTarget fvarIds
+    Lean.Meta.Tactic.Cbv.cbvGoalCore goal.mvarId
   match result with
   | none => replaceMainGoal []
   | some mvarId => replaceMainGoal [{ goal with mvarId }]

src/Lean/Meta/Tactic/Cbv/Main.lean

@@ -205,7 +205,7 @@ def handleProj : Simproc := fun e => do
   let res ← simp struct
   match res with
   | .rfl _ cd =>
-    let some reduced ← withCbvOpaqueGuard <| reduceProj? <| .proj typeName idx struct | do
+    let some reduced ← withCbvOpaqueGuard <| withDefault <| reduceProj? <| .proj typeName idx struct | do
       return .rfl (done := true) cd
 
     let reduced ← Sym.share reduced
@@ -223,7 +223,7 @@ def handleProj : Simproc := fun e => do
       return .step (← Lean.Expr.updateProjS! e e') newProof cd
     else
       -- If the type of the projection function is dependent, we first try to reduce the projection
-      let reduced ← withCbvOpaqueGuard <| reduceProj? e
+      let reduced ← withCbvOpaqueGuard <| withDefault <| reduceProj? e
       match reduced with
       | .some reduced =>
         let reduced ← Sym.share reduced

tests/elab/sym_cbv.lean

@@ -9,17 +9,22 @@ example (h : a = 8) : Nat.succ 7 = a := by
     cbv
     exact h.symm
 
-example (h : Nat.succ 7 = a) : 8 = a := by
-  sym =>
-    cbv at h
-    exact h
-
-example (h : Nat.succ 7 = a) : Nat.succ 7 = a := by
-  sym =>
-    cbv at h ⊢
-    exact h
+example :
+  have v :=
+    BitVec.ofNat 64 ((BitVec.ofNat (64 - 0) ((BitVec.setWidth 64 (Int64.toBitVec 2)).toNat >>> 0)).toNat >>> 0) - 1;
+  have v_1 := BitVec.ofNat 64 ((BitVec.ofNat (64 - 0) (v.toNat >>> 0)).toNat >>> 0) - 1;
+  v ≠ v_1
+:= by
+  cbv
+  intro hyp
+  trivial
 
-example (h : Nat.succ 7 = a) : Nat.succ 7 = a := by
+example :
+  have v :=
+    BitVec.ofNat 64 ((BitVec.ofNat (64 - 0) ((BitVec.setWidth 64 (Int64.toBitVec 2)).toNat >>> 0)).toNat >>> 0) - 1;
+  have v_1 := BitVec.ofNat 64 ((BitVec.ofNat (64 - 0) (v.toNat >>> 0)).toNat >>> 0) - 1;
+  v ≠ v_1
+:= by
   sym =>
-    cbv at *
-    exact h
+    cbv
+    intro hyp