------------------------------------------------------------------------ -- Pointwise lifting of relations to vectors ------------------------------------------------------------------------ {-# OPTIONS --universe-polymorphism #-} module Relation.Binary.Vec.Pointwise where open import Category.Applicative.Indexed open import Data.Fin open import Data.Plus as Plus hiding (equivalent; map) open import Data.Vec as Vec hiding ([_]; map) import Data.Vec.Properties as VecProp open import Function open import Function.Equality using (_⟨$⟩_) open import Function.Equivalence as Equiv using (_⇔_; module Equivalent) open import Level open import Relation.Binary open import Relation.Binary.PropositionalEquality as P using (_≡_) open import Relation.Nullary private module Dummy {a} {A : Set a} where -- Functional definition. record Pointwise (_∼_ : Rel A a) {n} (xs ys : Vec A n) : Set a where constructor ext field app : ∀ i → lookup i xs ∼ lookup i ys -- Inductive definition. infixr 5 _∷_ data Pointwise′ (_∼_ : Rel A a) : ∀ {n} (xs ys : Vec A n) → Set a where [] : Pointwise′ _∼_ [] [] _∷_ : ∀ {n x y} {xs ys : Vec A n} (x∼y : x ∼ y) (xs∼ys : Pointwise′ _∼_ xs ys) → Pointwise′ _∼_ (x ∷ xs) (y ∷ ys) -- The two definitions are equivalent. equivalent : ∀ {_∼_ : Rel A a} {n} {xs ys : Vec A n} → Pointwise _∼_ xs ys ⇔ Pointwise′ _∼_ xs ys equivalent {_∼_} = Equiv.equivalent (to _ _) from where to : ∀ {n} (xs ys : Vec A n) → Pointwise _∼_ xs ys → Pointwise′ _∼_ xs ys to [] [] xs∼ys = [] to (x ∷ xs) (y ∷ ys) xs∼ys = Pointwise.app xs∼ys zero ∷ to xs ys (ext (Pointwise.app xs∼ys ∘ suc)) nil : Pointwise _∼_ [] [] nil = ext λ() cons : ∀ {n x y} {xs ys : Vec A n} → x ∼ y → Pointwise _∼_ xs ys → Pointwise _∼_ (x ∷ xs) (y ∷ ys) cons {x = x} {y} {xs} {ys} x∼y xs∼ys = ext helper where helper : ∀ i → lookup i (x ∷ xs) ∼ lookup i (y ∷ ys) helper zero = x∼y helper (suc i) = Pointwise.app xs∼ys i from : ∀ {n} {xs ys : Vec A n} → Pointwise′ _∼_ xs ys → Pointwise _∼_ xs ys from [] = nil from (x∼y ∷ xs∼ys) = cons x∼y (from xs∼ys) -- Pointwise preserves reflexivity. refl : ∀ {_∼_ : Rel A a} {n} → Reflexive _∼_ → Reflexive (Pointwise _∼_ {n = n}) refl rfl = ext (λ _ → rfl) -- Pointwise preserves symmetry. sym : ∀ {_∼_ : Rel A a} {n} → Symmetric _∼_ → Symmetric (Pointwise _∼_ {n = n}) sym sm xs∼ys = ext λ i → sm (Pointwise.app xs∼ys i) -- Pointwise preserves transitivity. trans : ∀ {_∼_ : Rel A a} {n} → Transitive _∼_ → Transitive (Pointwise _∼_ {n = n}) trans trns xs∼ys ys∼zs = ext λ i → trns (Pointwise.app xs∼ys i) (Pointwise.app ys∼zs i) -- Pointwise preserves equivalences. isEquivalence : ∀ {_∼_ : Rel A a} {n} → IsEquivalence _∼_ → IsEquivalence (Pointwise _∼_ {n = n}) isEquivalence equiv = record { refl = refl (IsEquivalence.refl equiv) ; sym = sym (IsEquivalence.sym equiv) ; trans = trans (IsEquivalence.trans equiv) } -- Pointwise _≡_ is equivalent to _≡_. Pointwise-≡ : ∀ {n} {xs ys : Vec A n} → Pointwise _≡_ xs ys ⇔ xs ≡ ys Pointwise-≡ = Equiv.equivalent (to ∘ _⟨$⟩_ (Equivalent.to equivalent)) (λ xs≡ys → P.subst (Pointwise _≡_ _) xs≡ys (refl P.refl)) where to : ∀ {n} {xs ys : Vec A n} → Pointwise′ _≡_ xs ys → xs ≡ ys to [] = P.refl to (P.refl ∷ xs∼ys) = P.cong (_∷_ _) $ to xs∼ys -- Pointwise and Plus commute when the underlying relation is -- reflexive. ⁺∙⇒∙⁺ : ∀ {_∼_ : Rel A a} {n} {xs ys : Vec A n} → Plus (Pointwise _∼_) xs ys → Pointwise (Plus _∼_) xs ys ⁺∙⇒∙⁺ [ ρ≈ρ′ ] = ext (λ x → [ Pointwise.app ρ≈ρ′ x ]) ⁺∙⇒∙⁺ (ρ ∼⁺⟨ ρ≈ρ′ ⟩ ρ′≈ρ″) = ext (λ x → _ ∼⁺⟨ Pointwise.app (⁺∙⇒∙⁺ ρ≈ρ′ ) x ⟩ Pointwise.app (⁺∙⇒∙⁺ ρ′≈ρ″) x) ∙⁺⇒⁺∙ : ∀ {_∼_ : Rel A a} {n} {xs ys : Vec A n} → Reflexive _∼_ → Pointwise (Plus _∼_) xs ys → Plus (Pointwise _∼_) xs ys ∙⁺⇒⁺∙ {_∼_} x∼x = Plus.map (_⟨$⟩_ (Equivalent.from equivalent)) ∘ helper ∘ _⟨$⟩_ (Equivalent.to equivalent) where helper : ∀ {n} {xs ys : Vec A n} → Pointwise′ (Plus _∼_) xs ys → Plus (Pointwise′ _∼_) xs ys helper [] = [ [] ] helper (_∷_ {x = x} {y = y} {xs = xs} {ys = ys} x∼y xs∼ys) = x ∷ xs ∼⁺⟨ Plus.map (λ x∼y → x∼y ∷ xs∼xs) x∼y ⟩ y ∷ xs ∼⁺⟨ Plus.map (λ xs∼ys → x∼x ∷ xs∼ys) (helper xs∼ys) ⟩∎ y ∷ ys ∎ where xs∼xs : Pointwise′ _∼_ xs xs xs∼xs = Equivalent.to equivalent ⟨$⟩ refl x∼x open Dummy public -- Note that ∙⁺⇒⁺∙ cannot be defined if the requirement of reflexivity -- is dropped. private module Counterexample where data D : Set where i j x y z : D data _R_ : Rel D zero where iRj : i R j xRy : x R y yRz : y R z xR⁺z : x [ _R_ ]⁺ z xR⁺z = x ∼⁺⟨ [ xRy ] ⟩ y ∼⁺⟨ [ yRz ] ⟩∎ z ∎ ix = i ∷ x ∷ [] jz = j ∷ z ∷ [] ix∙⁺jz : Pointwise′ (Plus _R_) ix jz ix∙⁺jz = [ iRj ] ∷ xR⁺z ∷ [] ¬ix⁺∙jz : ¬ Plus′ (Pointwise′ _R_) ix jz ¬ix⁺∙jz [ iRj ∷ () ∷ [] ] ¬ix⁺∙jz ((iRj ∷ xRy ∷ []) ∷ [ () ∷ yRz ∷ [] ]) ¬ix⁺∙jz ((iRj ∷ xRy ∷ []) ∷ (() ∷ yRz ∷ []) ∷ _) counterexample : ¬ (∀ {n} {xs ys : Vec D n} → Pointwise (Plus _R_) xs ys → Plus (Pointwise _R_) xs ys) counterexample ∙⁺⇒⁺∙ = ¬ix⁺∙jz (Equivalent.to Plus.equivalent ⟨$⟩ Plus.map (_⟨$⟩_ (Equivalent.to equivalent)) (∙⁺⇒⁺∙ (Equivalent.from equivalent ⟨$⟩ ix∙⁺jz))) -- Map. map : ∀ {a} {A : Set a} {_R_ _R′_ : Rel A a} {n} → _R_ ⇒ _R′_ → Pointwise _R_ ⇒ Pointwise _R′_ {n} map R⇒R′ xsRys = ext λ i → R⇒R′ (Pointwise.app xsRys i) -- A variant. gmap : ∀ {a} {A A′ : Set a} {_R_ : Rel A a} {_R′_ : Rel A′ a} {f : A → A′} {n} → _R_ =[ f ]⇒ _R′_ → Pointwise _R_ =[ Vec.map {n = n} f ]⇒ Pointwise _R′_ gmap {_R′_ = _R′_} {f} R⇒R′ {i = xs} {j = ys} xsRys = ext λ i → let module M = Morphism (VecProp.lookup-morphism i) in P.subst₂ _R′_ (P.sym $ M.op-<$> f xs) (P.sym $ M.op-<$> f ys) (R⇒R′ (Pointwise.app xsRys i))