Zulip Chat Archive

Stream: lean4

Topic: New simp feature


Gabriel Ebner (Nov 19 2021 at 13:50):

I've just stumbled upon a new simp feature:

example : 42 < 10^100 := by simp

Interestingly, 42 < 10^1000 is no longer provable by simp.

Floris van Doorn (Nov 23 2021 at 14:16):

I hope this is something we can disable with a simp configuration option? It looks useful for many small things though.

Gabriel Ebner (Nov 23 2021 at 14:29):

It can be disabled with decide := ff. I agree, this feature seems useful mostly for small demos (e.g. being able to simplify 10 < 42 out of the box) but I'm afraid it will cause real performance issues. For example, when it sees isTaut (pigeonholePrinciple 7 6) or unfolds noncomputable functions.

Gabriel Ebner (Nov 23 2021 at 14:30):

On the other hand it won't do anything about x < 10 * 42 which should be simplified to x < 420 (the often requested integration of normNum into simp).

Leonardo de Moura (Nov 23 2021 at 16:09):

Interestingly, 42 < 10^1000 is no longer provable by simp.

We have a checkMaxHeartbeats and withIncRecDepth at whnfImp.
It fails because the maximum recursion depth has been reached.

We will eventually have better support for arithmetic that simplifies this kind of proposition without relying on whnf.

I'm afraid it will cause real performance issues. For example, when it sees isTaut (pigeonholePrinciple 7 6) or unfolds noncomputable functions.

If there are serious performance problems in practice, we can set the default to decide := false.
Some random thoughts:

  • I think the feature is useful and it is handy because it works for any decidable proposition.
  • It is not clear to me how often we will hit examples such as isTaut (pigeonholePrinciple 7 6). I am assuming new users will not, and advanced users may set decide := false. Not sure.
  • Regarding non-computable functions, we can block them from being unfolded when we execute whnf at decide.
  • We can also dramatically reduce the maximum number of heartbeats for this whnf, and produce a nice trace message when it is reached.
  • We can also report whether a lot of time is spent in these whnf calls, and suggest decide := false to users.

Gabriel Ebner (Nov 23 2021 at 19:01):

It fails because the maximum recursion depth has been reached.

Ah that's what's happening! I blindly assumed that we had special support for Nat.pow (like we have for +/-/*///%/...).

We will eventually have better support for arithmetic that simplifies this kind of proposition without relying on whnf.

This is a good plan. Users are often asking for this feature; in mathlib we have a norm_num tactic which essentially does simp; evaluate_arithmetic_expressions and it's used heavily.


Last updated: Dec 20 2023 at 11:08 UTC