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)