Tales of Tails by Lost_dog_

module Theorem where

open import Definitions
open import Data.List hiding (map)
open import Data.List.Any hiding (map)
open Data.List.Any.Membership-≡
open import Data.Product

open import Relation.Binary.PropositionalEquality using (_≡_; cong)
open import Function.Equality using (_⟨$⟩_)
open import Function.Equivalence using (equivalence)
open Function.Equivalence.Equivalence using (to; from)

-- proving by induction on List
listInd :
  ∀ {a} {A : Set a}
  → (P : List A → Set a)
  → (P [])
  → (∀ x xs → P xs → P (x ∷ xs))
  → (∀ xs → P xs)
listInd P pn pc []       = pn
listInd P pn pc (x ∷ xs) = pc x xs (listInd P pn pc xs)

-- proving by induction on Any
anyInd :
  ∀ {a} {A : Set a} {x : A} {xs : List A}
  → (P : A → Set a)
  → (Q : Any P (x ∷ xs) → Set a)
  → (∀ px → Q (here px))
  → (∀ pxs → Q (there pxs))
  → (∀ a → Q a)
anyInd P Q h t (here px)   = h px
anyInd P Q h t (there pxs) = t pxs 


mytails : ∀ {a} {A : Set a} (ys : List A) → Σ[ xss ∈ List (List A) ] (xss isAllSuffixOf ys)
mytails {a} {A} = listInd P pn pc
  where
  P : List A → Set a
  P ys = Σ[ xss ∈ List (List A) ] (xss isAllSuffixOf ys)

  pn : P []
  pn = [ [] ] , (λ ys → 
      (equivalence 
        (λ w → listInd (λ zs → zs ++ ys ≡ [] → ys ∈ [ [] ]) 
                         here 
                         (λ _ _ _ → λ ())
                         (proj₁ w)
                         (proj₂ w))
        (anyInd (_≡_ ys)
                (λ _ → Σ (List A) (λ v → v ++ ys ≡ []))
                (_,_ [])
                (λ ()) )))

  pc : ∀ x xs → P xs → P (x ∷ xs)
  pc x xs (tss , p) = (x ∷ xs) ∷ tss , (λ ys → 
      (equivalence
        (λ w → listInd (λ zs → zs ++ ys ≡ x ∷ xs → ys ∈ (x ∷ xs) ∷ tss)
                         here
                         (λ v vs r s → there (to (p ys) ⟨$⟩ (vs , cong (drop 1) s)))
                         (proj₁ w)
                         (proj₂ w))
        (anyInd (_≡_ ys)
                (λ _ → Σ (List A) (λ zs → zs ++ ys ≡ x ∷ xs))
                (_,_ [])
                (λ pxs → map (_∷_ x) (cong (_∷_ x)) (from (p ys) ⟨$⟩ pxs)))))