mailing-list for TeXmacs Users

["David G. Wonnacott" <address@hidden>]

Hi fellow TeXmacs users ---

I'm working on formatting some examples for a course in which we teach students about algebraic substitution as a way to reason about code (formal semantics/verification). On the board, we use a format that's somewhat like the "two-column proof" from high-school math, except that the "justification" column on the right is offset so each entry is vertically between the two subsequent statement lines that it connects, rather than to the right of the statement it just transformed. I've got two challenges, one probably easy, the other potentially hard.

You may want to peek at the attached PDF files for things I've tried, to get a sense of what we're doing here. Note that we're still figuring out how much detail to use in this example (a simplified version of something from a lab involving the Fibonacci sequence), so the last "justification" line is still under discussion. Also, a Warning to Python-haters: for a variety of reasons I'd rather not get into, we use a pseudocode that's similar to Python, so please prepare yourself for some horror before looking at the attached files :-)


Problem 1: Horizontal Lines in Tables (easy?)

I'd like to have lines separating the "statement" elements, to the left of each justification. I'd like these lines centered vertically alongside the justification, so the easiest thing seems to be to just have a table row with a horizontal line on the left, and the justification on the right. Formatting this in LaTeX or TeXmacs is a bit tricky but quite possible: I've got something tolerable in LaTeX, though entering it is (as always) terribly tedious and annoying. TeXmacs is (as usual) much more fun, but I can't find enough online/Manual content to figure out how to get the line I want separating each pair of "statement" elements. It looks like "hrule" is perhaps what I want, but the hrule command seems to fill the page, not the column. I've done some online searches for other ways to make a horizontal line, and searched the online Manual for the documentation for hrule, but I don't see any way to control its width.

Any suggestions? If I just use a bottom border on each "statement" element, it doesn't line up properly. hrule makes the thing too wide, and any fixed-size line (such as three -'s) has to be re-defined for each table. (see the hrule and triple-minus PDF files attached).


Problem 2: Multi-line Justifications (very hard?)

In some cases, e.g. the third justification line of our example, we'd like to use longer justification lines, e.g. one or more "trivial" steps (typically just stated as "algebra") along with something of interest. We are often short of horizontal space, so I'd like to write above/below each other rather than across a line. But, of course, if I put several lines into that cell of the table, it pushes the "statement" rows apart, and I don't want that. Possibly I'd have to abandon the standard "table" system and write something new for offset tables, but that's way beyond my TeXmacs skill level at this point.


A Side-Issue (not critical): LaTeX import

I've also attached our LaTeX version, which currently relies on a fixed-size horizontal rule; importing it into TeXmacs would be somewhat nice, as that would simplify our software infrastructure somewhat, but that seems to be beyond the LaTeX import feature's ability at this time.


Thanks for any help you can provide,
   Dave W

Attachment: fig-exec-by-subst-symbolic-hrule.pdf
Description: Adobe PDF document

Attachment: fig-exec-by-subst-symbolic-triple-minus.pdf
Description: Adobe PDF document

<TeXmacs|1.0.7.18>

<style|generic>

<\body>
  The macro whatSep is defined here --\<gtr\>
  <assign|whatSep|<macro|<hrule>>> \<less\><emdash>. I've tried hrule and
  triple minus, but not yet gotten what I want. In particular, why is that
  table so huge with whatSep defined as hrule? I've already got width
  problems, but this just makes it <with|font-shape|italic|much> worse.

  \;

  <tabular|<tformat|<cwith|1|-1|2|2|cell-lborder|0.5mm>|<cwith|1|-1|1|1|cell-rsep|0mm>|<cwith|6|6|2|2|cell-hyphen|c>|<table|<row|<cell|<verbatim|<underline|2*>f<verbatim|ib(>n-1)
  - fib(n-3)>>|<cell|>>|<row|<cell|<whatSep>>|<cell|Expand constant
  *>>|<row|<cell|<verbatim|fib(n-1)+<underline|fib(n-1)> -
  fib(n-3)>>|<cell|>>|<row|<cell|<whatSep>>|<cell|Expand
  fib>>|<row|<cell|<verbatim|fib(n-1)+<tabular|<tformat|<table|<row|<cell|<math|<around*|\<llbracket\>||\<nobracket\>>>>|<cell|if
  (n-1) \<less\> 3:>|<cell|<math|>>>|<row|<cell|>|<cell| \ return
  1>|<cell|>>|<row|<cell|>|<cell|else:>|<cell|<math|<around*|\<rrbracket\>||\<nobracket\>>>>>|<row|<cell|>|<cell|
  \ return fib((n-1)-1)+fib((n-1)-2)>|<cell|>>>>>- fib(n-3)
  >>|<cell|>>|<row|<cell|<whatSep>>|<\cell>
    Negation of ``if'' test; algebra
  </cell>>|<row|<cell|<verbatim|fib(n-1)+<tabular|<tformat|<table|<row|<cell|<math|<around*|\<llbracket\>||\<nobracket\>>>>|<cell|if
  False:>|<cell|<math|>>>|<row|<cell|>|<cell| \ return
  1>|<cell|>>|<row|<cell|>|<cell|else:>|<cell|<math|<around*|\<rrbracket\>||\<nobracket\>>>>>|<row|<cell|>|<cell|
  \ return fib((n-1)-1)+fib((n-1)-2)>|<cell|>>>>>-
  fib(n-3)>>|<cell|>>|<row|<cell|<whatSep>>|<cell|if False
  rule>>|<row|<cell|<verbatim|fib(n-1)+<tabular|<tformat|<table|<row|<cell|<math|<around*|\<llbracket\>||\<nobracket\>>>>|<cell|
  \ return fib((n-1)-1)+fib((n-1)-2)>|<cell|<math|<around*|\<rrbracket\>||\<nobracket\>>>>>>>>-
  fib(n-3)>>|<cell|>>|<row|<cell|<whatSep>>|<cell|return
  <math|<around*|\<llbracket\>|\<ldots\>|\<rrbracket\>>>
  rule>>|<row|<cell|<verbatim|fib(n-1)+ (fib(n-2)+fib(n-3)) -
  fib(n-3)>>|<cell|>>|<row|<cell|<whatSep>>|<cell|algebra>>|<row|<cell|<verbatim|fib(n-1)+fib(n-2)>>|<cell|>>|<row|<cell|<whatSep>>|<cell|??
  rev def of fib ??? given n\<gtr\>2>>|<row|<cell|<verbatim|fib(n)>>|<cell|>>>>>

  \;

  \;

  This is some text after the table. This is some text after the table. This
  is some text after the table. This is some text after the table. This is
  some text after the table. This is some text after the table. This is some
  text after the table. This is some text after the table. This is some text
  after the table. This is some text after the table. This is some text after
  the table. This is some text after the table.\ 
</body>

Attachment: fig-exec-by-subst-symbolic-from-LaTeX.pdf
Description: Adobe PDF document

\documentclass{article}
\usepackage[utf8]{inputenc}

\usepackage{color}
\usepackage{mathtools}

\newcommand*{\xdash}[1][3em]{\rule[0.5ex]{#1}{0.3333pt}}

\newcommand{\capR}{\quad \\}
\newcommand{\what}[2]{{\tt \hspace{#1 em} #2} \capR}
\newcommand{\changed}[1]{{\underline{#1}}}
\newcommand{\clicked}[1]{{\color[rgb]{1,0.5,0}#1}}

\newcommand{\capL}{\multicolumn{1}{@{}r|}{\xdash[64mm]} & \xdash[6pt] \hspace{1mm}}
\newcommand{\why}[1]{\capL #1 \\}

\newcommand{\lambl}{$[\![$\ }	% other style was [\mid
\newcommand{\lambr}{$]\!]$}	% other style was \mid]
\newcommand{\lamb}[1]{\lambl #1 \lambr}

\begin{document}

\setlength\tabcolsep{0pt}
\begin{tabular}{l|l}
    \what{0}{\changed{power(x, 2)}}
        \why{Substitute function body, including parameter values}
    \what{0}{\lambl if (\changed{2==1}):}
    \what{2}{return x}
    \what{1}{else:}
    \what{2}{bttemo = power(x, \changed{2-1})}
    \what{2}{return x * bttemo \lambr}

    \why{Arithmetic}

    \what{0}{\lambl \changed{if (False)}:}
    \what{2}{\changed{return x}}
    \what{1}{\changed{else:}}
    \what{2}{bttemo = power(x, 1)}
    \what{2}{return x * bttemo \lambr }

        \why{if False rule}

    \what{0}{\lambl bttemo = \changed{power(x, 1)}}
    \what{1}{return x * bttemo \lambr }

        \why{Substitute function body, including parameter values}

    \what{0}{\lambl    bttemo$_1$ = \lambl}
    \what{4}{if (\changed{1==1}):}
    \what{4}{return x}
    \what{3}{else:}
    \what{4}{bttemo$_2$ = power(x, \changed{1-1})}
    \what{4}{return x * bttemo$_2$ \lambr}
    \what{1}{return x * bttemo$_1$ \lambr}

	\why{Arithmetic}

    \what{0}{\lambl    bttemo$_1$ = \lambl}
    \what{4}{\changed{if (True):}}
    \what{4}{return x}
    \what{3}{\changed{else:}}
    \what{4}{\changed{bttemo$_2$ = power(x, 0)}}
    \what{4}{\changed{return x * bttemo$_2$ \lambr}}
    \what{1}{return x * bttemo$_1$ \lambr}

	\why{if True rule}

    \what{0}{\lambl    bttemo$_1$ = \lambl \changed{         return x } \lambr}
    \what{1}{return x * bttemo$_1$ \lambr}

	\why{return \lambl ... \lambr \ rule}

    \what{0}{\lambl    bttemo$_1$ = x}
    \what{1}{return x * \changed{bttemo$_1$} \lambr}

	\why{variable substitution rule}

    \what{0}{\lambl return \changed{x * x} \lambr}

	\why{return \lambl ... \lambr \ rule}

    \what{0}{x * x}
\end{tabular}

\end{document}