coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- Re: [Coq-Club] "simpl" control, Ralf Jung, 06/04/2015
- Re: [Coq-Club] "simpl" control, Enrico Tassi, 06/05/2015
- Re: [Coq-Club] "simpl" control, Ralf Jung, 06/05/2015
- Re: [Coq-Club] "simpl" control, Enrico Tassi, 06/05/2015
Archive powered by MHonArc 2.6.18.