HOL中用THENL组合TAC_PROOF出错，求子目标策略匹配方案

架构老林

2026-5-27

修正你的HOL战术组合代码问题

你代码的核心问题是错误地连续使用了两次THENL，而THENL的设计是接收一个战术列表，列表中的每个元素对应前序战术生成的每个子目标的处理逻辑。我们只需要把两个子目标的处理战术放在同一个THENL的列表里即可。

修正后的代码

val constructiveDilemmaRule = TAC_PROOF (
  ([], ``!p q r s. (p ==> q) /\ (r ==> s) ==> p \/ r ==> q \/ s``),
  REPEAT STRIP_TAC THENL [
    DISJ1_TAC THEN RES_TAC,  # 专门处理第一个子目标：从p推导q，再用DISJ1完成q\/s的证明
    DISJ2_TAC THEN RES_TAC   # 专门处理第二个子目标：从r推导s，再用DISJ2完成q\/s的证明
  ]
);

为什么这样能解决问题？

执行REPEAT STRIP_TAC后，你的目标会被拆分成两个独立子目标：

第一个子目标的上下文包含p、p ==> q、r ==> s，需要证明q \/ s。DISJ1_TAC会把目标简化为证明q，紧接着RES_TAC会自动匹配p ==> q的假设，结合已知的p直接得到q，完成该子目标。
第二个子目标的上下文包含r、p ==> q、r ==> s，需要证明q \/ s。DISJ2_TAC会把目标简化为证明s，RES_TAC则匹配r ==> s的假设，结合已知的r得到s，完成该子目标。