The Coq mailing list

[Pierre Letouzey <Pierre.Letouzey AT pps.jussieu.fr>]

On Fri, Jun 06, 2008 at 07:21:53PM -0400, Aaron Bohannon wrote:
> The first code snippet below is the smallest complete example I could
> find of the problematic situation.  (The "rewrite" tactic in the lemma
> foo2 fails.)  I am using Coq version 8.1pl3.  We are trying to develop
> a library on top of the FSets library that would hopefully be
> compatible with Coq 8.1pl3.  But if that is not possible, I would at
> least really hope there is a fix for this scenario in Coq 8.2.
> 

Ok, now I've a blatant proof that I'm _really_ tired these days and
that my brain is far from working at full speed. From our previous
mail exchanges, I concluded erroneously that you were using a recent
svn version of Coq (since you were interested in recent FSets
evolutions), and I was thus wondering what could go wrong with the
new setoid rewrite implementation of M. Sozeau. 

In fact, the situation is the exact opposite, your snippets of code
are working out-of-the-box with current coq svn version, while the old
version of setoid rewrite in 8.1 is indeed faulty. Moreover, I even
recall now having encountered this very same bug a long time ago, and
submitted a bug report:

https://logical.futurs.inria.fr/coq-bugs/show_bug.cgi?id=1738

By the way, another workaround is mentionned in this report: you can
simply use "Defined" instead of "Qed" while building the Setoid_Theory.

This bug with the old implementation of rewrite is very unlikely to be
solved in the 8.1 branch: this implementation was a nightmare to
debug, that's precisely one of the main reasons for a new
implementation.

More generally, I can understand of course your wish to build
8.1-compatible developments. But I cannot refrain myself either to
advocate the use of the current coq svn tree. The fact that is hasn't
been officially declared "stable" doesn't mean that it's less reliable
that the year-and-a-half-old 8.1 family (the discussion here shows at
least an example of the opposite), it only means that the release
cycle of coq is very far from ideal. Backporting stuff like the last
evolutions of FSets to 8.1 is meant to be somewhere between painful
and impossible, due to the new features of the soon-to-be-called 8.2
in terms of modules, rewrite, and other new cool features.

Best regards, 
Pierre Letouzey