coq - 引理不能用作提示

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似乎通过将目标的形状与提示数据库的返回类型的形状相匹配来工作。在这里，您的目标只是一个量化变量这一事实可能会令您感到不安。我不确定这是否是一个合理的绊脚石，但是这个特定的实例可能是唯一一个你可能有这样一个无形的返回类型的情况（显然与Setand的情况相同Type），所以这没什么大不了的。

所以，您可能不需要这个作为提示？...只需使用诸如tauto，intuition或对您的环境中类型的值执行任何类型的消除/破坏/反转False...不是很令人满意，但是 eh :\