Add Arguments bool_decide : simpl never

As discussed on Mattermost, I've encountered a case where simpl on a goal containing bool_decide took 1.5 seconds without making any progress, but was instantaneous after adding Arguments bool_decide : simpl never. .

Actually, for some RefinedC case studies adding Arguments bool_decide : simpl never leads to a significant slowdown: https://coq-speed.mpi-sws.org/d/1QE_dqjiz/coq-compare?orgId=1&var-project=refinedc&var-branch1=master&var-commit1=089ad9e8a3b71c74a0aee8570f690d3c84b9828d&var-config1=build-coq.8.13.2-timing&var-branch2=master&var-commit2=bcf29bb3c8d394f0015499184bc077276c911f49&var-config2=build-coq.8.13.2-timing&var-metric=instructions&var-group=(.*) Not sure what is going on there...

While I investigated this, I noticed that without this MR simpl reduces bool_decide (0 = 0) to True. This could be the cause of this slowdown as without this simplification, RefinedC needs to call more solvers which can be quite slow. The large slowdowns in RefinedC are in files that use a more experimental solver which can be quite a bit slower than the standard solver of RefinedC.

Indeed, should we add a test for that behavior? I rely more often on if bool_decide (0 = 0) then ... else ..., which probably still reduces, but I bet the other one shows up too.

I also wonder if the other change is too breaking (especially short before the next release).

Indeed, if bool_decide (0 = 0) then ... else ... still reduces. But I am also afraid that this change could break some/too much downstream code.

The fact that match x with ... end reduces even if x is simpl never is a Coq bug IMHO. I think there's a bug issue for that, but since plenty of developments rely on it, it's likely never going to be changed. For cbn this behavior is also different IIRC.

I think it actually makes lots of sense that bool_decide (0 = 0) reduces to true, so I am no longer that sure about this MR.

I am fine with closing this MR. I can manually add Arguments bool_decide : simpl never in the developments where I need it.

The fact that match x with ... end reduces even if x is simpl never is a Coq bug IMHO.

The Coq devs call it "the desired spec"...

No strong opinion on this MR.

But I feel like when reducing decision things, we usually want to use vm_compute, not the regular simpl reduction machinery -- we do expect large terms here occasionally, after all. So I am not sure I agree that simpl should reduce bool_decide closed_term.

I am on the fence with the MR.

1. It seems like it causes some backwards compatibility because things no longer reduce. It's not so clear how large is the fall out.
2. It's a bit weird that if bool_decide ... then ... else ... reduces, but bool_decide itself not. I suppose the same happens for many other functions, so that should not necessarily be an argument.

Since @msammler is fine with closing this MR, I propose we do that.

If someone wants to reopen, I propose they figure out the compatibility impact.

closed