A proof environment for LaTeX

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.

 \assumestep{A \lor (B\land C)}
   \step[pjmll]{A \lor B}{by \ref{step:nhsbp}}
  \casestep[fipkc]{B\land C}
   \step[sqjid]{B}{by \ref{step:fipkc}}
   \step[kurri]{A\lor B}{by \ref{step:sqjid}}
  \step[xefuc]{A \lor B}{by \ref{step:pjmll}, \ref{step:kurri}}
 \step[fhqna]{A \lor (B\land C) \rightarrow A \lor B}
                                        {by \ref{step:xefuc}}

Corresponding output:

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)))
   (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 ()
 (insert (five_random_letters)))

(global-set-key (kbd "C-c C-d") 'insert_five_random_letters)

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s