coqauto表示，简单的应用程序会失败，但它可以手动工作

Question

(练习来自软件基础，我可以给出所有相关的定义，但会有很多(考虑一下：

Goal empty_st =[ X := 1 ]=> (X ↦ 1).
debug auto.    (* (* debug auto: *)
* assumption. (*fail*)
* intro. (*fail*)
* simple apply E_Ass (in core). (*fail*) <- note this fails
* simple apply E_Skip (in core). (*fail*) *)
simple apply E_Ass. (* <- but this works *)
Qed.

通常，我对auto的问题是它找不到相关的东西来应用。在这里，它完美地做到了这一点，但由于某种原因未能应用它。我如何说服它更加努力？

(是的，它是相同的E_Ass。不，展开没有帮助。(

Answer 1

它可能会失败，因为E_Ass的结论与您的目标不符。auto确实提前检查了这一点，如果结论不直接匹配，甚至不会尝试应用引理。Afairfail包括"；没有尝试"；。甚至simple_apply也会在应用引理和目标之间进行一些转换。您可以尝试添加一个带有E_Ass变体的提示，该变体将被转换为与目标相匹配。E_Ass的类型是什么？