Isabelle中simp无法简化含Some/let/case的units_propagate目标的原因？

一、simp失效的具体原因 #

你的场景里simp没能自动把case表达式简化到Some分支，主要有这几个核心原因：

• simp的匹配逻辑偏保守：simp默认只会用预设重写规则和显式加入的等式做简化，不会主动把假设里的find (λc. length c = 1) f = Some [l]代入到units_propagate展开后的case分支判断中。而metis是一阶逻辑自动证明器，能做更灵活的逻辑关联推导，所以能直接完成证明。
• case分支的模式匹配未触发：如果units_propagate的定义里，case分支是针对find的结果，但simp没有对应的规则把find ... = Some x转化为case分支的选择。你可以试试手动把假设加入simp规则池，比如用simp add: assms（假设你的假设被命名为assms），或者先显式拆分case：cases (find (λc. length c = 1) f)，再对每个分支用simp，就能触发简化。
• 变量绑定或隐式类型差异：有时候units_propagate内部的局部变量和假设里的变量存在隐式绑定冲突，或者类型参数未完全统一，simp的统一算法没匹配上，但metis的匹配能力更强，能忽略这类上下文小差异。

二、重构units_propagate的可行方向 #

如果想让这类证明更顺畅，可以从函数结构上调整：

• 拆分unit检测与传播逻辑：把find (λc. length c = 1) f的结果作为参数传给units_propagate，而非让函数内部自行调用find。比如定义新函数：

  units_propagate_with_unit :: 'a formula ⇒ 'a literal option ⇒ 'a formula × bool
  

  第二个参数就是预先找到的unit，这样函数内部的case分支会更直接，simp更容易识别并简化。
• 解耦递归与unit检测：如果units_propagate是递归定义的，把unit检测逻辑抽成单独的辅助函数，比如find_unit :: 'a formula ⇒ 'a literal option，再在units_propagate里调用这个辅助函数。证明时可以先给find_unit做单独的引理，再将引理应用到units_propagate的证明中，逻辑更清晰。
• 添加自定义simp规则：如果不想修改函数结构，可以先证明一个针对该场景的引理，比如：

  lemma units_propagate_with_unit_found:
    assumes "find (λc. length c = 1) f = Some [l]"
    shows "units_propagate f = ..."  -- 填入展开后的Some分支结果
  

  把这个引理加入simp规则集（declare units_propagate_with_unit_found[simp]），之后用simp就能自动触发简化。

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