Data.List.Relation.Unary.Linked.Properties

------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties related to Linked
------------------------------------------------------------------------

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

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

open import Data.Bool.Base using (true; false)
open import Data.List.Base hiding (any)
open import Data.List.Relation.Unary.AllPairs as AllPairs
  using (AllPairs; []; _∷_)
import Data.List.Relation.Unary.AllPairs.Properties as AllPairs
open import Data.List.Relation.Unary.All using (All; []; _∷_)
open import Data.List.Relation.Unary.Linked as Linked
  using (Linked; []; [-]; _∷_)
open import Data.Nat.Base using (zero; suc; _<_; z<s; s<s)
open import Data.Nat.Properties using (≤-refl; m≤n⇒m≤1+n)
open import Data.Maybe.Relation.Binary.Connected
  using (Connected; just; nothing; just-nothing; nothing-just)
open import Level using (Level)
open import Function.Base using (_∘_; flip; _on_)
open import Relation.Binary.Core using (Rel)
open import Relation.Binary.Bundles using (DecSetoid)
open import Relation.Binary.Definitions using (Transitive)
open import Relation.Binary.PropositionalEquality.Core using (_≢_)
open import Relation.Unary using (Pred; Decidable)
open import Relation.Nullary.Decidable using (yes; no; does)

private
  variable
    a b p ℓ : Level
    A : Set a
    B : Set b

------------------------------------------------------------------------
-- Relationship to other predicates
------------------------------------------------------------------------

module _ {R : Rel A ℓ} where

  AllPairs⇒Linked : ∀ {xs} → AllPairs R xs → Linked R xs
  AllPairs⇒Linked []                    = []
  AllPairs⇒Linked (px ∷ [])             = [-]
  AllPairs⇒Linked ((px ∷ _) ∷ py ∷ pxs) =
    px ∷ (AllPairs⇒Linked (py ∷ pxs))

module _ {R : Rel A ℓ} (trans : Transitive R) where

  Linked⇒All : ∀ {v x xs} → R v x →
               Linked R (x ∷ xs) → All (R v) (x ∷ xs)
  Linked⇒All Rvx [-]         = Rvx ∷ []
  Linked⇒All Rvx (Rxy ∷ Rxs) = Rvx ∷ Linked⇒All (trans Rvx Rxy) Rxs

  Linked⇒AllPairs : ∀ {xs} → Linked R xs → AllPairs R xs
  Linked⇒AllPairs []          = []
  Linked⇒AllPairs [-]         = [] ∷ []
  Linked⇒AllPairs (Rxy ∷ Rxs) = Linked⇒All Rxy Rxs ∷ Linked⇒AllPairs Rxs

------------------------------------------------------------------------
-- Introduction (⁺) and elimination (⁻) rules for list operations
------------------------------------------------------------------------
-- map

module _ {R : Rel A ℓ} {f : B → A} where

  map⁺ : ∀ {xs} → Linked (R on f) xs → Linked R (map f xs)
  map⁺ []           = []
  map⁺ [-]          = [-]
  map⁺ (Rxy ∷ Rxs)  = Rxy ∷ map⁺ Rxs

  map⁻ : ∀ {xs} → Linked R (map f xs) → Linked (R on f) xs
  map⁻ {[]}         []           = []
  map⁻ {x ∷ []}     [-]          = [-]
  map⁻ {x ∷ y ∷ xs} (Rxy ∷ Rxs)  = Rxy ∷ map⁻ Rxs

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

module _ {R : Rel A ℓ} where

  ++⁺ : ∀ {xs ys} →
        Linked R xs →
        Connected R (last xs) (head ys) →
        Linked R ys →
        Linked R (xs ++ ys)
  ++⁺ []          _          Rys         = Rys
  ++⁺ [-]         _          []          = [-]
  ++⁺ [-]         (just Rxy) [-]         = Rxy ∷ [-]
  ++⁺ [-]         (just Rxy) (Ryz ∷ Rys) = Rxy ∷ Ryz ∷ Rys
  ++⁺ (Rxy ∷ Rxs) Rxsys      Rys         = Rxy ∷ ++⁺ Rxs Rxsys Rys

------------------------------------------------------------------------
-- applyUpTo

module _ {R : Rel A ℓ} where

  applyUpTo⁺₁ : ∀ f n → (∀ {i} → suc i < n → R (f i) (f (suc i))) →
                Linked R (applyUpTo f n)
  applyUpTo⁺₁ f 0               Rf = []
  applyUpTo⁺₁ f 1               Rf = [-]
  applyUpTo⁺₁ f (suc n@(suc _)) Rf =
    Rf (s<s z<s) ∷ (applyUpTo⁺₁ (f ∘ suc) n (Rf ∘ s<s))

  applyUpTo⁺₂ : ∀ f n → (∀ i → R (f i) (f (suc i))) →
                Linked R (applyUpTo f n)
  applyUpTo⁺₂ f n Rf = applyUpTo⁺₁ f n (λ _ → Rf _)

------------------------------------------------------------------------
-- applyDownFrom

module _ {R : Rel A ℓ} where

  applyDownFrom⁺₁ : ∀ f n → (∀ {i} → suc i < n → R (f (suc i)) (f i)) →
                    Linked R (applyDownFrom f n)
  applyDownFrom⁺₁ f 0               Rf = []
  applyDownFrom⁺₁ f 1               Rf = [-]
  applyDownFrom⁺₁ f (suc n@(suc _)) Rf =
    Rf ≤-refl ∷ applyDownFrom⁺₁ f n (Rf ∘ m≤n⇒m≤1+n)

  applyDownFrom⁺₂ : ∀ f n → (∀ i → R (f (suc i)) (f i)) →
                    Linked R (applyDownFrom f n)
  applyDownFrom⁺₂ f n Rf = applyDownFrom⁺₁ f n (λ _ → Rf _)

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

module _ {P : Pred A p} (P? : Decidable P)
         {R : Rel A ℓ} (trans : Transitive R)
         where

  ∷-filter⁺ : ∀ {x xs} → Linked R (x ∷ xs) → Linked R (x ∷ filter P? xs)
  ∷-filter⁺ [-] = [-]
  ∷-filter⁺ {xs = y ∷ _} (r ∷ [-]) with does (P? y)
  ... | false = [-]
  ... | true  = r ∷ [-]
  ∷-filter⁺ {x = x} {xs = y ∷ ys} (r ∷ r′ ∷ rs)
    with does (P? y) | ∷-filter⁺ {xs = ys} | ∷-filter⁺ (r′ ∷ rs)
  ... | false | ihf | _   = ihf (trans r r′ ∷ rs)
  ... | true  | _   | iht = r ∷ iht

  filter⁺   : ∀ {xs} → Linked R xs → Linked R (filter P? xs)
  filter⁺ [] = []
  filter⁺ {xs = x ∷ []} [-] with does (P? x)
  ... | false = []
  ... | true  = [-]
  filter⁺ {xs = x ∷ _} (r ∷ rs) with does (P? x)
  ... | false = filter⁺ rs
  ... | true  = ∷-filter⁺ (r ∷ rs)