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