Coq中如何从sumbool假设提取成立分支并简化if对应子目标

分支保留与子目标化简方案 #

你可以通过以下两步实现需求：

1. 拆解可判定求和假设消去矛盾分支
   对已有的假设H使用destruct tactic拆分求和类型：

destruct H as [H_le | H_gt].

执行后会生成两个子目标：

• 第一个子目标携带假设H_le : 2 <= 1，这是明显不成立的命题，直接调用整数算术tacticlia即可自动证明矛盾，关闭该分支，无需手动处理。
• 第二个子目标会保留你需要的成立假设H_gt : 2 > 1。

2. 化简if语句分支
   此时直接对目标中的check_smaller_thm 1 2做重写即可：

rewrite H.

因为H已经是check_smaller_thm 1 2的求值结果，重写后if语句会自动匹配到{2 > 1}对应的右分支，目标直接化简为some other stuff相关的证明义务。
你也可以用更短的组合写法一步完成：

destruct H; [lia | rewrite H].

补充问题：if始终走then分支的可能性 #

这种情况完全可能出现，常见原因有两类：

• check_smaller_thm的实现逻辑错误：如果该函数的比较逻辑写反，或者求和类型的左右分支定义顺序和你预期不符，比如你实际把{a > b}放在了求和类型的左侧，就会导致check_smaller_thm 1 2返回左分支，触发then逻辑。
• 上下文引入了矛盾的公理/假设：如果你的证明上下文中添加了和自然数序关系冲突的公理，也会导致Coq的判定逻辑出现不符合预期的结果。
  你可以直接执行Compute check_smaller_thm 1 2查看该表达式的实际求值结果，快速定位问题根源。

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