Exercise 5.7
Prove that the following propositions are tautologies by giving shortened λP-derivations:
(a) $(A ⇒B) ⇒((B ⇒C) ⇒(A ⇒C))$
(b) $((A ⇒B) ⇒A) ⇒((A ⇒B) ⇒B)$
(c) $(A ⇒(B ⇒C)) ⇒((A ⇒B) ⇒(A ⇒C))$
(a) The type associated with $(A ⇒B) ⇒((B ⇒C) ⇒(A ⇒C))$ is
$$ \Pi x:(\Pi a:A.B).(\Pi y:(\Pi b:B.C).(\Pi a:A.C)) $$
By inspection, the inhabitant should be
$$ \lambda x:(\Pi a:A.B).(\lambda y:(\Pi b:B.C).(\lambda a:A.y(xa))) $$
The following is a shortened derivation in λP, first deriving the type, then the inhabitant.
(b) The type associated with $((A ⇒B) ⇒A) ⇒((A ⇒B) ⇒B)$ is
$$ \Pi x:(\Pi s:(\Pi a:A.B).A) . (\Pi t:(\Pi a:A.B).B) $$
By inspection, the inhabitant should be
$$ \lambda x:(\Pi s:(\Pi a:A.B).A) . (\lambda t:(\Pi a:A.B). t(xt)) $$
The following is a shortened derivation λP, first deriving the type, then the inhabitant.
(c) The type associated with $(A ⇒(B ⇒C)) ⇒((A ⇒B) ⇒(A ⇒C))$ is
$$ \Pi x:(\Pi a:A . (\Pi b:B.C)) . (\Pi y:(\Pi a:A .B).(\Pi a:A.C)) $$
By inspection, the inhabitant should be
$$ \lambda x:(\Pi a:A . (\Pi b:B.C)) . (\lambda y:(\Pi a:A .B). (\lambda a:A.xa(ya))) $$
The following is a shortened derivation in λP, first deriving the type, then the inhabitant.
