The Coq mailing list

[Adam Chlipala <(e6fa90e88c%hidden_head%e6fa90e88c)adamc(e6fa90e88c%hidden_at%e6fa90e88c)hcoop.net(e6fa90e88c%hidden_end%e6fa90e88c)>]

Christian Doczkal wrote:
> I'm planning some development with uses sets in various places and my
> (preliminary) experience is that the Sets libraries that ship with Coq
> are somewhat cumbersome to work with. 
>
> Has anyone used this for some (larger) development? I'm not overly
> worried about having to assume classical logic and various
> extensionality axioms. I'm more interested in increased automation for
> the set reasoning part.
>   

I don't know if anyone has implemented one for Coq yet, but there are 
some very effective automated decision procedures for set expressions.  
It's pretty straightforward to reduce most relations between sets (e.g., 
subset) into statements about membership of abstract elements in sets, 
and then, applying the definitions of set operators, you quickly arrive 
at formulas that standard SAT and SMT solvers can discharge quickly.