Are metric isometries smooth at the boundary? Let $M,N$ be smooth Riemannian manifolds with boundary (In particular, we assume the boundaries are smooth).
Suppose we have a map $\phi:M \to N$ which satisfies the following properties:
$$(1) \, \, \phi:M \to N \, \, \text{is a bijection}$$
$$ (2) \, \, \phi(\operatorname{int}M)=\operatorname{int}N,\phi(\partial M)=\partial N $$
$$ (3) \, \, \phi:M \to N \, \,\text{is a metric isometry}$$
By the Myers-steenrod theorem, applied to $\phi|_{\operatorname{int}M} :\operatorname{int} M \to \operatorname{int}N $, $\phi$ is a diffeomorphism between $\operatorname{int} M , \operatorname{int}N$.
Question: Is $\phi$ necessarily smooth as a map $M \to N$?

When looking at the proof of Myers-steenrod theorem here, the problem seems to be that initial conditions do not determine a unique geodesic, if the starting point is on the boundary. 
The basic idea of the proof is to express the map $\phi$ in exponential coordinates, then show this representation is linear, hence smooth. However, constructing this representation relies on the uniqueness of geodesics. 
I suspect there might be a counter example where singularity occurs at the boundary, but I could not fine one.
 A: Yes, $\phi$ is smooth. Indeed, fix any $x\in\partial M$ and take any nieghbourhood $x\in U\subseteq\partial M$ with compact closure. Calling $\nu:\partial M\to TM$ the (unit) inward-pointing normal vector, we can find some $\epsilon>0$ so small that


*

*the map $\alpha:U\times [0,\epsilon]\to M$, $\alpha(y,t):=\exp(t\nu(y))$ is well-defined and is a diffeomorphism onto its image;

*$\text{dist}(\alpha(y,t),\partial M)=t$ for all $(y,t)\in U\times [0,\epsilon]$.


For any $y\in U$, the curve $t\mapsto\phi\circ\alpha(y,t)$ is a unit-speed geodesic: this is true on the interval $(0,\epsilon]$ by interior smoothness of $\phi$, so it is true on $[0,\epsilon]$ by continuity. Since $\text{dist}(\phi\circ\alpha(y,t),\partial N)=t$, we deduce that it is a minimizing geodesic from $\partial N$ to $\phi\circ\alpha(y,\epsilon)$, implying that $\frac{d}{dt}(\phi\circ\alpha)|_{t=0}\perp\partial M$, i.e.
$$ \phi\circ\alpha(y,t)=\exp(t\nu(\phi(y)))\qquad (*)$$
(now $\nu$ denotes the inward-pointing normal in $N$).
Up to shrinking $\epsilon$, we can assume that $(z,t)\mapsto\exp(t\nu(z))$ gives a diffeomorphism from $\phi(U)\times [0,\epsilon]$ onto its image, as well. We call $(\beta,\tau)$ its smooth inverse.
Finally, $\phi|_U$ is smooth (as $\phi(y)=\beta\circ\phi\circ\alpha(y,\epsilon)$ and as $\phi$ is smooth on $\text{int}(M)$), so also
$\phi|_{\alpha(U\times[0,\epsilon])}$ (by $(*)$).
