BySym.agda

module BySym where

open import Data.List
open import Data.Sum as ⊎
open import Relation.Binary.PropositionalEquality

module _ {a} {A : Set a} where
  infix 4 _≤_
  data _≤_ : (xs ys : List A) → Set where
    []≤[] : [] ≤ []
    []≤∷ : ∀ {x xs} → [] ≤ x ∷ xs
    ∷≤∷ : ∀ {x y xs ys} → xs ≤ ys → x ∷ xs ≤ y ∷ ys

  total : (xs ys : List A) → xs ≤ ys ⊎ ys ≤ xs
  total [] [] = inj₁ []≤[]
  total [] (y ∷ ys) = inj₁ []≤∷
  total (x ∷ xs) [] = inj₂ []≤∷
  total (x ∷ xs) (y ∷ ys) = ⊎.map ∷≤∷ ∷≤∷ (total xs ys)

  cancel-≤ : (xs ys : List A) → xs ≤ ys → List A
  cancel-≤ [] [] []≤[] = []
  cancel-≤ [] (y ∷ ys) []≤∷ = y ∷ ys
  cancel-≤ (x ∷ xs) (y ∷ ys) (∷≤∷ xs≤ys) = cancel-≤ xs ys xs≤ys

  cancel : (xs ys : List A) → List A
  cancel xs ys with total xs ys
  ... | inj₁ xs≤ys = cancel-≤ xs ys xs≤ys
  ... | inj₂ ys≤xs = cancel-≤ ys xs ys≤xs

  cancel-is-drop-≤ : (xs ys : List A) (xs≤ys : xs ≤ ys) →
                     cancel-≤ xs ys xs≤ys ≡ drop (length xs) ys
  cancel-is-drop-≤ [] [] []≤[] = refl
  cancel-is-drop-≤ [] (y ∷ ys) []≤∷ = refl
  cancel-is-drop-≤ (x ∷ xs) (y ∷ ys) (∷≤∷ xs≤ys) = cancel-is-drop-≤ xs ys xs≤ys

  cancel-is-drop : (xs ys : List A) →
                     cancel xs ys ≡ drop (length xs) ys
                   ⊎ cancel xs ys ≡ drop (length ys) xs
  cancel-is-drop xs ys with total xs ys
  ... | inj₁ xs≤ys = inj₁ (cancel-is-drop-≤ xs ys xs≤ys)
  ... | inj₂ ys≤xs = inj₂ (cancel-is-drop-≤ ys xs ys≤xs)