48 lines
1.6 KiB
Agda
48 lines
1.6 KiB
Agda
|
{-# 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 (α ∘ β)
|