Equational Reasoning for Functional Programming

Question

How can I create equational reasoning proof like the ones in CS literatures:
  A + (B + C)
=   { Associativity }
  (A + B) + C
=   { Commutativity }
  (B + A) + C

I can't seem to find the right package except maybe with lhs2tex. Thanks!

Mico · Accepted Answer

A possible solution, using an align* environment.

documentclass{article}
usepackage{amsmath} % for 'align*' env.
begin{document}

begin{align*}
 &quad A + ( B + C ) 
=&qquad text{{ Associativity }} 
 &quad (A + B) + C 
=&qquad text{{ Commutativity }} 
 &quad (B+A)+C 
end{align*}

end{document}

user238301 · Answer

This is almost identical to the first example of the witharrows package documentation. There are many ways to customize things, but it does seem to match the requirements.
documentclass{article}
usepackage{witharrows}
begin{document}
$begin{WithArrows}
F&=A + (B + C) Arrow{Associativity}
&=  (A + B) + CArrow{Commutativity}
&=  (B + A) + C%<-------don't put  here 
end{WithArrows}$
end{document}

Equational Reasoning for Functional Programming

2 Answers

Add your own answers!

Ask a Question