New simp feature

Stream: lean4

[Gabriel Ebner]

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.

Simp now tries to simplify every closed subterm p : Prop by synthesizing an instance Decidable p and reducing the decidable instance. There seems to be some timeout built in because it only works up to some small size, but grep Heartbeat doesn't turn up anything relevant.

[Floris van Doorn]

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

[Gabriel Ebner]

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]

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]

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]

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.