如何在Agda中实现Floyd的Hare和Tortoise算法？

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在评论中提出的相同但是与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在标准库中的某个地方,但我懒得搜索.

这是我喜欢做的傻事:

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建议.