    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Properties of general interleavings
    ------------------------------------------------------------------------

    {-# OPTIONS --cubical-compatible --safe #-}

    module Data.List.Relation.Ternary.Interleaving.Properties where

    open import Data.Nat.Base
    open import Data.Nat.Properties using (+-suc)
    open import Data.List.Base hiding (_∷ʳ_)
    open import Data.List.Properties using (reverse-involutive)
    open import Data.List.Relation.Ternary.Interleaving hiding (map)
    open import Function.Base using (_$_)
    open import Relation.Binary.Core using (REL)
    open import Relation.Binary.PropositionalEquality.Core
      using (_≡_; refl; sym; cong)
    open import Relation.Binary.PropositionalEquality.Properties
      using (module ≡-Reasoning)
    open ≡-Reasoning

    ------------------------------------------------------------------------
    -- length

    module _ {a b c l r} {A : Set a} {B : Set b} {C : Set c}
             {L : REL A C l} {R : REL B C r} where

      interleave-length : ∀ {as l r} → Interleaving L R l r as →
                          length as ≡ length l + length r
      interleave-length []        = refl
      interleave-length (l ∷ˡ sp) = cong suc (interleave-length sp)
      interleave-length {as} {l} {r ∷ rs} (_ ∷ʳ sp) = begin
        length as                   ≡⟨ cong suc (interleave-length sp) ⟩
        suc (length l + length rs)  ≡⟨ sym $ +-suc _ _ ⟩
        length l + length (r ∷ rs)  ∎

    ------------------------------------------------------------------------
    -- _++_

      ++⁺ : ∀ {as₁ as₂ l₁ l₂ r₁ r₂} →
            Interleaving L R as₁ l₁ r₁ →
            Interleaving L R as₂ l₂ r₂ →
            Interleaving L R (as₁ ++ as₂) (l₁ ++ l₂) (r₁ ++ r₂)
      ++⁺ []         sp₂ = sp₂
      ++⁺ (l ∷ˡ sp₁) sp₂ = l ∷ˡ (++⁺ sp₁ sp₂)
      ++⁺ (r ∷ʳ sp₁) sp₂ = r ∷ʳ (++⁺ sp₁ sp₂)

      ++-disjoint : ∀ {as₁ as₂ l₁ r₂} →
                    Interleaving L R l₁ [] as₁ →
                    Interleaving L R [] r₂ as₂ →
                    Interleaving L R l₁ r₂ (as₁ ++ as₂)
      ++-disjoint []         sp₂ = sp₂
      ++-disjoint (l ∷ˡ sp₁) sp₂ = l ∷ˡ ++-disjoint sp₁ sp₂

    ------------------------------------------------------------------------
    -- map

    module _ {a b c d e f l r}
             {A : Set a} {B : Set b} {C : Set c}
             {D : Set d} {E : Set e} {F : Set f}
             {L : REL A C l} {R : REL B C r}
             (f : E → A) (g : F → B) (h : D → C)
             where

      map⁺ : ∀ {as l r} →
             Interleaving (λ x z → L (f x) (h z)) (λ y z → R (g y) (h z)) l r as  →
             Interleaving L R (map f l) (map g r) (map h as)
      map⁺ []        = []
      map⁺ (l ∷ˡ sp) = l ∷ˡ map⁺ sp
      map⁺ (r ∷ʳ sp) = r ∷ʳ map⁺ sp

      map⁻ : ∀ {as l r} →
             Interleaving L R (map f l) (map g r) (map h as) →
             Interleaving (λ x z → L (f x) (h z)) (λ y z → R (g y) (h z)) l r as
      map⁻ {[]}    {[]}    {[]}    []        = []
      map⁻ {_ ∷ _} {[]}    {_ ∷ _} (r ∷ʳ sp) = r ∷ʳ map⁻ sp
      map⁻ {_ ∷ _} {_ ∷ _} {[]}    (l ∷ˡ sp) = l ∷ˡ map⁻ sp
      map⁻ {_ ∷ _} {_ ∷ _} {_ ∷ _} (l ∷ˡ sp) = l ∷ˡ map⁻ sp
      map⁻ {_ ∷ _} {_ ∷ _} {_ ∷ _} (r ∷ʳ sp) = r ∷ʳ map⁻ sp

    ------------------------------------------------------------------------
    -- reverse

    module _ {a b c l r} {A : Set a} {B : Set b} {C : Set c}
             {L : REL A C l} {R : REL B C r}
             where

      reverseAcc⁺ : ∀ {as₁ as₂ l₁ l₂ r₁ r₂} →
                    Interleaving L R l₁ r₁ as₁ →
                    Interleaving L R l₂ r₂ as₂ →
                    Interleaving L R (reverseAcc l₁ l₂) (reverseAcc r₁ r₂) (reverseAcc as₁ as₂)
      reverseAcc⁺ sp₁ []         = sp₁
      reverseAcc⁺ sp₁ (l ∷ˡ sp₂) = reverseAcc⁺ (l ∷ˡ sp₁) sp₂
      reverseAcc⁺ sp₁ (r ∷ʳ sp₂) = reverseAcc⁺ (r ∷ʳ sp₁) sp₂

      ʳ++⁺ : ∀ {as₁ as₂ l₁ l₂ r₁ r₂} →
             Interleaving L R l₁ r₁ as₁ →
             Interleaving L R l₂ r₂ as₂ →
             Interleaving L R (l₁ ʳ++ l₂) (r₁ ʳ++ r₂) (as₁ ʳ++ as₂)
      ʳ++⁺ sp₁ sp₂ = reverseAcc⁺ sp₂ sp₁

      reverse⁺ : ∀ {as l r} → Interleaving L R l r as →
                 Interleaving L R (reverse l) (reverse r) (reverse as)
      reverse⁺ = reverseAcc⁺ []

      reverse⁻ : ∀ {as l r} → Interleaving L R (reverse l) (reverse r) (reverse as) →
                 Interleaving L R l r as
      reverse⁻ {as} {l} {r} sp with reverse⁺ sp
      ... | sp′ rewrite reverse-involutive as
                      | reverse-involutive l
                      | reverse-involutive r = sp′