Простые задачки на Карри-Говарда

[deniok]

Доказать, используя Хаскель, что следующие тавтологии верны интуиционистски

(a -> c) /\ (b -> c) -> a \/ b -> c
(a \/ b -> c) -> (a -> c) /\ (b -> c)

(Понятно, что конъюнкция - это пара, а дизъюнкция - Either.)

UPD. Стоит напомнить, что изоморфизм Карри-Говарда имеет место между интуиционистской версией пропозициональной логики и подмножеством Хаскеля без рекурсии. То есть использовать рекурсию нельзя - ни явно, ни неявно. Ну и определение отрицания требует в Хаскелле некоторых хаков, но при доказательстве этих формул оно не требуется.

Comments

[gds.livejournal.com]

мой вариант:

Extraction Language Haskell.

Inductive Either A B := Left : A -> Either A B | Right : B -> Either A B.

Extraction Inline prod_rect.
Extraction Inline Either_rect.

Lemma l1 : forall a b c,
(a -> c) * (b -> c) -> Either a b -> c.
firstorder.
Defined.
Extraction l1.

Lemma l2 : forall a b c,
(Either a b -> c) -> (a -> c) * (b -> c).
firstorder.
Defined.
Extraction l2.

(результат в отдельной пасте, http://pastebin.com/H2T1cw7B , чтобы не спойлерить.)
(до канонiчного можно довести, указав, во что экстрактить Prod и Pair.)