对单个构造函数参数进行归纳时证明总数

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上的函数，但是要对k构造函数的Twice参数进行归纳，而不是对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类型的任何值（见证）对于某些Twice k都是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)。但是，可以通过sizeAccessible (k + k)中的Prelude.WellFounded进行帮助。在每个递归调用中，提供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