On Wed, Jan 07, 2004 at 17:35:52 -0500,
Tom Lane <tgl@sss.pgh.pa.us> wrote:
>
> There's still no intelligence about NOT in the theorem prover, but it
> turns out that it's not seeing NOT. By the time the expressions get to
> the point of being compared, NOT (a=b) has been folded to a<>b, and it
> turned out to be fairly straightforward to extend the existing logic to
> reason about such cases. The above example requires a process like
> "a = x implies a <> y if x <> y" (where x and y are constants, so the
> "if" part can be checked). This fits right in with what the code could
> do already, which was cases like "a > x implies a > y if x > y".
> So it'll work more naturally in 7.5.
This implication relies on = being transitive. I was curious about how you
test for that since there doesn't seem to be a direct way to know that.
My guess would be that operators used in an opclass are assumed to be
transitive, since I don't think indexing would work if they weren't.
This same test would also work for other transitive operators with a negator.
For example:
a < x implies y >= a if y >= x
You can do a bit better if you know that exactly one of the relations
=, <, > is true for any ordered pair of operands. But there may be cases
where you don't have that much structure.
