[Haskell-cafe] Help with Bird problem 3.3.3

[Peter Hilal]

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...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20090224/7b6a8767/attachment.htm