{-# OPTIONS --safe --without-K #-}

module Thinning where

open import Data.List.Base using (List; []; _∷_)
open import Level using (Level)
open import Relation.Binary.Core using (Rel)

private
  variable
    a : Level
    A : Set a
    xs ys zs : List A

-- The type of a Thinning
------------------------------------------------------------------------

-- A thinning is a way of saying how we can find every element of a list in
-- another list, in the right order.
data Thinning (A : Set a) : Rel (List A) a where
  -- We can certainly find every element of the empty list in the empty list.
  -- This is generally the base case for recursion on thinnings.
  end : Thinning A [] []
  -- It's possible we'll find the first element of the smaller list at the head
  -- of the larger list.
  include : {x : A} → Thinning A xs ys → Thinning A (x ∷ xs) (x ∷ ys)
  -- It's also possible that we won't, and have to look deeper in the larger
  -- list.
  exclude : {x : A} → Thinning A xs ys → Thinning A xs (x ∷ ys)

-- Operations on Thinnings
------------------------------------------------------------------------

-- I'm choosing the names here to emphasize that there is a category of
-- Thinnings.

-- There is always a Thinning from the list to itself. We include at every step.
id : Thinning A xs xs
id {xs = []} = end
id {xs = x ∷ xs} = include id

-- We can compose two Thinnings!
_∘_ : Thinning A ys zs → Thinning A xs ys → Thinning A xs zs
end ∘ end = end
include α ∘ include β = include (α ∘ β)
include α ∘ exclude β = exclude (α ∘ β)
exclude α ∘ β = exclude (α ∘ β)

-- There is always a Thinning from the empty list to any list. Here we exclude
-- at every step.
¡ : Thinning A [] xs
¡ {xs = []} = end
¡ {xs = x ∷ xs} = exclude ¡