How to simplify expressions by closing open inequalities?

Question

Recently I have often acquired results which consist of combinations of 0, 1 and 2-dimensional (in)equalities. For instance, consider a very simple case with ineq1 and ineq2 below:

With[
 {ineq1 = x == 0 && y == 0 || x > 0 && -x <= y <= x,
  ineq2 = -x <= y <= x},
 Resolve[ForAll[{x, y}, ineq1 \[Equivalent] ineq2], Reals]]

True

Mathematica thinks they're equivalent over $\mathbb{R}^2$. How can I simplify an inequality ineq1 to form like ineq2? I have tried at least FullSimplify, Reduce and Refine, but none of them seem to grok my goal.

EDIT: Note that above example is really roughly the simplest one that can be imagined. On my ongoing experiments, especially maintaining (and creating) chained inequalities like a <= x < b as a part of the expression seems to be curiously complicated.

Answer 1

Here's some work-in-progress code I have been playing with.

First we define a helper function which attempts to combine Anded comparisons (which result when using functions such as LogicalExpand) into Inequality, Equal and Unequal chains. It does this by making graphs of expressions, and finding paths connected components and cliques on them. It doesn't try to move components of comparison between sides of the comparison operator - there's clearly room for improvement in that regard.

ClearAll[collectInequalityChains];

collectInequalityChains[eq_] :=
 Module[{
   normeq,
   eqExtract, eqExtractStep,
   ineqExtract, ineqExtractStep,
   uneqExtract, uneqExtractStep},

  normeq = BooleanMinimize@LogicalExpand@eq //. {
     a_ > b_ :> b < a,
     a_ >= b_ :> b <= a};

  ineqExtractStep[{graph_Graph, ineqs_List}] :=
   Module[{largestpath, pathedges},
    largestpath = 
     First@TakeLargestBy[
       Flatten[FindPath[graph, Sequence @@ #, Infinity, All] & /@ 
         Flatten[{#, Reverse@#} & /@ Subsets[VertexList@graph, {2}], 
          1], 1], Length, 1];
    pathedges = DirectedEdge @@@ Partition[largestpath, 2, 1];
    {Subgraph[graph,
      DeleteCases[EdgeList@graph, Alternatives @@ pathedges], 
      EdgeLabels -> PropertyValue[graph, EdgeLabels]],
     Append[ineqs, 
      Inequality @@ 
       Riffle[largestpath, 
        PropertyValue[{graph, #}, EdgeLabels] & /@ pathedges]]}];
  ineqExtract[graph_Graph] := 
   And @@ Last@
     NestWhile[ineqExtractStep, {graph, {}}, 
      Not@*EmptyGraphQ@*First];

  eqExtractStep[{graph_Graph, eqs_List}] :=
   Module[{largestconnected},
    largestconnected = 
     First@TakeLargestBy[ConnectedComponents@graph, Length, 1];
    {GraphDifference[graph,
      Subgraph[graph, largestconnected]],
     Append[eqs, largestconnected]}];
  eqExtract[graph_Graph, op_Symbol] := 
   And @@ (op @@@ 
      NestWhile[eqExtractStep, {graph, {}}, 
        Not@*EmptyGraphQ@*First][[2]]);

  uneqExtractStep[{graph_Graph, eqs_List}] :=
   Module[{largestconnected},
    largestconnected = 
     First@TakeLargestBy[FindClique@graph, Length, 1];
    {GraphDifference[graph,
      Subgraph[graph, largestconnected]],
     Append[eqs, largestconnected]}];
  uneqExtract[graph_Graph, op_Symbol] := 
   And @@ (op @@@ 
      NestWhile[uneqExtractStep, {graph, {}}, 
        Not@*EmptyGraphQ@*First][[2]]);

  MapAt[eqExtract[Graph[UndirectedEdge @@@ Cases[#, _Equal, {0, 1}]], 
      Equal] &&
     uneqExtract[Graph[UndirectedEdge @@@ Cases[#, _Unequal, {0, 1}]],
       Unequal] &&
     ineqExtract[
      Graph[Property[DirectedEdge @@ #, EdgeLabels -> Head@#] & /@ 
        Cases[#, _Less | _LessEqual, {0, 1}]]] &, normeq, 
   Most /@ Position[normeq, And]]]

A simple example:

collectInequalityChains[
 a < b && c >= b && a == d && d == e || b > a || x != y && y != z]

(d == a == e && a < b <= c) || (y != x && y != z) || a < b

Then we use this function as prettifier in a function which attempts to simplify inequalities by searching exhaustively for equivalence of original inequality and transformed variants of it. These variants either leave an comparison unchanged, replace it with True or False, or expand open inequality to closed one. The variant with smallest LeafCount after collectInequalityChains is given out as the solution.

ClearAll[simplifyComparisons];

simplifyComparisons[ineqtmp_, vars_] :=
 Module[{ineq, eqpos, ineqpos, eqtrans, ineqtrans},
  ineq = BooleanMinimize@LogicalExpand@ineqtmp;

  eqpos = Position[ineq, _Equal | _Unequal];
  ineqpos = 
   Position[ineq, _Less | _LessEqual | _Greater | _GreaterEqual];

  eqtrans = 
   Thread[eqpos -> MapThread[#1[Extract[ineq, #2]] &, {#, eqpos}]] & /@
     Tuples[{Identity, True &, False &}, Length@eqpos];

  ineqtrans = 
   Thread[ineqpos -> 
       MapThread[#1[Extract[ineq, #2]] &, {#, ineqpos}]] & /@ 
    Tuples[{Identity, # /. {Less -> LessEqual, 
         Greater -> GreaterEqual} &, True &, False &}, Length@ineqpos];

  First@TakeSmallestBy[
    collectInequalityChains@ReplacePart[ineq, #] & /@ 
     Select[Flatten[Table[Join[a, b], {a, eqtrans}, {b, ineqtrans}], 
       1],
      Resolve[
        ForAll[vars, 
         Evaluate[ineq \[Equivalent] ReplacePart[ineq, #]]], 
        Reals] &], LeafCount, 1]]

Now we can simplify our original toy problem:

simplifyComparisons[
 x == 0 && y == 0 || x > 0 && -x <= y <= x, {x, y}]

-x <= y <= x