Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] "simpl" control

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] "simpl" control


Chronological Thread 
  • From: Ralf Jung <jung AT mpi-sws.org>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] "simpl" control
  • Date: Thu, 04 Jun 2015 11:29:27 +0200

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



Archive powered by MHonArc 2.6.18.

Top of Page