Proving totality when doing induction on single constructor argument

Question

We have the following type with a single constructor:

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

I'm trying to define a function on IsTwice n for any n, but by doing induction on the k argument to the Twice constructor, rather than the n argument to IsTwice. My problem is that I can't get Idris to accept my definition as total.

Here's a specific example. Let's say we have a second type:

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

I'd like to prove that IsTwice n implies IsEven n. My intuition is: We know that any value (witness) of type IsTwice n is of the form Twice k for some k, so it should be enough to inductively show that

• Twice Z : IsTwice Z implies IsEven Z, and
• if Twice k : IsTwice (k+k) implies IsEven (k+k),
  then Twice (S k) : IsTwice ((S k) + (S k)) implies 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

This works except for the fact that Idris is not convinced that the proof is total:

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

How can I make it total?

Answer 1

Even so k is smaller than S k, the totality checker cannot figure out that k + k is smaller than S k + S k as it will only reduce to S (k + S k). However, it can be helped with sizeAccessible (k + k) in Prelude.WellFounded. On each recursive call you provide a LTE proving k + k always gets smaller.

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