pearls-ch10-equational_reasoning.txt

hub ws (x : xs)
= minimum [is ++ nub ((x : xs) \\ is) | is <- inits ws]
= minimum [is ++ nub ((x : xs) \\ is) | is <- inits (us ++ vs)]
= minimum [is ++ nub ((x : xs) \\ is) | is <- inits us ++ map (us ++) (inits+ vs)]
= minimum ([is ++ nub ((x : xs) \\ is) | is <- inits us] ++ [is ++ nub ((x : xs) \\ is) | is <- map (us ++) (inits+ vs)])
= minimum ([is ++ nub ((x : xs) \\ is) | is <- inits us] ++ [us ++ is ++ nub ((x : xs) \\ (us ++ is)) | is <- inits+ vs])
= min (minimum [is ++ nub ((x : xs) \\ is) | is <- inits us]) (minimum [us ++ is ++ nub ((x : xs) \\ (us ++ is)) | is <- inits+ vs])
= min A B

A, when x not in xs
= minimum [is ++ nub ((x : xs) \\ is) | is <- inits us]
= minimum [is ++ [x] ++ nub (xs \\ is) | is <- inits us] -- This is allowed because by definition of us, x is not in us, and is is drawn from us
{ since us < is ++ [x] for is in inits us } -- This is true because x is greater than every element of us
 also, us ++ [x] <= is ++ [x], and nub (xs \\ us) <= nub (xs \\ is)
= us ++ [x] ++ nub (xs \\ us)
{ since nub xs = hub [] xs }
us ++ [x] ++ hub [] (xs \\ us)

A, when x in xs
= minimum [is ++ nub ((x : xs) \\ is) | is <- inits us]
= minimum [is ++ nub (x : (xs \\ is)) | is <- inits us] -- This is allowed because by definition of us, x is not in us, and is is drawn from us
{ recursive definition of nub since x in xs and x not in us } -- who said it's not in us? oh, by definition of (us, vs)
= minimum [is ++ ([x] ++ nub (xs \\ (is ++ [x])) `min` nub (xs \\ is))
  | is <- inits us]
{ taking min outside the comprehension }
= minimum [is ++ ([x] ++ nub (xs \\ (is ++ [x])) | is <- inits us] `min`
  minimum [nub (xs \\ is) | is <- inits us]
{ since us < is ++ [x] for is <- inits us } -- This is true for the same reason as in the last case
(us ++ [x] ++ nub (xs \\ (us ++ [x]))) `min` minimum [is ++ nub (xs \\ is) | is <- inits us]
minimum [is ++ nub (xs \\ is) | is <- inits us] `min` (us ++ [x] ++ nub (xs \\ us ++ [x]))
minimum [is ++ nub (xs \\ is) | is <- inits us] `min` minimum [is ++ nub (xs \\ is) | is <- [us ++ [x]]]
minimum [is ++ nub (xs \\ is) | is <- inits us ++ [us ++ [x]])]
{ since inits (us ++ [x]) = inits us ++ [us ++ [x]] } -- ? neither of these patterns occurs in the previous line
minimum [is ++ nub (xs \\ is) | is <- inits (us ++ [x]))]