{-# 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)
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