时间戳

首页 > 解决方案 > 如何调试匹配目标分支中的战术失败？

coq - 如何调试匹配目标分支中的战术失败？

问题描述

假设我在一个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, B, C;
            solve [discriminate F]
    end.

先感谢您！

标签： coqcoq-tactic

解决方案

最简单的方法是使用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.

将找到第一个匹配的分支，然后应用该策略，如果失败，则不回溯lazymatch，它会在相应的分支中给出该策略的错误。

请注意lazymatch，当我找不到回溯的用例时，我将始终使用 ，而不仅仅是出于调试目的。

如果，lazymatch在语义上不等同于您match并且需要涉及回溯，那么它会更难，但实际上，使用idtac A B C可以帮助您在启动错误之前查看它选择了哪个分支。有时，写作

Fail three_applications.

而不仅仅是

three_applications.

会有所帮助，因为Fail通常会保留您在命令中进行的打印，即使它最终失败。

一旦你知道了分支，只需手动应用你的策略。

推荐阅读