You keep on modifiying the original post. Makes it hard to keep up a coherent discussion. However, your new version of f[x] is equal to g[x], if one applies Gianluca's suggestion of using PiecewiseExpand:

f[x_] := Which[
  0 <= Mod[x, 2 Pi] < Pi, Mod[x, Pi], 
  Pi <= Mod[x, 2 Pi] < 2 Pi,-Mod[x,Pi]+Pi
]
g[x_] := Pi (1 - (-1)^Quotient[x, Pi])/2 + (-1)^Quotient[x, Pi] Mod[x, Pi]

PiecewiseExpand[f[x] - g[x], 0 <= x < 4 Pi]
(* 0 *)

That should answer your question:

But how can this be proved with Wolfram tools?

You can use PiecewiseExpand:

h[x_] := Which[0 <= Mod[x, 2 Pi] < Pi, Mod[x, Pi],
   Pi <= Mod[x, 2 Pi] < 2 Pi, Mod[-x, Pi]];
g[x_] := 
  Pi (1 - (-1)^Quotient[x, Pi])/2 + (-1)^Quotient[x, Pi] Mod[x, Pi];
PiecewiseExpand[h[x] - g[x], 0 <= x < 4 Pi]

First, let me corrected the syntax error of enclosing Pi in square brackets:

f[x_] := Which[
  0 <= Mod[x, 2 Pi] < Pi, Mod[x, Pi], 
  Pi <= Mod[x, 2 Pi] < 2 Pi, Mod[-x, Pi]
]
g[x_] := Pi (1 - (-1)^Quotient[x, Pi])/2 + (-1)^Quotient[x, Pi] Mod[x, Pi]

Then, checking equality of f[x] and g[x] over a range of values for x:

Table[f[x], {x, -10, 10, 1/10}] == Table[g[x], {x, -10, 10, 1/10}]
(* True *)

You're right! Thank you. But my question is still valid about the function f in the form of

f[x_] := Which[0 <= Mod[x, 2 \[Pi]] < \[Pi], Mod[x, \[Pi]], \[Pi] <= Mod[x, 2 \[Pi]] < 2 \[Pi], -Mod[x, \[Pi]] +  \Pi]]

You're right! Thank you. But my question is still valid about the function f in the form of

f[x_] := Which[0 <= Mod[x, 2 \[Pi]] < \[Pi], Mod[x, \[Pi]], \[Pi] <= Mod[x, 2 \[Pi]] < 2 \[Pi], -Mod[x, \[Pi]] +  \Pi]]

As they say in my language: It was a long time ago and not true. I have long since corrected it. Check the attached file ArcCosCos, please. Copying to text causes errors.

And I remember your trick with ArcTan[1/x] + ArcTan[x]. Bravo! I've never seen that before anywhere. If there is any literature on this subject, please tell me.