I will attempt to explain how I would work out the problem. If my description is incomplete or wrong sure some more experienced reader will tell us.

I want to learn how to go about proving things like (p >>= j) >= k == p >>= (\x->(j x >>= k)) where p >>= k = \s0 -> let (s1, a) = p s0 in k a s1

First, I give the results of my (3-minute) analysis: Substitution of the given definition leads for the left-hand side to (\s0 -> let { (s1, a) = p s0 (s2, b) = j a s1 } in k b s2 ) The right-hand side is (\s0 -> let { (s1, a) = p s0 (s2, b) = j a s1 } in k b s2 ) These are clearly the same I used 3 main properties for the process: 1. Renaming of variables for example: (\x -> x + y) == (\z -> z + y) Changing x to z is legal here. However, we can not rename x to y because y is already used. So be carefull with renaming actions. 2. Lifting local let definitions to a higher level let f = let g = gExpr in fExpr in expr can be translated into let g = gExpr f = fExpr in expr The definition of g which is local for f in the first expression is made more global in the second one. The translation back is not always possible (impossible if g and f are mutual recursive, that is: use each other) 3. Lambda elimination (\x -> x + 3) y == y + 3 --------------------------------------------------- Complete example (left-hand side) ---------------------------------------------------

I want to learn how to go about proving things like (p >>= j) >= k == p >>= (\x->(j x >>= k)) where p >>= k = \s0 -> let (s1, a) = p s0 in k a s1

(p >== j) equals (\s0 -> let (s1, a) = p s0 in j a s1) rename s0, s1 and a to s2, s3 and b resp. (\s2 -> let (s3, b) = p s2 in j b s3) This avoids name-conflicts later on. Say this last expression is called f (just to make reading easier), so f == (\s2 -> let (s3, b) = p s2 in j b s3) f >= k equals (\s0 -> let (s1, a) = f s0 in k a s1) Now substitute de definition for f (\s0 -> let (s1, a) = (\s2 -> let (s3, b) = p s2 in j b s3) s0 in k a s1 ) Lambda elimination is the next step. ((\s2 -> ...) s0) is candidate for this step. The result is (\s0 -> let (s1, a) = let (s3, b) = p s0 in j b s3 in k a s1 ) This was the step which eliminated s2, so we can rename s3 to s2 now, just to remove the gap between s1 and s3: (\s0 -> let (s1, a) = let (s2, b) = p s0 in j b s2 in k a s1 ) At this point, lifting a local definition to a higher level comes in view: let (s1, a) = let (s2, b) = p s0 in j b s2 in ... is the same as let (s2, b) = p s0 (s1, a) = j b s2 in ... This yields (\s0 -> let (s2, b) = p s0 (s1, a) = j b s2 in k a s1 ) Which is the result above, except that the names of s1 and s2 are swapped. This makes no real difference though and a renaming action is enough to fix it. Now, try to write out the right-hand side yourself. These three transformations are enough for now. There are lots of such equality (or half- equality) transformations, but I don't know concrete resources. Others on the mailing list can probably point out some good resources. Rijk-Jan