A visual proof of an identity involving triangular numbers, created for this blog post, which also contains several other similar proofs.

Author: Brent Yorgey

Download raw source code

> import Diagrams.Backend.SVG.CmdLine
> {-# LANGUAGE NoMonomorphismRestriction #-}
> import Diagrams.Prelude hiding (dot)
> 
> import Data.Colour

Draw a group of dots in a triangular array, all with the same color and backed by a solid-colored triangle to visually group them. Note how the dots are laid out by creating a trail called edge, rotating it 60 degrees, and using decorateTrail to lay out the rows of dots.

> mkTri c n = dots <> (strokeLoop edges # lc c # lw thin # fcA (c `withOpacity` 0.5))
>   where rows = map (hcat' (with & sep .~ 1 ))
>              . zipWith replicate [n,n-1..1]
>              . repeat
>              $ dot c
>         dots = cat' v (with & sep .~ 3 & catMethod .~ Distrib) rows
>         v = rotateBy (1/6) unitX
>         edge = fromOffsets . replicate (n-1) $ unitX # scale 3
>         edges = glueLine (edge <> rotateBy (1/3) edge <> rotateBy (2/3) edge)
> 
> dot c = unitCircle
>       # lw none
>       # fc c
> 
> rowSpc = height (rotateBy (1/6) $ strutY 1 :: D V2 Double)

row k n s c draws a row of k size-n triangles with color c, separated by enough space for s dots.

> row k n s c = hcat' (with & sep .~ 1 + 3*s) (replicate k (mkTri c n))

The visual proof, which simply consists in assembling various sub-triangles into a larger triangle, using appropriately transformed and aligned instances of row.

> law4 k n c1 c2 = vcat' (with & sep .~ rowSpc) (map tRow [1..k])
>   where tRow k = (row k n 0 c1 # centerX # alignT)
>                  <>
>                  (row (k-1) (n-1) 1 c2 # reflectY # centerX # alignT)

Finally, create a row of diagrams showing the proof at different sizes.

> exampleRow f = hcat' (with & sep .~ 4) . map f --(alignB . f)
> 
> law4Dia = exampleRow law4' [2..4]
>   where law4' k = law4 k 3 purple gold
> 
> example = law4Dia # frame 0.2
> main = mainWith (example :: Diagram B)