The Coq mailing list

["Aaron Bohannon" <bohannon AT cis.upenn.edu>]

On 10/19/07, Pierre Letouzey 
<Pierre.Letouzey AT pps.jussieu.fr>
 wrote:
> One last comment about Fsets and automation. Since this discussion:
>   http://pauillac.inria.fr/pipermail/coq-club/2007/002949.html
> I plan someday to write a specialize tactic aiming at FSet proofs.
> For instance, doing in Ltac something more clever that eauto + the
> aforementioned hints should not be difficult. Now, writing a _fast_
> and _complete_ tactic solving the class of problems mentionned by
> Aaron Bohannon can be more challenging.

In fact, I have been working on implementing an idea of the form I
proposed earlier.  I realized that by narrowing the scope somewhat, it
would be feasible to write such a tactic in the Ltac language.
However, the narrower scope is still large enough to be extremely
useful.  By the same token the scope is large enough to make it very
difficult to write a comprehensive set of unit tests, so I have been
waiting to see what bugs were found as my friends at Penn tried use it
in their own projects.  I have worked out enough bugs that I think it
might be at a beta-level of quality, so I am attaching the code here
for others to look at -- and perhaps even consider for inclusion in
the standard library at some point in the future.

There are two files: DecidableProp.v, which extends Decidable.v from
the standard library, and FSetDecide.v, a very well-documented file
which implements a tactic [decideFSet] that is a decision procedure
for a certain class of goals involving finite sets.  The precise class
of goals is clearly stated within the comments of the file.  I'd love
to hear any comments anyone has about this.  In particular, I'd like
to know if people find bugs or stumble across reasonable-sized cases
where it runs too slowly to be practical.

-Aaron

Attachment: DecidableProp.v
Description: Binary data

Attachment: FSetDecide.v
Description: Binary data