Wie implementiert man Floyds Hare and Tortoise-Algorithmus in Agda?

Question

Ich möchte folgendes Haskell-Code in Agda übersetzen: us

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 

Dies ermöglicht es, effizient eine Liste in zwei Teile aufgeteilt:

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

Also habe ich versucht, diesen Code zu Agda konvertieren:

Das einzige Problem ist, dass Agda beschwert, dass ich den Fall für vermisse. Dieser Fall sollte jedoch niemals auftreten. Wie kann ich Agda beweisen, dass dieser Fall niemals auftauchen sollte?

---

Hier ist ein visuelles Beispiel dafür, wie dieser Algorithmus funktioniert:

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

Hier ein weiteres Beispiel:

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

Wenn der Hase (das zweite Argument zu floyd) das Ende der erreicht Liste, die Schildkröte (das erste Argument zu floyd) erreicht die Mitte der Liste. Indem wir zwei Zeiger verwenden (der zweite bewegt sich doppelt so schnell wie der erste), können wir eine Liste effizient in zwei teilen.

Answer 1

Das gleiche wie Twan van Laarhoven schlägt in den Kommentaren aber mit Vec s. Seine Version ist wahrscheinlich besser.

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 

Auch Funktionen wie ≤-refl und ≤-step sind irgendwo in der Standard-Bibliothek, aber ich war faul zu suchen.

---

Hier ist eine dumme Sache, die ich like zu tun:

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 

Dies ist zum Teil auf der Grundlage des Benjamin Hodgson Vorschlag im Kommentar unten.