HOL中TAC_PROOF封装策略时ACCEPT_TAC抛出异常的问题

数据老陈

2026-5-27

问题原因分析

你的问题出在策略执行顺序错误上。咱们先拆解一下你的代码逻辑：

当你执行REPEAT STRIP_TAC后，HOL会把全称量词!(p q)剥除，同时把外层的两个蕴含式前件（p ==> q和p）加入到假设集合里。此时当前的证明子目标是p /\ q——但你紧接着调用了ACCEPT_TAC(ASSUME ``p:bool``)，这个策略的作用是用已有的假设直接匹配当前子目标，可现在子目标是合取式p /\ q，和假设里的p完全不匹配，自然会抛出异常。

而你分步执行时一切正常，大概率是因为你手动在REPEAT STRIP_TAC之后，先对合取目标做了拆分（比如执行了CONJ_TAC），把p /\ q拆成了p和q两个子目标，这时候再用ACCEPT_TAC处理第一个子目标就完全匹配了——但封装成TAC_PROOF时你漏掉了这个关键的拆分步骤。

修正后的代码方案

这里给你三种可行的修正方式，覆盖不同的证明风格：

方式一：显式拆分合取目标（最贴合你的原始思路）

val absorptionRule = TAC_PROOF(
    ([], ``!(p:bool) (q:bool). (p ==> q) ==> p ==> p /\ q``),
    REPEAT STRIP_TAC THEN CONJ_TAC THENL [
        ACCEPT_TAC (ASSUME ``p:bool``),  (* 直接用假设证明子目标p *)
        RES_TAC                         (* 从p==>q和p推导出q，完成第二个子目标 *)
    ]
);

方式二：利用重写规则简化证明

如果不想手动拆分合取式，可以用ASM_REWRITE_TAC结合布尔运算的定义直接完成证明：

val absorptionRule = TAC_PROOF(
    ([], ``!(p:bool) (q:bool). (p ==> q) ==> p ==> p /\ q``),
    REPEAT STRIP_TAC THEN ASM_REWRITE_TAC [CONJ_DEF, IMP_DEF]
);

方式三：自动定理证明器（最简洁）

HOL提供了自动证明器METIS_TAC，可以直接完成这类简单的布尔逻辑证明：

val absorptionRule = TAC_PROOF(
    ([], ``!(p:bool) (q:bool). (p ==> q) ==> p ==> p /\ q``),
    METIS_TAC []
);

验证说明

修正后的代码里，REPEAT STRIP_TAC处理完前置条件后，CONJ_TAC会把合取目标拆分成两个独立的子目标，分别对应合取式的左右两边。第一个子目标p可以直接用已有的假设通过ACCEPT_TAC证明，第二个子目标q则通过RES_TAC从p ==> q和p这两个假设中推导出来，整个证明流程就通顺了。

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