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

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为 any定义一个函数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 ksome的形式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

除了伊德里斯不相信证明是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