Brent Yorgey byorgey at seas.upenn.edu
Wed May 19 11:30:31 EDT 2010

```On Wed, May 19, 2010 at 01:37:49PM +0000, R J wrote:
>
> This is another proof-layout question, this time from Bird 1.4.7.
> We're asked to define the functions curry2 and uncurry2 for currying and uncurrying functions with two arguments.  Simple enough:
> curry2             :: ((a, b) -> c) -> (a -> (b -> c))curry2 f x y       =  f (x, y)
> uncurry2           :: (a -> (b -> c)) -> ((a, b) -> c)uncurry2 f (x, y)  =  f x y
> The following two assertions are obviously true theorems, but how are the formal proofs laid out?

There are lots of variations, I wouldn't say there's one "right" way
to organize/lay out the proofs.  But here's how I might do it:

curry2 (uncurry2 f) x y
=                      { def. of curry2 }
uncurry2 f (x,y)
=                      { def. of uncurry2 }
f x y

I'll let you do the other one.

By the way, are you working through these problems just for
self-study, or is it homework for a class?

-Brent
```