(练习来自软件基础，我可以给出所有相关的定义，但会有很多)考虑一下:
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。不，展开没有帮助。)
最佳答案
它可能会失败，因为 E_Ass 的结论并不立即符合您的目标。 auto 确实会预先检查这一点，如果结论不直接匹配，甚至不会尝试应用引理。 Afair fail 包括“没有尝试”。甚至 simple_apply 也会在应用的引理和目标之间进行一些转换。您可以尝试添加带有 E_Ass 变体的提示，该变体将被转换以匹配目标。 E_Ass 的类型是什么？
关于automation - coq auto 说简单的应用失败，但它可以手动工作，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/67020464/