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目標の形をヒントデータベースのリターンタイプの形と一致させることで機能するようです。ここで、あなたの目標が単なる定量化された変数であるという事実に動揺するかもしれません。これがつまずくのが合理的かどうかはわかりませんが、この特定のインスタンスが、このような形のないリターンタイプ（との場合は明らかに同じ）を持つ唯一のケースである可能性があるためSet、Type大したことではありません。

したがって、これをヒントとして必要としない可能性がありますか？...などの戦術を使用するtautoか、環境内intuitionの型の値に対して任意の種類の除去/破棄/反転を実行Falseします...あまり満足のいくものではありませんが、ええと：\