{-# OPTIONS --cubical-compatible --safe #-}
module Data.List.Relation.Binary.Pointwise where
open import Algebra.Core using (Op₂)
open import Function.Base
open import Function.Bundles using (Inverse)
open import Data.Bool.Base using (true; false)
open import Data.Product.Base hiding (map)
open import Data.List.Base as List hiding (map; head; tail; uncons)
open import Data.List.Properties using (≡-dec; length-++)
open import Data.List.Relation.Unary.All as All using (All; []; _∷_)
open import Data.List.Relation.Unary.AllPairs using (AllPairs; []; _∷_)
open import Data.List.Relation.Unary.Any using (Any; here; there)
open import Data.Fin.Base using (Fin; toℕ; cast) renaming (zero to fzero; suc to fsuc)
open import Data.Nat.Base using (ℕ; zero; suc)
open import Data.Nat.Properties
open import Level
open import Relation.Nullary hiding (Irrelevant)
import Relation.Nullary.Decidable as Dec using (map′)
open import Relation.Unary as U using (Pred)
open import Relation.Binary.Core renaming (Rel to Rel₂)
open import Relation.Binary.Definitions using (_Respects_; _Respects₂_)
open import Relation.Binary.Bundles using (Setoid; DecSetoid; Preorder; Poset)
open import Relation.Binary.Structures using (IsEquivalence; IsDecEquivalence; IsPartialOrder; IsPreorder)
open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
import Relation.Binary.PropositionalEquality.Properties as ≡
private
variable
a b c d p q ℓ ℓ₁ ℓ₂ : Level
A B C D : Set d
x y z : A
ws xs ys zs : List A
R S T : REL A B ℓ
open import Data.List.Relation.Binary.Pointwise.Base public
open import Data.List.Relation.Binary.Pointwise.Properties public
isEquivalence : IsEquivalence R → IsEquivalence (Pointwise R)
isEquivalence eq = record
{ refl = refl Eq.refl
; sym = symmetric Eq.sym
; trans = transitive Eq.trans
} where module Eq = IsEquivalence eq
isDecEquivalence : IsDecEquivalence R → IsDecEquivalence (Pointwise R)
isDecEquivalence eq = record
{ isEquivalence = isEquivalence DE.isEquivalence
; _≟_ = decidable DE._≟_
} where module DE = IsDecEquivalence eq
isPreorder : IsPreorder R S → IsPreorder (Pointwise R) (Pointwise S)
isPreorder pre = record
{ isEquivalence = isEquivalence Pre.isEquivalence
; reflexive = reflexive Pre.reflexive
; trans = transitive Pre.trans
} where module Pre = IsPreorder pre
isPartialOrder : IsPartialOrder R S →
IsPartialOrder (Pointwise R) (Pointwise S)
isPartialOrder po = record
{ isPreorder = isPreorder PO.isPreorder
; antisym = antisymmetric PO.antisym
} where module PO = IsPartialOrder po
setoid : Setoid a ℓ → Setoid a (a ⊔ ℓ)
setoid s = record
{ isEquivalence = isEquivalence (Setoid.isEquivalence s)
}
decSetoid : DecSetoid a ℓ → DecSetoid a (a ⊔ ℓ)
decSetoid d = record
{ isDecEquivalence = isDecEquivalence (DecSetoid.isDecEquivalence d)
}
preorder : Preorder a ℓ₁ ℓ₂ → Preorder _ _ _
preorder p = record
{ isPreorder = isPreorder (Preorder.isPreorder p)
}
poset : Poset a ℓ₁ ℓ₂ → Poset _ _ _
poset p = record
{ isPartialOrder = isPartialOrder (Poset.isPartialOrder p)
}
All-resp-Pointwise : ∀ {P : Pred A p} → P Respects R →
(All P) Respects (Pointwise R)
All-resp-Pointwise resp [] [] = []
All-resp-Pointwise resp (x∼y ∷ xs) (px ∷ pxs) =
resp x∼y px ∷ All-resp-Pointwise resp xs pxs
Any-resp-Pointwise : ∀ {P : Pred A p} → P Respects R →
(Any P) Respects (Pointwise R)
Any-resp-Pointwise resp (x∼y ∷ xs) (here px) = here (resp x∼y px)
Any-resp-Pointwise resp (x∼y ∷ xs) (there pxs) =
there (Any-resp-Pointwise resp xs pxs)
AllPairs-resp-Pointwise : R Respects₂ S →
(AllPairs R) Respects (Pointwise S)
AllPairs-resp-Pointwise _ [] [] = []
AllPairs-resp-Pointwise resp@(respₗ , respᵣ) (x∼y ∷ xs) (px ∷ pxs) =
All-resp-Pointwise respₗ xs (All.map (respᵣ x∼y) px) ∷
(AllPairs-resp-Pointwise resp xs pxs)
Pointwise-length : Pointwise R xs ys → length xs ≡ length ys
Pointwise-length [] = ≡.refl
Pointwise-length (x∼y ∷ xs∼ys) = ≡.cong ℕ.suc (Pointwise-length xs∼ys)
tabulate⁺ : ∀ {n} {f : Fin n → A} {g : Fin n → B} →
(∀ i → R (f i) (g i)) → Pointwise R (tabulate f) (tabulate g)
tabulate⁺ {n = zero} f∼g = []
tabulate⁺ {n = suc n} f∼g = f∼g fzero ∷ tabulate⁺ (f∼g ∘ fsuc)
tabulate⁻ : ∀ {n} {f : Fin n → A} {g : Fin n → B} →
Pointwise R (tabulate f) (tabulate g) → (∀ i → R (f i) (g i))
tabulate⁻ {n = suc n} (x∼y ∷ xs∼ys) fzero = x∼y
tabulate⁻ {n = suc n} (x∼y ∷ xs∼ys) (fsuc i) = tabulate⁻ xs∼ys i
++⁺ : Pointwise R ws xs → Pointwise R ys zs →
Pointwise R (ws ++ ys) (xs ++ zs)
++⁺ [] ys∼zs = ys∼zs
++⁺ (w∼x ∷ ws∼xs) ys∼zs = w∼x ∷ ++⁺ ws∼xs ys∼zs
++-cancelˡ : ∀ xs → Pointwise R (xs ++ ys) (xs ++ zs) → Pointwise R ys zs
++-cancelˡ [] ys∼zs = ys∼zs
++-cancelˡ (x ∷ xs) (_ ∷ xs++ys∼xs++zs) = ++-cancelˡ xs xs++ys∼xs++zs
++-cancelʳ : ∀ ys zs → Pointwise R (ys ++ xs) (zs ++ xs) → Pointwise R ys zs
++-cancelʳ [] [] _ = []
++-cancelʳ (y ∷ ys) (z ∷ zs) (y∼z ∷ ys∼zs) = y∼z ∷ (++-cancelʳ ys zs ys∼zs)
++-cancelʳ {xs = xs} [] (z ∷ zs) eq =
contradiction (≡.trans (Pointwise-length eq) (length-++ (z ∷ zs))) (m≢1+n+m (length xs))
++-cancelʳ {xs = xs} (y ∷ ys) [] eq =
contradiction (≡.trans (≡.sym (length-++ (y ∷ ys))) (Pointwise-length eq)) (m≢1+n+m (length xs) ∘ ≡.sym)
concat⁺ : ∀ {xss yss} → Pointwise (Pointwise R) xss yss →
Pointwise R (concat xss) (concat yss)
concat⁺ [] = []
concat⁺ (xs∼ys ∷ xss∼yss) = ++⁺ xs∼ys (concat⁺ xss∼yss)
reverseAcc⁺ : Pointwise R ws xs → Pointwise R ys zs →
Pointwise R (reverseAcc ws ys) (reverseAcc xs zs)
reverseAcc⁺ rs′ [] = rs′
reverseAcc⁺ rs′ (r ∷ rs) = reverseAcc⁺ (r ∷ rs′) rs
ʳ++⁺ : Pointwise R ws xs → Pointwise R ys zs →
Pointwise R (ws ʳ++ ys) (xs ʳ++ zs)
ʳ++⁺ rs rs′ = reverseAcc⁺ rs′ rs
reverse⁺ : Pointwise R xs ys → Pointwise R (reverse xs) (reverse ys)
reverse⁺ = reverseAcc⁺ []
map⁺ : ∀ (f : A → C) (g : B → D) →
Pointwise (λ a b → R (f a) (g b)) xs ys →
Pointwise R (List.map f xs) (List.map g ys)
map⁺ f g [] = []
map⁺ f g (r ∷ rs) = r ∷ map⁺ f g rs
map⁻ : ∀ (f : A → C) (g : B → D) →
Pointwise R (List.map f xs) (List.map g ys) →
Pointwise (λ a b → R (f a) (g b)) xs ys
map⁻ {xs = []} {[]} f g [] = []
map⁻ {xs = _ ∷ _} {_ ∷ _} f g (r ∷ rs) = r ∷ map⁻ f g rs
foldr⁺ : ∀ {_•_ : Op₂ A} {_◦_ : Op₂ B} →
(∀ {w x y z} → R w x → R y z → R (w • y) (x ◦ z)) →
∀ {e f} → R e f → Pointwise R xs ys →
R (foldr _•_ e xs) (foldr _◦_ f ys)
foldr⁺ _ e~f [] = e~f
foldr⁺ pres e~f (x~y ∷ xs~ys) = pres x~y (foldr⁺ pres e~f xs~ys)
module _ {P : Pred A p} {Q : Pred B q}
(P? : U.Decidable P) (Q? : U.Decidable Q)
(P⇒Q : ∀ {a b} → R a b → P a → Q b)
(Q⇒P : ∀ {a b} → R a b → Q b → P a)
where
filter⁺ : Pointwise R xs ys →
Pointwise R (filter P? xs) (filter Q? ys)
filter⁺ [] = []
filter⁺ {x ∷ _} {y ∷ _} (r ∷ rs) with P? x | Q? y
... | true because _ | true because _ = r ∷ filter⁺ rs
... | false because _ | false because _ = filter⁺ rs
... | yes p | no ¬q = contradiction (P⇒Q r p) ¬q
... | no ¬p | yes q = contradiction (Q⇒P r q) ¬p
replicate⁺ : R x y → ∀ n → Pointwise R (replicate n x) (replicate n y)
replicate⁺ r 0 = []
replicate⁺ r (suc n) = r ∷ replicate⁺ r n
lookup⁻ : length xs ≡ length ys →
(∀ {i j} → toℕ i ≡ toℕ j → R (lookup xs i) (lookup ys j)) →
Pointwise R xs ys
lookup⁻ {xs = []} {ys = []} _ _ = []
lookup⁻ {xs = _ ∷ _} {ys = _ ∷ _} |xs|≡|ys| eq = eq {fzero} ≡.refl ∷
lookup⁻ (suc-injective |xs|≡|ys|) (eq ∘ ≡.cong ℕ.suc)
lookup⁺ : ∀ (Rxys : Pointwise R xs ys) →
∀ i → (let j = cast (Pointwise-length Rxys) i) →
R (lookup xs i) (lookup ys j)
lookup⁺ (Rxy ∷ _) fzero = Rxy
lookup⁺ (_ ∷ Rxys) (fsuc i) = lookup⁺ Rxys i
Pointwise-≡⇒≡ : Pointwise {A = A} _≡_ ⇒ _≡_
Pointwise-≡⇒≡ [] = ≡.refl
Pointwise-≡⇒≡ (≡.refl ∷ xs∼ys) with Pointwise-≡⇒≡ xs∼ys
... | ≡.refl = ≡.refl
≡⇒Pointwise-≡ : _≡_ ⇒ Pointwise {A = A} _≡_
≡⇒Pointwise-≡ ≡.refl = refl ≡.refl
Pointwise-≡↔≡ : Inverse (setoid (≡.setoid A)) (≡.setoid (List A))
Pointwise-≡↔≡ = record
{ to = id
; from = id
; to-cong = Pointwise-≡⇒≡
; from-cong = ≡⇒Pointwise-≡
; inverse = Pointwise-≡⇒≡ , ≡⇒Pointwise-≡
}