Add Data.List.Relation.Interleaving

[gallais]

This is a generalization of the idea that a list is split into two sublists in an order-respecting
way. The core definition is as follows. As usual we should have specialized versions for
Setoid & PropositionalEquality.

open import Relation.Binary

module Interleaving {a b l r} {A : Set a} {B : Set b} (L : REL A B l) (R : REL A B r) where

open import Data.List.Base

infix 3 _≣_⨝_
data _≣_⨝_ : List A → List B → List B → Set r where
  []   : [] ≣ [] ⨝ []
  _ˡ∷_ : ∀ {a as b l r} → L a b → as ≣ l ⨝ r → a ∷ as ≣ b ∷ l ⨝ r
  _ʳ∷_ : ∀ {a as l b r} → R a b → as ≣ l ⨝ r → a ∷ as ≣ l ⨝ b ∷ r

This thing has interesting interactions with OPEs e.g.

split : xs' ⊆ xs → xs ≣ us ⨝ vs →
        ∃ λ us' → ∃ λ vs' → xs' ≣ us' ⨝ vs' × us' ⊆ us × vs' ⊆ vs

[MatthewDaggitt]

Closed with ab43a34