Kata

According to Curry–Howard correspondence, propositions can be translated to types. To prove such proposition, one must construct a value conforming to the translated type.

In this kata, you would practice translating some simple propositions to types, and then proving these propositions by constructing appropriate functions.

Notations

∧ is the logical AND.
∨ is the logical OR.
⇒ is IMPLICATION.

A ∧ B can be read as "A and B"
A ⇒ B can be read as "A implies B"

Example

The proposition P ≡ (A ⟹ B) ⟹ (B ⟹ C) ⟹ (A ⟹ C) can be encoded as a function, with type signature

p :: (a -> b) -> (b -> c) -> (a -> c)

To prove such proposition P, one only needs to construct a function conforming to the type signature written above.

In this case, it is trivial to construct such function:

p f g = g . f

Thus the proposition P is proven.

Translating Propositions to Types

For simplicity, we only concern ourselves with propositional logic; thus we do not have logical quantifiers.

The following code snippet should give a quick reference on how to translate propositions to types for the purpose of this kata:

-- (plain text)
-- let T be the translation function

T : Proposition -> Type
T(A ∧ B) = T(A) * T(B) -- product type, Tuple in Haskell
T(A ∨ B) = T(A) + T(B) -- sum type, Either in Haskell
T(A ⇒ B) = T(A) -> T(B)

Thus the tautology A ∧ B ⇒ B can be broken down the following way:

Steps:
1) T(A ∧ B ⇒ B)
2) T(A ∧ B) -> T(B)
3) T(A) * T(B) -> T(B)
4) (a, b) -> b

The snd function (in prelude) proves this tautology:

snd :: (a, b) -> b
snd (a, b) = b

Special Rules

Make ∧, ∨ left associative, so a ∧ b ∧ c should have Haskell type ((a, b), c)

Every function should be practically total. (Specifically, your pattern-matching should always be exhaustive.)

Sum types, such as a + b, should be encoded using Either like this: Either a b.

Goal

Prove the following tautologies using the method mentioned above, name the defined values p1, p2, p3 respectively.

1) ((A ⇒ B) ∧ (B ⇒ C)) ⇒ (A ⇒ C)
2) (A ⇒ B ⇒ C) ⇒ ((A ∧ B) ⇒ C)
3) ((A ∨ B) ∧ (A ⇒ C) ∧ (B ⇒ C)) ⇒ C