The Coq mailing list

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

On Tue, Jul 03, 2007 at 01:45:03PM -0400, Aaron Bohannon wrote:
> Specialized tactics should be able to make working with finite sets
> much, much easier.  In particular, there should be a certain class of
> goals that could be immediately solved by a specialized tactic if
> their truth is justified by your hypotheses (or, to be more precise,
> the subset of your hypotheses not involving first-order quantifiers).
> 
> I am tempted to write my own such tactic for the FSets library, but in
> order to avoid duplicating effort, I should first ask:  Has anyone
> else already done this?  Which tactics defined in FSets.OrderedType
> and the other FSet libraries are intended for use by clients of the
> library?  Do they have any documentation or specification other than
> the text of the "Ltac" defintion?  (Deducing the intended behavior and
> scope of a tactic from the code of its definition is not an easy
> task.)
> 
> -Aaron
> 

Hi

Indeed, FSets/FMap lacks a proper documentation. Now that I'm more or
less satisfied with the content of this library, documenting it is
clearly TheNextThingToDo (TM). I hope to tackle that task during this
summer, but I'm notoriously bad at making forecasts.

Concerning automated tactics for FSets, there are currently two of
them: 

In functor FSetFacts.Facts, the tactic "set_iff" allows to transform an
arbitrary complex expression like (In x (union s (inter s' s''))) into
the corresponding propositional expression, say (In x s \/ (In x s' /\
In x s')). The idea is then to take advantage of intuition/firstorder
on this kind of expressions. Goals of the form Equal or Subset can also
been dealt with, since an unfold on them leads to (forall x, In x ...).
For instance, you can have a look at all the results in
FSetProperties.Properties that are proved using something like
(set_iff; intuition). At the same time, this set_iff could be much
improved. Especially for the moment it can only operate on the goal,
not on the hyps. 

In functor OrderedType.OrderedTypeFacts, the tactic "order" has a
different purpose: during the development of FSet implementations and
property functors, it was quite painful to manipulate by hand stuff
about (in)equalities about elements of the sets, so I wrote this
little "order" tactic. It looks for every hyps of the form
   E.eq a b
   ~E.eq a b
   E.lt a b
   ~E.lt a b 
The goal could be of the same form, or False. It then tries to combine
all these facts by transitivity and symmetry in order to either obtain
the goal or a contradiction. The tactic has been coded as a quick and 
dirty hack to ease a development, in particular i've no idea whether 
it is complete or not on its domain of activity (Coq svn contains now 
a slightly improved version compared with official 8.1). 

I now recall that I also have a few helpers about decidability of the
orders used in FSets, but I would barely call that "automated
tactics". 

Concerning the usability of set_iff and order by the user, well, these
tactics were first made to help me, but if they can help you as well,
(especially "set_iff" I would guess), sure, go ahead, Concerning
"order", if you're working with some concrete base type for elements
(let's say Z), then you can consider unfolding E.eq and E.lt down to
the usual = and <, and then use standard coq tools like omega. On the
contrary, if you're in an abstract context (e.g. a functor on any
OrderedType), then "order" might help.

By the way, what kind of goals would you like to see automatically
solved ? Of course, if you design better automated tactics, I would
gladly include them in FSet/FMap.

Best regards, 

Pierre Letouzey