为何Idris2无法证明div 1 2 < 1 = True？及Nat除法验证问题

原始问题场景 #

编写以下除法相关的Agda代码时出现错误：

div_1_2_lower_than_1 : div (S Z) 2 < (S Z) = True
div_1_2_lower_than_1 = Refl

错误提示：

处理div_1_2_lower_than_1的右侧时，无法解决约束：True 与 compare (1 div 2) 1 == LT 不匹配。

但编写类似的减法代码时，却能正常通过：

minus_1_2_lower_than_1 : minus (S Z) 2 < (S Z) = True
minus_1_2_lower_than_1 = Refl

更新验证场景 #

使用Data.Nat和natDiv尝试验证基础除法等式，仍然报错：

div_1_2_eq_0 : div (S Z) (S (S Z)) = 0
div_1_2_eq_0 = Refl

错误提示：

处理div_1_2_eq_0的右侧时，无法解决约束：0 与 divNat 1 2 不匹配。

原因分析 #

Agda中minus和div的定义展开规则存在本质差异：

• **自然数减法minus**是构造性的可直接归约定义：当被减数小于减数时，minus会直接展开为0。比如minus 1 2会立刻归约成0，后续0 < 1的结果True能和等式右边完全匹配，因此Refl可以直接生效。
• **除法div/divNat**的定义依赖递归或商余关系，属于非直接归约的定义：Agda不会自动将divNat 1 2归约为0，因为除法的计算规则需要满足更复杂的前置条件（比如商余的存在性），导致等式两边的表达式无法被Agda的统一器识别为相等，所以Refl无法直接应用。

解决方法 #

要证明这类除法等式，需要显式利用除法的性质引理，或者手动引导归约：

1. 调用Data.Nat.Division中的现成引理，比如处理被除数小于除数的divNat-lt：

open import Data.Nat
open import Data.Nat.Division

div_1_2_eq_0 : div (S Z) (S (S Z)) = 0
div_1_2_eq_0 = divNat-lt (s≤s z≤n)

2. 也可以使用rewrite关键字配合除法的计算规则，逐步引导Agda完成表达式的归约。

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