Dave Tapley dukedave at gmail.com
Mon Jun 25 15:41:56 EDT 2007

```Hopefully this is just about on topic enough..
(Oh and it's not home work, I just can't bring myself to let it go!)

Taken from "Simon Thompson: Type Theory and Functional Programming"

Section 1.1
Exercise 1.3

Question: Give a proof of (A => (B => C)) => ((A /\ B) => C).

Now I can easily perform (and verify, it's given earlier in the
section) the proof of implication with the terms flipped around:
((A /\ B) => C) => (A => (B => C))
Thus:

[A]2  [B]1
----------- (/\ I)      [(A /\ B) => C]3
A /\ B
---------------------------------------- (=> E)
C
--------- (=> I) 1
B => C
------------------ (=> I) 2
A => (B => C)
--------------------------- (=> I) 3
((A /\ B) => C) => (A => (B => C))

My problem arrives finding a solution to the exercise question, my
approach is to basically run the above proof backwards.
Thus:

A => (B => C)     A
--------------------- (=> E)     B
B => C
--------------------- (=> E)
C

Now at this point I thought "aha, I can use (=> I) to introduce (A /\
B)" and get:

--------------------- (=> I) 1
(A /\ B) => C

But here I am only entitled to discharge (A /\ B) in the preceding
proof and not A and B on their own.
What proof which would allow me to discharge my assumptions A and B?

I can see in my head how it makes perfect sense, but can't jiggle a
way to do it using only the given derivations.

Many thanks,
Dave
```