open import Data.List
open import Data.List.Properties
open import Data.Nat using (ℕ; zero; suc; _+_; pred; _∸_)
open import Data.Nat.Properties
open import Data.Nat.Properties.Simple
open import Data.Product

open import Relation.Binary.PropositionalEquality as ≡
open ≡-Reasoning

-- Two trivial lemmata about append.

postulate
  append-nil : ∀{A : Set} (xs : List A) → xs ++ [] ≡ xs
  append-assoc :  ∀{A : Set} (xs ys zs : List A) →
    xs ++ (ys ++ zs) ≡ (xs ++ ys) ++ zs

-- Logical definition of suffix.

_IsSuffixOf_ : ∀{A} → List A → List A → Set
ys IsSuffixOf zs = ∃ λ xs → xs ++ ys ≡ zs

-- Lemma: drop always returns a suffix.

drop-suffix : ∀{A : Set} (n : ℕ) (xs : List A) →
  drop n xs IsSuffixOf xs
drop-suffix 0       xs       = [] , refl
drop-suffix (suc n) []       = [] , refl
drop-suffix (suc n) (x ∷ xs) with drop-suffix n xs
... | ws , p =  (x ∷ ws) , cong (λ zs → x ∷ zs) p

-- Lemma: dropping after prefixing is the identity.

drop-prefix : ∀{A : Set} (ws xs : List A) →
  drop (length ws) (ws ++ xs) ≡ xs
drop-prefix []       xs = refl
drop-prefix (w ∷ ws) xs = drop-prefix ws xs

-- Lemma: dropping all returns the empty list.

drop-all : ∀{A : Set} (xs : List A) →
  drop (length xs) xs ≡ []
drop-all []       = refl
drop-all (x ∷ xs) = drop-all xs

-- Variant 1: compute candiate for xs being suffix ys by
--
--   drop (length ys - length xs) ys

module LengthDiff where

  -- Soundness of suffix-test.

  drop-monus-suffix : ∀{A : Set} (xs ys : List A) →
    drop (length ys ∸ length xs) ys ≡ xs → xs IsSuffixOf ys

  drop-monus-suffix xs ys p = subst (λ ws → ws IsSuffixOf ys) p
                                 (drop-suffix (length ys ∸ length xs) ys)

  -- Lemma: Substracting the length of an added suffix
  --        gives the length of the original list.

  length-monus-suffix :  ∀{A : Set} (ws xs : List A) →
    length (ws ++ xs) ∸ length xs ≡ length ws

  length-monus-suffix ws xs = begin
    length (ws ++ xs)     ∸ length xs   ≡⟨ cong (λ l → l ∸ length xs) (length-++ ws) ⟩
    length ws + length xs ∸ length xs   ≡⟨ m+n∸n≡m (length ws) (length xs) ⟩
    length ws
    ∎

  -- Lemma: Dropping the a prefix computed from the length of the whole list.

  drop-prefix+- : ∀{A : Set} (ws xs : List A) →
    drop (length (ws ++ xs) ∸ length xs) (ws ++ xs) ≡ xs

  drop-prefix+- ws xs = begin
    drop (length (ws ++ xs) ∸ length xs) (ws ++ xs)    ≡⟨  cong (λ l → drop l (ws ++ xs)) (length-monus-suffix ws xs) ⟩
    drop (length ws) (ws ++ xs)                        ≡⟨  drop-prefix ws xs ⟩
    xs
    ∎

  -- Completeness of suffix-test.

  suffix-drop-monus : ∀{A : Set} (xs ys : List A) →
    xs IsSuffixOf ys → drop (length ys ∸ length xs) ys ≡ xs

  suffix-drop-monus xs .(ws ++ xs) (ws , refl) = drop-prefix+- ws xs

-- Variant 2: compute candiate for xs being suffix ys by
--
--   drop (length (drop length xs) ys) ys

module LengthDrop where

  -- Soundness of suffix-test.

  drop-length-suffix : ∀{A : Set} (xs ys : List A) →
    drop (length (drop (length xs) ys)) ys ≡ xs → xs IsSuffixOf ys

  drop-length-suffix xs ys p = subst (λ ws → ws IsSuffixOf ys) p
                                 (drop-suffix (length (drop (length xs) ys)) ys)

  -- Lemma.

  length-drop-suffix : ∀{A : Set} (ws xs : List A)
     → length (drop (length xs) (ws ++ xs)) ≡ length ws

  length-drop-suffix ws []       = cong length (append-nil ws)
  length-drop-suffix [] (x ∷ xs) = cong length (drop-all xs)
  length-drop-suffix (w ∷ ws) (x ∷ xs) = begin

      length (drop (length (x ∷ xs)) (w ∷ ws ++ x ∷ xs))

   ≡⟨⟩

      length (drop (length xs) (ws ++ x ∷ xs))

   ≡⟨ cong (λ ys → length (drop (length xs) ys)) (append-assoc ws (x ∷ []) xs) ⟩

      length (drop (length xs) ((ws ++ x ∷ []) ++ xs))

   ≡⟨ length-drop-suffix (ws ++ x ∷ []) xs ⟩

      length (ws ++ x ∷ [])

   ≡⟨ length-++ ws ⟩

      length ws + 1

   ≡⟨ +-comm _ 1 ⟩

      length (w ∷ ws)
   ∎

  -- Lemma 2.

  drop-prefix+- : ∀{A : Set} (ws xs : List A) →
      drop (length (drop (length xs) (ws ++ xs))) (ws ++ xs) ≡ xs

  drop-prefix+- ws xs = begin
      drop (length (drop (length xs) (ws ++ xs))) (ws ++ xs)

    ≡⟨  cong (λ l → drop l (ws ++ xs)) (length-drop-suffix ws xs)  ⟩

      drop (length ws) (ws ++ xs)

    ≡⟨  drop-prefix ws xs ⟩

      xs
    ∎

  -- Completeness of suffix-test.

  suffix-drop-length : ∀{A : Set} (xs ys : List A) →
    xs IsSuffixOf ys → drop (length (drop (length xs) ys)) ys ≡ xs

  suffix-drop-length xs .(ws ++ xs) (ws , refl) = drop-prefix+- ws xs

-- There should be a short way from Variant 1 to Variant 2 proving
-- length (drop (length xs) ys) ≡ length ys ∸ length xs