------------------------------------------------------------------------ -- The Agda standard library -- -- Pointwise equality over lists parameterised by a setoid ------------------------------------------------------------------------ {-# OPTIONS --without-K --safe #-} open import Algebra.Core using (Op₂) open import Relation.Binary using (Setoid) module Data.List.Relation.Binary.Equality.Setoid {a ℓ} (S : Setoid a ℓ) where open import Data.Fin.Base open import Data.List.Base open import Data.List.Relation.Binary.Pointwise as PW using (Pointwise) open import Data.List.Relation.Unary.Unique.Setoid S using (Unique) open import Function.Base using (_∘_) open import Level open import Relation.Binary renaming (Rel to Rel₂) open import Relation.Binary.PropositionalEquality as P using (_≡_) open import Relation.Binary.Properties.Setoid S using (≉-resp₂) open import Relation.Unary as U using (Pred) open Setoid S renaming (Carrier to A) private variable p q : Level ------------------------------------------------------------------------ -- Definition of equality ------------------------------------------------------------------------ infix 4 _≋_ _≋_ : Rel₂ (List A) (a ⊔ ℓ) _≋_ = Pointwise _≈_ open PW public using ([]; _∷_) ------------------------------------------------------------------------ -- Relational properties ------------------------------------------------------------------------ ≋-refl : Reflexive _≋_ ≋-refl = PW.refl refl ≋-reflexive : _≡_ ⇒ _≋_ ≋-reflexive P.refl = ≋-refl ≋-sym : Symmetric _≋_ ≋-sym = PW.symmetric sym ≋-trans : Transitive _≋_ ≋-trans = PW.transitive trans ≋-isEquivalence : IsEquivalence _≋_ ≋-isEquivalence = PW.isEquivalence isEquivalence ≋-setoid : Setoid _ _ ≋-setoid = PW.setoid S ------------------------------------------------------------------------ -- Relationships to predicates ------------------------------------------------------------------------ open PW public using () renaming ( Any-resp-Pointwise to Any-resp-≋ ; All-resp-Pointwise to All-resp-≋ ; AllPairs-resp-Pointwise to AllPairs-resp-≋ ) Unique-resp-≋ : Unique Respects _≋_ Unique-resp-≋ = AllPairs-resp-≋ ≉-resp₂ ------------------------------------------------------------------------ -- List operations ------------------------------------------------------------------------ ------------------------------------------------------------------------ -- length ≋-length : ∀ {xs ys} → xs ≋ ys → length xs ≡ length ys ≋-length = PW.Pointwise-length ------------------------------------------------------------------------ -- map module _ {b ℓ₂} (T : Setoid b ℓ₂) where open Setoid T using () renaming (_≈_ to _≈′_) private _≋′_ = Pointwise _≈′_ map⁺ : ∀ {f} → f Preserves _≈_ ⟶ _≈′_ → ∀ {xs ys} → xs ≋ ys → map f xs ≋′ map f ys map⁺ {f} pres xs≋ys = PW.map⁺ f f (PW.map pres xs≋ys) ------------------------------------------------------------------------ -- foldr foldr⁺ : ∀ {_•_ : Op₂ A} {_◦_ : Op₂ A} → (∀ {w x y z} → w ≈ x → y ≈ z → (w • y) ≈ (x ◦ z)) → ∀ {xs ys e f} → e ≈ f → xs ≋ ys → foldr _•_ e xs ≈ foldr _◦_ f ys foldr⁺ ∙⇔◦ e≈f xs≋ys = PW.foldr⁺ ∙⇔◦ e≈f xs≋ys ------------------------------------------------------------------------ -- _++_ ++⁺ : ∀ {ws xs ys zs} → ws ≋ xs → ys ≋ zs → ws ++ ys ≋ xs ++ zs ++⁺ = PW.++⁺ ++-cancelˡ : ∀ xs {ys zs} → xs ++ ys ≋ xs ++ zs → ys ≋ zs ++-cancelˡ xs = PW.++-cancelˡ xs ++-cancelʳ : ∀ {xs} ys zs → ys ++ xs ≋ zs ++ xs → ys ≋ zs ++-cancelʳ = PW.++-cancelʳ ------------------------------------------------------------------------ -- concat concat⁺ : ∀ {xss yss} → Pointwise _≋_ xss yss → concat xss ≋ concat yss concat⁺ = PW.concat⁺ ------------------------------------------------------------------------ -- tabulate tabulate⁺ : ∀ {n} {f : Fin n → A} {g : Fin n → A} → (∀ i → f i ≈ g i) → tabulate f ≋ tabulate g tabulate⁺ = PW.tabulate⁺ tabulate⁻ : ∀ {n} {f : Fin n → A} {g : Fin n → A} → tabulate f ≋ tabulate g → (∀ i → f i ≈ g i) tabulate⁻ = PW.tabulate⁻ ------------------------------------------------------------------------ -- filter module _ {P : Pred A p} (P? : U.Decidable P) (resp : P Respects _≈_) where filter⁺ : ∀ {xs ys} → xs ≋ ys → filter P? xs ≋ filter P? ys filter⁺ xs≋ys = PW.filter⁺ P? P? resp (resp ∘ sym) xs≋ys ------------------------------------------------------------------------ -- reverse ʳ++⁺ : ∀{xs xs′ ys ys′} → xs ≋ xs′ → ys ≋ ys′ → xs ʳ++ ys ≋ xs′ ʳ++ ys′ ʳ++⁺ = PW.ʳ++⁺ reverse⁺ : ∀ {xs ys} → xs ≋ ys → reverse xs ≋ reverse ys reverse⁺ = PW.reverse⁺