The johnproof style file provides an environment for typesetting proofs. Features include:

- It automatically handles page breaks, for those occasions when a long proof splits over multiple pages.
- It deals with assumptions and case splits.
- It assigns a label to each step in the proof, for referencing.
- It indicates the scope of each assumption using vertical lines and indentation.

Known bug: the spacing before and after the proof isn’t great, so it’s best to leave a blank line before `\begin{johnproof}`

and after `\end{johnproof}`

.

Example usage:

The proof is as follows.
\begin{johnproof}
\assumestep{A \lor (B\land C)}
\casestep[nhsbp]{A}
\step[pjmll]{A \lor B}{by \ref{step:nhsbp}}
\assumed
\casestep[fipkc]{B\land C}
\step[sqjid]{B}{by \ref{step:fipkc}}
\step[kurri]{A\lor B}{by \ref{step:sqjid}}
\assumed
\step[xefuc]{A \lor B}{by \ref{step:pjmll}, \ref{step:kurri}}
\assumed
\step[fhqna]{A \lor (B\land C) \rightarrow A \lor B}
{by \ref{step:xefuc}}
\end{johnproof}

Corresponding output:

For generating the random letter sequences used to label steps of a proof, I recommend the following *emacs* macro, made by Tom Ridge.

(defun five_random_letters ()
(let ((my_letters '"abcdefghijklmnopqrstuvwxyz")
(r1 (random 26)) (r2 (random 26)) (r3 (random 26))
(r4 (random 26)) (r5 (random 26)))
(concat
(substring my_letters r1 (+ r1 1))
(substring my_letters r2 (+ r2 1))
(substring my_letters r3 (+ r3 1))
(substring my_letters r4 (+ r4 1))
(substring my_letters r5 (+ r5 1)))
))
(defun insert_five_random_letters ()
(interactive)
(insert (five_random_letters)))
(global-set-key (kbd "C-c C-d") 'insert_five_random_letters)

### Like this:

Like Loading...