[Haskell-cafe] Help with Bird problem 3.3.3

[Ryan Ingram]

Try starting with
   (m * n) / m = n  -- given m /= 0

Then do case analysis on n.

I found this process quite enlightening, thanks for posting.

  -- ryan

2009/2/24 Peter Hilal <peter at hilalcapital.com>:
> 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.
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
>