------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of interleaving using setoid equality
------------------------------------------------------------------------

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

open import Relation.Binary.Bundles using (Setoid)

module Data.List.Relation.Ternary.Interleaving.Setoid.Properties
  {c ℓ} (S : Setoid c ℓ) where

open import Data.List.Base using (List; []; _∷_; filter; _++_)
open import Data.Bool.Base using (true; false)
open import Relation.Unary using (Decidable)
open import Relation.Nullary.Decidable using (does)
open import Relation.Nullary.Decidable using (¬?)
open import Function.Base using (_∘_)

open import Data.List.Relation.Binary.Equality.Setoid S using (≋-refl)
open import Data.List.Relation.Ternary.Interleaving.Setoid S
open Setoid S renaming (Carrier to A)

------------------------------------------------------------------------
-- Re-exporting existing properties

open import Data.List.Relation.Ternary.Interleaving.Properties public

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

++-linear : (xs ys : List A) → Interleaving xs ys (xs ++ ys)
++-linear xs ys = ++-disjoint (left ≋-refl) (right ≋-refl)

------------------------------------------------------------------------
-- filter

module _ {p} {P : A → Set p} (P? : Decidable P) where

  filter⁺ : ∀ xs → Interleaving (filter P? xs) (filter (¬? ∘ P?) xs) xs
  filter⁺ []       = []
  filter⁺ (x ∷ xs) with does (P? x)
  ... | true  = refl ∷ˡ filter⁺ xs
  ... | false = refl ∷ʳ filter⁺ xs