Experimental `cbv`and `cbv_decide` tactic in nightly

Stream: lean4

[Wojciech Różowski]

The recent nightly (2026-02-16) includes experimental tactics that perform call-by-value evaluation. Unlike rfl, these tactics can handle definitions that use well-founded recursion. Unlike native_decide these tactics do not require additional axioms, or need to trust the compiler. For example:

def nofib : Nat → Nat
| 0 => 0
| 1 => 1
| n + 2 => nofib (n + 1) + nofib n

example : nofib 10 = 55 := rfl -- works
example : nofib 10 = 55 := by cbv -- works

example : nofib 200 % 3 = 0 := rfl -- fails
example : nofib 200 % 3 = 0 := by cbv -- works

The cbv tactic is non-terminal: it attempts to reduce both sides of an equation and either closes the goal if they are equal or produces a simplified goal. It can also be used in conv mode.

In addition, I am working on a decide_cbv tactic for Decidable propositions. It evaluates Decidable.decide using cbv, which avoids the reduction limitations that sometimes cause decide to fail.

A nice motivating example comes from a recent discussion about checking whether a number is a prime power.
Alastair Irving said:

import Mathlib.Algebra.IsPrimePow

example : ¬ IsPrimePow 15 := by
  decide

Fails on both 4.28.0-rc1 and a more recent checkout of main with with

Tactic `decide` failed for proposition
  ¬IsPrimePow 15
because its `Decidable` instance
  instDecidableNot
did not reduce to `isTrue` or `isFalse`.

It succeeds for smaller values and for larger even values but seems to fail on odd products of primes.

Is this a bug and/or is there a better way of proving this?

This can be handled in a following way:

import Mathlib.Algebra.IsPrimePow

example : IsPrimePow 10093 := by decide_cbv

example : IsPrimePow 100999 := by decide_cbv

example : ¬ IsPrimePow 15 := by decide_cbv

example : ¬ IsPrimePow 111111111111111155 := by decide_cbv

With decide_cbv, this example does work.
A draft PR demonstrating this on the mathlib4-nightly-testing fork is available.

All of these tactics are experimental and not yet intended for production use. I'm sharing them as an invitation to try them out - if you run into any issues or rough edges, I'd be happy to hear about them.