Come implementare l'algoritmo Hare e Tortoise di Floyd in Agda?

Question

Voglio tradurre il seguente codice Haskell in 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 

Questo ci permette di dividere in modo efficiente un elenco in due:

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

Così, ho provato a convertire questo codice per 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)) 

L'unico problema è che Agda si lamenta che mi manca il caso di floyd [] (y :: ys). Tuttavia, questo caso non dovrebbe mai sorgere. Come posso dimostrare ad Agda che questo caso non dovrebbe mai sorgere?

---

Ecco un esempio visivo di come funziona questo algoritmo:

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

Ecco un altro esempio:

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

Quando la lepre (il secondo argomento di floyd) raggiunge la fine della elenco, la tartaruga (il primo argomento a floyd) raggiunge il centro dell'elenco. Pertanto, utilizzando due puntatori (il secondo si muove due volte più velocemente del primo) possiamo dividere in modo efficiente una lista in due.

Answer 1

La stessa cosa di Twan van Laarhoven suggerisce nei commenti ma con Vec s. La sua versione è probabilmente migliore.

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 

Inoltre, funzioni come ≤-refl e ≤-step sono da qualche parte nella libreria standard, ma ero pigro per la ricerca.

---

Ecco una cosa sciocca che like di fare:

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 

Questo è in parte basato sul Benjamin Hodgson suggerimento nel commento qui sotto.