Simple annotation + primitive for columns with 0/1 increments

[OlivierBBB]

Main point

We often find ourselves writing constraints of the form

If C[i + 1] ≠     C[i] Then A
If C[i + 1] ≠ 1 + C[i] Then B

for columns C that have 0/1 increments. We do this in stead of e.g. writing the more natural

If C[i + 1] ≠ C[i] Then A
If C[i + 1] = C[i] Then B

in order to avoid the equality check. If columns C could be tagged as having 0/1 increments corset could handle that for us and make the code more readable.

Proposal

Add annotation for columns

(defcolumn
    (A  :zero-one-increments@prove))

which adds the following constraint

(is-binary   (-  (next  COL)  COL))

and add a simple primitives to the stdlib called (hopefully with better names)

(if-increments-next-else   COL A B)
(if-incremented-now-else   COL A B)     ;; or if-was-incremented-else

which require that COL have the :zero-one-increments property and unfolds to, respectively

(if-not-zero   (force-bool  (-  (next  COL)  COL)  A  B)
(if-not-zero   (force-bool  (-  COL  (prev  COL))  A  B)