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

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

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

open import Data.Vec.Base as Vec
open import Data.Vec.Relation.Unary.All as All using (All; []; _∷_)
import Data.Vec.Relation.Unary.All.Properties as All
open import Data.Vec.Relation.Unary.Linked as Linked
  using (Linked; []; [-]; _∷_)
open import Data.Fin.Base using (zero; suc; _<_)
open import Data.Nat.Base using (ℕ; zero; suc; s<s⁻¹)
open import Level using (Level)
open import Function.Base using (_on_)
open import Relation.Binary.Core using (Rel)
open import Relation.Binary.Definitions using (Transitive)
open import Relation.Unary using (Pred; Decidable)

private
  variable
    a b p r ℓ : Level
    m n : ℕ
    A : Set a
    B : Set b
    R : Rel A r

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

module _ (trans : Transitive R) where

  Linked⇒All : ∀ {v} {xs : Vec _ (suc n)} → R v (head xs) →
               Linked R xs → All (R v) xs
  Linked⇒All Rvx [-]         = Rvx ∷ []
  Linked⇒All Rvx (Rxy ∷ Rxs) = Rvx ∷ Linked⇒All (trans Rvx Rxy) Rxs

  lookup⁺ : ∀ {i j} {xs : Vec _ n} →
           Linked R xs → i < j →
           R (lookup xs i) (lookup xs j)
  lookup⁺ {i = zero}  {j = suc j} (rx ∷ rxs) i<j = All.lookup⁺ (Linked⇒All rx rxs) j
  lookup⁺ {i = suc i} {j = suc j} (_  ∷ rxs) i<j = lookup⁺ rxs (s<s⁻¹ i<j)

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

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

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