Tales of Tails by masahiro_sakai

module Theorem where

open import Definitions
open import Data.List
open import Data.List.Any
open import Data.Product
open import Data.Unit
open import Function.Equivalence
open import Function.Equality hiding (cong)
open import Relation.Binary.PropositionalEquality
open import Level
open Data.List.Any.Membership-≡

≡-tail : ∀ {a} {A : Set a} (x y : A) (xs ys : List A) → x ∷ xs ≡ y ∷ ys → xs ≡ ys
≡-tail {a} {A} x y xs ys x∷xs≡y∷ys = cong f x∷xs≡y∷ys
  where
    f : List A → List A
    f (x ∷ xs) = xs
    f [] = []

mytails : ∀ {a} {A : Set a} (ys : List A) → Σ[ xss ∈ List (List A) ] xss isAllSuffixOf ys
mytails {a} {A} [] = ( [] ∷ [] , (λ xs → equivalence (f xs) (g xs)) )
  where
    f : ∀ (xs : List A) → (xs isSuffixOf []) → (xs ∈ ([] ∷ []))
    f xs ([] , xs≡[]) = here xs≡[]
    f xs (z ∷ zs , ())

    g : ∀ (xs : List A) → (xs ∈ ([] ∷ [])) → (xs isSuffixOf [])
    g xs (here p) = ( [] , p )
    g xs (there ())
mytails {a} {A} (y ∷ ys) = ( (y ∷ ys) ∷ xss , (λ xs → equivalence (f xs) (g xs)) )
  where
    P : Σ[ xss ∈ List (List A) ] xss isAllSuffixOf ys
    P = mytails ys

    xss : List (List A)
    xss = proj₁ P 

    Q : xss isAllSuffixOf ys
    Q = proj₂ P

    f : ∀ (xs : List A) → xs isSuffixOf (y ∷ ys) → xs ∈ (y ∷ ys) ∷ xss
    f xs ([] , xs≡y∷ys) = here xs≡y∷ys
    f xs (z ∷ zs , zzs++xs≡y∷ys) = there (Equivalence.to (Q xs) ⟨$⟩ (zs , zs++xs≡ys))
      where
        zs++xs≡ys : zs ++ xs ≡ ys
        zs++xs≡ys = ≡-tail z y (zs ++ xs) ys zzs++xs≡y∷ys

    g : ∀ (xs : List A) → xs ∈ (y ∷ ys) ∷ xss → xs isSuffixOf (y ∷ ys)
    g xs (here R) =  ([] , R)
    g xs (there S) = (y ∷ proj₁ T , (cong (λ zs → y ∷ zs) (proj₂ T)))
      where
        T : Σ[ zs ∈ List A ] (zs ++ xs ≡ ys)
        T = Equivalence.from (Q xs) ⟨$⟩ S