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)

Advertisements