如何在 Agda 中实现 Floyd 的兔兔算法？

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

这使我们可以有效地将列表一分为二：

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) 的案例。但是，这种情况绝不应该出现。我如何向 Agda 证明这种情况永远不会发生？

---

这是该算法如何工作的直观示例：

+-------------+-------------+
|   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 ^ |
+---------------+---------------+

当兔子（floyd 的第二个参数）到达列表的末尾时，乌龟（floyd 的第一个参数）到达列表的中间。因此，通过使用两个指针（第二个的移动速度是第一个的两倍），我们可以有效地将一个列表一分为二。

Answer 1

与 Twan van Laarhoven 在 cmets 中建议的内容相同，但使用 Vecs。他的版本可能更好。

open import Function
open import Data.Nat.Base
open import Data.Product renaming (map to pmap)
open import Data.List.Base
open import Data.Vec hiding (split)

≤-step : ∀ {m n} -> m ≤ n -> m ≤ suc n
≤-step  z≤n     = z≤n
≤-step (s≤s le) = s≤s (≤-step le)

≤-refl : ∀ {n} -> n ≤ n
≤-refl {0}     = z≤n
≤-refl {suc n} = s≤s ≤-refl

floyd : ∀ {A : Set} {n m} -> m ≤ n -> Vec A n -> Vec A m -> List A × List A
floyd  z≤n            xs       []          = [] , toList xs
floyd (s≤s  z≤n)     (x ∷ xs) (y ∷ [])     = x ∷ [] , toList xs
floyd (s≤s (s≤s le)) (x ∷ xs) (y ∷ z ∷ ys) = pmap (x ∷_) id (floyd (≤-step le) xs ys)

split : ∀ {A : Set} -> List A -> List A × List A
split xs = floyd ≤-refl (fromList xs) (fromList xs)

open import Relation.Binary.PropositionalEquality

test₁ : split (1 ∷ 2 ∷ 3 ∷ 4 ∷ 5 ∷ []) ≡ (1 ∷ 2 ∷ 3 ∷ [] , 4 ∷ 5 ∷ [])
test₁ = refl

test₂ : split (1 ∷ 2 ∷ 3 ∷ 4 ∷ 5 ∷ 6 ∷ []) ≡ (1 ∷ 2 ∷ 3 ∷ [] , 4 ∷ 5 ∷ 6 ∷ [])
test₂ = refl

另外，≤-refl 和 ≤-step 之类的函数在标准库中的某个位置，但我懒得去搜索。

---

这是我like要做的一件傻事：

open import Function
open import Data.Nat.Base
open import Data.Product renaming (map to pmap)
open import Data.List.Base
open import Data.Vec hiding (split)

floyd : ∀ {A : Set}
      -> (k : ℕ -> ℕ)
      -> (∀ {n} -> Vec A (k (suc n)) -> Vec A (suc (k n)))
      -> ∀ n
      -> Vec A (k n)
      -> List A × List A
floyd k u  0            xs = [] , toList xs
floyd k u  1            xs with u xs
... | x ∷ xs' = x ∷ [] , toList xs'
floyd k u (suc (suc n)) xs with u xs
... | x ∷ xs' = pmap (x ∷_) id (floyd (k ∘ suc) u n xs')

split : ∀ {A : Set} -> List A -> List A × List A
split xs = floyd id id (length xs) (fromList xs)

open import Relation.Binary.PropositionalEquality

test₁ : split (1 ∷ 2 ∷ 3 ∷ 4 ∷ 5 ∷ []) ≡ (1 ∷ 2 ∷ 3 ∷ [] , 4 ∷ 5 ∷ [])
test₁ = refl

test₂ : split (1 ∷ 2 ∷ 3 ∷ 4 ∷ 5 ∷ 6 ∷ []) ≡ (1 ∷ 2 ∷ 3 ∷ [] , 4 ∷ 5 ∷ 6 ∷ [])
test₂ = refl

这部分基于以下评论中的 Benjamin Hodgson 建议。