Tales of Tails by notogawa

module Theorem where

open import Definitions
open import Data.List
open import Data.Product
open import Function.Equivalence
open import Data.List.Any
open Data.List.Any.Membership-≡
open import Relation.Binary.PropositionalEquality

suffix→tails : ∀ {a} {A : Set a} (xs ys : List A) →
               xs isSuffixOf ys → xs ∈ tails ys
suffix→tails xs [] ([] , []++xs≡[]) = here []++xs≡[]
suffix→tails xs (y ∷ ys) ([] , []++xs≡y∷ys) = here []++xs≡y∷ys
suffix→tails xs [] (p ∷ ps , ())
suffix→tails xs (y ∷ ys) (p ∷ ps , p∷ps++xs≡y∷ys) = there (suffix→tails xs ys (ps , inversion p∷ps++xs≡y∷ys))
  where
    inversion : ∀ {a} {A : Set a} {x y : A} {xs ys : List A} →
                x ∷ xs ≡ y ∷ ys → xs ≡ ys
    inversion refl = refl

tails→suffix : ∀ {a} {A : Set a} (xs ys : List A) →
               xs ∈ tails ys → xs isSuffixOf ys
tails→suffix xs [] (here px) = [] , px
tails→suffix xs [] (there ())
tails→suffix xs (y ∷ ys) (here px) = [] , px
tails→suffix xs (y ∷ ys) (there x) = ∷-keepSuffix (tails→suffix xs ys x)
  where
    ∷-keepSuffix : ∀ {a} {A : Set a} {xs ys : List A} →
                   xs isSuffixOf ys → ∀ {p} → xs isSuffixOf (p ∷ ys)
    ∷-keepSuffix (ps , ps++xs≡ys) {p} = (p ∷ ps) , cong (_∷_ p) ps++xs≡ys

mytails : ∀ {a} {A : Set a} (ys : List A) → Σ[ xss ∈ List (List A) ] xss isAllSuffixOf ys
mytails ys = (tails ys) , (λ xs → equivalence (suffix→tails xs ys) (tails→suffix xs ys))