lines/unlines and "inverse"

[Koen Claessen]

Lars Henrik Mathiesen wrote:

 | lines . unlines = id
 | unlines . lines . unlines == unlines
 | words . unwords . words = words

Don't be fooled by the information content of the second
equation -- the first equation directly implies it:

  unlines . lines . unlines    == {assoc (.)}
  unlines . (lines . unlines)  == {equation 1}
  unlines . id                 == {id is unit of (.)}
  unlines

I.e. in general, when f is g's left inverse:

  f . g == id

Then the following equation holds automatically:

  g . f . g == g

Regards,
/Koen.

--
Koen Claessen
http://www.cs.chalmers.se/~koen
Chalmers University, Gothenburg, Sweden.