<html><head><meta name="color-scheme" content="light dark"></head><body><pre style="word-wrap: break-word; white-space: pre-wrap;">%% *-* 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 &lt;
  y$ implies $f(x) &lt; 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 &lt; 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) &gt; 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 &lt; b$. Then
  there is some $x$ in $]a;b[$ with
  \[
  f'(x) = \frac{f(b) - f(a)}{b-a}.
  \]
  But $f'(x) &gt; 0$ for all $x$ in $]a;b[$, so
  \[
  \frac{f(b) - f(a)}{b-a} &gt; 0.
  \]
  Since $b-a&gt;0$ it follows that $f(b)&gt;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) &gt; 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 &lt; b$
      \end{pfenum*}
      and prove $f(b) &gt; 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) &gt; 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} &gt; 0$.}
    \begin{structproof}
      \pf\ By \stepref{2} and \stepref{3}.
    \end{structproof}
    \qedstep
    \begin{structproof}
      \pf\ Assumption 1.2 implies $b-a&gt;0$, so \stepref{4} implies
      $f(b)-f(b) &gt; 0$, which implies $f(b) &gt; 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) &gt; 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 &lt; b$
      and\jymanchor{increasing} show $f(a) &lt; 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) &gt; 0$\jymanchor{derposused} for
      all $x$ in $]a;b[$}}, so
  \[
  \frac{f(b) - f(a)}{b-a} &gt; 0.
  \]
  \jymanchor{concl}Since $b-a&gt;0$ it follows that $f(b)&gt;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&lt;b sufficient
\begin{tikzpicture}[remember picture, overlay, ocg={name=Increasing
    proof, ref=increasinghl, status=invisible}]
  \coordinate (anchorcallout) at ($(anchorincreasing) + (0,1.5ex)$);

  \node[draw=green, fill=green!20, rectangle callout, rounded corners,
  callout absolute pointer=(anchorcallout), text width=5cm, inner
  sep=1ex]
  (increasingexplanation) at ($(anchorincreasing) + (-0.5,1.8)$) {By
    definition of an increasing function, this suffices to prove the
    result.};

  \coordinate (innernw) at ($(increasingexplanation.north west) +
  (0.1,-0.1)$);
  \coordinate (innersw) at ($(increasingexplanation.south west) +
  (0.1,0.1)$);
  \coordinate (innerne) at ($(increasingexplanation.north east) +
  (-0.1,-0.1)$);
  \coordinate (innerse) at ($(increasingexplanation.south east) +
  (-0.1,0.1)$);
  \coordinate (inneranchor) at ($(innernw)!0.6!(innersw)$);

  \draw[red, line width=.3ex] (innernw) -- (innersw);

  \path[switch ocg={nested1}] (innersw) rectangle (innerne);

  \begin{scope}[ocg={name=Expanding def, ref=nested1,
      status=invisible}]
    \draw[red, line width=.3ex] (innersw) rectangle (innerne);

    \node[draw=red, fill=red!30, rectangle callout, rounded corners,
    callout absolute pointer=(inneranchor), text width = 7cm] at
    ($(inneranchor) + (-4,1)$) {By Definition~\ref{def:increasing},
      $f$ is increasing on $I$ iff $\forall a, b \in I$ with $a &lt; b$,
      we have $f(a) &lt; f(b)$. Thus, to prove that $f$ is increasing on
      $I$, it is sufficient to consider any two $a$ and $b$ in $I$
      with $a &lt; b$ and show $f(a) &lt; f(b)$.};
  \end{scope}
\end{tikzpicture}

% button for the MVT application
\begin{tikzpicture}[remember picture, overlay]
  \coordinate (existssw) at ($(anchormean) + (-0.2ex,2.3ex)$);
  \coordinate (existsne) at ($(anchorexists) + (9.6cm,2ex)$);
  \path[switch ocg={existshl}] (existssw) rectangle (existsne);
\end{tikzpicture}

% MVT details.
\begin{tikzpicture}[remember picture, overlay, ocg={name=Exists HL,
    ref=existshl, status=invisible}]

  \coordinate (existscallout) at ($(existsne) + (0,-0.2cm)$);

  \fill[blue, opacity=.2] (existssw) rectangle (existsne);

  \node[draw=blue, fill=blue!20, rectangle callout, rounded corners,
  callout absolute pointer=(existscallout), text width=5cm, inner
  sep=1ex] (existsexplanation) at ($(existscallout) + (3cm, -0.5cm)$)
  {By the Mean Value Theorem (Theorem~\ref{thm:mean-value}).};

  \coordinate (mvtnw) at ($(existsexplanation.north west) +
  (0.1,-0.1)$);
  \coordinate (mvtsw) at ($(existsexplanation.south west) +
  (0.1,0.1)$);
  \coordinate (mvtne) at ($(existsexplanation.north east) +
  (-0.1,-0.1)$);
  \coordinate (mvtse) at ($(existsexplanation.south east) +
  (-0.1,0.1)$);
  \coordinate (mvtanchor) at ($(mvtnw)!0.6!(mvtne)$);

  \draw[red, line width=.3ex] (mvtnw) -- (mvtsw);

  \path[switch ocg={mvtshort}] (mvtsw) rectangle (mvtne);
  \begin{scope}[ocg={name=Mean Value, ref=mvtshort, status=invisible}]
    \draw[red, line width=.3ex] (mvtsw) rectangle (mvtne);

    \node[draw=red, fill=red!30, rectangle callout, rounded corners,
    callout absolute pointer=(mvtanchor), text width = 6cm] at
    ($(mvtanchor) + (-0.5,2)$)
    {\textcolor{pink}{$\bullet$}\jymanchor{diffclose}%
      \switchocg{diffclose}{\ocghline{Foo}{diffclose}{off}{pink!20}{$f$
          is differentiable on $[a;b]$.}}\\
      \textcolor{pink}{$\bullet$}\jymanchor{diffopen}%
      \switchocg{diffopen}{\ocghline{Foo}{diffopen}{off}{pink!20}{$f$
          is differentiable on $]a;b[$.}}\\
      \textcolor{pink}{$\bullet$}\jymanchor{cont}%
      \switchocg{cont}{\ocghline{Foo}{cont}{off}{pink!20}{$f$
          is continuous on $[a;b]$.}}\\
      Therefore, by the Mean Value Theorem
      (Theorem~\ref{thm:mean-value}), there exists such an $x$.};

    \coordinate (calloutdiffclose) at ($(anchordiffclose) + (-1ex,0.7ex)$);
    \coordinate (calloutdiffopen) at ($(anchordiffopen) + (-1ex,0.7ex)$);
    \coordinate (calloutcont) at ($(anchorcont) + (-1ex,0.7ex)$);

    \begin{scope}[ocg={name=Differentiable on close, ref=diffclose,
        status=invisible}]
      \node[draw=pink, fill=pink!20, rectangle callout, rounded
      corners, callout absolute pointer=(calloutdiffclose), text
      width=8cm] at ($(anchordiffclose) + (-5cm, 1.2cm)$) {Because
        $[a;b] \subset I$ and $f$ is differentiable on $I$ by
        hypothesis.};
    \end{scope}
    \begin{scope}[ocg={name=Differentiable on open, ref=diffopen,
        status=invisible}]
      \node[draw=pink, fill=pink!20, rectangle callout, rounded
      corners, callout absolute pointer=(calloutdiffopen), text
      width=8cm] at ($(anchordiffopen) + (-5cm, 0.15cm)$) {Because
        $]a;b[ \subset I$ and $f$ is differentiable on $I$ by
        hypothesis.};
    \end{scope}
    \begin{scope}[ocg={name=Continuous, ref=cont,
        status=invisible}]
      \node[draw=pink, fill=pink!20, rectangle callout, rounded
      corners, callout absolute pointer=(calloutcont), text width=8cm]
      at ($(anchorcont) + (-5cm, -0.9cm)$) {Because $f$ is
        differentiable on $[a;b]$ by the previous points, thus it is
        continuous on $[a;b]$ by Theorem~\ref{thm:diff-cont}.};
    \end{scope}
  \end{scope}
\end{tikzpicture}

% f' positive by hypothesis.
\begin{tikzpicture}[remember picture, overlay, ocg={name=f' positive HL,
    ref=derposhl, status=invisible}]
  \coordinate (calloutderposused) at ($(anchorderposused) +
  (0,1.5ex)$);

  \node[draw=orange, fill=orange!20, rectangle callout, rounded
  corners, callout absolute pointer=(calloutderposused)] at
  ($(anchorderposused)!0.8!(anchorderposhyp)$) {By hypothesis, because
    $]a;b[ \subset I$.};
\end{tikzpicture}

\textbf{Comments.} In short, all parts with a coloured line or dot
next to them are buttons that can be clicked to show (or hide) a more
detailed explanation of the assertion.

This is more a ``proof of concept'' than a real attempt at having an
hypertext proof. Especially, the proof has a lot of ``bells and
whistles'' that are probably useless. Moreover, various different ways
of indicating that an explanation exists are mixed and this is
probably not a good idea in general.

However, this shows that it is possible to have such added details to
a proof in a reasonable way. This can be useful in many academic
situations, including hiding solution of exercises in a textbook, or
preparing an article with both a short and a long version mixed
without resorting to appendices (that are often clumsy to navigate
back and forth).

Due to restrictions in \texttt{pdf} (or in my knowledge of it), it is
not possible to have the extra explanations ``push down'' the
following text when appearing. All the space for them must be reserved
in advance. This is why I chose to used multiple ``pop-ups'' to
display the explanations rather than having huge white gaps in the
text like the following (\switchocg{text}{\textcolor{red}{Click me!}})

\begin{ocg}{Hidden text}{text}{off}
  Showing details of a proof might seem more natural if the details
  are shown as if they are part of the proof, rather than with pop-ups
  everywhere. However, the space for the hidden text must be reserved
  when the document is produced, it is not possible to have the
  following text pushed down when displaying it (contrarily to what
  happens in \texttt{html}, or between frames of a single
  \texttt{beamer} slide for example). Thus, having some hidden text
  displayed as if part of the running text creates huge white spaces
  when the text is hidden. This would destroy the gain in space of the
  short version and also make the short version appear clumsy and less
  readable. For these reasons, I chose to have the extra explanations
  as pop-ups covering the rest of the text and not as part of the
  ``natural'' flow of the proof.
\end{ocg}

The typesetting and (especially) positioning of all this is currently
done manually (and somewhat painfully). Among other, this means that
changes in the general layout of the document will require adaptations
of the positioning of everything. Typically, the proof was typeset
while being on the bottom of a page, hence many pop-ups are going
upward and out of the ``bounding box'' of the proof itself. When I
decided later to move the proof at the top of a new page, the pop-ups
went into the top margin of the page, which might be a bad idea
(especially since a document produced for electronic reading can use
very small margins and the pop-ups then might go out of the page).

The manual positioning can be somewhat improved by using more relative
coordinates and the various ``\texttt{north east}'' and so on anchors
on Ti\emph{k}Z nodes, but this was not my main goal\ldots

Lastly, the choice of the colours themselves is made according to a
``colourblind friendly'' scheme described at
\url{http://jfly.iam.u-tokyo.ac.jp/color/#pallet}. Because around 8\%
of all males (and around 0.45\% of females, hence a bit more than 4\%
of the total population) are colourblind, we should as much as
possible use colours than can be separated by most of the colour blind
people as well as by the non colour blind ones (rather than making our
documents less readable for 1 out of 20 readers). Since I'm not colour
blind myself, I only have second-hand (or second-eye?)  confirmation
that these colours indeed are easier to separate (at least for some
colour blind people; there are many different kind of colour blindness
and it is likely that we won't be able to have colours as friendly to
all of them as one could wish).

\smallskip

Obviously, the choice of what to explain further and to which depth of
explanation one should go is not an easy one. The choices I've made
here are disputable. I do not claim that I know how to answer these
questions which are probably very dependant on the audience of the
text anyway. Maybe some of the unexplained steps in the proof could
need more explanation. Maybe some of the explanations are too much or
could be merged in a single level rather than nesting them. I am
merely toying with the technical (and \LaTeX nichal, of course)
possibilities.


\vspace{10cm}

\hspace{5cm} \jymanchor{toto}

% button
\begin{tikzpicture}[remember picture, overlay]
  \coordinate (totosw) at ($(anchortoto) + (-1cm,-0.5cm)$);
  \coordinate (totone) at ($(anchortoto) + (1cm,0.5cm)$);
  \path[switch ocg={achievement}] (totosw) rectangle (totone);
\end{tikzpicture}

\begin{tikzpicture}[remember picture, overlay, ocg={name=Achievement,
    ref=achievement, status=invisible}]
  \node[starburst, draw, red,fill=yellow,line width=1.5pt, text
  width=5cm] at (anchortoto) {\begin{center} \textsc{\Large
        Achievement Unlocked!}\\
      Click in the middle of nowhere.\\
      \scriptsize \textcolor{orange}{Did you read the code to find
        me?}
  \end{center}
};
\end{tikzpicture}

\newpage
\section{Hypertext structured proof}
\begin{proof}[Hypertext structured proof]~\\[-.5cm]
  \begin{structproof}
    % Strange stuff happens if the anchor is placed before the 'It'
    % (it is actually placed at the very start of the proof, before
    % the first step). I assume strange behaviour of the \step
    % command.
    \step{1}{It\jymanchor{struct1} suffices to assume
      \begin{pfenum*}
      \item $a$ and $b$ are points in $I$\jymanchor{left1}
      \item $a &lt; b$
      \end{pfenum*}
      and prove $f(b) &gt; f(a)$.\jymanchor{struct1bis}
    }
    \step{2}{\switchocg{struct2 struct2proof}{\largeocghline{Structure
          2}{struct2}{off}{green!50}{There is some $x$ in $]a;b[$
          with $f'(x) = \frac{f(b) - f(a)}{b-a}$.}}\jymanchor{left2}}
    \step{3}{\switchocg{struct3}{\ocghline{Structure
          3}{struct3}{off}{red!50}{$f'(x) &gt; 0$ for all $x$ in
          $]a;b[$.}}\jymanchor{left3}}
    \step{4}{\switchocg{struct4}{\largeocghline{Structure
          4}{struct4}{off}{blue!50}{$\frac{f(b) - f(a)}{b-a} &gt;
          0$.}}\jymanchor{left4}}
    \step{5}{\switchocg{struct5}{\ocghline{Structure
            5}{struct5}{off}{orange!50}{Q.E.D.}}\jymanchor{left5}}
      % should use \qedPfkwd
  \end{structproof}
\end{proof}

% button for 1
\begin{tikzpicture}[remember picture, overlay]
  \coordinate (struct1nw) at ($(anchorstruct1) + (-2ex,2.3ex)$);
  \coordinate (struct1se) at ($(anchorstruct1bis) + (5.2ex,-0.5ex)$);
  \path[switch ocg={struct1hl}] (struct1nw) rectangle (struct1se);
\end{tikzpicture}

\begin{tikzpicture}[remember picture, overlay, ocg={name=Structure 1 HL,
    ref=struct1hl, status=invisible}]
  \fill[yellow, opacity=.3] (struct1nw) rectangle (struct1se);

  \node[draw=yellow, fill=yellow!20, rectangle, rounded corners] at
  ($(anchorleft1) + (3cm,2cm)$) {\pf\ By definition of an increasing
    function.};
\end{tikzpicture}

% Proof for 2
\begin{tikzpicture}[remember picture, overlay, ocg={name=Structure 2 Proof,
    ref=struct2proof, status=invisible}]
  \node[draw=green, fill=green!20, rectangle, rounded corners,
  text width=7cm] at ($(anchorleft2) + (4cm, 1.15cm)$) {%
    \begin{structproof}
      \nostep{no1}
      \nostep{no2}
      \begin{noproof}
        \step{2.1}{\switchocg{struct21}{$f$ is differentiable on
            $[a;b]$.}}
        \begin{ocg}{Structure 2.1}{struct21}{off}
          \begin{structproof}
            \pf\ By 1.1, since $f$ is differentiable on $I$ by
            hypothesis.
          \end{structproof}
        \end{ocg}
        \step{2.2}{\switchocg{struct22}{$f$ is continuous on
            $[a;b]$.}}
        \begin{ocg}{Structure 2.2}{struct22}{off}
          \begin{structproof}
            \pf\ By \stepref{2.1} and Theorem~\ref{thm:diff-cont}.
          \end{structproof}
        \end{ocg}
      % \qedstep is not easy to OCG-iseâ€¦
      % \qedstep
        \step{2.3}{\switchocg{struct23}{Q.E.D.}} % should use \qedPfkwd
        \begin{ocg}{Structure 2.3}{struct23}{off}
          \begin{structproof}
            \pf\ By \stepref{2.1}, \stepref{2.2}, and the Mean Value
            Theorem (Theorem~\ref{thm:mean-value}).
          \end{structproof}
        \end{ocg}
      \end{noproof}
    \end{structproof}
  };
\end{tikzpicture}

% Proof for 3
\begin{tikzpicture}[remember picture, overlay, ocg={name=Structure 3,
    ref=struct3, status=invisible}]

  \node[draw=red, fill=red!20, rectangle, rounded corners] at
  ($(anchorleft3) + (6cm,-0.6cm)$) {\pf\ By the hypothesis of the corollary
    and assumption 1.1.};
\end{tikzpicture}

% Proof for 4
\begin{tikzpicture}[remember picture, overlay, ocg={name=Structure 4,
    ref=struct4, status=invisible}]

  \node[draw=blue, fill=blue!20, rectangle, rounded corners] at
  ($(anchorleft4) + (3cm,-0.7cm)$) {\pf\ By 2 and 3.};
\end{tikzpicture}

% Proof for 5
\begin{tikzpicture}[remember picture, overlay, ocg={name=Structure 5,
    ref=struct5, status=invisible}]

  \node[draw=orange, fill=orange!20, rectangle, rounded corners, text
  width=15cm] at ($(anchorleft5) + (6.8cm,-1.2cm)$) {\pf\ Assumption 1.2
    implies $b-a&gt;0$, so 4 implies $f(b)-f(b) &gt; 0$, which implies
    $f(b) &gt; f(a)$. By 1, this proves the corollary.};
\end{tikzpicture}

\vspace{-1.5cm}

\textbf{Comments.} The very good point about the structured hypertext
proof is that we can make use of the structure. On the reader point of
view, that means that every assumption (proof step) that is not proved
can be clicked to display its proof; there is no need to the somewhat
clumsy lines indicating ``details available'' in the prose proof. I
also find it easier to locate steps 2 and 3 when reading the proof of
step 4, because they are not interleaved with their proofs. On the
writer point of view, that means that the \verb+\step+ command of the
\texttt{pf2} package can be modified to automatically produce all the
needed buttons.

On the other hand, the structured proof might go into deeper level of
nesting of proofs. I do not imagine how it would be possible to
correctly lay out 4 or 6 nested levels of proof pop-ups. Well, likely
by actually not hiding all of them and considering that, say, the
first and second levels are the backbone of the proof, and should
always be displayed, and that the pop-ups should only start at the
third or so level\ldots

The other bad point, on a purely technical point of view, is that the
pop-ups are not part of the structured proof environment. That means
that commands like \verb+\stepref+ do not work. In this precise case,
I entered the number of the steps by hand but this is obviously not a
good idea. \verb+\pflabel+ and \verb+\pfref+ should be used
instead. However, on a ``logical structure'' point of view it is still
somewhat unsatisfactory that the subproofs are not really parts of the
proof.

On the good side, when both the statements and the proofs are short,
as this is the case here, the global positioning is easier with an
implicit splitting of the page in two.

\smallskip

This time, I chose to inline the proofs of the substeps 2.1, 2.2, and
2.3. I feel that because it is already part of a pop-up and because
they are short enough, the white space (well, green space, actually)
left when they are hidden is acceptable. Moreover, having separate
pop-ups for these would not have been easy to position without putting
them on top of the main step 2 itself and I do think that it is a bad
idea to prevent the reader from seeing both an assumption and its
complete proof.

I also chose not to add any ``callout'' pointers from the proof to the
assumption. I think that the differences in colours are sufficient to
avoid any mistake. Again, this is also a case display of what can be
done and how it looks like, hence it is good to have different layouts
to choose from.

Also, due to the shortness of the proofs, I was able to fan out all
the pop-ups without any covering another. This allows for a rather
nice result of the whole proof being visible if wanted.

\bigskip

As a closing word, I just want to mention that \switchocg{explul
  explhl}{\jymulhl{Explanations}{expl}{blue}{this technique is
    not\jymanchor{expl} restricted to proofs.}}

\begin{tikzpicture}[remember picture, overlay, ocg={name=Explanations HL,
    ref=explhl, status=invisible}]
  \coordinate (calloutexpl) at ($(anchorexpl) + (0,1.5ex)$);

  \node[draw=blue, fill=blue!20, rectangle callout, rounded corners,
  callout absolute pointer=(calloutexpl), text width=12cm] at
  ($(anchorexpl) + (-2cm,4cm)$) {Explanations in a running text can
    also be provided, for example, to detail some arguments in a
    discussion; or for parts of a text that are useful on the first
    read but can be omitted when rereading because they go into a lot
    of details to make a point but after being read once, one normally
    can remember the idea and do not need the wordy explanation
    again. Thus this technique is not restricted to sciences. It can
    also be used, taking example from some of my hobby fields, for:
    \begin{itemize}
    \item \switchocg{history}{Writing history texts and have pop-ups
        recalling dates or details of events mentioned in the
        text.}\\
      \begin{ocg}{History}{history}{off}
        ``After \switchocg{bartul barthl}{\jymulhl{St
            Bartholomew}{bart}{red}{St Bartholomew's\jymanchor{bart}
            day massacre}}, French protestants went into hiding.''%
      \end{ocg}%
    \item \switchocg{rule}{Writing game rules and recall some rule
        when it is referenced.}\\
      \begin{ocg}{Rule}{rule}{off}
        ``A stack with no \switchocg{losul loshl}{\jymulhl{Line of
            Supply}{los}{pink}{Line of\,\jymanchor{los} Supply}} may not
        besiege.''
      \end{ocg}
    \end{itemize}
  };
\end{tikzpicture}

\begin{tikzpicture}[remember picture, overlay, ocg={name=St
    Bartholomew HL, ref=barthl, status=invisible}]
  \coordinate (calloutbart) at ($(anchorbart) + (0,1.5ex)$);

  \node[draw=red, fill=red!20, rectangle, rounded corners, text
  width=8cm] at ($(calloutbart) + (0,2.5cm)$) {\textbf{Wikipedia}: On
    the night of 23â€“24 August 1572, two days after the attempted
    assassination of Admiral Gaspard de Coligny, the military and
    political leader of the Huguenots. The king ordered the killing of
    a group of Huguenot leaders, including Coligny, and the slaughter
    spread throughout Paris. Lasting several weeks, the massacre
    expanded outward to other urban centres and the
    countryside. Modern estimates for the number of dead across France
    vary widely, from 5,000 to 30,000.};
\end{tikzpicture}

\begin{tikzpicture}[remember picture, overlay, ocg={name=Line of
    Supply HL, ref=loshl, status=invisible}]
  \coordinate (calloutlos) at ($(anchorlos) + (0,1.5ex)$);

  \node[draw=pink, fill=pink!20, rectangle, rounded corners, text
  width=5cm] at ($(calloutbart) + (0,-3cm)$) {A Line of Supply goes
    from the Source of Supply to the stack and may not be more than
    12MP. See IX.7 for details.};
  \end{tikzpicture}

\vspace{-1cm}

\begin{thebibliography}{Lam12}
\bibitem[Lam12]{LamportProof}
Leslie Lamport.
\newblock How to write a 21st century proof.
\newblock {\em Journal of Fixed Point Theory and Applications}, March 2012.

\bibitem[Spi67]{Spivak}
Michael Spivak.
\newblock {\em Calculus}.
\newblock W. A. Benjamin, Inc., New York, 1967.
\end{thebibliography}

\end{document}

%%% Local Variables: %%%
%%% mode: latex %%%
%%% ispell-local-dictionary: "british" %%%
%%% End: %%%
%  LocalWords:
</pre></body></html>