------------------------------------------------------------------------
-- The Agda standard library
--
-- Property related to Grouped
------------------------------------------------------------------------

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

module Data.List.Relation.Unary.Grouped.Properties where

open import Data.Bool.Base using (true; false)
open import Data.List.Base using ([]; [_]; _∷_; map; derun)
open import Data.List.Relation.Unary.All as All using (All; []; _∷_)
import Data.List.Relation.Unary.All.Properties as All
open import Data.List.Relation.Unary.AllPairs as AllPairs using (AllPairs; []; _∷_)
open import Data.List.Relation.Unary.Grouped
open import Data.Product.Base using (_,_)
open import Function.Base using (_∘_; _on_)
open import Level using (Level)
open import Relation.Binary.Definitions as B
open import Relation.Binary.Core using (_⇔_; REL; Rel)
open import Relation.Unary as U using (Pred)
open import Relation.Nullary.Decidable.Core using (does; yes; no)
open import Relation.Nullary.Negation.Core using (¬_; contradiction)

private
  variable
    a b c p q : Level
    A B C : Set a

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

module _ (P : Rel A p) (Q : Rel B q) where

  map⁺ : ∀ {f xs} → P ⇔ (Q on f) → Grouped P xs → Grouped Q (map f xs)
  map⁺ P⇔Q            []                      = []
  map⁺ P⇔Q@(_ , Q⇒P) (all[¬Px,xs] ∷≉ g[xs]) = All.gmap⁺ (_∘ Q⇒P) all[¬Px,xs] ∷≉ map⁺ P⇔Q g[xs]
  map⁺ P⇔Q@(P⇒Q , _) (Px₁x₂ ∷≈ g[xs])       = P⇒Q Px₁x₂ ∷≈ map⁺ P⇔Q g[xs]

  map⁻ : ∀ {f xs} → P ⇔ (Q on f) → Grouped Q (map f xs) → Grouped P xs
  map⁻ {xs = []}          P⇔Q            []                  = []
  map⁻ {xs = _ ∷ []}     P⇔Q            ([] ∷≉ [])         = [] ∷≉ []
  map⁻ {xs = _ ∷ _ ∷ _} P⇔Q@(P⇒Q , _) (all[¬Qx,xs] ∷≉ g) = All.gmap⁻ (_∘ P⇒Q) all[¬Qx,xs] ∷≉ map⁻ P⇔Q g
  map⁻ {xs = _ ∷ _ ∷ _} P⇔Q@(_ , Q⇒P) (Qx₁x₂ ∷≈ g)       = Q⇒P Qx₁x₂ ∷≈ map⁻ P⇔Q g

------------------------------------------------------------------------
-- [_]

module _ (P : Rel A p) where

  [_]⁺ : ∀ x → Grouped P [ x ]
  [_]⁺ x = [] ∷≉ []

------------------------------------------------------------------------
-- derun

module _ {P : Rel A p} (P? : B.Decidable P) where

  grouped[xs]⇒unique[derun[xs]] : ∀ xs → Grouped P xs → AllPairs (λ x y → ¬ P x y) (derun P? xs)
  grouped[xs]⇒unique[derun[xs]] [] [] = []
  grouped[xs]⇒unique[derun[xs]] (x ∷ []) ([] ∷≉ []) = [] ∷ []
  grouped[xs]⇒unique[derun[xs]] (x ∷ y ∷ xs) (all[¬Px,y∷xs]@(¬Pxy ∷ _) ∷≉ grouped[y∷xs]) with P? x y
  ... | yes Pxy  = contradiction Pxy ¬Pxy
  ... | no  _    = All.derun⁺ P? all[¬Px,y∷xs] ∷ grouped[xs]⇒unique[derun[xs]] (y ∷ xs) grouped[y∷xs]
  grouped[xs]⇒unique[derun[xs]] (x ∷ y ∷ xs) (Pxy ∷≈ grouped[xs]) with P? x y
  ... | yes _    = grouped[xs]⇒unique[derun[xs]] (y ∷ xs) grouped[xs]
  ... | no  ¬Pxy = contradiction Pxy ¬Pxy