{-# OPTIONS --cubical-compatible --safe #-}
module Data.Vec.Functional.Relation.Binary.Pointwise.Properties where
open import Data.Fin.Base using (zero; suc; _↑ˡ_; _↑ʳ_; splitAt)
open import Data.Fin.Properties using (all?; splitAt-↑ˡ; splitAt-↑ʳ)
open import Data.Nat.Base using (ℕ; zero; suc)
open import Data.Product.Base using (_×_; _,_; proj₁; proj₂)
open import Data.Product.Relation.Binary.Pointwise.NonDependent
using () renaming (Pointwise to ×-Pointwise)
open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_])
open import Data.Vec.Functional as VF hiding (map)
open import Data.Vec.Functional.Relation.Binary.Pointwise
open import Function.Base
open import Level using (Level)
open import Relation.Binary.Core using (Rel; REL)
open import Relation.Binary.Bundles using (Setoid; DecSetoid)
open import Relation.Binary.Structures
using (IsEquivalence; IsDecEquivalence)
open import Relation.Binary.Definitions
using (Reflexive; Transitive; Symmetric; Decidable)
open import Relation.Binary.PropositionalEquality.Core using (_≡_)
private
variable
a a′ a″ b b′ b″ r s t ℓ : Level
A : Set a
B : Set b
A′ : Set a′
B′ : Set b′
A″ : Set a″
B″ : Set b″
module _ {R : Rel A ℓ} where
refl : Reflexive R → ∀ {n} → Reflexive (Pointwise R {n})
refl r i = r
sym : Symmetric R → ∀ {n} → Symmetric (Pointwise R {n})
sym s xsys i = s (xsys i)
trans : Transitive R → ∀ {n} → Transitive (Pointwise R {n})
trans t xsys yszs i = t (xsys i) (yszs i)
decidable : Decidable R → ∀ {n} → Decidable (Pointwise R {n})
decidable r? xs ys = all? λ i → r? (xs i) (ys i)
isEquivalence : IsEquivalence R → ∀ n → IsEquivalence (Pointwise R {n})
isEquivalence isEq n = record
{ refl = refl Eq.refl
; sym = sym Eq.sym
; trans = trans Eq.trans
} where module Eq = IsEquivalence isEq
isDecEquivalence : IsDecEquivalence R →
∀ n → IsDecEquivalence (Pointwise R {n})
isDecEquivalence isDecEq n = record
{ isEquivalence = isEquivalence Eq.isEquivalence n
; _≟_ = decidable Eq._≟_
} where module Eq = IsDecEquivalence isDecEq
setoid : Setoid a ℓ → ℕ → Setoid a ℓ
setoid S n = record
{ isEquivalence = isEquivalence S.isEquivalence n
} where module S = Setoid S
decSetoid : DecSetoid a ℓ → ℕ → DecSetoid a ℓ
decSetoid S n = record
{ isDecEquivalence = isDecEquivalence S.isDecEquivalence n
} where module S = DecSetoid S
module _ {R : REL A B r} {S : REL A′ B′ s} {f : A → A′} {g : B → B′} where
map⁺ : (∀ {x y} → R x y → S (f x) (g y)) →
∀ {n} {xs : Vector A n} {ys : Vector B n} →
Pointwise R xs ys → Pointwise S (VF.map f xs) (VF.map g ys)
map⁺ f rs i = f (rs i)
module _ (R : REL A B r) {n} {xs : Vector A (suc n)} {ys} where
head⁺ : Pointwise R xs ys → R (head xs) (head ys)
head⁺ rs = rs zero
module _ (R : REL A B r) {n} {xs : Vector A (suc n)} {ys} where
tail⁺ : Pointwise R xs ys → Pointwise R (tail xs) (tail ys)
tail⁺ rs = rs ∘ suc
module _ (R : REL A B r) where
++⁺ : ∀ {m n xs ys xs′ ys′} →
Pointwise R {n = m} xs ys → Pointwise R {n = n} xs′ ys′ →
Pointwise R (xs ++ xs′) (ys ++ ys′)
++⁺ {m} rs rs′ i with splitAt m i
... | inj₁ i′ = rs i′
... | inj₂ j′ = rs′ j′
++⁻ˡ : ∀ {m n} (xs : Vector A m) (ys : Vector B m) {xs′ ys′} →
Pointwise R (xs ++ xs′) (ys ++ ys′) → Pointwise R xs ys
++⁻ˡ {m} {n} _ _ rs i with rs (i ↑ˡ n)
... | r rewrite splitAt-↑ˡ m i n = r
++⁻ʳ : ∀ {m n} (xs : Vector A m) (ys : Vector B m) {xs′ ys′} →
Pointwise R (xs ++ xs′) (ys ++ ys′) → Pointwise R xs′ ys′
++⁻ʳ {m} {n} _ _ rs i with rs (m ↑ʳ i)
... | r rewrite splitAt-↑ʳ m n i = r
++⁻ : ∀ {m n} xs ys {xs′ ys′} →
Pointwise R (xs ++ xs′) (ys ++ ys′) →
Pointwise R {n = m} xs ys × Pointwise R {n = n} xs′ ys′
++⁻ _ _ rs = ++⁻ˡ _ _ rs , ++⁻ʳ _ _ rs
module _ {R : REL A B r} {x y n} where
replicate⁺ : R x y → Pointwise R {n = n} (replicate n x) (replicate n y)
replicate⁺ = const
module _ {R : REL A B r} {S : REL A′ B′ s} {n} where
⊛⁺ : ∀ {fs : Vector (A → A′) n} {gs : Vector (B → B′) n} →
Pointwise (λ f g → ∀ {x y} → R x y → S (f x) (g y)) fs gs →
∀ {xs ys} → Pointwise R xs ys → Pointwise S (fs ⊛ xs) (gs ⊛ ys)
⊛⁺ rss rs i = (rss i) (rs i)
module _ {R : REL A B r} {S : REL A′ B′ s} {T : REL A″ B″ t} where
zipWith⁺ : ∀ {n xs ys xs′ ys′ f f′} →
(∀ {x y x′ y′} → R x y → S x′ y′ → T (f x x′) (f′ y y′)) →
Pointwise R xs ys → Pointwise S xs′ ys′ →
Pointwise T (zipWith f xs xs′) (zipWith f′ {n = n} ys ys′)
zipWith⁺ t rs ss i = t (rs i) (ss i)
module _ {R : REL A B r} {S : REL A′ B′ s} {n xs ys xs′ ys′} where
zip⁺ : Pointwise R xs ys → Pointwise S xs′ ys′ →
Pointwise (λ xx yy → R (proj₁ xx) (proj₁ yy) × S (proj₂ xx) (proj₂ yy))
(zip xs xs′) (zip {n = n} ys ys′)
zip⁺ rs ss i = rs i , ss i
zip⁻ : Pointwise (λ xx yy → R (proj₁ xx) (proj₁ yy) × S (proj₂ xx) (proj₂ yy))
(zip xs xs′) (zip {n = n} ys ys′) →
Pointwise R xs ys × Pointwise S xs′ ys′
zip⁻ rss = proj₁ ∘ rss , proj₂ ∘ rss
module _ {R : REL A B r} {S : REL A′ B′ s}
{f : A → A′ → A′} {g : B → B′ → B′}
where
foldr-cong : (∀ {w x y z} → R w x → S y z → S (f w y) (g x z)) →
∀ {d : A′} {e : B′} → S d e →
∀ {n} {xs : Vector A n} {ys : Vector B n} →
Pointwise R xs ys → S (foldr f d xs) (foldr g e ys)
foldr-cong fg-cong d~e {zero} rss = d~e
foldr-cong fg-cong d~e {suc n} rss =
fg-cong (rss zero) (foldr-cong fg-cong d~e (rss ∘ suc))