Perhaps this?:

Reduce[(y == 0 && x == 0) || (y == 1 && x == 1) || (0 < y < 1 && x == y), {y, x}, Reals]
(*  0 <= y <= 1 && x == y  *)

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 *)

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.)

I suppose it's because Head[Pi] is Symbol, and Pi is numeric but not a number. For instance, it seems Pi is replaced by an internal variable, the system reduced, and then the internal variable is replaced by Pi. The cylindrical decomposition seems to apply something like the trichotomy law and consider the three cases x < ..., x == ..., and x > ... separately. Actual numbers are handled more simply, or Reduce looks to see if cases can be combined for numbers and not for symbols. I'm just guessing here. I don't think these details are published.

Pursuing this line may be futile.

Here's a somewhat bizarre workaround, replacing Pi by a nonnumeric symbol:

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

On the other hand, it handles equivalence without tricks:

Reduce[
 Equivalent[
  (x == -\[Pi] && y == \[Pi]) || (-\[Pi] < x <= 0 && y == -x) ||
   (0 < x < \[Pi] && y == x),
  (-\[Pi] <= x <= 0 && y == -x) || (0 < x < \[Pi] && y == x)]
 , {x, y}, Reals]
(*  True  *)

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).

Dear Michael! It seems to me that the problem is not related to Pi properties. For some reason Wolfram breaks the calculation. It is the expression that Wolfram is evaluating.

Reduce[(\[Pi]/2 < x < \[Pi] && y == \[Pi] - x) || (x == \[Pi] && y == 0), {x, y}, Reals]
Out: \[Pi]/2 < x <= \[Pi] && y == \[Pi] - x

This one, which is a bit more complicated, does not:

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

What do you think about that?

Here is a way:

formula0 = (y == 0 && x == 0) || (y == 1 && x == 1) || (0 < y < 1 && 
    x == y)
CylindricalDecomposition[formula0, {x, y}]

As for proving the equivalence, here are my attempts:

formula0 = (y == 0 && x == 0) || (y == 1 && x == 1) || (0 < y < 1 && 
    x == y)
formula1 = 0 <= y <= 1 && x == y
Reduce[Equivalent[formula0, formula1], {x, y}]
Reduce[Not[Equivalent[formula0, formula1]]]
CylindricalDecomposition[
 Equivalent[formula0, formula1], {x, y}]

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.