On Wednesday 06 May 2009 4:26:15 pm Dan Doel wrote:
unfortunately it looks like I'm doing something wrong in that "coinductive hypothesis"
Sorry about the self-reply, but I realized where I went wrong. The principle of proof by coinduction for defining a function 'f' goes something like this (expressed all point-free like): if null . f = p' (and when not null) head . f = f' tail . f = f . g' then f = unfold p' f' g' now we have: null . (unfold p f g . h) = p . h = p' head . (unfold p f g . h) = f . h = f' tail . (unfold p f g . h) = unfold p f g . g . h = unfold p f g . h . g' = (unfold p f g . h) . g' now we have a system of equations for (unfold p f g . h) that fits the format, so by coinduction we have: unfold p f g . h = unfold p' f' g' And we're done. -- Dan