由于 with 块，递归函数不完整答案

【问题标题】：Recursive function is not total due to with block由于 with 块，递归函数不完整
【发布时间】：2022-06-22 13:01:04
【问题描述】：

我创建了一个函数，如果列表是一个带步长 +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)

但增加并不完全是因为：

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

谁能解释一下为什么它不完全以及如何使它完全？

【问题讨论】：

标签： idris

【解决方案1】：

我设法让它与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

【讨论】：