如何调试Coq中match goal分支内的tactic执行失败问题？

这确实是写复杂Coq Ltac时特别头疼的问题——当match goal分支里的子tactic（比如你例子里的apply A, B, C）执行失败时，Coq默认会直接跳过整个分支，最后只给你一句Error: No matching clauses for match goal，完全看不到内部tactic的真实错误原因。针对你写的three_applications，我分享几个实用的调试方法：

1. 用try...||fail强制暴露分支内错误 #

你可以给分支内的核心逻辑加上try包裹，失败时主动打印提示并抛出错误，这样Coq就不会跳过该分支，而是直接展示分支内的问题。修改你的Ltac如下：

Ltac three_applications := 
  match goal with 
  | [ A : (* something reasonable *), B : (* something reasonable *), C : (* something reasonable *) |- _ ] => 
    idtac "Executing branch with hypotheses:" A B C;
    try (
      assert (F: (* something reasonable *)) by apply A, B, C;
      solve [discriminate F]
    ) || (
      idtac "ERROR: Failed inside this branch!";
      fail 1 "Check the apply or assert step above for issues"
    )
  end.

当分支内的apply或assert出错时，try会捕获失败，然后执行||后的逻辑：先打印分支标识，再用fail 1抛出错误（1表示只向上传递一层错误，不会影响整个match的错误层级）。这时你就能明确知道是这个分支出了问题，结合之前的idtac输出，还能看到当前匹配到的hypotheses。

2. 开启Ltac调试模式看执行细节 #

Coq内置了Ltac调试工具，开启后会逐步骤执行你的tactic，包括进入match goal分支后的每一步操作，能直接看到apply失败的具体原因（比如类型不匹配、hypothesis无法应用等）。使用方法很简单：

Set Ltac Debug.
three_applications.

执行后你会看到详细的执行日志，比如：

Entering match goal
Trying clause 1: matches!
Executing idtac A B C
Executing assert (F: ...) by apply A, B, C
Error: Unable to apply lemma ...

这样就能精准定位到apply的真实错误了。调试完成后可以用Unset Ltac Debug关闭调试模式。

3. 拆分复杂子逻辑为独立Ltac #

把分支内的复杂逻辑拆成单独的Ltac函数，这样子tactic的错误会直接暴露，不会被match goal的默认行为掩盖。比如：

Ltac execute_three_apps A B C :=
  assert (F: (* something reasonable *)) by apply A, B, C;
  solve [discriminate F].

Ltac three_applications := 
  match goal with 
  | [ A : (* something reasonable *), B : (* something reasonable *), C : (* something reasonable *) |- _ ] => 
    idtac A B C;
    execute_three_apps A B C
  end.

当execute_three_apps里的apply出错时，Coq会直接报告这个子Ltac内的错误，而不是回到match goal的“无匹配分支”提示，让你一眼就能看到问题出在apply步骤。

额外小技巧：打印上下文信息 #

在执行核心tactic前，用idtac打印hypotheses的类型，提前确认匹配到的内容是否符合预期：

idtac "Type of A:" type of A;
idtac "Type of B:" type of B;
idtac "Type of C:" type of C;

这能帮你先排除match goal的模式匹配是否正确，再去调试后续的apply错误。

内容的提问来源于stack exchange，提问作者blaineh