Answering myself:

With a little nudge, Wolfram is up to the task

FullSimplify[
 LogicalExpand[(y == 0 && x == 0) || (y == 1 && 
      x == 1) || (0 < y < 1 && x == y)] \[Implies] (0 <= y <= 1 && 
    x == y), (x | y) \[Element] Reals]

    Out: True

However, the residue remains. It doesn't handle equivalence, requires two implications and LogicalExpand. And most importantly, it is unclear why there is a difficulty with this task.

Hi Sasha,

I didn't understand the first part of your reply.

For the second part, the following nearly does what you wrote as the desired result:

Reduce[
 (x == -1 && y == 1) || (-1 < x < 0 && y == -x) ||
  (x == 0 && y == 0) || (0 < x < 1 && y == x),
 {x, y}, (* or equivalently  y  instead of  {x, y}  *)
 Reals]
(*  (-1 <= x <= 0 && y == -x) || (0 < x < 1 && y == x)   *)

The conditions in front of the equations are disjoint; that is, the intervals -1 <= x <= 0 and 0 < x < 1 do not overlap. This is because of the way Reduce[] handles the cylindrical decomposition. I doubt there's anyway to get Reduce[] to close the interval. Of course x <= 1 is ruled out by the x < 1 in the input. (I assume one of them is a typo, or something was omitted from the input.)

Re-reducing the solution from the Pi example pairwise seems to work:

Simplify[
 Reduce[
  ((x == -\[Pi] && y == \[Pi]) || (-\[Pi] < x <= 0 && y == -x) ||
    (0 < x < \[Pi] && y == x)),
  {a, x, y}, Reals],
 TransformationFunctions -> {
   # /. Verbatim[Or][a___, A_, b___, B_, c___] :>
      Or[a, Reduce[A || B, {}, Reals], b, c] &
   }]

I'm not sure simplification is any more reliable than Reduce appears (reliable in the sense of producing the desired form).

I would have thought that the Reals domain wasn't necessary, because it is implicit in the expression...

Gianluca,

I think it's that y is implicitly real, but x is probably treated as complex. Specifying the domain Reals adds one further constraint beyond the variables belonging to the domain: namely, that the function values in the problem and solution must also belong to the domain. I'm not sure what that means practically in the OP's problem, but possibly a different algorithm is used that works better on inequalities. I strongly suspect that the algorithms over the Reals are distinct from the default ones, even if they overlap to a great extent. What exactly the methods are and how they're related seems to change over time, which is to be expected as it has been an area of active research for some decades now.

Concerning the additional constraint: In the casus irreducibilis, some real roots of a polynomial solvable can be expressed in terms of n-th roots that have complex values and cannot be expressed with roots that have only real values. So for instance, in the following which has three real solutions, we get the result in terms of complex-valued cube and square roots:

Reduce[0 == 2 x^3 - 9 x^2 - 6 x + 3, x, Cubics -> True]

But if I specify the domain Reals, the option Cubics -> True is ignored and we get real-valued Root[] objects:

Reduce[0 == 2 x^3 - 9 x^2 - 6 x + 3, x, Reals, Cubics -> True]

When Mathematica does not have an "out" like Root[] that is real-valued in the problem, Reduce fails:

Reduce[2 + Pi == ArcCos[x] + ArcCos[-x] + x, x, Reals] (* --> False *)
Reduce[2 + Pi == ArcCos[x] + ArcCos[-x] + x, x]  (* --> x == 2 *)

Thank you! What would I do without you?

The easiest way to get around this obstacle seems to be this:

Reduce[0 < pi && (x == -\[Pi] && y == \[Pi]) || (-\[Pi] < x <= 0 && 
  y == -x) || (0 < x < \[Pi] && y == x) /. Pi -> pi, {x, y}, Reals] /. pi -> Pi