Can't decide if 15 is a prime power

Stream: mathlib4

[Alastair Irving]

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?

[Thomas Browning]

Can you first rw with docs#isPrimePow_nat_iff_bounded (or one of the other lemmas there)?

[Thomas Browning]

Actually, I guess that's probably what decide is already doing?

[Thomas Browning]

The bounded_log version works up to the mid-two-digits:

example : ¬ IsPrimePow 55 := by
  rw [isPrimePow_nat_iff_bounded_log]
  decide

[Thomas Browning]

Not sure why the minFac version doesn't though

[Alastair Irving]

Yes, rewriting with the bounded_log version works so I'll rewrite with that. Its curious why the minFac doesn't work though.

[Alex Meiburg]

It looks like Nat.minFac is defined with well-founded recursion (and is appropriately irreducible), so decide won't unfold that.

[Bolton Bailey]

Could the decidable instance be rewritten in terms of Nat.nthRoot? I don't think that existed when I was doing these in September.

[Bolton Bailey]

Ideally something like

module

public import Mathlib.Data.Nat.NthRoot.Defs
public import Mathlib.Algebra.IsPrimePow

theorem isPrimePow_nat_iff_bounded_log_nthRoot (n : ℕ) :
    IsPrimePow n
      ↔ ∃ k : ℕ, k ≤ Nat.log 2 n ∧ 0 < k ∧ (Nat.nthRoot k n)^k = n \and (Nat.nthRoot k n).Prime := by sorry

instance {n : ℕ} : Decidable (IsPrimePow n) :=
  decidable_of_iff' _ (isPrimePow_nat_iff_bounded_log_nthRoot n)

example : ¬ IsPrimePow 15 := by
  decide

but it would be leaving the file this way.

[Wojciech Różowski]

The problem described above can be solved using an experimental decide_cbv tactic available in the latest nightly. This tactic mimics call-by-value evaluation, but unlike rfl it can handle functions defined via well-founded recursion. Unlike native_decide it does not rely on the additional axioms.

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

If you're interested here is the thread that describes it and here is the PR on mathlib4-nigthly-testing that tests the provided example.

[Kim Morrison]

Just noting that cbv and decide_cbv are availably in v4.29.0-rc1 (and hence in Mathlib) --- but also noting Wojciech's warning above that their behaviour will change underneath you! They are still experimental.