如何让Agda函数仅接受非零自然数参数？终止检查失败求助

问题背景 #

需要让Agda中的lessen函数仅接受非零自然数作为除数，添加.{{_ : NonZero divisor}}约束后，函数仍无法通过终止检查，报错如下：

Checking NumberTheory (D:@NURD@CODING@ALL\AgdaProject\AgdaFunctions\FromFunctions\NumberTheory.agda).
D:@NURD@CODING@ALL\AgdaProject\AgdaFunctions\FromFunctions\NumberTheory.agda:13,1-19,74
Termination checking failed for the following functions:
Problematic calls:
NumberTheory.with-22 i (numb %? i)
lessen (numb /? i) i
(at D:@NURD@CODING@ALL\AgdaProject\AgdaFunctions\FromFunctions\NumberTheory.agda:18,15-21)
lessen numb (suc i)
(at D:@NURD@CODING@ALL\AgdaProject\AgdaFunctions\FromFunctions\NumberTheory.agda:19,33-39)

完整可复现代码：

module NumberTheory where
open import Data.Bool.Base hiding (_<_)
open import Data.Integer.Base using (_/ℕ_; _%ℕ_; ∣_∣; +_)
open import Agda.Builtin.IO using (IO)
open import Agda.Builtin.Nat using (Nat; suc; _==_)
open import Data.Nat.Base using (NonZero; _≤ᵇ_)
open import Agda.Builtin.Bool
open import Agda.Builtin.Int
open import Agda.Builtin.List
open import Data.List.Base

-- |Check if this number is Hamming.
isHamming : Int -> Bool
isHamming what = lessen what 2 where
    lessen : (dividend : Int) (divisor : Nat) .{{_ : NonZero divisor}} -> Bool
    lessen (+ 0) _ = false
    lessen numb i with numb %ℕ i
    ... | 0 = lessen (numb /ℕ i) i
    ... | _ = if (i ≤ᵇ 5) then (lessen numb (suc i)) else (∣ numb ∣ == 1)

问题原因 #

Agda的终止检查器仅默认识别结构递归（如自然数直接递降、归纳类型结构缩小），当前代码的递归调用无法被检查器识别为终止：

• lessen (numb /ℕ i) i：numb /ℕ i的绝对值小于原numb，但检查器无法自动关联Int绝对值递降与终止性；
• lessen numb (suc i)：i从2递增到5后终止，但检查器看不到i不会无限递增的约束。

解决方案 #

1. 重构函数，显式提供终止递降依据 #

通过拆分递归逻辑，将终止条件转换为Agda可识别的自然数递降：

module NumberTheory where
open import Data.Bool.Base hiding (_<_)
open import Data.Integer.Base using (_/ℕ_; _%ℕ_; ∣_∣; +_)
open import Agda.Builtin.Nat using (Nat; suc; _==_)
open import Data.Nat.Base using (NonZero; _≤ᵇ_; _∸_)
open import Agda.Builtin.Bool
open import Agda.Builtin.Int

-- |Check if this number is Hamming.
isHamming : Int -> Bool
isHamming what = go what 2 where
  go : Int -> Nat -> Bool
  go (+ 0) _ = false
  go numb d with d ≤ᵇ 5
  -- 除数超过5时，检查剩余数是否为1
  ... | false = ∣ numb ∣ == 1
  -- 除数在2-5范围内时处理
  ... | true = case numb %ℕ d of λ
    { 0 -> go (numb /ℕ d) d  -- 能整除则继续除以当前除数，绝对值递降
    ; _ -> go numb (suc d)   -- 不能整除则递增除数，5 ∸ d 递降
    }

  -- 自动提供NonZero约束：d从2开始，suc d永远非零
  .{{_ : NonZero d}} : NonZero d
  .{{_ : NonZero 2}} = _
  .{{_ : NonZero (suc d)}} = _

2. 为什么能通过终止检查 #

• 对于go (numb /ℕ d) d：∣ numb /ℕ d ∣严格小于∣ numb ∣，Agda可通过∣_∣的定义识别此递降；
• 对于go numb (suc d)：5 ∸ d是严格递降的自然数，直到d超过5后触发终止分支；
• NonZero约束自动满足：除数从2开始，每次递增都是suc d，永远不会为0。

3. 严谨化终止证明（可选） #

如果需要更形式化的终止证明，可使用良基递归（基于自然数的<关系）：

module NumberTheory where
open import Data.Bool.Base hiding (_<_)
open import Data.Integer.Base using (_/ℕ_; _%ℕ_; ∣_∣; +_)
open import Agda.Builtin.Nat using (Nat; suc; _==_)
open import Data.Nat.Base using (NonZero; _≤ᵇ_; _<_)
open import Agda.Builtin.Bool
open import Agda.Builtin.Int
open import Relation.Binary.WellFounded using (WellFounded; <-wellFounded)

isHamming : Int -> Bool
isHamming what = wf-go (<-wellFounded) what 2 where
  wf-go : WellFounded _<_ -> Int -> Nat -> Bool
  wf-go wf numb d with d ≤ᵇ 5
  ... | false = ∣ numb ∣ == 1
  ... | true = case numb %ℕ d of λ
    { 0 -> let n' = numb /ℕ d
           in wf-go (wf ∣ n' ∣) n' d  -- 用绝对值递降作为良基依据
    ; _ -> wf-go wf numb (suc d)
    }

  .{{_ : NonZero d}} : NonZero d
  .{{_ : NonZero 2}} = _
  .{{_ : NonZero (suc d)}} = _

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