Применяя зависимый тип к аргументу, чтобы утверждать цель в Coq?

Question

Если у меня есть общие настройки, подобные следующей, как я могу доказать, что я утверждаю (fa)?

A : Type
f : A -> Prop
a : A
...
============================
f a

В частности, почему я не могу использовать ни одну из этих тактик и что означают ошибки?

specialize (f a).
Error: Cannot change f, it is used in conclusion.

apply (f a).
Unable to unify "Prop" with "f a".

Answer 1

Вы не можете специализироваться f, потому что оно используется в заключении, то есть в цели. specalize (f a) заменяет вашу гипотезу f ее примененной версией. Если мы забудем о цели, которая принесет вам f : Prop впоследствии. Однако, так как f появляется в цели, вам не разрешено менять ее значение.

Также f a - это предложение, и, конечно, не доказательство самого f a! Тот факт, что он называется f, не означает, что это не предикат.