Re: [Haskell-cafe] bottom case in proof by induction

On Thu, 2009-01-01 at 02:16 +0100, Martijn van Steenbergen wrote:

Luke Palmer wrote:

...

First, by simple definition, id _|_ = _|_. Now let's consider foo _|_. The Haskell semantics say that pattern matching on _|_ yields _|_, so foo _|_ = _|_. So they are equivalent on _|_ also. Thus foo and id are exactly the same function.

Would it in general also be interesting to look at foo == id for input (_|_:xs) and all other possible positions and combinations of positions for bottom? I wonder how many cases you need to take into consideration to have covered every possible situation.

That case is already covered by the (x:xs) case. The interesting, potentially "extra", case is an infinite list.