Formalize `Prefix`, `Suffix` and `Infix` as relations on Lists

[gallais]

Rather than Haskell's

isPrefixOf :: Eq a => [a] -> [a] -> Bool
isSuffixOf :: Eq a => [a] -> [a] -> Bool
isInfixOf :: Eq a => [a] -> [a] -> Bool

it would be nice to have evidence-producing versions of these functions. Note that Data.List.Relation.Sublist already gives us that for isSubsequenceOf.

• [x] Prefix (#522)
• [x] Suffix (#551)
• [ ] Infix

[gallais]

Something to think about: Suffix could be generalised to

module _ (R : REL (List A) (List B) r) where

  data Suffix : REL (List A) (List B) (a ⊔ b ⊔ r) where
    here  : ∀ {as bs} → R as bs → Suffix as bs
    there : ∀ {b as bs} → Suffix as bs → Suffix as (b ∷ bs)

We then recover the usual suffix as Suffix (Pointwise R) but we can also get Infix as Suffix (Prefix R).

[jamesmckinna]

Is this issue not already closed by the existing definitions under Data.List.Relation.Binary.*, or is there more to say/do here?

UPDATED: it seems as though Data.List.Relation.Binary.Infix.Homogeneous.Properties is an incomplete stub, but that Data.List.Relation.Binary.Infix.Heterogeneous{.Properties} is all there, so... leave this open? Or close?

[MatthewDaggitt]

I think close. If people want to open an issue for extending the Infix stub then they can...