Предположим, у нас есть A B C : Prop.
Учитывая контекст с H : A -> B -> C и единственной целью A -> B -> C,
почему можно apply H завершить доказательство, решив текущую и единственную цель?
Я думал, что тактика apply генерирует новую цель для каждого из аргументов применяемого термина, если его заключение совпадает (или может быть унифицировано) с текущей целью.
То, что вы описываете, произошло бы, если бы вашей целью было только C: чтобы доказать C от H: A -> B -> C, вам нужно будет предоставить свидетелей для A и B. Однако ваша текущая ситуация - всего лишь пример доказательства P знания P, какой бы формы P ни была. Следовательно, applying H, вы предоставляете достаточно информации, чтобы закрыть цель.
apply H работает? Применить попытки проверить вывод применяемого термина (согласно документации) - но в этом случае вывод будет C, а не A -> B -> C. Например, в этом сценарии я понимаю, почему assumption решает цель - я хочу доказать, что P знаю P.
- person ScarletAmaranth; 17.11.2015
apply пытается объединить полную цель с H, а не только с последней частью импликации. Здесь соответствие точное, поэтому у вас нет конечных подцелей.
- person Vinz; 17.11.2015
H как нулевой предикат, возвращающий данные типа A -> B -> C;)
- person Vinz; 17.11.2015
