The Coq mailing list

[Ralf Jung <jung AT mpi-sws.org>]

Hi,

> Coq 8.5 has a new replacement for simpl, called cbn. The manual says 
> "The cbn tactic is claimed to be a more principled, faster and more 
> predictable replacement for simpl". The cbn tactic can be fine tuned 
> using the Arguments command and with a few options. I made good 
> experiences with cbn. I think it would solve your problem as well.

Indeed, this looks great! In a small test on a sample file, it seems as
if I can prevent it from delta-unfolding even if that would result in a
match being reduced. Great! I'm looking forward to trying this on the
full development, once Coq 8.5 is released :D

> Coq 8.5 comes with a tactic called cbn that is barely a backward
> compatible in place remplacement for simpl (There is even an option
> SimplIsCbn so that any invocation of simpl calls the cbn machinery.
> It is not perfect and therefore not done by default: activating it on
> the standard library requires to modify 50 lines for example.)

I played around with SimplIsCbn, but it seems that ssreflect's "/=" will
still call the old simpl. At least, "move=>/=" does not behave like
"cbn" even with SimplIsCbn set. Is there any way to tell Ssreflect to
also use cbn?

> It use the same syntax as lazy or cbn to allow the control constant
> by constant of which one can be unfolded while doing the « simpl »
> refolding stuff. For example, ''cbn -[unit]'' means (more or less)
> apply simpl but do not unfold the constant unit where ''cbn [mult
> plus]'' means apply simpl but unfold only mult and plus, etc

That sounds *amazing*, very useful for local tuning in the few cases
where general "simpl" control does not work out so well.

Kind regards,
Ralf