[ARITH] Fix the rule y < x && x <= y (#4220)

src/arithmetic/rewrite_simplify.cc

@@ -1610,7 +1610,7 @@ Mutate_(const And* op, const Expr& self) {
   TVM_TRY_REWRITE(x != y && x == y, cfalse);
   TVM_TRY_REWRITE(x && !x, cfalse);
   TVM_TRY_REWRITE(x <= y && y < x, cfalse);
-  TVM_TRY_REWRITE(y < x && y <= x, cfalse);
+  TVM_TRY_REWRITE(y < x && x <= y, cfalse);
 
   TVM_TRY_REWRITE_IF(x < c1 && c2 < x, cfalse,
                      c2.Eval()->value + 1 >= c1.Eval()->value);

tests/python/unittest/test_arith_rewrite_simplify.py

@@ -783,7 +783,7 @@ def test_logical_simplify():
               tvm.const(False, "bool"))
     ck.verify(tvm.expr.And(x > 1, tvm.expr.Not(x > 1)), tvm.const(False, "bool"))
     ck.verify(tvm.expr.And(x <= y, y < x), tvm.const(False, "bool"))
-    ck.verify(tvm.expr.And(y < x, y <= x), tvm.const(False, "bool"))
+    ck.verify(tvm.expr.And(y < x, x <= y), tvm.const(False, "bool"))
     ck.verify(tvm.expr.And(x < 1, 0 < x), tvm.const(False, "bool"))
     ck.verify(tvm.expr.And(x < 0, 1 < x), tvm.const(False, "bool"))
     ck.verify(tvm.expr.And(x < 1, 1 <= x), tvm.const(False, "bool"))