Isabelle化简大合取公式引理时程序无法终止问题咨询

问题背景 #

在Isabelle定理证明中调用absTransfRule (env N) r化简引理时，参数r为包含数百个合取项的大型合取公式：小规模r下化简流程可正常终止，传入大型r时进程卡住无法继续执行。相关证明代码如下：

lemma abs_NI_Remote_GetX_PutX_Home_ref : 
"[|M <= N;dst <= M|] 
==> absTransfRule (env N) M (NI_Remote_GetX_PutX_Home_ref N dst) = 
NI_Remote_GetX_PutX_Home_ref M dst"             
"[|M <= N;dst > M|] 
==> absTransfRule (env N) M (NI_Remote_GetX_PutX_Home_ref N dst) = 
ABS_NI_Remote_GetX_PutX_Home M"
unfolding NI_Remote_GetX_PutX_Home_ref_def 
NI_Remote_GetX_PutX_Home_ref_def ABS_NI_Remote_GetX_PutX_Home_def  apply(auto simp 
add: Let_def )   
done

针对提出的两个核心问题，解答如下：

1. Isabelle 化简过程的具体执行逻辑 #

Isabelle 常用的化简由simp重写引擎实现，auto战术会在simp基础上组合经典逻辑推理模块，核心执行逻辑如下：

• 初始化重写规则集：加载全局默认注册的simp规则、证明中通过simp add:手动指定的规则、unfolding关键字标注的定义展开规则，以及当前证明上下文中的已知假设、已证等式。
• 自底向上项遍历重写：从待化简项的最内层子项开始，逐个匹配规则集中所有重写规则的左式，匹配成功就将子项替换为规则右式；每次替换完成后，会对新生成的项重新启动全量遍历检查，直到不存在任何可匹配的重写规则才会停止。
• 条件规则判定：如果匹配到带前置条件的重写规则，化简器会递归调用自身尝试证明前置条件，证明成功才执行重写，证明失败则跳过当前规则继续匹配。
• 逻辑结构拆分：auto战术额外会对合取、析取、蕴含等逻辑连接词做自动拆分，生成独立子目标，再调用上下文假设、推理规则逐个消解子目标。
  需要注意：化简器没有内置的终止性校验，如果存在循环重写规则、或者计算复杂度超出阈值，进程就会表现为无响应的卡住状态。

2. 大型合取公式场景下化简卡住的核心原因 #

结合当前代码和使用场景，化简卡住基本由以下几类问题导致：

• 合取拆分引发组合爆炸：auto战术遇到合取结构会自动拆分出独立子目标，数百个合取项拆分后子目标数量会呈指数级增长，每个子目标都需要执行全量的重写遍历、条件证明，计算量会快速超出常规处理阈值。
• 函数递归计算复杂度过高：如果absTransfRule本身是按合取结构递归定义的函数，没有做尾递归优化，或者每处理一个合取支都需要全量遍历env N的结构，整体时间复杂度会达到合取项数的平方甚至更高，合取项达到数百级别时耗时会陡增，表现为进程卡住。
• 重写规则触发无限循环：证明中通过unfolding展开了三个自定义常量的定义，如果展开后的结构和现有simp规则存在可互相触发重写的路径，化简器会陷入无限重写循环，永远无法到达终止状态。
• 条件证明回溯开销过大：引理本身带M <= N、dst <= M/dst > M的前置条件，auto处理每个拆分出的子目标时，都会反复尝试调用这些条件做判定，大量无效回溯会占用全部计算资源，导致进程无法推进。

优化建议：处理这类大型合取公式时，不要直接用auto做一次性化简，可以先手动按合取结构拆分目标，逐个对单个合取支调用simp化简；也可以提前证明absTransfRule处理合取的专用simp引理，避免每次化简都展开原始定义做递归遍历；如果怀疑是循环重写导致的卡住，可以开启simp_trace跟踪化简步骤，定位触发循环的规则后将其移出simp规则集即可。

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