# [Haskell-cafe] Help with Bird problem 3.3.3

Peter Hilal peter at hilalcapital.com
Tue Feb 24 10:25:56 EST 2009

```I'm working my way through Bird's _Introduction to Functional
Programming Using Haskell_. I'd appreciate any help with problem
3.3.3, which is:

"Division of natural numbers can be specified by the condition (n *
m) / n = m for all positive n and all m.  Construct a program for
division and prove that it meets the specification."

The required construction relies on the following definitions:

data Nat        = Zero| Succ Nat

(+)             :: Nat -> Nat
m + Zero        =  m
m + Succ n      =  Succ (m + n)

(*)             :: Nat -> Nat
m * Zero        =  Zero
m * Succ n      =  m * n + m

Proceeding as Bird does in Sec. 3.2.2, where he derives the definition
of "-" from the specification "(m + n) - n = m", I've so far gotten
the first case, in which m matches the pattern "Zero", simply by (i)
substituting Zero for m in the specification, (ii) substituting Succ n
for n in the specification (solely because n is constrained to be
positive), and (iii) reducing by applying the first equation of "*":

Case Zero:

(Succ n * Zero) / Succ n = Zero
≡  {first equation of "*"}
Zero / Succ n = Zero

Easy enough, and completely intuitive, since we expect Zero divided by
any non-Zero finite number to be Zero.  The next case, in which m
matches the pattern "Succ m", is where I get stuck, and I really have
no intuition about what the definition is supposed to be.  My first
step is to substitute "Succ m" for "m" in the given specification, and
to substitute Succ n for n in the specification (for the same reason,
as above, that n is constrained to be positive), and then to use the
definition of "*" to reduce the equation:

Case Succ m:

Succ n * Succ m / Succ n = Succ m
≡  {second equation of "*"}
(Succ n * m + Succ n) / Succ n = Succ m

Where do I go from here?  Thank you so much.
-------------- next part --------------
An HTML attachment was scrubbed...
```