3

I am trying to typeset a structured proof as demonstrated by Leslie Lamport in his paper How to Write a 21st Century Proof. In particular, I am trying to typeset Figure 3 (shown below).

enter image description here

My code and the output is shown below.

\documentclass[12pt,letterpaper]{article}

\usepackage{amsmath}
\usepackage{amsthm}
\usepackage{enumitem}

% LSP is short for Lamport Structured Proof
\newlist{lsp}{enumerate}{10}
\setlist[lsp]{label=\arabic*.}
\newcommand{\lspproof}{{\scshape Proof:\ \ }}
\newcommand{\lspqed}{Q.E.D.}

\newtheorem{corollary}{Corollary}

\begin{document}

\begin{corollary}
If $f'(x) > 0$ for all $x$ on an interval $I$,
then $f$ is increasing on $I$.
\end{corollary}

\begin{lsp}
    \item It suffices to assume
        \begin{lsp}
        \item $a$ and $b$ are points in $I$
        \item $a < b$
        \end{lsp}
    \lspproof By definition of an increasing function

    \item There is some $x$ in $(a,b)$
    with $\displaystyle f'(x) = \frac{f(b)-f(a)}{b-a}$.\\*
    \lspproof By assumptions 1.1 and 1.2,
    the hypothesis that $f$ is differentiable on $I$,
    and the Mean Value Theorem.

    \item $f'(x) > 0$ for all $x$ in $(a,b)$.\\*
    \lspproof By the induction hypothesis of the corollary and assumption 1.1.

    \item $\displaystyle \frac{f(b)-f(a)}{b-a} > 0$\\*
    \lspproof By 2 and 3.

    \item \lspqed\\*
    \lspproof Assumption 1.2 implies $b - a > 0$,
    so 4 implies $f(b) - f(a) > 0$,
    which implies $f(b) > f(a)$.
    By 1, this proves the corollary
\end{lsp}


\end{document}

enter image description here

While I am quite happy with the result, I find it a bit irritating that I have to manually tell LaTeX to start a new line using \\* before each \lspproof.

Questions:

  1. Is there a way to define \lspproof such that it will automatically start a new line when needed? Notice that I did not need to insert \\* before the "Proof:" in step 1 because the "Proof:" occurs after an enumerate environment.
  2. Is there a way to slightly increase the vertical space between the "Proof." from \lspproof and the previous line?
  • 1
    We could just ask Leslie for the code :-) – Joseph Wright Feb 28 '14 at 22:23
  • 1
    I don't know him personally, or rather I know who he is but he doesn't know who I am. However, I would love it for you or anyone else to ask him. :-) – I Like to Code Feb 28 '14 at 22:25
4

Here's one option that uses a paragraph break rather than a forced line break:

enter image description here

\documentclass[12pt,letterpaper]{article}

\usepackage{amsmath,amsthm,enumitem}

% LSP is short for Lamport Structured Proof
\newlist{lsp}{enumerate}{10}
\setlist[lsp]{label=\arabic*.,ref=\arabic*}
\newcommand{\lspproof}{\par\nobreak{\scshape Proof:}\quad}
\newcommand{\lspqed}{Q.E.D.}

\newtheorem{corollary}{Corollary}

\begin{document}

\begin{corollary}
If $f'(x) > 0$ for all $x$ on an interval~$I$, then $f$ is increasing on~$I$.
\end{corollary}

\begin{lsp}
  \item It suffices to assume \label{proof1}
    \begin{lsp}
    \item $a$ and~$b$ are points in~$I$ \label{assump1}
    \item $a < b$ \label{assump2}
    \end{lsp}
  \lspproof By definition of an increasing function.

  \item There is some~$x$ in $(a,b)$ with $ f'(x) = \dfrac{f(b)-f(a)}{b-a}$. \label{proof2}
  \lspproof By assumptions~\ref{proof1}.\ref{assump1} and~\ref{proof1}.\ref{assump2}, the hypothesis that~$f$ is differentiable on~$I$,
  and the Mean Value Theorem.

  \item $f'(x) > 0$ for all $x$ in $(a,b)$. \label{proof3}
  \lspproof By the induction hypothesis of the corollary and assumption~\ref{proof1}.\ref{assump1}.

  \item $\dfrac{f(b)-f(a)}{b-a} > 0$ \label{proof4}
  \lspproof By~\ref{proof2} and~\ref{proof3}.

  \item \lspqed
  \lspproof Assumption~\ref{proof1}.\ref{assump2} implies $b - a > 0$, so~\ref{proof4} implies $f(b) - f(a) > 0$, which implies $f(b) > f(a)$.
  By~\ref{proof1}, this proves the corollary
\end{lsp}


\end{document}

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.