------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of permutation (with K)
------------------------------------------------------------------------

{-# OPTIONS --safe --with-K #-}

module Data.List.Relation.Binary.Permutation.Propositional.Properties.WithK where

open import Function.Base using (_$_)
open import Function.Bundles using (_⇔_; mk⇔)
open import Function.Related.Propositional using (SK-sym; module EquationalReasoning)

open import Data.List.Base using (deduplicate; _++_)
open import Data.List.Membership.Propositional using (_∈_)
open import Data.List.Membership.Propositional.Properties using (++-∈⇔; deduplicate-∈⇔)
open import Data.List.Membership.Propositional.Properties.WithK using (unique∧set⇒bag)
open import Data.List.Relation.Unary.Unique.Propositional.Properties using (++⁺)
open import Data.List.Relation.Binary.Disjoint.Propositional using (Disjoint)
open import Data.List.Relation.Binary.Disjoint.Propositional.Properties
  using (deduplicate⁺)
open import Data.List.Relation.Binary.Permutation.Propositional using (_↭_)
open import Data.List.Relation.Binary.BagAndSetEquality using (∼bag⇒↭)

open import Data.Sum as Sum using (_⊎_)
open import Data.Sum.Function.Propositional using (_⊎-cong_)

open import Relation.Binary.Definitions using (DecidableEquality)

------------------------------------------------------------------------
-- deduplicate

module _ {a} {A : Set a} (_≟_ : DecidableEquality A) where

  private
    dedup≡   = deduplicate    _≟_
    ∈-dedup≡ = deduplicate-∈⇔ _≟_

  open import Data.List.Relation.Unary.Unique.DecPropositional.Properties _≟_
    using (deduplicate-!)

  dedup-++-↭ : ∀ {xs ys} → Disjoint xs ys → dedup≡ (xs ++ ys) ↭ dedup≡ xs ++ dedup≡ ys
  dedup-++-↭ {xs} {ys} disj
    = ∼bag⇒↭
    $ unique∧set⇒bag
        (deduplicate-! _)
        (++⁺ (deduplicate-! _) (deduplicate-! _) (deduplicate⁺ _≟_ disj))
    λ {x} → begin
    x ∈ dedup≡ (xs ++ ys)           ∼⟨ SK-sym ∈-dedup≡ ⟩
    x ∈ xs ++ ys                    ∼⟨ ++-∈⇔ ⟩
    (x ∈ xs ⊎ x ∈ ys)               ∼⟨ ∈-dedup≡ ⊎-cong ∈-dedup≡ ⟩
    (x ∈ dedup≡ xs ⊎ x ∈ dedup≡ ys) ∼⟨ SK-sym ++-∈⇔ ⟩
    x ∈ dedup≡ xs ++ dedup≡ ys      ∎ where open EquationalReasoning