The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

Hi,

> - Some well thought design decisions were already taken and
> implemented in ssreflect's tactics, which leaves little incentive to
> re-implement them.

Two years ago, I made a private patch providing more conversion in
rewrite (using a strategy closed to the one experimented by Georges
Gonthier in the context of his own developments, namely preventing the
head constant to be unfolded). This induced a certain number of
incompatibilities, just for the standard library of Coq (*), and, for that
purpose, I followed the approach we had taken for "apply" when
(almost) full conversion were introduced for it, namely renaming the
old version "simple apply". In the current case, this would mean
providing a "simple rewrite" tactic for the compatibility. [I could
not talk with Matthieu Sozeau who may have found a better heuristic to
deal with the compatibility.]

So, I seize this opportunity to ask: what would be the best way to
achieve compatibility? To have the same syntax, i.e. "rewrite", and
have, say, a "simple rewrite" for the version which does not consider
conversion? To have an option, some kind of "Set Rewrite Conversion"
flag to give to the syntax "rewrite" the old behavior? [These are the
two basic tricks we use for compatibility.]

Or, maybe, more works could be done in analyzing the reasons for
incompatibilies of the rewrite with full conversion, to see if a more
optimal one can be implemented. For instance, we could simply try to
address the question not of full conversion but of full conversion
over implicit arguments, if this is what would stem out of the general
wish of users.

Or, maybe, other more long-term alternatives should be considered, if
ever some developers or even external contributors had time and energy
to work on it, like building automatic script translators, which would
allow to improve tactics without having users to care about the
migration...

Note: setoid rewrite supports more conversion than rewrite, so, even
if this is a bit a detour, this provides an alternative for rewriting
up to conversion.

> - The usual argument: the academic system does not reward such work
> as it is very hard to publish. So spending time on it, at least for
> young researchers, is very risky due to peer pressure to publish,
> and the low number of positions.

Giving priority to his/her own conviction about what is meaningful is
a possible choice in life!

> Omega's example is of a very different nature, because an easy fix
> is probably indeed doable. In the long term though, it would also
> deserve an abstract interface à la ring instead of hard-coding the
> type of integers.

As noticed by Thomas, replacing (e.g.) some "eq_constr" by some
"is_conv" in the source of omega would be pretty easy, and probably
inoffensive in terms of efficiency or "intuitive user expectations" in
most situations. If someone comes with a patch, we can probably
integrate it.

Hugo

(*) There were 62 incompatibilities in the standard library, a typical
example being in rewriting "x * (y * z)" which started to match
expressions of the form "t * power x 2". I have no idea how common
this would occur in arbitrary developments.