Equivalent Inequalities¶

There’s a StackOverflow question that asks “How to check the overlap of date ranges in MySQL?”

The top two answers each offer inequalities. The top answer states that it is equivalent to the second answer but a comment on the second answer states that they are different. I trusted both answers but was unable to prove equivalence.

The Z3 Theorem Solver can prove equivalence so I thought I’d give it a try.

>>> import z3

Define Integer variables.

>>> new_start = z3.Int('new_start')
>>> new_end = z3.Int('new_end')
>>> existing_start = z3.Int('existing_start')
>>> existing_end = z3.Int('existing_end')

Answer 1 is the AND of two inequalities.

>>> ans_1 = z3.And(
...     new_start <= existing_end,
...     new_end >= existing_start,
... )

Answer 2 is the OR of three BETWEEN operator inequalities.

>>> def between(value, start, end):
...     """Model SQL BETWEEN operator.
...
...     The BETWEEN operator is inclusive of the
...     start and end.
...
...     Written in Python as (start <= value <= end).
...
...     """
...     return z3.And(start <= value, value <= end)
>>> ans_2 = z3.Or(
...     between(existing_start, new_start, new_end),
...     between(existing_end, new_start, new_end),
...     between(new_start, existing_start, existing_end),
... )

Initialize a Z3 solver.

>>> solver = z3.Solver()

Add constraint that requires the existing start be less than or equal to the existing end.

>>> solver.add(existing_start <= existing_end)

Add constraint that requires the new start be less than or equal to the new end.

>>> solver.add(new_start <= new_end)

Add constraint that the XOR of both answers be true. XOR will require answers 1 and 2 differ in order to be true. Akin to asking for a counter-example to the theory of equivalence.

>>> solver.add(z3.Xor(ans_1, ans_2) == True)

>>> solver
[existing_start <= existing_end,
 new_start <= new_end,
 Xor(And(new_start <= existing_end,
         new_end >= existing_start),
     Or(And(new_start <= existing_start,
            existing_start <= new_end),
        And(new_start <= existing_end,
            existing_end <= new_end),
        And(existing_start <= new_start,
            new_start <= existing_end))) ==
 True]

Ask the solver to check whether the inequality is satisfiable.

>>> solver.check()
unsat

The inequality is unsatisfiable which means answer 1 and answer 2 will always yield the same result.