proofs

[Rijk-Jan van Haaften]

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