The Coq mailing list

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

On 7/4/07, Pierre Letouzey 
<Pierre.Letouzey AT pps.jussieu.fr>
 wrote:
> By the way, what kind of goals would you like to see automatically
> solved ?

To be very precise, I would like to have a tactic that will solve any
goal of the form

 forall s1 ... sn, forall x1 ... xm, P

where P is an expression over the grammar

P :=
| E.eq X X'
| In X F
| Empty F
| Subset F F'
| Equal F F'
| P /\ P'
| P \/ P'
| P -> P'
| ~ P

F :=
| S
| empty
| singleton X
| add X F
| remove X F
| union F F'
| inter F F'
| diff F F'

X := x1 | ... | xm
S := s1 | ... | sn

Unless I am mistaken, statements of this form can be rather easily be
viewed as formulas in the (classical) monadic predicate calculus with
equality (each set variable corresponds to a predicate symbol), and
the validity of formulas in that logic is decidable.

It is reasonably simple to write an Ltac that solves goals that do not
involve "E.eq", "singleton", "add", or "remove" because the statements
can be systematically translated into a form that "tauto" can solve
(in the manner of "set_iff").  With equality, it is not so easy.  I
suspect that one would pretty much be required to write the tactic in
ML for reasons of efficiency, since it will duplicate all of the
machinery of "tauto".  That might be more of an undertaking than I
have time for.  However, assuming I wanted to do such a thing, I'd be
interested in hearing any warnings or advice that comes to anyone's
mind.

-Aaron