\documentclass[12pt, a4paper]{article} \usepackage[margin=1in]{geometry} \usepackage[T1]{fontenc} \renewcommand\floatpagefraction{.9} \renewcommand\rmdefault{ptm} \newcommand\COLORcom{MediumPurple} \newcommand\COLORkey{SeaGreen} \newcommand\COLORenv{MediumPurple} \newcommand\COLORpkg{Chocolate} \newcommand\COLORdef{blue} \renewcommand{\refname}{Bibliography} \usepackage[nottoc]{tocbibind} \usepackage{makeidx} \makeindex \newcommand*\indexkey[1]{\index{% #1 key@\texttt{\color{\COLORkey}#1} key}} \newcommand*\indexenv[1]{\index{% #1 environment@\texttt{\color{\COLORenv}#1} environment}} \newcommand*\indexcom[1]{\index{% #1 command@\texttt{\color{\COLORcom}\textbackslash #1} command}} \newcommand*\packagename[1]{\textsf{\color{\COLORpkg}#1}} \newcommand*\varsasresonly{\emph{[Variables-as-resource only.]}\index{variables-as-resource}} \newcommand*\Ienv[1]{% {\color{\COLORenv}\ttfamily #1}\indexenv{#1}} \newcommand*\Icom[1]{% {\color{\COLORcom}\ttfamily\textbackslash #1}\indexcom{#1}} \newcommand*\Ikey[1]{% {\color{\COLORkey}\ttfamily #1}\indexkey{#1}} \usepackage{ribbonproofs} \usepackage{framed} \definecolor{shadecolor}{rgb}{0.95,0.95,1} \usepackage{tkzexample} \colorlet{graphicbackground}{white} \colorlet{codebackground}{shadecolor} % \usepackage{listings} \lstset{% numbers=left, numberstyle=\tiny, stepnumber=5, basicstyle=\tt, columns=flexible } % \usepackage{standalone} \usepackage{filecontents} % Otherwise filecontents is % only available in preamble. \usepackage{fancyvrb} \makeatletter \renewcommand\FV@FontFamily{\color{\COLORdef}\ttfamily} \makeatother \DefineShortVerb{\"} \newcommand{\dotneq}{\mathrel{\not\doteq}} \newcommand\ls{\mathit{ls}} \newcommand\x{\texttt{x}} \newcommand\y{\texttt{y}} \renewcommand\t{\texttt{t}} \renewcommand\u{\texttt{u}} \newcommand\List{\mathit{list}} \newcommand*\rev[1]{#1^{\dagger}} \newcommand\z{\texttt{z}} \title{The \packagename{ribbonproofs} package} \author{John Wickerson} \date{Version 1.0 -- 26 June 2013} \begin{document} \maketitle \begin{abstract} \noindent The \packagename{ribbonproofs} package provides a mechanism for drawing ribbon proofs in \LaTeX{}. Ribbon proofs form a diagrammatic proof system, due to Wickerson, Dodds and Parkinson~\cite{wickerson+13}, for \emph{separation logic}~\cite{reynolds02}\index{separation logic}. They build on an earlier system, due to Bean~\cite{bean06}, for \emph{bunched implications logic}~\cite{ohearn+99}. \end{abstract} \tableofcontents \begin{figure} \begin{tkzexample}[] \documentclass{standalone} \usepackage{ribbonproofs} \begin{document} \def\to{\mapsto} \begin{ribbonproof}[start ribbons={ a/{left=0, right=16, label={\tt x}\to0}, b/{left=18, right=34, label={\tt y}\to0}, c/{left=36, right=52, label={\tt z}\to0}}] \com[finish ribbons={a}, start ribbons={ a/{label={\tt x}\to1}}]{[x]:=1} \\ \com[finish ribbons={b}, start ribbons={ b/{label={\tt y}\to1}}]{[y]:=1} \\ \com[finish ribbons={c}, start ribbons={ c/{label={\tt z}\to1}}]{[z]:=1} \\ \end{ribbonproof} \end{document} \end{tkzexample} \caption{A test document and its expected result} \label{fig:threeassign} \end{figure} \section{Getting started} \subsection{Installation} Place "ribbonproofs.sty" into the same directory as the ".tex" file you are compiling. To test that the package is working correctly, you might try to compile the little document given in Fig.~\ref{fig:threeassign}. The code is given on the lefthand side, with the expected output to the right. \subsection{A simple example} Figure~\ref{fig:threeassign} provides a good starting point for examining how the \packagename{ribbonproofs} package works. All the action takes place within the \Ienv{ribbonproof} environment. Upon entering this environment, we provide the \Ikey{start ribbons} key, in order to introduce some ribbons at the top of the diagram. We name them "a", "b" and "c", give the horizontal positions of their \Ikey{left} and \Ikey{right} edges, and provide a \Ikey{label}. We then proceed to build up the diagram in a series of rows, each terminated with \Icom{\textbackslash}. In this example, each row comprises a single \Icom{com} step (\Icom{com} stands for `command'). Each \Icom{com} has a number of optional parameters. The \Ikey{finish ribbons} key lists those ribbons that end at this step; they form the step's precondition. The \Ikey{start ribbons} key defines ribbons that begin at this step; they form the step's postcondition. Note that we used the same syntax (\Ikey{start ribbons}) to introduce some ribbons at the beginning of the proof. Each \Icom{com} has one mandatory parameter: the text, which is printed in white on the step. \section{Examples} \subsection{List append} Figure~\ref{fig:listappend} shows the result. \begin{filecontents*}{temp_example_listappend.tex} \begin{ribbonproof}[start ribbons={ c/{left=35,right=53,label=\ls\,\x\,0}, e/{left=74,right=86,label=\ls\,\y\,0}}] \startblock[extra left=33, extra right=2, fit ribbons={c,e}, start ribbons={ d/{left=\RIBcRIGHT+2,right=\RIBeLEFT-4,label=\x\doteq 0} }]{if (x==0) \{} \\ \jus[finish ribbons={c,d}]{Unfold $\ls$ def} \com[finish ribbons={e}, start ribbons={ e/{label=\ls\,\x\,0}}]{x:=y} \\[-6] \moveribbons{e/{left=4}} \\[-1] \continueblock[repeat labels, start ribbons={ d/{label=\x\dotneq 0}}]{\} else \{} \\[-1] \jus[start ribbons={ a/{left=6,right=\RIBcLEFT-2,label=\ls\,\x\,\x}}]{Fold $\ls$ def} \\[-4] \moveribbons{c/{left=20},a/{right=18}} \\[-4] \com[finish ribbons={a,c,d}, start ribbons={ a/{label=\ls\,\x\,\t}, c/{label=\ls\,\t\,0}, d/{label=\t\dotneq 0}}]{t:=x} \\ \jus[finish ribbons={c,d}, start ribbons={ c/{label=\exists U\ldotp\t\mapsto U * \ls\,U\,0}}]{Unfold $\ls$ def} \\ \com[finish ribbons={c}, start ribbons={ b/{left=\RIBcLEFT,right=33,label=\t\mapsto\u}, c/{left=35,right=\RIBcRIGHT,label=\ls\,\u\,0}}]{u:=[t]} \\ \startblock[fit ribbons={a}, extra left=2, extra right=2,start ribbons={ d/{label=\u\dotneq 0}}]{while (u!=0) \{} \\ \jus[finish ribbons={a,b,c}, height=10, start ribbons={ a/{right=\RIBbRIGHT, label=\ls\,\x\,\u}, c/{label=\ls\,\u\,0}}]{Lemma: $\ls\,a\,b *\ls\,b\,c * \ls\,c\,0$ \\ implies $\ls\,a\,c * \ls\,c\,0$} \\ \moveribbons{a/{right=18},c/{left=20}} \\[-3] \com[finish ribbons={a,c,d}, start ribbons={ a/{label=\ls\,\x\,\t}, c/{label=\ls\,\t\,0}, d/{label=\t\dotneq 0}}]{t:=u} \\ \jus[finish ribbons={c,d}, start ribbons={ c/{label=\exists U\ldotp\t\mapsto U * \ls\,U\,0}}]{Unfold $\ls$ def} \\ \com[finish ribbons={c}, start ribbons={ b/{left=\RIBcLEFT,right=33,label=\t\mapsto\u}, c/{left=35,right=\RIBcRIGHT,label=\ls\,\u\,0}}]{u:=[t]} \\ \finishblock[start ribbons={ d/{label=\u\doteq 0}}]{\}} \\ \jus[finish ribbons={b,c,d}, start ribbons={ b/{label=\t\mapsto0}}]{Unfold $\ls$ def} \\ \com[finish ribbons={b}, start ribbons={ b/{label=\t\mapsto\y}}]{[t]:=y} \\ \jus[finish ribbons={b,e}, start ribbons={ b/{right=\RIBeRIGHT,label=\ls\,\t\,0}}]{Fold $\ls$ def} \\ \jus[finish ribbons={a,b}, start ribbons={ a/{right=\RIBeRIGHT,label=\ls\,\x\,0}}]{ Lemma: $\ls\,a\,b * \ls\,b\,0$ implies $\ls\,a\,0$} \\ \finishblock{\}} \\ \end{ribbonproof} \end{filecontents*} \begin{shaded} \lstinputlisting{temp_example_listappend.tex} \end{shaded} \begin{figure} \small\centering \include{temp_example_listappend} \caption{A ribbon proof of list append} \label{fig:listappend} \end{figure} \clearpage \subsection{List reverse} Figure~\ref{fig:listrev} shows the result. \begin{filecontents*}{temp_example_listrev.tex} \begin{ribbonproof}[start ribbons={ b/{left=20,right=38,label=\List\,\delta\,\x}}] \com[start ribbons={ c/{left=40,right=78,label=\List\,\varepsilon\,\y}}]{y:=0}; \\ \jus[finish ribbons={b,c}, start ribbons={ b/{label=\List\,\alpha\,\x}, d/{label=\delta\doteq \rev{\beta}\cdot\alpha, left=60, right=\RIBcRIGHT}, c/{label=\List\,\beta\,\y, right=58} }, start boxes={ alpha/{left=14,right=82,label=\exists\alpha,color=SeaGreen}, beta/{left=18,right=80,label=\exists\beta,color=MediumPurple} }]{Choose $\alpha:=\delta$ and $\beta:=\varepsilon$} \\ \startblock[fit boxes={alpha}, extra left=10, extra right=2, start ribbons={ a/{left=0,right=10,label=\x\dotneq 0}}]{while (x!=0) \{} \\ \extendboxes{alpha/{left=-4}} \\[-9] \extendboxes{beta/{left=-8}} \\[-9] \jus[finish ribbons={a,b}, start ribbons={ ab/{left=\RIBaLEFT, right=\RIBbRIGHT, label={\exists\alpha',i,Z\ldotp\x\mapsto i,Z \\ {} * \List\,\alpha'\,Z * \alpha \doteq i \cdot \alpha'}} }]{Unfold $\List$ def} \\[-11] \moveribbons{ c/{left=70,right=\RIBdRIGHT}, d/{left=40,right=64}} \moveboxes{ alpha/{right=\RIBdRIGHT+4}} \\[4] \jus[finish boxes={alpha}, start boxes={ alpha/{label=\exists\alpha}, i/{left=\RIBabLEFT-2,right=\RIBdRIGHT+2,color=Chocolate, vertical offset=10,label=\exists i} }, finish ribbons={ab,d}, start ribbons={ ab/{label={\exists Z\ldotp\x \mapsto i,Z * \List\,\alpha\,Z}}, d/{label=\delta\doteq \rev{\beta}\cdot(i\cdot\alpha)} }]{Choose $\alpha:=\alpha'$} \\ \com[finish ribbons={ab}, start ribbons={ a/{right=14,label=\List\,\alpha\,\z}, b/{label={\x\mapsto i,\z}} }]{z:=[x+1]} \moveribbons{ c/{left=\RIBdLEFT, right=50}, d/{left=52, right=76}} \moveboxes{ alpha/{left=-8,right=82}, beta/{left=-6}, i/{right=78}} \\ \com[finish ribbons={b}, start ribbons={ b/{label={\x\mapsto i,\y}}}]{[x+1]:=y} \jus[finish ribbons={d}, start ribbons={ d/{label={\delta\doteq \rev{(i\cdot\beta)}\cdot\alpha}}}] {Reassociate $i$} \moveboxes{ i/{left=\RIBbLEFT-2}, beta/{left=\RIBbLEFT-4}} \\ \jus[finish ribbons={b,c}, start ribbons={ c/{left=\RIBbLEFT,label={\List (i\cdot\beta)\,\x}}}]{Fold $\List$ def} \\ \jus[finish ribbons={c,d}, finish boxes={i,beta}, start boxes={ beta/{vertical offset=10,horizontal offset=2,label=\exists\beta}}, start ribbons={ c/{label={\List\,\beta\,\x}}, d/{label={\delta\doteq\rev{\beta}\cdot\alpha}}}] {Choose $\beta:=(i\cdot\beta)$} \\[-6] \moveribbons{ d/{left=60,right=78}, c/{left=40,right=58}, a/{left=20,right=38}} \moveboxes{ alpha/{left=14}, beta/{left=18}} \\ \com[finish ribbons={c}, start ribbons={ c/{label={\List\,\beta\,\y}}}]{y:=x} \\[-5] \com[finish ribbons={a}, start ribbons={ b/{left=\RIBaLEFT,right=\RIBaRIGHT,label={\List\,\alpha\,\z}}}]{x:=z} \\ \finishblock[start ribbons={ a/{left=0,right=10,label={\x\doteq 0}} }]{\}} \\ \extendboxes{alpha/{left=-8}} \\[-9] \extendboxes{beta/{left=-6}} \\[-9] \jus[finish ribbons={a,b},start ribbons={ a/{right=\RIBbRIGHT,label=\alpha\doteq \varepsilon}}] {Unfold $\List$ def} \swapribbons{c,d}{d,c} \\ \jus[finish ribbons={a,d}, start ribbons={ a/{right=\RIBdRIGHT,label=\delta\doteq\rev{\beta}}}] {Concatenate empty sequence} \\ \jus[finish ribbons={a,c}, finish boxes={alpha,beta}, start ribbons={ a/{right=\RIBcRIGHT,label={\List\,\rev{\delta}\,\y}}}] {Fold $\List$ def} \\ \end{ribbonproof} \end{filecontents*} \begin{shaded} \lstinputlisting{temp_example_listrev.tex} \end{shaded} \begin{figure} \small\centering \include{temp_example_listrev} \caption{A ribbon proof of list reverse} \label{fig:listrev} \end{figure} \clearpage \subsection{List reverse with variables-as-resource} Figure~\ref{fig:listrevvar} shows the result. \begin{filecontents*}{temp_example_listrevvar.tex} \begin{ribbonproof}[start ribbons={ b/{left=20,right=38,var width=5,label=\x&\List\,\delta\,\x}, e/{left=40,right=45, var width=5,label=\z&}, c/{left=50,right=55, var width=5,label=\y&}}] \jus[finish ribbons={b}, start ribbons={ a/{left=-5,right=0,var width=5, label={\frac12\x&}}, b/{label={\frac12\x&\List\,\delta\,\x}} }]{Split $\x$} \com[finish ribbons={c},start ribbons={ c/{left=50,right=88,label=\y&\List\,\varepsilon\,\y}}]{y:=0}; \\ \jus[finish ribbons={b,c}, start ribbons={ b/{label=\frac12\x&\List\,\alpha\,\x}, c/{label=\y&\List\,\beta\,\y, right=68}, d/{label=\delta\doteq \rev{\beta}\cdot\alpha, left=70, right=88} }, start boxes={ alpha/{left=14,right=94,label=\exists\alpha,color=SeaGreen}, beta/{left=18,right=92,label=\exists\beta,color=MediumPurple} }]{Choose $\alpha:=\delta$ and $\beta:=\varepsilon$} \\ \startblock[fit boxes={alpha}, extra left=10, extra right=2, finish ribbons={a}, start ribbons={ a/{left=-5,right=10,label=\frac12\x&\x\dotneq 0}}]{while (x!=0) \{} \\ \extendboxes{alpha/{left=-9}} \\[-9] \extendboxes{beta/{left=-13}} \\[-9] \jus[finish ribbons={a,b}, start ribbons={ ab/{left=\RIBaLEFT, right=\RIBbRIGHT, var width=5, label={\x&\exists\alpha',i,Z\ldotp\x\mapsto i,Z \\{} * \List\,\alpha'\,Z * \alpha \doteq i \cdot \alpha'}}}] {Unfold $\List$ def} \moveboxes{ alpha/{right=92}, beta/{right=94}} \\[4] \jus[finish boxes={alpha}, start boxes={ alpha/{label=\exists\alpha}, i/{left=-7,right=90,color=Chocolate, vertical offset=11,label=\exists i} }, finish ribbons={ab,d}, start ribbons={ ab/{label={\x&\exists Z\ldotp\x \mapsto i,Z * \List\,\alpha\,Z}}, d/{label=\delta\doteq{}\\\rev{\beta}\cdot(i\cdot\alpha)} }]{Choose $\alpha:=\alpha'$} \\ \com[finish ribbons={ab,e}, start ribbons={ a/{right=14,label=\frac12\z&\List\,\alpha\,\z}, b/{var width=10,left=16,right=\RIBeRIGHT, label={\x,\frac12\z&\x\mapsto i,\z}} }]{z:=[x+1]} \jus[finish ribbons={c}, start ribbons={ cc/{left=57, right=\RIBcRIGHT, var width=5, rotated label={\List\,\beta\,\y}, label=\frac12\y&}, c/{right=55, label=\frac12\y&} }]{Split $\y$} \moveboxes{alpha/{left=-11}} \\ \com[finish ribbons={b,c}, start ribbons={ b/{var width=5,right=21, label=\frac12\z&}, c/{left=27, var width=10,label={\x,\frac12\y&\x\mapsto i,\y}} }]{[x+1]:=y} \jus[finish ribbons={d}, start ribbons={ d/{label={\delta\doteq {}\\ \rev{(i\cdot\beta)}\cdot\alpha}}}]{Reassoc. $i$} \\[-6] \moveboxes{ i/{left=25}, beta/{left=23,right=92}, alpha/{right=94}} \\ \jus[finish ribbons={a,b}, start ribbons={ a/{right=\RIBbRIGHT, label={\z&\List\,\alpha\,\z}} }]{Combine $\z$} \jus[finish ribbons={c,cc}, start ribbons={ c/{var width=5, label={\x&\List (i\cdot\beta)\,\x}}, cc/{left=63, label=\y&} }]{Fold $\List$ def} \\ \jus[finish ribbons={c,d}, finish boxes={i,beta}, start boxes={ beta/{horizontal offset=2,label=\exists\beta}}, start ribbons={ c/{label={\List\,\beta\,\x}, label=\x&}, d/{label={\delta\doteq\rev{\beta}\cdot\alpha}}}] {Choose $\beta:=(i\cdot\beta)$} \\[-2] \moveribbons{c/{left=43,right=61},a/{left=20,right=41}} \moveboxes{alpha/{left=14},beta/{left=18}} \\ \com[finish ribbons={c,cc}, start ribbons={ e/{left=\RIBcLEFT, right=\RIBcLEFT+5, label=\x&}, c/{left=50,right=\RIBccRIGHT,label={\List\,\beta\,\y}, label=\y&} }]{y:=x} \\ \com[finish ribbons={a,e}, start ribbons={ b/{left=\RIBaLEFT,right=\RIBaRIGHT,label=\frac12\x&\List\,\alpha\,\x}, a/{left=-5,right=0,var width=5, label=\frac12\x&}, e/{label=\z&} }]{x:=z} \\ \finishblock[finish ribbons={a},start ribbons={ a/{right=10,label={\frac12\x&\x\doteq 0}} }]{\}} \\ \extendboxes{alpha/{left=-8}} \\[-9] \extendboxes{beta/{left=-6}} \\[-9] \jus[finish ribbons={a,b},start ribbons={ a/{right=0, label=\x&}, b/{left=6,label=\alpha\doteq \varepsilon, var width=0} }]{Unfold $\List$ def} \moveribbons{ d/{left=43,right=48}, e/{left=74,right=79} } \moveboxes{ alpha/{right=72}, beta/{right=70}} \\ \jus[finish ribbons={b,d}, start ribbons={ b/{right=\RIBdRIGHT,label=\delta\doteq\rev{\beta}} }]{Concatenate empty seq.} \moveboxes{alpha/{left=2},beta/{left=4}} \\ \jus[finish ribbons={b,c}, finish boxes={alpha,beta}, start ribbons={ c/{label={\y&\List\,\rev{\delta}\,\y}} }]{Fold $\List$ def} \\ \end{ribbonproof} \end{filecontents*} \begin{shaded} \lstinputlisting{temp_example_listrevvar.tex} \end{shaded} \begin{figure} \small\centering \include{temp_example_listrevvar} \caption{A ribbon proof of list reverse using variables-as-resource} \label{fig:listrevvar} \end{figure} \clearpage \section{Reference} \subsection{Package dependencies} The \packagename{ribbonproofs} package relies upon: \begin{itemize} \item the \packagename{xcolor} package for colours; \item the \packagename{tikz} package, plus its \packagename{calc}, \packagename{fadings} and \packagename{decorations.pathmorphing} libraries, for drawing; \item the \packagename{xstring} package for manipulating strings; and \item the \packagename{etextools} package for controlling the expansion of \TeX{} macros. \end{itemize} \subsection{The \Ienv{ribbonproof} environment} \begin{description} \item "\begin{"\Ienv{ribbonproof}"}["$\mathit{options}$"]"$\ldots$"\end{"\Ienv{ribbonproof}"}" \quad This is the top-level environment for creating ribbon proofs. All of the ribbon-proof-building commands must only appear inside this environment. Available $\mathit{options}$ are: \begin{description} \item \Ikey{extra height}"="$n$ \quad (Default: "0".) This option adds $n$ (an integer or integer expression) to the height of the diagram's first row. \item \label{key:startribbons}\Ikey{start ribbons}"={"$\mathit{ribbon}_1$","$\dots$","$\mathit{ribbon}_k$"}" \quad (Default: empty.) This defines a list of $k$ ribbons that henceforth are \emph{active}. Each $\mathit{ribbon}$ takes the form \begin{center} $\mathit{name}$"/{"$\mathit{options}$"}" \end{center} where $\mathit{name}$ is an alphabetic string that henceforth identifies the ribbon, and the available $\mathit{options}$ are: \begin{description} \item \Ikey{left}"="$n$ \quad (Default: "0".) The horizontal position of the ribbon's left edge. The value $n$ must either be an integer or an expression that evaluates to an integer. The value is stored in the command \Icom{RIBnameLEFT}, where "name" is the name of the ribbon. Ribbons can be positioned relatively by accessing this value. For instance, one can write "left=\RIBfooLEFT-20" to set the current ribbon's left edge 20 units to the left of the ribbon "foo"'s left edge. \item \Ikey{right}"="$n$ \quad (Default: "0".) The horizontal position of the ribbon's right edge. The value $n$ must either be an integer or an expression that evaluates to an integer. The value is stored in the command \Icom{RIBnameRIGHT}, where "name" is the name of the ribbon. \item \Ikey{label}"="$L$ \quad (Default: empty.) The label that is written on the ribbon. The value $L$ is parsed in math-mode. There are three complications here. \begin{itemize} \item If $L$ contains a comma or an equals-sign, it must be wrapped in braces; otherwise the parser will become confused. For instance, be sure to write "label={0