C[omp]ute

From: "andrew cooke" <andrew@...>

Date: Mon, 23 Jan 2006 00:27:16 -0300 (CLST)

ere's my initial attempt at the first few exercises in TTFP (Type Theory
and Functional Programming; see posts at
http://www.acooke.org/cute/MoreConstr0.html).  Hopefully I'll keep
updating this thread as I get further through the book.

Notation:
- for negation
! for bottom (the uspide down T)
So -X is equivalent to X => !

1.1 Prove transivity of implication

[A]1  A => B
------------ (=> E)
     B                B => C
---------------------------- (=> E)
             C
          ------ (=> I1)
          A => C

((A => B) => (B => C)) => (A => C)

Note that it's OK to introduce extra propositions (like A above) at the
start, as long as you eliminate them later (this is what "elimination"
means)


1.2 Prove ((A u B) => C) => ((A => C) n (B => C))

                         (A u B) => C
             ---------------------------------------------- (n I)
             (A u B) => C        n             (A u B) => C
[A]1            .                . [B]2            .
----- (u I)     .                . ----- (u I)     .
A u B           .                . A u B           .
------------------------- (=> E) . ------------------------- (=> E)
          C                      .           C
       ------ (=> I1)            .        ------ (=> I2)
       A => C                             B => C

So ((A u B) => C) => ((A => C) n (B => C))


1.3 Prove (A => (B => C)) => ((A n B) => C)

[A n B]1
-------- (n E x 2)
 B   A
 .   .
 .   .  (A => (B => C))
 .   ------------------ (=> E)
 .           B => C
 ------------------ (=> E)
          C
    ------------ (=> I)
    (A n B) => C


1.4 Joke question?
[later] - book author (Simon Thompson) replied saying it was a mistake!


1.5 Prove (B u C) => -(-A n -B)

This looks so much like De Morgan's law I'm going to assume it's a typo
and instead prove (A u B) => -(-A n -B)

However, I can't find a solution (looks like it needs the excldued middle?)


1.6 (a) Prove ((A => B) n (A => -B)) => -A

 [A]1  A => B         [A]1  A => (B => !)
 ------------ (=> E)  ------------------- (=> E)
      B                      (B => !)
      ------------------------------- (=> E)
                    !
                  ------ (=> I1)
                  A => !

I'm not that sure about this because it might contradict (! E):
  !
 ---
  X
I think it doesn't because there's "more above" than just !.

Also, there are assumptions about how the "deduction process" corresponds
to a formula:
 - n being implicit between different "tracks" in the argument (OK, I
   think, since n appears to be associative and commutative).
 - vertical steps being equivalent to =>

(b) Prove (A n -A) => B

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