如何解决如何在比赛目标分支中调试战术失败?
假设我在 match goal
分支的主体中有一些复杂的策略,这些策略很容易以我可能需要调试的方式出错。如果某些策略失败,有没有办法从分支获取“真实”错误消息,而不是简单地获取“错误:匹配目标没有匹配子句”?
以这种虚假策略为例,其中 apply A,B,C
有多次出错的机会。我一直在使用与今天有点类似的真实战术。
Ltac three_applications :=
match goal with
| [
A : (* something reasonable *),B : (* something reasonable *),C : (* something reasonable *)
|- _ ] =>
idtac A B C;
assert (F: (* something reasonable *))
by apply A,C;
solve [discriminate F]
end.
先谢谢你!
解决方法
最简单的方法是使用 lazymatch goal
代替,但它具有不同的语义,但我看到您只匹配一种形状,这对您来说可能没问题。
这个想法是 match goal
可能会回溯:如果你有
match goal with
| n : nat |- _ => destruct n ; reflexivity
| |- nat => exact 0
end.
它会首先尝试在您的假设中找到一些 n : nat
,从最近的开始,然后尝试策略 destruct n ; reflexivity
。如果失败,它将尝试找到另一个自然数。如果它们都失败了,那么它将查看目标是否与第二个子句匹配,如果匹配则执行 exact 0
。
如果再次失败,它将再次回溯并得出No matching clauses for match goal
。
另一方面,
lazymatch goal with
| n : nat |- _ => destruct n ; reflexivity
| |- nat => exact 0
end.
会找到第一个匹配的分支,然后应用tactic,如果失败,在lazymatch
中没有回溯,它会给你相应分支中tactic的错误。
请注意,当我找不到用于回溯的用例时,我将始终使用 lazymatch
,而不仅仅是出于调试目的。
如果 lazymatch
在语义上不等同于您的 match
并且需要涉及回溯那么它会更难,但实际上,使用 idtac A B C
可以帮助您查看它的哪个分支在启动错误之前选择。
有时,写作
Fail three_applications.
而不仅仅是
three_applications.
会有所帮助,因为 Fail
通常会保留您在命令中进行的打印,即使最终失败。
了解分支后,只需手动应用您的策略。
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。