[Haskell-cafe] bottom case in proof by induction

[Derek Elkins]

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.