CODEWITHSUNDEEP
idris
Stefan Dorn
Stefan Dorn

Reputation: 599

Recursive function is not total due to with block

I created a function which returns decidable property if the list is an ordered sequence with a step +1.

data Increasing : List Nat -> Type where
  IncreasingSingle : Increasing [x]
  IncreasingMany   : Increasing (S k :: xs) -> Increasing (k :: S k :: xs)

emptyImpossible : Increasing [] -> Void
emptyImpossible IncreasingSingle impossible
emptyImpossible (IncreasingMany _) impossible

firstElementWrong : (contraFirst : (S x = y) -> Void) -> Increasing (x :: y :: xs) -> Void
firstElementWrong contraFirst (IncreasingMany seq) = contraFirst Refl

nextElementWrong : (contraNext : Increasing ((S x) :: xs) -> Void) -> Increasing (x :: (S x) :: xs) -> Void
nextElementWrong contraNext (IncreasingMany seq) = contraNext seq

increasing : (xs : List Nat) -> Dec (Increasing xs)
increasing [] = No emptyImpossible
increasing (x :: []) = Yes IncreasingSingle
increasing (x :: y :: xs) with ((S x) `decEq` y)
  increasing (x :: y :: xs) | No contraFirst = No (firstElementWrong contraFirst)
  increasing (x :: (S x) :: xs) | Yes Refl with (increasing ((S x) :: xs))
    increasing (x :: (S x) :: xs) | Yes Refl | No contraNext = No (nextElementWrong contraNext)
    increasing (x :: (S x) :: xs) | Yes Refl | Yes prf = Yes (IncreasingMany prf)

However increasing is not total because of:

increasing [] = No emptyImpossible
| ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Main.increasing is possibly not total due to: with block in Main.increasing

Can someone explain me why it's not total and how to make it total?

Upvotes: 1

Views: 68

Answers (1)

michaelmesser
michaelmesser

Reputation: 3726

I managed to get it working with case:

increasing : (xs : List Nat) -> Dec (Increasing xs)
increasing [] = No emptyImpossible
increasing (x :: []) = Yes IncreasingSingle
increasing (x :: y :: xs) = case S x `decEq` y of
    Yes Refl => case increasing (S x :: xs) of
        Yes p => Yes $ IncreasingMany p
        No p => No $ \(IncreasingMany x) => p x
    No p => No $ \(IncreasingMany x) => p Refl

Upvotes: 1

Related Questions