Isabelle中使用metis证明引理出现无限循环的解决方案咨询

问题原因 #

metis是一阶自动证明工具，本身不支持结构归纳推导，而你要证明的目标和归纳谓词star、star'的性质相关。仅传入step规则时，metis会反复匹配该规则做无限展开，最终陷入死循环挂起。

解决方法 #

• 归纳谓词的性质优先用归纳法证明，不要直接交给自动证明器处理需要归纳的子目标。你定义的lemma 21本质是证明单步关系r x y可以追加到star'关系的左端，直接对star' r y z做归纳即可完成证明，无需调用metis匹配step规则：

lemma 21  : "r x y ⟹
       star r y z ⟹
       star' r y z ⟹
       star' r x z"
  apply (induction rule: star'.induct)
  (* 基础情况：y = z，直接用step'加refl'得证 *)
  apply (simp add: refl' step')
  (* 步级情况：用归纳假设结合step'构造结论 *)
  apply (metis step')
  done

• 补全lemma 2的归纳步骤，直接调用已经证明的lemma 21即可完成证明，不会出现挂死问题：

lemma 2 : "star r x y ⟹ star' r x y"
  apply (induction rule: star.induct)
  apply (metis refl')
  (* 归纳步直接调用引理21 *)
  apply (metis "21")
  done

• 另外你的lemma 1目前仅完成了基础情况的证明，步级子目标需要结合star的性质补全，参考实现如下：

lemma star_snoc: "star r x y ⟹ r y z ⟹ star r x z"
  apply (induction rule: star.induct)
  apply (simp add: refl step)
  apply (metis step)
  done

lemma 1 : "star' r x y ⟹ star r x y"
  apply (induction rule : star'.induct)                
  apply (metis refl)
  apply (metis star_snoc)
  done

• 如果确实需要调用自动证明器处理此类目标，可以给metis加上搜索深度限制参数，例如apply (metis (depth_limit = 5) step)，或者使用sledgehammer工具筛选更合适的引理组合，避免触发无限搜索。

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