Вопрос немного расплывчатый ... Вы задаетесь вопросом, возможно ли это (да), каков ответ (см. Комментарий Артура выше) или как думать о решении этих проблем?
ВВ последнем случае помните, что целью является создание «лямбда-термина» с указанным типом.Вы можете использовать «тактику», которая помогает вам построить термин «снаружи и изнутри». Хорошо бы сделать это вручную пару раз, чтобы понять, что происходит и что на самом деле делает тактика, что, я думаю,почему вам дано это упражнение.
Если вы посмотрите на свой пример,
(P -> (Q /\ R)) -> (~Q) -> ~P
, вы увидите, что это функция трех (!) аргументов. Это потому, что последний тип~P на самом деле означает P -> False, поэтому типов аргументов функции, которые нужно создать, являются
P -> (Q /\ R)
Q -> False
P
, и функция должна создать член типа
False
Вы можете создать термин fun A B C => _, где A, B, C имеет типы выше (это то, что делает тактика intros), и вам нужно придумать термин, который должен войти вдыра _ путем объединения терминов A, B, C и необработанных конструкций Галлина.
В этом случае, когда вам удалось создать термин типа Q /\ R, вам придется «уничтожить» его, чтобы получитьтермин типа Q, (подсказка: fили что вам придется использовать конструкцию match).
Надеюсь, это поможет, не испортив веселья!