Difference between decide and decide!

Stream: new members

[Yicheng Tao]

I found that decide fail to prove the following theorem:

import Mathlib

example : Nat.primeFactors 18 = {2, 3} := by decide -- fail

I am using v4.14.0 of Mathlib. And this version has a tactic named decide!, which the newest version (the version that web editor uses) doesn't have. decide! solves this problem successfully.

So what's the difference? And why decide! is deleted?

[Yicheng Tao]

I found native_decide. Seem to work in the example above. But what's the difference?

[Edward van de Meent]

as i understand it, decide (and i suspect decide! too) uses the kernels reduction powers, while native_decide uses the native reduction powers of the compiler (which you may or may not trust).

[Yicheng Tao]

It seems decide in 4.15.0-rc1 has changed a lot. decide! may be equivalent with deicde +kernel.

[Kyle Miller]

Yes, it's become decide +kernel.

[Kyle Miller]

The idea is that it skips straight to the kernel type checker, which doesn't know anything about concepts like transparency and irreducibility.

[Kyle Miller]

Maybe it's like scrying tea leaves, but the error message to decide suggests that Nat.primeFactorsList could be responsible for the reduction failure. Indeed, it's defined using decreasing_by, meaning it's defined using well-founded recursion, and a few releases ago definitions by well-founded recursion became irreducible. To work around this on a case-by-case basis, at the same time the language provided the unseal command to temporarily make such definitions semireducible (the default).

unseal Nat.primeFactorsList in
example : Nat.primeFactors 18 = {2, 3} := by decide

[Yicheng Tao]

Cool. I remember that prove Irrational (sqrt 2) can also use decide and needs to unseal Nat.sort.iter.