Tales of Tails by trigott

module Theorem where

open import Definitions
open import Data.List
open import Data.List.Any hiding (map)
open import Data.Product using (Σ; _×_; _,_; proj₁; proj₂; Σ-syntax)
open import Data.Sum using (_⊎_; inj₁; inj₂; [_,_])
open import Relation.Binary.PropositionalEquality using (_≡_; cong; refl; trans; sym)
open import Function.Equivalence hiding (map; sym)
open import Function.Equality hiding (cong)

drop-∷ : ∀ {a} {A : Set a} {x y : A} {xs ys : List A} → x ∷ xs ≡ y ∷ ys → xs ≡ ys
drop-∷ refl = refl

[]-identity : ∀ {a} {A : Set a} (l : List A) → l ++ [] ≡ l
[]-identity [] = refl
[]-identity (x ∷ l) = cong (_∷_ x) ([]-identity l)

mytails : ∀ {a} {A : Set a} (ys : List A) → Σ[ xss ∈ List (List A) ] xss isAllSuffixOf ys
mytails {A = A} [] =
  [ [] ] ,
  λ xs → record {
    to = record {
      _⟨$⟩_ = $₁ xs;
      cong = λ eq → cong ($₁ xs) eq
    };
    from = record {
      _⟨$⟩_ = $₂ xs;
      cong = λ eq → cong ($₂ xs) eq
    }
  }
  where $₁ : (xs : List A) → (x : Σ (List A) (λ zs → zs ++ xs ≡ [])) → Any (_≡_ xs) ([] ∷ [])
        $₁ xs x = here (proj₂ (lem (proj₁ x) xs (proj₂ x)))
          where lem : ∀ {a} {A : Set a} (l r : List A) → l ++ r ≡ [] → l ≡ [] × r ≡ []
                lem [] r eq = refl , eq
                lem (x ∷ l) r ()
        $₂ : (xs : List A) → (x : Any (_≡_ xs) ([] ∷ [])) → Σ (List A) (λ zs → zs ++ xs ≡ [])
        $₂ xs x = xs , lem₁ (f xs x) (f xs x)
          where lem₁ : ∀ {a} {A : Set a} {l r : List A} → l ≡ [] → r ≡ [] → l ++ r ≡ []
                lem₁ refl refl = refl
                f : (xs : List A) → Any (_≡_ xs) ([] ∷ []) → xs ≡ []
                f xs (here px) = px
                f xs (there ())
mytails {A = A} (y ∷ ys) =
  new ,
  λ xs → record {
    to = record {
      _⟨$⟩_ = $₁ xs;
      cong = λ eq → cong ($₁ xs) eq
    };
    from = record {
      _⟨$⟩_ = $₂ xs;
      cong = λ eq → cong ($₂ xs) eq
    }
  }
  where pre-prf = proj₂ (mytails ys)
        pre = proj₁ (mytails ys)
        new = (y ∷ ys) ∷ pre

        $₁ : (xs : List A) → (p : Σ (List A) (λ zs → zs ++ xs ≡ y ∷ ys)) → Any (_≡_ xs) new
        $₁ xs ([] , eq) = here eq
        $₁ xs (z ∷ zs , eq) = there ((Π._⟨$⟩_ (Equivalence.to (pre-prf xs))) (zs , drop-∷ eq))

        $₂ : (xs : List A) → (p : Any (_≡_ xs) new) → Σ (List A) (λ zs → zs ++ xs ≡ y ∷ ys)
        $₂ xs (here px) = [] , px
        $₂ xs (there p) with (Π._⟨$⟩_ (Equivalence.from (pre-prf xs))) p
        ... | zs , eq = y ∷ zs , cong (_∷_ y) eq