devide vs #eval

Stream: new members

[Justus Springer]

I would have guessed that if #eval can evaluate a proposition to true, then decide should be able to prove it. This does not seem to be the case however, here's a MWE:

import Mathlib.Data.Nat.Factors

#eval Nat.primeFactorsList 60 -- [2, 2, 3, 5]
#eval Nat.primeFactorsList 60 = [2, 2, 3, 5] -- true
example : Nat.primeFactorsList 60 = [2, 2, 3, 5] := by decide -- error

Here's the error message:

▶ 5:56-5:62: error:
tactic 'decide' failed for proposition
  Nat.primeFactorsList 60 = [2, 2, 3, 5]
since its 'Decidable' instance
  instDecidableEqList (Nat.primeFactorsList 60) [2, 2, 3, 5]
did not reduce to 'isTrue' or 'isFalse'.

After unfolding the instance 'instDecidableEqList', reduction got stuck at the 'Decidable' instance
  (Nat.primeFactorsList 60).hasDecEq [2, 2, 3, 5]

Can someone enlighten me as to what's going on and how to make this work?

[Edward van de Meent]

the issue for this (i think) is that Nat.primeFactorsList is marked irreducible because it is recursive, and as such the decidable instance can't reduce.

[Edward van de Meent]

The reason why #eval does work, is because unlike the decide tactic, eval does reduce definitions marked as irreducible

[Eric Wieser]

Making norm_num solve this is on my todo list

[llllvvuu]

IIUC #eval is similar to native_decide and #reduce is similar to with_unfolding_all decide, so maybe you can bash through many such cases by using these tactics (although native_decide is less safe in terms of soundness). I guess decide +kernel works here too.

[Justus Springer]

Both decide +kernel and with_unfolding_all decide work, thanks!