How to formulate the following constraint in OPL (or mathematical program)? (Originally posted here https://stackoverflow.com/q/72687231/10291218)
Suppose I have an integer array A of size n with two specific indices x and y of this array, where say x < y. How would I go about adding the constraint which ensures either an "increasing path" between array[x] and array[y] by increasing the indices (so array[x] < array[x+1] < ... < array[y]), or an increasing path by decreasing the indices (so array[x] < array[x-1] < ... array[0] < array[n-1] < ... < array[y]).
I've tried the following but I get at least two errors:
ctIncreasingX2Y:
  (forall (i in x..y-1) A[i] < A[i+1])
  || (forall (i in x..-(n-y)+1) A[(i+n)%n] < A[(i-1+n)%n]);


*

*The forall keyword doesn't like to be inside of the parantheses, but without the parantheses the || operator seems to get applied inside of the forall environment;

*The second range goes from 0 to -1, and not the wanted x to (basically) y.

Maybe there's other problems as well, I'm pretty new to linear programming, but I'd like to solve these ones first.
After some searching around the web, the first problem seems to be me trying to formulate something inherently not LP-like, so maybe there is simply no fix.
Concerning the second problem, I could fix it by using an increasing range and modifying the constraint accordingly, but I find it astonishing that there seems to be no way to use a descending range, which is typically possible in any coding language.
 A: First, strict inequalities are not allowed in integer linear programs, but since $A$ is integer-valued, we can translate $A_i < A_j$ into $A_i + 1 \le A_j$ and so on. Second, although I am not positive, I do not think OPL supports writing a disjunction of conjunctions in a single constraint. That said, you can reformulate the model to get what you want.
To model your disjunction, we introduce a new binary variable $y,$ where $y=1$ if and only if the relevant sequence of values of $A$ is ascending and $y=0$ if and only if it is descending. To do this, we need an upper bound $M_j$ on $\vert A_{j+1} - A_j \vert$ for every $j.$ To enforce the ascending instance, we add the constraints $$A_{j+1} \ge A_j + 1 - M_j(1-y)\quad \forall j\in \lbrace x, \dots, y-1 \rbrace.$$ Because the indices in the descending case "wrap around", I'm going to get a bit creative with notation. I will use $\overline{j}$ as shorthand for $j \textrm{ mod } n.$ The descending case uses the constraints $$A_\overline{j + 1} \le A_\overline{j} - 1 + \overline{M}_j y \quad \forall j\in \lbrace x, \dots, y-1 \rbrace,$$ where $\overline{M}_j$ is an upper bound on $\vert A_\overline{j + 1} - A_\overline{j} \vert.$
