# Tales of Tails by Rotsor

module Theorem {a} {A : Set a} where
open import Definitions
open import Data.List
open import Data.List.Any
open import Data.Product
open import Function.Equivalence
import Relation.Binary.PropositionalEquality as PropEq
open Data.List.Any.Membership-≡
mutual
data PTails : List (List A) → List A → Set a where
ptails0 : PTails [] []
ptails+ : ∀ x {xs tt} → Tails tt xs → PTails tt (x ∷ xs)
data Tails : List (List A) → List A → Set a where
tailss : ∀ {xs tt} → PTails tt xs → Tails (xs ∷ tt) xs
mytails' : ∀ (ys : List A) → Σ[ xss ∈ List (List A) ] Tails xss ys
mytails' [] = [] ∷ [] , tailss ptails0
mytails' (x ∷ ys) with mytails' ys
... | (xss , xss-good) = (x ∷ ys) ∷ xss , tailss (ptails+ x xss-good)
to' : ∀ xs ps {xss} → Tails xss (ps ++ xs) → (xs ∈ xss)
to' xs [] (tailss x) = here PropEq.refl
to' xs (x ∷ ps) (tailss (ptails+ .x x₁)) = there (to' xs ps x₁)
th : ∀ {ys xss} → Tails xss ys → xss isAllSuffixOf ys
th t xs = equivalence (to xs t) (from xs t) where
to : ∀ xs {ys xss} → Tails xss ys → xs isSuffixOf ys → (xs ∈ xss)
to xs t (ps , PropEq.refl) = to' _ ps t
from : ∀ xs {ys xss} → Tails xss ys → (xs ∈ xss) → xs isSuffixOf ys
from _ (tailss _) (here h) = [] , h
from _ (tailss ptails0) (there ())
from _ (tailss (ptails+ x t)) (there i) with from _ t i
... | p , g = x ∷ p , PropEq.cong (_∷_ x) g
mytails : ∀ (ys : List A) → Σ[ xss ∈ List (List A) ] xss isAllSuffixOf ys
mytails l with mytails' l
... | (r , t) = (r , th t)