Take the 2-minute tour ×
TeX - LaTeX Stack Exchange is a question and answer site for users of TeX, LaTeX, ConTeXt, and related typesetting systems. It's 100% free, no registration required.

Does anyone know of any packages that support this style of writing proofs?

A non-trivial example of "Structured Derivation" syntax, taken as a screenshot from Ralph-Johan Back's paper

The only things that I've found are: tex-ewd, a bunch of plain TeX macros on CTAN written specifically with Dijkstra in mind; and a Windows-only version of LyX that's been extended with support with structured derivations. (It's too bad that the LyX-SD is limited to Windows, because I'd guess that writing proofs in LyX would be wonderful)

In the case that there's nothing out there and that I have to roll my own, are there any packages that are similar enough that I could learn the "right way" to go about making a Structured Derivations package for LaTeX?

And I offer a pre-emptive "thank you" :) I'll be really grateful for any help.

If you need more information to be helpful (or even if I've just piqued your interest) here are some good resources:

share|improve this question
    
You can put the additional links without the http pershaps as code by tabbing 4 spaces and one of us of the moderators will activate the links. –  Yiannis Lazarides Mar 25 '12 at 19:30
    
There's a continuation/follow-up here about implementation. –  Josh Tilles Jun 16 '12 at 17:44

1 Answer 1

up vote 11 down vote accepted

I'd be tempted to use a sequence of itemize and enumerate environment, using the enumitem package to help with formatting

enter image description here

In the code below I've used the resume feature provided by the enumitem package to help keep the numbering of the enumerate environment without having to hardcode any of the numbers.

I've also used the optional argument of the \item command, which can be used, for example

\item[$\Vdash$]

If you plan to use this a lot though, you could always make this into a \newcommand

\documentclass{article}
\usepackage{geometry}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{enumitem}

% global settings for enumerate environment
\setlist[enumerate]{label*=(\arabic*),leftmargin=0mm}

% itemize environment, when at nested depths 2, 3, 4
\setlist[itemize,2]{label=\textbullet,leftmargin=1cm}
\setlist[itemize,3]{label=\textbullet,leftmargin=1cm}
\setlist[itemize,4]{label=\textbullet,leftmargin=1cm}

\begin{document}
\begin{itemize}
    \item Show that $f$ is continuous at $x_0$, when
        \begin{enumerate}
            \item\label{item:range} $f(x)=\sqrt{x}$ when $x\geq 0$, and
            \item\label{item:pos} $x_0>0$
        \end{enumerate}
    \item[$\Vdash$] $f$ is continuous at $x_0$
    \item[$\equiv$] $\{\text{definition of continuity}\}$

            $(\forall\epsilon>0\cdot \exists\delta>0\cdot\forall x\geq 0\cdot |x-x_0|<\delta\Rightarrow|f(x)-f(x_0)|<\epsilon)$
    \item[$\equiv$] $\{\text{choose arbitrary }\epsilon \text{generilization rule}\}$
    \begin{itemize}
        \item Show that $(\exists\delta>0\cdot\forall x\geq 0\cdot |x-x_0|<\delta\Rightarrow |f(x)-f(x_0)|<\epsilon)$, when
        \begin{enumerate}[resume]
            \item $\epsilon>0$
        \end{enumerate}
        \item[$\Vdash$] $\{\text{find a suitable value for } \delta\text{ witness rule}\}$
        \begin{itemize}
            \item Show that $\delta>0\wedge(\forall x\geq 0\cdot|x-x_0|<\delta\Rightarrow|f(x)-f(x_0)|<\epsilon)$, when
            \begin{enumerate}[resume]
                \item $\delta=?$ $\sharp$ $\delta=\epsilon\cdot\sqrt{x_0}$
            \end{enumerate}
            \item[$\Vdash$] $\{\text{show the two conjuncts separately, use generalization rule for second conjunct}\}$
            \begin{itemize}
                \item Show that $|f(x)-f(x_0)|<\epsilon$, when
                \begin{enumerate}[resume]
                    \item\label{item:xnonneg} $x\geq 0$, and
                    \item $|x-x_0|<\delta$
                \end{enumerate}
                \item[$\Vdash$] $|f(x)-f(x_0)|$
                \item[$=$] $\{$assumption \ref{item:range}, $f(x)$ and $f(x_0)$ are defined by assumptions \ref{item:xnonneg} and \ref{item:range}$\}$
                \item[] $|\sqrt{x}-\sqrt{x_0}|$
                \item[$=$] $\{$extend with conjugate value for $\sqrt{x}-\sqrt{x_0}$, i.e., with $\sqrt{x}+\sqrt{x_0}>0$$\}$
                \item[] $\dfrac{|x-x_0|}{\sqrt{x}+\sqrt{x_0}}$
                \item[$\leq$] $\{$make divisor smaller, $\sqrt{x}\geq 0$ $\}$
            \end{itemize}
        \end{itemize}
    \end{itemize}
\end{itemize}
\end{document}
share|improve this answer

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

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