%% *-* latex-mode *-* \documentclass[a4paper]{article} \usepackage[T1]{fontenc} \usepackage[utf8]{inputenc} \usepackage{url} \usepackage{fullpage} \usepackage{amsmath,stmaryrd} \usepackage{color} \usepackage{pf2} % annoying conflict with amsthm on environment proof % renamed to structproof. \beforePfSpace{0pt} \usepackage{amsthm} \newtheorem{theorem}{Theorem}[section] \newtheorem{corollary}[theorem]{Corollary} \theoremstyle{definition} \newtheorem{definition}[theorem]{Definition} \usepackage[normalem]{ulem} \usepackage{hyperref} % do NOT set [ocgcolorlinks] here! \usepackage[tikz,ocgcolorlinks]{ocgx2} \usetikzlibrary{calc, shapes.callouts, shapes.symbols} % Colourblind friendly colours % http://jfly.iam.u-tokyo.ac.jp/color/#pallet \definecolor{orange}{RGB}{230,159,0} \definecolor{skyblue}{RGB}{86,180,230} % light blue \definecolor{green}{RGB}{0,158,115} % blueish green \definecolor{yellow}{RGB}{240,228,66} \definecolor{blue}{RGB}{0,114,178} \definecolor{red}{RGB}{213,94,0} % vermillon \definecolor{pink}{RGB}{204,121,167} % reddish purple %%% OCG handling commands % #1: OCG name, #2: OCG refname, #3: OCG visibility, #4: colour % \newcommand{\ocguline}[4]{\bgroup\markoverwith % {\begin{ocg}{#1}{#2}{#3}\textcolor{#4}{\rule[-0.5ex]{2pt}{0.4pt}}\end{ocg}}\ULon} \newcommand{\ocghline}[4]{\bgroup\markoverwith {\begin{ocg}{#1}{#2}{#3}\textcolor{#4}{\rule[-0.65ex]{.1pt}{2.5ex}}\end{ocg}}\ULon} \newcommand{\largeocghline}[4]{\bgroup\markoverwith {\begin{ocg}{#1}{#2}{#3}\textcolor{#4}{\rule[-0.75ex]{.1pt}{3.2ex}}\end{ocg}}\ULon} % We cannot put the OCGs in a radio button group because the % \switchocg acts on each OCG in order of the list. When the off OCG % is turned on, the radio button group automatically turn off the % other, but then the \switchocg acts on it… and turn it on again! % #1: OCG name, #2: OCG refname, #3: colour \newcommand{\jymulhl}[3]{\bgroup% \markoverwith{% \rlap{% \begin{ocg}{#1HL}{#2hl}{off}% \textcolor{#3!50}{\rule[-0.65ex]{.1pt}{2.5ex}}% \end{ocg}}% \begin{ocg}{#1UL}{#2ul}{on}% \textcolor{#3}{\rule[-0.5ex]{.1pt}{0.4pt}}% \end{ocg}}\ULon} % TikZ anchors in the text need to be \hbox-ed to allow the % underlining to work correctly. \newcommand{\jymanchor}[1]{% \hbox{\tikz[remember picture]{\coordinate (anchor#1);}}} \begin{document} \begin{center} {\Large Hypertext proofs}\\ Jean-Yves Moyen \end{center} \begin{abstract} Using Optional Contents Group to hide and show parts of texts and to structure proofs (following some of L.~Lamport's ideas~\cite{LamportProof} and creating hypertext proofs). \end{abstract} In \cite{LamportProof}, L.~Lamport advocates the use of ``Structured proofs'' instead of ``prose proofs'' in order to write 21\textup{th} century mathematical proofs. He compares this to the use of equations rather than prose for mathematical statements. Moreover, he reflects briefly on the fact that paper and ink is likely to become less and less used while electronic devices are likely to become more frequent for reading. Thus, we can also make use of features of electronic text, namely hypertext used to hide part of the text, in order to make our proofs even better. While I do not want to comment on the idea of Structured proofs (some parts I like, some I don't), this document is a proof of concept of how hypertext can be used in proofs, whether prose or structured. It serves both as a display case of the result and as a (quick and dirty) display of implementation in \LaTeX\ (the \texttt{ocgx2} package is used to hide and show content, the \texttt{ulem} package is used for underlining and highlighting sentence, and Ti\emph{k}Z is heavily used to position all the optional content). \smallskip A common problem with proofs, whether prose or structured, is to find the correct ``granularity'' of details needed to convince the reader that the proof is correct. Anyone who has taught knows that ``obvious'' steps in the proof are not so obvious to students. Anyone who has tried to write a formal proof in Coq or any other proof assistant knows that going down to that level of details is not only a tedious job but also makes the proof almost unreadable for humans. While not completely solving the problem (and especially not telling you to what level of details you should go), hypertext can help providing proofs that are suitable for audiences with different knowledge of the field. Indeed, some steps in a proof may appear ``obvious'' for readers with a good familiarity of the concepts while they may need more explanations for beginners. Hypertext allows to hide the extra explanations and let the reader decides whether they are needed or not. An expert reader can thus skip the explanations that are not necessarily (and would actually slow down reading and hampers the flow of the reasoning) while a beginner can display them and read them whenever a step in the proof is ``too big''. This can allow the text to reach a larger audience by being neither too complicated nor too ``dumbed down''. In a sense, hypertext can be used to provide both the sketch of the proof (and intuition) and the proof itself. \smallskip Due to the hypertext ``proof of concept'' nature of this document, it is a bad idea to print it. It should be read on an electronic device. Not all PDF readers are able to handle correctly the optional content\ldots From my tests on Linux, \texttt{acrobat reader 9} performs a good job; the embedded viewer in Firefox displays everything and thus is not really usable; \texttt{evince} (3.20) does a relatively good job but has trouble to deactivate buttons that are part of an invisible layer, hence has trouble when handling buttons from different layers that are at the same on-page position; \texttt{xpdf} seems to be unable to display the layers, I have not tested \texttt{okular}. The ``case of study'' proof that I use is the same as the one used by Lamport, taken from M.~Spivak's calculus book~\cite{Spivak}. \section{Definitions and Spivak's proof} \label{sec:spivak-proof} We note $[a;b]$ a closed interval and $]a;b[$ an open one. \begin{definition}[Increasing function] \label{def:increasing} Let $I$ be an interval and $f$ a function defined on $I$. $f$ is (strictly) \emph{increasing} on $I$ iff for all $x, y \in I$, $x < y$ implies $f(x) < f(y)$. \end{definition} Note that for the degenerate cases of empty or singleton interval, any function is increasing on them as there exists no $x < y$ in $I$. This fact is somewhat important in Lamport's discussion on Spivak's proof. \begin{theorem}[Differentiable implies continuous] \label{thm:diff-cont} If $f$ is differentiable at $x$, then it is continuous at $x$. If $f$ is differentiable on an interval $I$, then it is continuous on $I$. \end{theorem} \begin{theorem}[Mean Value Theorem] \label{thm:mean-value} If $f$ is continuous on $[a;b]$ and differentiable on $]a;b[$, then there exists $x \in ]a;b[$ such that \[ f'(x) = \frac{f(b) - f(a)}{b-a} \] \end{theorem} As pointed by Lamport, both these Theorems are important in Spivak's proof. We do not provide here the proofs of these, they are standard results. \begin{corollary} \label{cor:spivak} If $f'(x) > 0$ for all $x$ in an interval, then $f$ is increasing on the interval. \end{corollary} \begin{proof}[Spivak's Proof]~\\ Let $a$ and $b$ be two points in the interval with $a < b$. Then there is some $x$ in $]a;b[$ with \[ f'(x) = \frac{f(b) - f(a)}{b-a}. \] But $f'(x) > 0$ for all $x$ in $]a;b[$, so \[ \frac{f(b) - f(a)}{b-a} > 0. \] Since $b-a>0$ it follows that $f(b)>f(a)$. \end{proof} As pointed by Lamport, the proof is incorrect in the sense that it does not handle the cases where the interval contains only 0 or 1 point. These cases are actually useless by definition of increasing function, but all this is kept silent and left to the reader. Similarly, the proof uses implicitly the Mean Value Theorem (Theorem~\ref{thm:mean-value}) and, in turn, its application requires using Theorem~\ref{thm:diff-cont} to show continuity. \section{Lamport's structured proof} \label{sec:lamport-proof} I give here the formulation (naming the interval) and proof of Corollary~\ref{cor:spivak} given by Lamport. The structured proof is typeset using Lamport's \texttt{pf2} package\footnote{ \url{http://research.microsoft.com/en-us/um/people/lamport/latex/latex.html}, the package redefines a \texttt{proof} environment which I have renamed as \texttt{structproof} to avoid conflict with the one from the \texttt{amsthm} package\ldots}. \begin{corollary} \label{cor:lamport} If $f'(x) > 0$ for all $x$ in an interval $I$, then $f$ is increasing on $I$. \end{corollary} \pflongnumbers \begin{proof}[Lamport's Proof]~\\[-.5cm] \begin{structproof} \step{1}{It suffices to assume \begin{pfenum*} \item $a$ and $b$ are points in $I$ \item $a < b$ \end{pfenum*} and prove $f(b) > f(a)$. } \begin{structproof} \pf\ By definition of an increasing function. \end{structproof} \step{2}{There is some $x$ in $]a;b[$ with $f'(x) = \frac{f(b) - f(a)}{b-a}$.} \begin{structproof} \step{2.1}{$f$ is differentiable on $[a;b]$.} \begin{structproof} \pf\ By 1.1, since $f$ is differentiable on $I$ by hypothesis. \end{structproof} \step{2.2}{$f$ is continuous on $[a;b]$.} \begin{structproof} \pf\ By \stepref{2.1} and Theorem~\ref{thm:diff-cont}. \end{structproof} \qedstep \begin{structproof} \pf\ By \stepref{2.1}, \stepref{2.2}, and the Mean Value Theorem (Theorem~\ref{thm:mean-value}). \end{structproof} \end{structproof} \step{3}{$f'(x) > 0$ for all $x$ in $]a;b[$.} \begin{structproof} \pf\ By the hypothesis of the corollary and assumption 1.1 \end{structproof} \step{4}{$\frac{f(b) - f(a)}{b-a} > 0$.} \begin{structproof} \pf\ By \stepref{2} and \stepref{3}. \end{structproof} \qedstep \begin{structproof} \pf\ Assumption 1.2 implies $b-a>0$, so \stepref{4} implies $f(b)-f(b) > 0$, which implies $f(b) > f(a)$. By \stepref{1}, this proves the corollary. \end{structproof} \end{structproof} \end{proof} \newpage \section{Hypertext prose proof} \begin{corollary} \label{cor:jym} % some slanted/italic letters go out of their bounding box and a \, % must be added to avoid the highlight of the space to 'eat' the % letter. If \ocghline{f' positive HL}{derposhl}{off}{orange}{$f'(x) > 0$\jymanchor{derposhyp} for\, all\, $x$ in an interval\, $I$}, then $f$ is increasing on $I$. \end{corollary} \begin{proof}[Hypertext prose proof] \switchocg{increasingul increasinghl}{\jymulhl{Increasing}{increasing}{green}{Let us consider any two points in $I$, $a$ and $b$ , with $a < b$ and\jymanchor{increasing} show $f(a) < f(b)$.}}\\ \jymanchor{exists}There exists some $x$ in $]a;b[$ with \[ f'(x) = \frac{f(b) - f(a)}{b-a}. \] \jymanchor{mean}But \switchocg{derposul derposhl}{\jymulhl{f' positive}{derpos}{orange}{$f'(x) > 0$\jymanchor{derposused} for all $x$ in $]a;b[$}}, so \[ \frac{f(b) - f(a)}{b-a} > 0. \] \jymanchor{concl}Since $b-a>0$ it follows that $f(b)>f(a)$. \end{proof} % Extra decorations \begin{tikzpicture}[remember picture, overlay] \draw[blue, line width=.3ex] ($(anchorexists) + (-0.2ex,2ex)$) -- ($(anchormean) + (-0.2ex,2.3ex)$); \end{tikzpicture} % OCGs % a