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
_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
