将依存类型应用于主张以确立Coq中的目标的争论吗？

Question

如果我具有如下所示的常规设置，如何证明我主张（f a）？

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的事实并不意味着它不是谓词。