by rfl won't complete simple proofs in v4.19.0-rc2 anymore

Stream: lean4

[Mario Weitzer]

import Mathlib.Data.Nat.Factors

def l10 := [2, 5]

#eval Nat.primeFactorsList 10
--[2, 5]

lemma hl10 : l10 = Nat.primeFactorsList 10 := by
  rfl

This doesn't work in v4.19.0-rc2 anymore but it used to work in v4.12.0-rc1. Also

#reduce Nat.primeFactorsList 10

won't reduce to [2, 5] anymore. I assume the two are related? Maybe a reduced default number of iterations in reduce? Is there a way to increase it by setting some option? Or is there another simple way to complete the proof of the lemma hl10?

[Eric Wieser]

#15420 is the eventual answer here

[Eric Wieser]

Or redefining primeFactorsList to not use well-founded recursion

[Mario Weitzer]

So there is no easy way anymore to complete the proof or #reduce the term with primeFactorsList defined the way it is?

[Robin Arnez]

The culprit here is https://github.com/leanprover/lean4/commit/41a2e9af19b88b29070542bcd71ace95cd5d64ac but this now "intended" behavior. You usually don't want to unfold functions defined by well-founded recursion. The way you could make it work again is to make Nat.primeFactorsList @[semireducible] at its definition. But the way it is, no, reducing is impossible.

[Mario Weitzer]

I see. And how would one complete the (supposedly easy) proof of the lemma then?

[Robin Arnez]

e.g. simp [Nat.primeFactorsList, Nat.minFac, Nat.minFacAux, l10] although that isn't very pretty

[Yury G. Kudryashov]

Another option is to locally unseal some definitions.

[Robin Arnez]

No, see the commit above:

This changes renders unseal ineffective for such definitions. To avoid the opaque proof, annotate the function definition with @[semireducible].

[Yury G. Kudryashov]

Ah, I've missed this change. Sorry.

[Robin Arnez]

A bit of prettier way is norm_num [Nat.primeFactorsList, l10] perhaps though

[Robin Arnez]

Although maybe lean4#7965 will make it possible to have it be rfl again