haskell - アグダでフロイドのウサギとカメのアルゴリズムを実装するには?

Question

次の Haskell コードを Agda に変換したい:

import Control.Arrow (first)
import Control.Monad (join)

safeTail :: [a] -> [a]
safeTail []     = []
safeTail (_:xs) = xs

floyd :: [a] -> [a] -> ([a], [a])
floyd xs     []     = ([], xs)
floyd (x:xs) (_:ys) = first (x:) $ floyd xs (safeTail ys)

split :: [a] -> ([a], [a])
split = join floyd

これにより、リストを効率的に 2 つに分割できます。

split [1,2,3,4,5]   = ([1,2,3], [4,5])
split [1,2,3,4,5,6] = ([1,2,3], [4,5,6])

そこで、このコードを Agda に変換しようとしました。

floyd : {A : Set} → List A → List A → List A × List A
floyd xs        []        = ([] , xs)
floyd (x :: xs) (_ :: ys) = first (x ::_) (floyd xs (safeTail ys))

唯一の問題は、Agda が のケースが見つからないと不平を言うことですfloyd [] (y :: ys)。ただし、このケースは決して発生してはなりません。このケースが決して起こらないことをアグダにどのように証明できますか?

---

このアルゴリズムがどのように機能するかの視覚的な例を次に示します。

+-------------+-------------+
|   Tortoise  |     Hare    |
+-------------+-------------+
| ^ 1 2 3 4 5 | ^ 1 2 3 4 5 |
| 1 ^ 2 3 4 5 | 1 2 ^ 3 4 5 |
| 1 2 ^ 3 4 5 | 1 2 3 4 ^ 5 |
| 1 2 3 ^ 4 5 | 1 2 3 4 5 ^ |
+-------------+-------------+

別の例を次に示します。

+---------------+---------------+
|    Tortoise   |      Hare     |
+---------------+---------------+
| ^ 1 2 3 4 5 6 | ^ 1 2 3 4 5 6 |
| 1 ^ 2 3 4 5 6 | 1 2 ^ 3 4 5 6 |
| 1 2 ^ 3 4 5 6 | 1 2 3 4 ^ 5 6 |
| 1 2 3 ^ 4 5 6 | 1 2 3 4 5 6 ^ |
+---------------+---------------+

ウサギ ( の 2 番目の引数floyd) がリストの最後に到達すると、カメ ( の最初の引数floyd) がリストの中央に到達します。したがって、2 つのポインター (2 番目のポインターは最初のポインターの 2 倍の速度で移動する) を使用することで、リストを効率的に 2 つに分割できます。