------------------------------------------------------------------------
-- The Agda standard library
--
-- Interleavings of lists using propositional equality
------------------------------------------------------------------------

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

module Data.List.Relation.Ternary.Interleaving.Propositional {a} {A : Set a} where

open import Data.List.Base as List using (List; []; _∷_; _++_)
open import Data.List.Relation.Binary.Permutation.Propositional as Perm using (_↭_)
open import Data.List.Relation.Binary.Permutation.Propositional.Properties using (shift)
import Data.List.Relation.Ternary.Interleaving.Setoid as General
open import Relation.Binary.PropositionalEquality.Core using (refl)
open import Relation.Binary.PropositionalEquality.Properties using (setoid)
open Perm.PermutationReasoning

------------------------------------------------------------------------
-- Re-export the basic combinators

open General hiding (Interleaving) public

------------------------------------------------------------------------
-- Definition

Interleaving : List A → List A → List A → Set a
Interleaving = General.Interleaving (setoid A)

pattern consˡ xs = refl ∷ˡ xs
pattern consʳ xs = refl ∷ʳ xs

------------------------------------------------------------------------
-- New combinators

toPermutation : ∀ {l r as} → Interleaving l r as → as ↭ l ++ r
toPermutation []         = Perm.refl
toPermutation (consˡ sp) = Perm.prep _ (toPermutation sp)
toPermutation {l} {r ∷ rs} {a ∷ as} (consʳ sp) = begin
  a ∷ as       ↭⟨ Perm.prep a (toPermutation sp) ⟩
  a ∷ l ++ rs  ↭⟨ Perm.↭-sym (shift a l rs) ⟩
  l ++ a ∷ rs  ∎