Consider switching from simpl to cbn
@robbertkrebbers writes in !171 (comment 53223):
I have the feeling we should try to switch to
cbn
once more. It solves at least the issue of over-eager unfolding, and the issue of not folding back.
Last time I tried, I ran into several other blockers, but maybe these are either fixed in Coq, or there are better workarounds than [what] we currently need to get
simpl
to work.
I agree; the only problems I'm aware of with cbn
are that:
- it crashes on 8.11.0 with mutual inductives, but that was fixed immediately, and 8.11.1 and .2 are out; it was due to a general refactoring.
- with ssreflect, you can write
rewrite [pattern]/=
(tosimpl
a subterm matching a pattern) a but notrewrite [pattern]/ltac:(cbn)
(tocbn
the same subterm).
Maybe Set SimplIsCbn
would help with the latter, but it might be too strong (it didn't work for https://github.com/HoTT/HoTT/issues/709, never tried it myself, tho I probably should since I use Autosubst which is cbn
-based). I expect exporting Set SimplIsCbn
is probably best avoided.