在对单个构造函数参数进行归纳时证明完整性

Question

我们有以下具有单个构造函数的类型：

-- IsTwice n is inhabited if n = k + k for some k
data IsTwice : Nat -> Type where
  Twice : (k : Nat) -> IsTwice (k + k)

我试图在 IsTwice n 上为任何 n 定义一个函数，但是通过对 Twice 构造函数的 k 参数进行归纳，而不是n 到 IsTwice 的参数。我的问题是我无法让 Idris 接受我的定义 total.

这是一个具体的例子。假设我们有第二种类型：

data IsEven : Nat -> Type where
  IsZero : IsEven 0
  PlusTwo : (n : Nat) -> IsEven n -> IsEven (2 + n)

我想证明 IsTwice n 蕴含 IsEven n。我的直觉是：我们知道 IsTwice n 类型的任何值（witness）对于某些 k 都是 Twice k 的形式，因此应该足以归纳地表明

Twice Z : IsTwice Z 表示 IsEven Z，
如果Twice k : IsTwice (k+k)意味着IsEven (k+k)，
那么Twice (S k) : IsTwice ((S k) + (S k))意味着IsEven ((S k) + (S k))。

total isTwiceImpliesIsEven : IsTwice n -> IsEven n
isTwiceImpliesIsEven (Twice Z) = IsZero
isTwiceImpliesIsEven (Twice (S k))
  = let twoKIsEven = isTwiceImpliesIsEven (Twice k) in
    let result = PlusTwo (plus k k) twoKIsEven in
    rewrite sym (plusSuccRightSucc k k) in result

除了 Idris 不相信证明是 total:

之外，这是可行的

Main.isTwiceImpliesIsEven is possibly not total due to recursive path Main.isTwiceImpliesIsEven --> Main.isTwiceImpliesIsEven

我怎样才能做到total？

Answer 1

即使 k 小于 S k，完整性检查器也无法计算出 k + k 小于 S k + S k，因为它只会减少到 S (k + S k).但是，Prelude.WellFounded 中的 sizeAccessible (k + k) 会有所帮助。在每次递归调用中，您提供 LTE 证明 k + k 总是变小。

LTERightSucc : (k:Nat) -> LTE k (S k)
LTERightSucc Z = LTEZero
LTERightSucc (S k) = LTESucc $ LTERightSucc k

total
isTwiceImpliesIsEven : IsTwice n -> IsEven n
isTwiceImpliesIsEven (Twice k) with (sizeAccessible (k + k))
  isTwiceImpliesIsEven (Twice Z) | acc = IsZero
  isTwiceImpliesIsEven (Twice (S k)) | (Access rec) =
    let twoKIsEven = (isTwiceImpliesIsEven (Twice k) |
      rec _ (LTESucc $ rewrite plusCommutative k (S k) in LTERightSucc (k+k))) in
        let result = PlusTwo (plus k k) twoKIsEven in
    rewrite sym (plusSuccRightSucc k k) in result

在对单个构造函数参数进行归纳时证明完整性

Proving totality when doing induction on single constructor argument

idris