Re: Optimization rules for semi and anti joins

Gianni Ciolli <gianni.ciolli@2ndquadrant.it> writes:
> On Tue, Feb 10, 2009 at 09:41:46PM +0100, Dimitri Fontaine wrote:
>> I don't know how easy it would be to do, but maybe the Coq formal proof 
>> management system could help us here:
>> http://coq.inria.fr/
>> 
>> The harder part in using coq might well be to specify the problem the  
>> way you just did, so...

> formal theorem proving and mechanized mathematics happen to be one of
> my research topics in the last few years; so I think that my
> experience could be helpful with such problems.

Unless you've got a prover that already understands the concepts of
outer joins etc, I'd think that teaching it about that would require
enough work and introduce enough possibilities for human error so as
to make the exercise pretty much moot.  The identities I put up don't
look that complicated to me...
        regards, tom lane