A Universe of Sorts

§ Quantifier Elimination for Presburger Arithmetic

We start with (N, +).
However, see that in the first order theory, we can talk about e.g. x > y as ∃z, x + z + 1 = y.
so, we need to add this > symbol into the theory when we try to do QE.
Furthermore, we also add in 0, 1.
Finally, we add in the divisibility predicate, where Dn(x) is true iff n divides x.

Answer: yes we do!
Key idea: the other predicates, of equality and disequality, give, for any variable x, either a finite set of solutions or a cofinite set of solutions (complement is fiinite).
However, divisibility by 2 is neither finite nor cofinite! Thus, it is an extra predicate we need to add into the theory to make it work :)

In this theory, we can always convert negations of predicates into a disjunct of purely positive predicates:
x != y becomes x < y \/ x > y.
!D3(x) becomes D3(x + 1) \/ D3(x + 2), which is pretty interesting: we are writing x != 0 (mod 3) as (x = 1 (mod 3)) \/ (x = 2 (mod 3)).
Finally, we can write !(x < y) as x = y \/ x > y.

∃ x: 2x + 3y < 4z /\
  x + z < 2y + 3 /\
  2z + 4 < 5x + y /\
  D2 (3x + 2y + 1) /\
  D3 (5x + z)

From this, we want to extract out a finite list of candidates for x.
So, we create a disjunction where we convert the ∃ x into (x = v1 /\ P) \/ (x = v2 /\ P) ... \/ (x = vN /\ P).
First, we normalize the inequalities to make the coefficient of x to be 30.
For f < g, we can simply rescale as kf < kg.
For divisibility, we can write n | x as kn | kx, or in our notation, Dn(x) becomes Dkn(kx).

∃ x,
30x + 45y < 60z
30x + 30z < 60y + 90z
12z + 24 < 30x + 6y
D20 (30x + 20y + 10)
D18 (30x + 6z)

Next, we want to say that there exists an x that is divisible by 30, instead of having 30x.
This now becomes:

∃ x,
x + 45y < 60z
x + 30z < 60y + 90z
12z + 24 < x + 6y
D20 (x + 20y + 10)
D18 (x + 6z)
D30(x) # NEW

We now get lower and upper bounds on x, and we get divisbility constraints.
The inequality 12z + 24 < x + 6y gives a lower bound: 12z + 24 - 6y < x.
the other two inequalities give an upper bound: x < 60z - 45y and x < 60y + 90z - 30z.
We can't directly enumerate this list, since the list's length is symbolic (depends on values of y and z).
Finally, for the divisibility, we want numbers with these particular remainders.
The chinese remainder theorem will tell us that such a number will occur in a consecutive set of lcm(20, 18, 30) numbers!
Finally, what do we do with the minus sign?
We can always change the minus to a plus, in an inequality: -y < 0 if y > 0.
For divisibility, to check D18(12x + 24 -6y + 7 + 6z), we write it as (18 - 6) y, i.e. 12y.

If we have multiple lower bounds, then we make the search from all lower bounds.
If we no lower bounds, we start from zero.
If we have no divisibility constraint, then we can do fourier motzkin? [Question: Why can't I think of it as modulo by zero? Aha, I can, but the LCM will be infinity ]