%%% Formato schermo di fune (1280x800)
%\documentclass{article}\usepackage[paperheight=15.8cm,paperwidth=27.05cm,footskip=2em,hdivide={1ex,*,1ex},vdivide={1ex,*,2ex},nohead,dvips]{geometry}

%%% Formato cartaceo A4
\documentclass[a4paper]{article}

\title{A certified proof of a theorem of Cartan}
\author{Gianni Ciolli\and Graziano Gentili\and Marco Maggesi}
\date{March 5, 2008}

%\usepackage[latin1]{inputenc}
%\usepackage[italian]{babel}
%\usepackage[T1]{fontenc}

\usepackage{amsmath,amsfonts,amsthm}

\newcommand{\CC}{\mathbb{C}}

\theoremstyle{plain}
\newtheorem{thm}{Teorema}
\newtheorem{lemma}{Lemma}
\theoremstyle{definition}
\newtheorem{defi}{Definizione}
\theoremstyle{remark}
\newtheorem{rem}{Nota}

\setlength{\parindent}{0pt}
\setlength{\parskip}{6pt}

\begin{document}

\maketitle

\begin{abstract}
  In the present paper we present a machine-certified proof for a
  theorem of Cartan, using the HOL Light theorem prover by John
  Harrison.
\end{abstract}

\section{Introduction}

\begin{thm}[Cartan]
  Let $D=D(z_0,r)=\big\{z\in \CC\ \big|\ |z-z_0|<r\big\}$, and let
  $f:D\to D$ be holomorphic. Assume that $f(z_0)=z_0$ and $f'(z_0)=1$;
  then $f$ is the identity on $D$.
\end{thm}

\section{How to run the proof}

The HOL Light environment \cite{hol-light-080219,harrison-demo-1996}
is built on top of the Objective CAML (OCaml) programming language
\cite{ocaml}.

From a logical point of view, in HOL Light there are two main
categories of objects:
\begin{itemize}
\item ``term'', which is any term in typed $\lambda$-calculus;
\item ``theorem'', corresponding to terms of type \verb+boolean+ which
  are derived from other terms and theorems via the legitimate
  inference rules.
\end{itemize}

These two categories are implemented in OCaml by suitable type
constructors, whose purpose is to mimick the standard inference rules
of logic. In particular, the constructor for the ``theorem'' type
implements the ten basic inference rules (see
\cite{hol-light-tutorial}) so that to construct a theorem (i.~e., an
object of type \verb+thm+) there are only two ways:
\begin{itemize}
\item either derive it by any combination of the basic inference
  rules, some of which require pre-existing theorems;
\item or declare it as an {\em axiom} (at any moment you can examine
  the list of current axioms by means of the \verb+axioms()+
  function).
\end{itemize}

This means that, assuming that the computer and the OCaml
implementation are not broken, any object of type \verb+thm+ is a
proven statement, that is, it can be deducted formally from the axioms
listed by the \verb+axioms()+ function.

At the present, the latest version of the HOL Light theorem prover
(snapshot of the 19th february 2008) comes with many proved theorems,
including some multivariate real and complex analysis; everything is
built on top of the following three axioms (for a discussion of such
axioms, see e.~g.~\cite{hol-light-tutorial}):
\begin{itemize}
\item \verb+INFINITY_AX+\\
  \verb+|- ?f. ONE_ONE f /\ ~ONTO f+
\item \verb+SELECT_AX+\\
  \verb+|- !P x. P x ==> P ((@) P)+
\item \verb+ETA_AX+\\
  \verb+|- !t. (\x. t x) = t+
\end{itemize}

Hence, to verify that the proof in the \texttt{cartan.ml} file is
correct, the following steps must be carried out:
\begin{enumerate}
\item install and compile HOL Light, snapshot of the 19th february
  2008, as available from \cite{hol-light-080219}, following the
  instruction on that website;
\item put the file \verb+cartan.ml+ in the HOL Light directory;
\item run \verb+hol+ and type
\begin{verbatim}
#use "hol.ml";;
loadt "Multivariate/make_complex.ml";;
loadt "cartan.ml";;
\end{verbatim}
\item after some time (on present-day personal computers, about half
  an hour) HOL Light stops writing
\begin{verbatim}
val ( FIRST_CARTAN_THEOREM ) : thm =
  |- !f z r n m w.
         f holomorphic_on ball (z,r) /\
         f continuous_on cball (z,r) /\
         &0 < r /\
         f z = z /\
         (!w. w IN ball (z,r) ==> f w IN ball (z,r)) /\
         (!w. w IN cball (z,r) ==> f w IN cball (z,r)) /\
         complex_derivative f z = Cx (&1) /\
         w IN ball (z,r)
         ==> f w = w
\end{verbatim}
  showing that the above term has type \verb+thm+. As we have showed
  before, this means that the corresponding claim has a complete
  proof.
\end{enumerate}

\begin{rem}
  At the present our proof uses some new theorems available only in
  the 19th february 2008 snapshot; these features should become
  ``permanent'' in the subsequent stable release of HOL Light, which
  at the present has not been released. When that will happen, we will
  update the present document and remove this notice.
\end{rem}

\section{Proof of the theorem}

%\begin{rem}
%  Bisognerebbe innanzitutto generalizzare al caso in cui $D$ � un
%  qualunque aperto connesso limitato.
%\end{rem}

In this section we sketch the structure of the proof.

\begin{enumerate}
\item We prove four additional assumptions:
  \begin{itemize}
  \item $f:D\to D \implies f^{\circ m}:D\to D$
  \item $f:\overline D\to \overline D \implies f^{\circ m}: \overline
    D\to\overline D$
  \item $f^{\circ m}$ is holomorphic on $D$
  \item $f^{\circ m}$ is continuous on $\overline D$
  \end{itemize}

\item We reduce the goal to
\begin{verbatim}
!n. higher_complex_derivative n f z = higher_complex_derivative n (\x. x) z
\end{verbatim}
  using the following theorem:
\begin{verbatim}
HOLOMORPHIC_FUN_EQ_ON_BALL;;
val it : thm =
  |- !f g z r w.
         f holomorphic_on ball (z,r) /\
         g holomorphic_on ball (z,r) /\
         w IN ball (z,r) /\
         (!n. higher_complex_derivative n f z =
              higher_complex_derivative n g z)
         ==> f w = g w
\end{verbatim}

\item We assume $n>1$, since:
  \begin{itemize}
  \item If $n=0$, the goal follows trivially via\\
    \verb+ASM_REWRITE_TAC[higher_complex_derivative]+;
  \item If $n=1$, the goal follows trivially via\\
    \verb+ASM_REWRITE_TAC[ONE;higher_complex_derivative;COMPLEX_DERIVATIVE_ID]+
  \end{itemize}
\item Using the explicit form of the derivatives of the identity
  (\verb+HIGHER_COMPLEX_DERIVATIVE_ID+) we reduce the goal to:
\begin{verbatim}
higher_complex_derivative n f z = Cx (&0)
\end{verbatim}

\item We use generalized induction on $n$, assuming the goal for each
  $m<n$.

\item The norm is injective on zero (\verb+COMPLEX_NORM_ZERO+), so the
  goal is reduced to
\begin{verbatim}
norm (higher_complex_derivative n f z) = &0
\end{verbatim}

\item We reduce the goal via an ``Archimedean'' real theorem:
\begin{verbatim}
REAL_ARCH_RDIV_EQ_0;;
val it : thm =
  |- !x c. &0 <= x /\ &0 <= c /\ (!m. 0 < m ==> &m * x <= c) ==> x = &0
\end{verbatim}

\item We supply $\frac{n!r}{r^n}$ as the correct value for $c$, so
  that the goal, after some integer arithmetic, is reduced to
\begin{verbatim}
!m. 0 < m
    ==> &m * norm (higher_complex_derivative n f z) <=
        &(FACT n) * r / r pow n
\end{verbatim}

\item We prove that $mD^nf(z)=D^n(f^{\circ m})(z)$, using the
  following theorem specialized to the case where \verb+s+ is the open
  disc \verb+ball(z,r)+:
\begin{verbatim}
HIGHER_COMPLEX_DERIVATIVE_ITER_TOP_LEMMA;;
val it : thm =
  |- !f s z n m.
         open s /\
         f holomorphic_on s /\
         (!w. w IN s ==> f w IN s) /\
         z IN s /\
         f z = z /\
         complex_derivative f z = Cx (&1) /\
         (!i. 1 < i /\ i < n ==> higher_complex_derivative i f z = Cx (&0)) /\
         1 < n
         ==> higher_complex_derivative n (ITER m f) z =
             Cx (&m) * higher_complex_derivative n f z
\end{verbatim}
  % \begin{rem}
  %   � importante osservare come questo risultato sia valido per \verb+s+
  %   generico, anche non disco.
  % \end{rem}

\item We reduce the goal using the following theorem:
\begin{verbatim}
CAUCHY_HIGHER_COMPLEX_DERIVATIVE_BOUND;;
val it : thm =
  |- !f z y r B0 n.
         &0 < r /\
         0 < n /\
         f holomorphic_on ball (z,r) /\
         f continuous_on cball (z,r) /\
         (!w. w IN ball (z,r) ==> f w IN ball (y,B0))
         ==> norm (higher_complex_derivative n f z) <=
             &(FACT n) * B0 / r pow n
\end{verbatim}

\item The goal is now a straightforward consequence of the
  assumptions.
\end{enumerate}

\bibliographystyle{alpha}
\bibliography{hol}

\end{document}
