The Coq mailing list

[Francois-Rene Rideau <fare AT idealx.com>]

> Has anyone implemented a workable encoding of finite (sub)sets in Coq?
What about list-coded sets, with suitable primitives to add and/or
remove elements? We (at idealx) have just used that during a formal proof
we were developping. We have lots of lemmas about lists being (ab)used
in lots of weird ways; the collection is quite ugly, and would require
quite some cleaning up, but might prove useful as additions to the standard
library, unless some tactic we haven't heard of trivializes all these lemmas.

Basically, we hand-proved lots of lemmas involving pointing to a specific
element within a list, removing it, splitting a list in two from one end
or the other, etc. We also have developped a simple associative list
data structure (that could be used as a way to encode finite set, when
the domain Set is the unit Set).

> So, if any of you has, or knows about, a suitable implementation: please 
> SHOOT...!
What I have is certainly not a "suitable implementation". Lots of lemmas
thrown around as we needed them (sometimes, we only discovered the elegant
way long after we had begun proving things one way; since the lemmas are
written in a purely utilitarian perspective, we didn't stop to rewrite them).

This leads me to a more general question:
if I have a bunch of petty theorems and lemmas about lists and suches,
more than half of them quite inelegant, what am I supposed to do with them?
Add them to the standard library? How? (Submit them as is to someone? whom?
write a patch against existing files?)
Or is the Right Thing(tm) to write some decision tactic and despise
stupid lemma-proving slaves (as we've been)?
What if we have lots of slightly different versions of the "same" theorem?

Yours freely,

[ François-René ÐVB Rideau | Reflection&Cybernethics | http://fare.tunes.org ;]
[  TUNES project for a Free Reflective Computing System  | http://tunes.org  ;]
"I think sex is better than logic, but I can't prove it." -- Monty Python