引理不能用作提示

Question

为什么 Coq 不接受这个引理作为提示？

Lemma contr : forall p1 : Prop, False -> p1.
Proof. tauto. Qed.

Hint Resolve contr : Hints.

或其他以

Prop

变量结尾的引理？

Answer 1

查看

Hint Resolve

的文档 ( http://coq.inria.fr/distrib/V8.4/refman/Reference-Manual011.html#@command232 ):

term cannot be used as a hint

The type of term contains products over variables which do not appear in the conclusion. A typical example is a transitivity axiom. In that case the apply tactic fails, and thus is useless.

然而，（在我看来）这里的情况似乎并非如此，因为唯一的产品已经结束了

p1

，这确实出现在结论中。

这里的问题似乎是你的结论完全没有形状。

auto

似乎是通过将目标的形状与提示数据库的返回类型的形状相匹配来工作的。在这里，它可能会因为你的目标只是一个量化变量而感到不安。我不确定这是否是一个合理的事情，但这个特定的实例可能是唯一可能有这种无形返回类型的情况（显然

Set

和

Type

的情况相同），所以它是没什么大不了的。

那么，您可能不需要这个提示？...只需使用

tauto

、

intuition

等策略或在您的环境中对

False

类型的值执行任何类型的消除/破坏/反转...不是很令人满意但是呃:\

Answer 2

建立在已接受的答案之上：

今天（Coq 8.20），Hint Resolve

的文档解释了这个错误，如下：

错误

qualid

不能用作提示

qualid

类型的头符号是一个绑定变量，因此该策略不能与常量关联。

在这种情况下，我将其解释为

p1

是提到的头符号，它由

forall

量词绑定。特别是，该头部符号不是全局定义的常量，当尝试应用建议的提示时，

auto

可以在目标中查找。