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?
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