# 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))