The Coq mailing list

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

On Mon, Oct 22, 2007 at 10:03:34PM -0400, Aaron Bohannon wrote:
> 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


Hi Aaron, 

I've just tried your tactic and it looks great. For instance, all 
lemmas in section BasicProperties of FSetProperties are solved 
automatically by it, apart from 

  Lemma double_inclusion : s1[=]s2 <-> s1[<=]s2 /\ s2[<=]s1.

which is indeed not in the scope you describe in FSetDecide (logical 
combinators involving [=] and [<=], not just In and E.eq). And anyway
a simple "intuition decideFSet" does the job here. The only other 
manual help given to decideFSet concerns lemmas involving the
predicate Add: since decideFSet knows nothing about Add, I rewrite
first every (Add x s s') into s'[=]add x s. 

By the way, I've encountered one situation that has puzzled me: 

Lemma Solvable : forall a x s, 
 E.eq x a \/ In a s <-> In a (add x s).

The previous lemma is solved ok by decideFSet, but if there is an 
artificial s' in the middle of the iff, it stops working: 

Lemma Not_Solvable : forall a x s s', 
 (In a s' <-> E.eq x a \/ In a s) -> 
 (In a s' <-> In a (add x s)).

I haven't investigated further, I'll have a closer look later. 

Now comes the key question: have you anything against an inclusion of
FSetDecide.v in the Standard Library of Coq ? Of course, you would
retain proper credit for this file (and all our thanks). Such files of
Coq are then released under the LGPL 2.1 license. In a first time, the
only modifications I would do is ... changing the name of the tactic,
since the rest of the system uses lowercase tactic names. What about
fsetdec ? I may also try to allow using FSetDecide on both FSets and 
FSetWeak (via some subtyping, work in progress). 

Best regards, 
Pierre Letouzey