  Equational reasoning is among the most important tools that functional
programming provides us. Curiously, relatively less attention has been paid to
reasoning about monadic programs.
  In this report we derive a backtracking algorithm for problem specifications
that use a monadic unfold to generate possible solutions, which are filtered
using a $\mathit{scanl}$-like predicate. We develop theorems that convert a
variation of $\mathit{scanl}$ to a $\mathit{foldr}$ that uses the state monad,
as well as theorems constructing hylomorphism. The algorithm is used to solve
the $n$-queens puzzle, our running example. The aim is to develop theorems and
patterns useful for the derivation of monadic programs, focusing on the
intricate interaction between state and non-determinism.
