# 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