diff --git a/src/Codata/Guarded/Stream/Relation/Binary/Pointwise.agda b/src/Codata/Guarded/Stream/Relation/Binary/Pointwise.agda index a4908e851f..0ba8d9539c 100644 --- a/src/Codata/Guarded/Stream/Relation/Binary/Pointwise.agda +++ b/src/Codata/Guarded/Stream/Relation/Binary/Pointwise.agda @@ -17,8 +17,8 @@ open import Relation.Binary.Bundles using (Setoid) open import Relation.Binary.Definitions using (Reflexive; Sym; Trans; Antisym; Symmetric; Transitive) open import Relation.Binary.Structures using (IsEquivalence) -open import Relation.Binary.PropositionalEquality.Core as P using (_≡_) -import Relation.Binary.PropositionalEquality.Properties as P +open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_) +import Relation.Binary.PropositionalEquality.Properties as ≡ private variable @@ -114,16 +114,16 @@ module _ {A : Set a} where _≈_ = Pointwise _≡_ refl : Reflexive _≈_ - refl = reflexive P.refl + refl = reflexive ≡.refl sym : Symmetric _≈_ - sym = symmetric P.sym + sym = symmetric ≡.sym trans : Transitive _≈_ - trans = transitive P.trans + trans = transitive ≡.trans ≈-setoid : Setoid _ _ - ≈-setoid = setoid (P.setoid A) + ≈-setoid = setoid (≡.setoid A) ------------------------------------------------------------------------ -- Pointwise DSL @@ -161,7 +161,7 @@ module pw-Reasoning (S : Setoid a ℓ) where `head : ∀ {as bs} → `Pointwise as bs → as .head ∼ bs .head `head (`lift rs) = rs .head - `head (`refl eq) = S.reflexive (P.cong head eq) + `head (`refl eq) = S.reflexive (≡.cong head eq) `head (`bisim rs) = S.reflexive (rs .head) `head (`step `rs) = `rs .head `head (`sym `rs) = S.sym (`head `rs) @@ -169,7 +169,7 @@ module pw-Reasoning (S : Setoid a ℓ) where `tail : ∀ {as bs} → `Pointwise as bs → `Pointwise (as .tail) (bs .tail) `tail (`lift rs) = `lift (rs .tail) - `tail (`refl eq) = `refl (P.cong tail eq) + `tail (`refl eq) = `refl (≡.cong tail eq) `tail (`bisim rs) = `bisim (rs .tail) `tail (`step `rs) = `rs .tail `tail (`sym `rs) = `sym (`tail `rs) @@ -196,8 +196,8 @@ module pw-Reasoning (S : Setoid a ℓ) where pattern _≈⟨_⟨_ as bs∼as bs∼cs = `trans {as = as} (`sym (`bisim bs∼as)) bs∼cs pattern _≡⟨_⟩_ as as∼bs bs∼cs = `trans {as = as} (`refl as∼bs) bs∼cs pattern _≡⟨_⟨_ as bs∼as bs∼cs = `trans {as = as} (`sym (`refl bs∼as)) bs∼cs - pattern _≡⟨⟩_ as as∼bs = `trans {as = as} (`refl P.refl) as∼bs - pattern _∎ as = `refl {as = as} P.refl + pattern _≡⟨⟩_ as as∼bs = `trans {as = as} (`refl ≡.refl) as∼bs + pattern _∎ as = `refl {as = as} ≡.refl -- Deprecated v2.0 @@ -226,7 +226,7 @@ module pw-Reasoning (S : Setoid a ℓ) where module ≈-Reasoning {a} {A : Set a} where - open pw-Reasoning (P.setoid A) public + open pw-Reasoning (≡.setoid A) public infix 4 _≈∞_ _≈∞_ = `Pointwise∞ diff --git a/src/Codata/Sized/Colist/Properties.agda b/src/Codata/Sized/Colist/Properties.agda index a4196bb952..c03b3c2096 100644 --- a/src/Codata/Sized/Colist/Properties.agda +++ b/src/Codata/Sized/Colist/Properties.agda @@ -14,24 +14,24 @@ open import Codata.Sized.Thunk as Thunk using (Thunk; force) open import Codata.Sized.Colist open import Codata.Sized.Colist.Bisimilarity open import Codata.Sized.Conat -open import Codata.Sized.Conat.Bisimilarity as coℕᵇ using (zero; suc) -import Codata.Sized.Conat.Properties as coℕₚ +open import Codata.Sized.Conat.Bisimilarity as Conat using (zero; suc) +import Codata.Sized.Conat.Properties as Conat open import Codata.Sized.Cowriter as Cowriter using ([_]; _∷_) -open import Codata.Sized.Cowriter.Bisimilarity as coWriterᵇ using ([_]; _∷_) +open import Codata.Sized.Cowriter.Bisimilarity as Cowriter using ([_]; _∷_) open import Codata.Sized.Stream as Stream using (Stream; _∷_) open import Data.Vec.Bounded as Vec≤ using (Vec≤) open import Data.List.Base as List using (List; []; _∷_) open import Data.List.NonEmpty as List⁺ using (List⁺; _∷_) open import Data.List.Relation.Binary.Equality.Propositional using (≋-refl) open import Data.Maybe.Base as Maybe using (Maybe; nothing; just) -import Data.Maybe.Properties as Maybeₚ +import Data.Maybe.Properties as Maybe open import Data.Maybe.Relation.Unary.All using (All; nothing; just) open import Data.Nat.Base as ℕ using (zero; suc; z≤n; s≤s) -open import Data.Product.Base as Prod using (_×_; _,_; uncurry) +open import Data.Product.Base as Product using (_×_; _,_; uncurry) open import Data.These.Base as These using (These; this; that; these) open import Data.Vec.Base as Vec using (Vec; []; _∷_) open import Function.Base -open import Relation.Binary.PropositionalEquality.Core as Eq using (_≡_) +open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_) private variable @@ -47,13 +47,13 @@ private map-id : ∀ (as : Colist A ∞) → i ⊢ map id as ≈ as map-id [] = [] -map-id (a ∷ as) = Eq.refl ∷ λ where .force → map-id (as .force) +map-id (a ∷ as) = ≡.refl ∷ λ where .force → map-id (as .force) map-∘ : ∀ (f : A → B) (g : B → C) as {i} → i ⊢ map g (map f as) ≈ map (g ∘ f) as map-∘ f g [] = [] map-∘ f g (a ∷ as) = - Eq.refl ∷ λ where .force → map-∘ f g (as .force) + ≡.refl ∷ λ where .force → map-∘ f g (as .force) ------------------------------------------------------------------------ -- Relation to Cowriter @@ -62,24 +62,24 @@ fromCowriter∘toCowriter≗id : ∀ (as : Colist A ∞) → i ⊢ fromCowriter (toCowriter as) ≈ as fromCowriter∘toCowriter≗id [] = [] fromCowriter∘toCowriter≗id (a ∷ as) = - Eq.refl ∷ λ where .force → fromCowriter∘toCowriter≗id (as .force) + ≡.refl ∷ λ where .force → fromCowriter∘toCowriter≗id (as .force) ------------------------------------------------------------------------ -- Properties of length -length-∷ : ∀ (a : A) as → i coℕᵇ.⊢ length (a ∷ as) ≈ 1 ℕ+ length (as .force) -length-∷ a as = suc (λ where .force → coℕᵇ.refl) +length-∷ : ∀ (a : A) as → i Conat.⊢ length (a ∷ as) ≈ 1 ℕ+ length (as .force) +length-∷ a as = suc (λ where .force → Conat.refl) -length-replicate : ∀ n (a : A) → i coℕᵇ.⊢ length (replicate n a) ≈ n +length-replicate : ∀ n (a : A) → i Conat.⊢ length (replicate n a) ≈ n length-replicate zero a = zero length-replicate (suc n) a = suc λ where .force → length-replicate (n .force) a length-++ : (as bs : Colist A ∞) → - i coℕᵇ.⊢ length (as ++ bs) ≈ length as + length bs -length-++ [] bs = coℕᵇ.refl + i Conat.⊢ length (as ++ bs) ≈ length as + length bs +length-++ [] bs = Conat.refl length-++ (a ∷ as) bs = suc λ where .force → length-++ (as .force) bs -length-map : ∀ (f : A → B) as → i coℕᵇ.⊢ length (map f as) ≈ length as +length-map : ∀ (f : A → B) as → i Conat.⊢ length (map f as) ≈ length as length-map f [] = zero length-map f (a ∷ as) = suc λ where .force → length-map f (as .force) @@ -89,51 +89,51 @@ length-map f (a ∷ as) = suc λ where .force → length-map f (as .force) replicate-+ : ∀ m n (a : A) → i ⊢ replicate (m + n) a ≈ replicate m a ++ replicate n a replicate-+ zero n a = refl -replicate-+ (suc m) n a = Eq.refl ∷ λ where .force → replicate-+ (m .force) n a +replicate-+ (suc m) n a = ≡.refl ∷ λ where .force → replicate-+ (m .force) n a map-replicate : ∀ (f : A → B) n a → i ⊢ map f (replicate n a) ≈ replicate n (f a) map-replicate f zero a = [] map-replicate f (suc n) a = - Eq.refl ∷ λ where .force → map-replicate f (n .force) a + ≡.refl ∷ λ where .force → map-replicate f (n .force) a lookup-replicate : ∀ k n (a : A) → All (a ≡_) (lookup (replicate n a) k) lookup-replicate k zero a = nothing -lookup-replicate zero (suc n) a = just Eq.refl +lookup-replicate zero (suc n) a = just ≡.refl lookup-replicate (suc k) (suc n) a = lookup-replicate k (n .force) a ------------------------------------------------------------------------ -- Properties of unfold map-unfold : ∀ (f : B → C) (alg : A → Maybe (A × B)) a → - i ⊢ map f (unfold alg a) ≈ unfold (Maybe.map (Prod.map₂ f) ∘ alg) a + i ⊢ map f (unfold alg a) ≈ unfold (Maybe.map (Product.map₂ f) ∘ alg) a map-unfold f alg a with alg a ... | nothing = [] -... | just (a′ , b) = Eq.refl ∷ λ where .force → map-unfold f alg a′ +... | just (a′ , b) = ≡.refl ∷ λ where .force → map-unfold f alg a′ module _ {alg : A → Maybe (A × B)} {a} where unfold-nothing : alg a ≡ nothing → unfold alg a ≡ [] unfold-nothing eq with alg a - ... | nothing = Eq.refl + ... | nothing = ≡.refl unfold-just : ∀ {a′ b} → alg a ≡ just (a′ , b) → i ⊢ unfold alg a ≈ b ∷ λ where .force → unfold alg a′ unfold-just eq with alg a - unfold-just Eq.refl | just (a′ , b) = Eq.refl ∷ λ where .force → refl + unfold-just ≡.refl | just (a′ , b) = ≡.refl ∷ λ where .force → refl ------------------------------------------------------------------------ -- Properties of scanl length-scanl : ∀ (c : B → A → B) n as → - i coℕᵇ.⊢ length (scanl c n as) ≈ 1 ℕ+ length as + i Conat.⊢ length (scanl c n as) ≈ 1 ℕ+ length as length-scanl c n [] = suc λ where .force → zero length-scanl c n (a ∷ as) = suc λ { .force → begin length (scanl c (c n a) (as .force)) ≈⟨ length-scanl c (c n a) (as .force) ⟩ 1 ℕ+ length (as .force) ≈⟨ length-∷ a as ⟨ - length (a ∷ as) ∎ } where open coℕᵇ.≈-Reasoning + length (a ∷ as) ∎ } where open Conat.≈-Reasoning module _ (cons : C → B → C) (alg : A → Maybe (A × B)) where @@ -145,15 +145,15 @@ module _ (cons : C → B → C) (alg : A → Maybe (A × B)) where scanl-unfold : ∀ nil a → i ⊢ scanl cons nil (unfold alg a) ≈ nil ∷ (λ where .force → unfold alg′ (a , nil)) scanl-unfold nil a with alg a in eq - ... | nothing = Eq.refl ∷ λ { .force → - sym (fromEq (unfold-nothing (Maybeₚ.map-nothing eq))) } - ... | just (a′ , b) = Eq.refl ∷ λ { .force → begin + ... | nothing = ≡.refl ∷ λ { .force → + sym (fromEq (unfold-nothing (Maybe.map-nothing eq))) } + ... | just (a′ , b) = ≡.refl ∷ λ { .force → begin scanl cons (cons nil b) (unfold alg a′) ≈⟨ scanl-unfold (cons nil b) a′ ⟩ (cons nil b ∷ _) - ≈⟨ Eq.refl ∷ (λ where .force → refl) ⟩ + ≈⟨ ≡.refl ∷ (λ where .force → refl) ⟩ (cons nil b ∷ _) - ≈⟨ unfold-just (Maybeₚ.map-just eq) ⟨ + ≈⟨ unfold-just (Maybe.map-just eq) ⟨ unfold alg′ (a , nil) ∎ } where open ≈-Reasoning ------------------------------------------------------------------------ @@ -164,10 +164,10 @@ map-alignWith : ∀ (f : C → D) (al : These A B → C) as bs → map-alignWith f al [] bs = map-∘ (al ∘′ that) f bs map-alignWith f al as@(_ ∷ _) [] = map-∘ (al ∘′ this) f as map-alignWith f al (a ∷ as) (b ∷ bs) = - Eq.refl ∷ λ where .force → map-alignWith f al (as .force) (bs .force) + ≡.refl ∷ λ where .force → map-alignWith f al (as .force) (bs .force) length-alignWith : ∀ (al : These A B → C) as bs → - i coℕᵇ.⊢ length (alignWith al as bs) ≈ length as ⊔ length bs + i Conat.⊢ length (alignWith al as bs) ≈ length as ⊔ length bs length-alignWith al [] bs = length-map (al ∘ that) bs length-alignWith al as@(_ ∷ _) [] = length-map (al ∘ this) as length-alignWith al (a ∷ as) (b ∷ bs) = @@ -181,10 +181,10 @@ map-zipWith : ∀ (f : C → D) (zp : A → B → C) as bs → map-zipWith f zp [] _ = [] map-zipWith f zp (_ ∷ _) [] = [] map-zipWith f zp (a ∷ as) (b ∷ bs) = - Eq.refl ∷ λ where .force → map-zipWith f zp (as .force) (bs .force) + ≡.refl ∷ λ where .force → map-zipWith f zp (as .force) (bs .force) length-zipWith : ∀ (zp : A → B → C) as bs → - i coℕᵇ.⊢ length (zipWith zp as bs) ≈ length as ⊓ length bs + i Conat.⊢ length (zipWith zp as bs) ≈ length as ⊓ length bs length-zipWith zp [] bs = zero length-zipWith zp as@(_ ∷ _) [] = zero length-zipWith zp (a ∷ as) (b ∷ bs) = @@ -208,25 +208,25 @@ map-drop f zero as = refl map-drop f (suc m) [] = [] map-drop f (suc m) (a ∷ as) = map-drop f m (as .force) -length-drop : ∀ m (as : Colist A ∞) → i coℕᵇ.⊢ length (drop m as) ≈ length as ∸ m -length-drop zero as = coℕᵇ.refl -length-drop (suc m) [] = coℕᵇ.sym (coℕₚ.0∸m≈0 m) +length-drop : ∀ m (as : Colist A ∞) → i Conat.⊢ length (drop m as) ≈ length as ∸ m +length-drop zero as = Conat.refl +length-drop (suc m) [] = Conat.sym (Conat.0∸m≈0 m) length-drop (suc m) (a ∷ as) = length-drop m (as .force) drop-fromList-++-identity : ∀ (as : List A) bs → drop (List.length as) (fromList as ++ bs) ≡ bs -drop-fromList-++-identity [] bs = Eq.refl +drop-fromList-++-identity [] bs = ≡.refl drop-fromList-++-identity (a ∷ as) bs = drop-fromList-++-identity as bs drop-fromList-++-≤ : ∀ (as : List A) bs {m} → m ℕ.≤ List.length as → drop m (fromList as ++ bs) ≡ fromList (List.drop m as) ++ bs -drop-fromList-++-≤ [] bs z≤n = Eq.refl -drop-fromList-++-≤ (a ∷ as) bs z≤n = Eq.refl +drop-fromList-++-≤ [] bs z≤n = ≡.refl +drop-fromList-++-≤ (a ∷ as) bs z≤n = ≡.refl drop-fromList-++-≤ (a ∷ as) bs (s≤s p) = drop-fromList-++-≤ as bs p drop-fromList-++-≥ : ∀ (as : List A) bs {m} → m ℕ.≥ List.length as → drop m (fromList as ++ bs) ≡ drop (m ℕ.∸ List.length as) bs -drop-fromList-++-≥ [] bs z≤n = Eq.refl +drop-fromList-++-≥ [] bs z≤n = ≡.refl drop-fromList-++-≥ (a ∷ as) bs (s≤s p) = drop-fromList-++-≥ as bs p drop-⁺++-identity : ∀ (as : List⁺ A) bs → @@ -236,7 +236,7 @@ drop-⁺++-identity (a ∷ as) bs = drop-fromList-++-identity as (bs .force) ------------------------------------------------------------------------ -- Properties of cotake -length-cotake : ∀ n (as : Stream A ∞) → i coℕᵇ.⊢ length (cotake n as) ≈ n +length-cotake : ∀ n (as : Stream A ∞) → i Conat.⊢ length (cotake n as) ≈ n length-cotake zero as = zero length-cotake (suc n) (a ∷ as) = suc λ where .force → length-cotake (n .force) (as .force) @@ -245,7 +245,7 @@ map-cotake : ∀ (f : A → B) n as → i ⊢ map f (cotake n as) ≈ cotake n (Stream.map f as) map-cotake f zero as = [] map-cotake f (suc n) (a ∷ as) = - Eq.refl ∷ λ where .force → map-cotake f (n .force) (as .force) + ≡.refl ∷ λ where .force → map-cotake f (n .force) (as .force) ------------------------------------------------------------------------ -- Properties of chunksOf @@ -255,20 +255,20 @@ module Map-ChunksOf (f : A → B) n where open ChunksOf n using (chunksOfAcc) map-chunksOf : ∀ as → - i coWriterᵇ.⊢ Cowriter.map (Vec.map f) (Vec≤.map f) (chunksOf n as) + i Cowriter.⊢ Cowriter.map (Vec.map f) (Vec≤.map f) (chunksOf n as) ≈ chunksOf n (map f as) map-chunksOfAcc : ∀ m as {k≤ k≡ k≤′ k≡′} → (∀ vs → Vec≤.map f (k≤ vs) ≡ k≤′ (Vec≤.map f vs)) → (∀ vs → Vec.map f (k≡ vs) ≡ k≡′ (Vec.map f vs)) → - i coWriterᵇ.⊢ Cowriter.map (Vec.map f) (Vec≤.map f) + i Cowriter.⊢ Cowriter.map (Vec.map f) (Vec≤.map f) (chunksOfAcc m k≤ k≡ as) ≈ chunksOfAcc m k≤′ k≡′ (map f as) - map-chunksOf as = map-chunksOfAcc n as (λ vs → Eq.refl) (λ vs → Eq.refl) + map-chunksOf as = map-chunksOfAcc n as (λ vs → ≡.refl) (λ vs → ≡.refl) map-chunksOfAcc zero as eq-≤ eq-≡ = eq-≡ [] ∷ λ where .force → map-chunksOf as - map-chunksOfAcc (suc m) [] eq-≤ eq-≡ = coWriterᵇ.[ eq-≤ Vec≤.[] ] + map-chunksOfAcc (suc m) [] eq-≤ eq-≡ = Cowriter.[ eq-≤ Vec≤.[] ] map-chunksOfAcc (suc m) (a ∷ as) eq-≤ eq-≡ = map-chunksOfAcc m (as .force) (eq-≤ ∘ (a Vec≤.∷_)) (eq-≡ ∘ (a Vec.∷_)) @@ -280,21 +280,21 @@ open Map-ChunksOf using (map-chunksOf) public fromList-++ : (as bs : List A) → i ⊢ fromList (as List.++ bs) ≈ fromList as ++ fromList bs fromList-++ [] bs = refl -fromList-++ (a ∷ as) bs = Eq.refl ∷ λ where .force → fromList-++ as bs +fromList-++ (a ∷ as) bs = ≡.refl ∷ λ where .force → fromList-++ as bs fromList-scanl : ∀ (c : B → A → B) n as → i ⊢ fromList (List.scanl c n as) ≈ scanl c n (fromList as) -fromList-scanl c n [] = Eq.refl ∷ λ where .force → refl +fromList-scanl c n [] = ≡.refl ∷ λ where .force → refl fromList-scanl c n (a ∷ as) = - Eq.refl ∷ λ where .force → fromList-scanl c (c n a) as + ≡.refl ∷ λ where .force → fromList-scanl c (c n a) as map-fromList : ∀ (f : A → B) as → i ⊢ map f (fromList as) ≈ fromList (List.map f as) map-fromList f [] = [] -map-fromList f (a ∷ as) = Eq.refl ∷ λ where .force → map-fromList f as +map-fromList f (a ∷ as) = ≡.refl ∷ λ where .force → map-fromList f as length-fromList : (as : List A) → - i coℕᵇ.⊢ length (fromList as) ≈ fromℕ (List.length as) + i Conat.⊢ length (fromList as) ≈ fromℕ (List.length as) length-fromList [] = zero length-fromList (a ∷ as) = suc (λ where .force → length-fromList as) @@ -304,19 +304,19 @@ length-fromList (a ∷ as) = suc (λ where .force → length-fromList as) fromStream-++ : ∀ (as : List A) bs → i ⊢ fromStream (as Stream.++ bs) ≈ fromList as ++ fromStream bs fromStream-++ [] bs = refl -fromStream-++ (a ∷ as) bs = Eq.refl ∷ λ where .force → fromStream-++ as bs +fromStream-++ (a ∷ as) bs = ≡.refl ∷ λ where .force → fromStream-++ as bs fromStream-⁺++ : ∀ (as : List⁺ A) bs → i ⊢ fromStream (as Stream.⁺++ bs) ≈ fromList⁺ as ++ fromStream (bs .force) fromStream-⁺++ (a ∷ as) bs = - Eq.refl ∷ λ where .force → fromStream-++ as (bs .force) + ≡.refl ∷ λ where .force → fromStream-++ as (bs .force) fromStream-concat : (ass : Stream (List⁺ A) ∞) → i ⊢ concat (fromStream ass) ≈ fromStream (Stream.concat ass) fromStream-concat (as@(a ∷ _) ∷ ass) = begin concat (fromStream (as ∷ ass)) - ≈⟨ Eq.refl ∷ (λ { .force → ++⁺ ≋-refl (fromStream-concat (ass .force))}) ⟩ + ≈⟨ ≡.refl ∷ (λ { .force → ++⁺ ≋-refl (fromStream-concat (ass .force))}) ⟩ a ∷ _ ≈⟨ sym (fromStream-⁺++ as _) ⟩ fromStream (Stream.concat (as ∷ ass)) ∎ where open ≈-Reasoning @@ -325,12 +325,12 @@ fromStream-scanl : ∀ (c : B → A → B) n as → i ⊢ scanl c n (fromStream as) ≈ fromStream (Stream.scanl c n as) fromStream-scanl c n (a ∷ as) = - Eq.refl ∷ λ where .force → fromStream-scanl c (c n a) (as .force) + ≡.refl ∷ λ where .force → fromStream-scanl c (c n a) (as .force) map-fromStream : ∀ (f : A → B) as → i ⊢ map f (fromStream as) ≈ fromStream (Stream.map f as) map-fromStream f (a ∷ as) = - Eq.refl ∷ λ where .force → map-fromStream f (as .force) + ≡.refl ∷ λ where .force → map-fromStream f (as .force) ------------------------------------------------------------------------ -- DEPRECATED diff --git a/src/Data/Char/Properties.agda b/src/Data/Char/Properties.agda index cd4ccdce29..b9c7270881 100644 --- a/src/Data/Char/Properties.agda +++ b/src/Data/Char/Properties.agda @@ -27,10 +27,10 @@ open import Relation.Binary.Definitions import Relation.Binary.Construct.On as On import Relation.Binary.Construct.Subst.Equality as Subst import Relation.Binary.Construct.Closure.Reflexive as Refl -import Relation.Binary.Construct.Closure.Reflexive.Properties as Reflₚ -open import Relation.Binary.PropositionalEquality.Core as PropEq +import Relation.Binary.Construct.Closure.Reflexive.Properties as Refl +open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_; _≢_; refl; cong; sym; trans; subst) -import Relation.Binary.PropositionalEquality.Properties as PropEq +import Relation.Binary.PropositionalEquality.Properties as ≡ ------------------------------------------------------------------------ -- Primitive properties @@ -59,13 +59,13 @@ _≟_ : Decidable {A = Char} _≡_ x ≟ y = map′ ≈⇒≡ ≈-reflexive (toℕ x ℕ.≟ toℕ y) setoid : Setoid _ _ -setoid = PropEq.setoid Char +setoid = ≡.setoid Char decSetoid : DecSetoid _ _ -decSetoid = PropEq.decSetoid _≟_ +decSetoid = ≡.decSetoid _≟_ isDecEquivalence : IsDecEquivalence _≡_ -isDecEquivalence = PropEq.isDecEquivalence _≟_ +isDecEquivalence = ≡.isDecEquivalence _≟_ ------------------------------------------------------------------------ -- Boolean equality test. @@ -114,11 +114,11 @@ _>=_ @@ -307,13 +307,13 @@ module _ (_≈?_ : B.Decidable {A = A} _≡_) where -- length ∈-length : ∀ {x : A} {xs} → x ∈ xs → 1 ≤ length xs -∈-length = Membershipₛ.∈-length (P.setoid _) +∈-length = Membership.∈-length (≡.setoid _) ------------------------------------------------------------------------ -- lookup ∈-lookup : ∀ {xs : List A} i → lookup xs i ∈ xs -∈-lookup {xs = xs} i = Membershipₛ.∈-lookup (P.setoid _) xs i +∈-lookup {xs = xs} i = Membership.∈-lookup (≡.setoid _) xs i ------------------------------------------------------------------------ -- foldr @@ -322,7 +322,7 @@ module _ {_•_ : Op₂ A} where foldr-selective : Selective _≡_ _•_ → ∀ e xs → (foldr _•_ e xs ≡ e) ⊎ (foldr _•_ e xs ∈ xs) - foldr-selective = Membershipₛ.foldr-selective (P.setoid A) + foldr-selective = Membership.foldr-selective (≡.setoid A) ------------------------------------------------------------------------ -- allFin @@ -380,7 +380,7 @@ finite inj (x ∷ xs) fᵢ∈x∷xs = ¬¬-excluded-middle helper f′-injective′ : Injective _≡_ _≡_ f′ f′-injective′ {j} {k} eq with i ≤ᵇ j | Reflects.invert (≤ᵇ-reflects-≤ i j) | i ≤ᵇ k | Reflects.invert (≤ᵇ-reflects-≤ i k) - ... | true | p | true | q = P.cong pred (f-inj eq) + ... | true | p | true | q = ≡.cong pred (f-inj eq) ... | true | p | false | q = contradiction (f-inj eq) (lemma p q) ... | false | p | true | q = contradiction (f-inj eq) (lemma q p ∘ sym) ... | false | p | false | q = f-inj eq @@ -388,7 +388,7 @@ finite inj (x ∷ xs) fᵢ∈x∷xs = ¬¬-excluded-middle helper f′-inj : ℕ ↣ _ f′-inj = record { to = f′ - ; cong = P.cong f′ + ; cong = ≡.cong f′ ; injective = f′-injective′ } @@ -398,4 +398,4 @@ finite inj (x ∷ xs) fᵢ∈x∷xs = ¬¬-excluded-middle helper there-injective-≢∈ : ∀ {xs} {x y z : A} {x∈xs : x ∈ xs} {y∈xs : y ∈ xs} → there {x = z} x∈xs ≢∈ there y∈xs → x∈xs ≢∈ y∈xs -there-injective-≢∈ neq refl eq = neq refl (P.cong there eq) +there-injective-≢∈ neq refl eq = neq refl (≡.cong there eq) diff --git a/src/Data/List/Membership/Propositional/Properties/WithK.agda b/src/Data/List/Membership/Propositional/Properties/WithK.agda index 60a86ee5e3..a86f23a8ea 100644 --- a/src/Data/List/Membership/Propositional/Properties/WithK.agda +++ b/src/Data/List/Membership/Propositional/Properties/WithK.agda @@ -12,9 +12,9 @@ module Data.List.Membership.Propositional.Properties.WithK where open import Data.List.Base open import Data.List.Relation.Unary.Unique.Propositional open import Data.List.Membership.Propositional -import Data.List.Membership.Setoid.Properties as Membershipₛ +import Data.List.Membership.Setoid.Properties as Membership open import Relation.Unary using (Irrelevant) -open import Relation.Binary.PropositionalEquality.Properties as P +open import Relation.Binary.PropositionalEquality.Properties as ≡ open import Relation.Binary.PropositionalEquality.WithK ------------------------------------------------------------------------ @@ -22,4 +22,4 @@ open import Relation.Binary.PropositionalEquality.WithK unique⇒irrelevant : ∀ {a} {A : Set a} {xs : List A} → Unique xs → Irrelevant (_∈ xs) -unique⇒irrelevant = Membershipₛ.unique⇒irrelevant (P.setoid _) ≡-irrelevant +unique⇒irrelevant = Membership.unique⇒irrelevant (≡.setoid _) ≡-irrelevant diff --git a/src/Data/List/Membership/Setoid/Properties.agda b/src/Data/List/Membership/Setoid/Properties.agda index 1a74ace45f..fe7b47efb7 100644 --- a/src/Data/List/Membership/Setoid/Properties.agda +++ b/src/Data/List/Membership/Setoid/Properties.agda @@ -28,10 +28,10 @@ open import Function.Base using (_$_; flip; _∘_; _∘′_; id) open import Function.Bundles using (_↔_) open import Level using (Level) open import Relation.Binary.Core using (Rel; _Preserves₂_⟶_⟶_; _Preserves_⟶_) -open import Relation.Binary.Definitions as B hiding (Decidable) +open import Relation.Binary.Definitions as Binary hiding (Decidable) open import Relation.Binary.Bundles using (Setoid) -open import Relation.Binary.PropositionalEquality.Core as P using (_≡_) -open import Relation.Unary as U using (Decidable; Pred) +open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_) +open import Relation.Unary as Unary using (Decidable; Pred) open import Relation.Nullary using (¬_; does; _because_; yes; no) open import Relation.Nullary.Reflects using (invert) open import Relation.Nullary.Negation using (contradiction) @@ -85,11 +85,11 @@ module _ (S : Setoid c ℓ) where ∉×∈⇒≉ : ∀ {x y xs} → All (y ≉_) xs → x ∈ xs → x ≉ y ∉×∈⇒≉ = All.lookupWith λ y≉z x≈z x≈y → y≉z (trans (sym x≈y) x≈z) - unique⇒irrelevant : B.Irrelevant _≈_ → ∀ {xs} → Unique xs → U.Irrelevant (_∈ xs) + unique⇒irrelevant : Binary.Irrelevant _≈_ → ∀ {xs} → Unique xs → Unary.Irrelevant (_∈ xs) unique⇒irrelevant ≈-irr _ (here p) (here q) = - P.cong here (≈-irr p q) + ≡.cong here (≈-irr p q) unique⇒irrelevant ≈-irr (_ ∷ u) (there p) (there q) = - P.cong there (unique⇒irrelevant ≈-irr u p q) + ≡.cong there (unique⇒irrelevant ≈-irr u p q) unique⇒irrelevant ≈-irr (≉s ∷ _) (here p) (there q) = contradiction p (∉×∈⇒≉ ≉s q) unique⇒irrelevant ≈-irr (≉s ∷ _) (there p) (here q) = @@ -130,18 +130,18 @@ module _ (S : Setoid c ℓ) where length-mapWith∈ : ∀ {a} {A : Set a} xs {f : ∀ {x} → x ∈ xs → A} → length (mapWith∈ xs f) ≡ length xs - length-mapWith∈ [] = P.refl - length-mapWith∈ (x ∷ xs) = P.cong suc (length-mapWith∈ xs) + length-mapWith∈ [] = ≡.refl + length-mapWith∈ (x ∷ xs) = ≡.cong suc (length-mapWith∈ xs) mapWith∈-id : ∀ xs → mapWith∈ xs (λ {x} _ → x) ≡ xs - mapWith∈-id [] = P.refl - mapWith∈-id (x ∷ xs) = P.cong (x ∷_) (mapWith∈-id xs) + mapWith∈-id [] = ≡.refl + mapWith∈-id (x ∷ xs) = ≡.cong (x ∷_) (mapWith∈-id xs) map-mapWith∈ : ∀ {a b} {A : Set a} {B : Set b} → ∀ xs (f : ∀ {x} → x ∈ xs → A) (g : A → B) → map g (mapWith∈ xs f) ≡ mapWith∈ xs (g ∘′ f) - map-mapWith∈ [] f g = P.refl - map-mapWith∈ (x ∷ xs) f g = P.cong (_ ∷_) (map-mapWith∈ xs (f ∘ there) g) + map-mapWith∈ [] f g = ≡.refl + map-mapWith∈ (x ∷ xs) f g = ≡.cong (_ ∷_) (map-mapWith∈ xs (f ∘ there) g) ------------------------------------------------------------------------ -- map @@ -164,8 +164,8 @@ module _ (S₁ : Setoid c₁ ℓ₁) (S₂ : Setoid c₂ ℓ₂) where map-∷= : ∀ {f} (f≈ : f Preserves _≈₁_ ⟶ _≈₂_) {xs x v} → (x∈xs : x ∈₁ xs) → map f (x∈xs M₁.∷= v) ≡ ∈-map⁺ f≈ x∈xs M₂.∷= f v - map-∷= f≈ (here x≈y) = P.refl - map-∷= f≈ (there x∈xs) = P.cong (_ ∷_) (map-∷= f≈ x∈xs) + map-∷= f≈ (here x≈y) = ≡.refl + map-∷= f≈ (there x∈xs) = ≡.cong (_ ∷_) (map-∷= f≈ x∈xs) ------------------------------------------------------------------------ -- _++_ @@ -350,7 +350,7 @@ module _ (S : Setoid c ℓ) {P : Pred (Carrier S) p} ------------------------------------------------------------------------ -- derun and deduplicate -module _ (S : Setoid c ℓ) {R : Rel (Carrier S) ℓ₂} (R? : B.Decidable R) where +module _ (S : Setoid c ℓ) {R : Rel (Carrier S) ℓ₂} (R? : Binary.Decidable R) where open Setoid S using (_≈_) open Membership S using (_∈_) diff --git a/src/Data/List/Relation/Binary/BagAndSetEquality.agda b/src/Data/List/Relation/Binary/BagAndSetEquality.agda index 17af3d8955..f39397770f 100644 --- a/src/Data/List/Relation/Binary/BagAndSetEquality.agda +++ b/src/Data/List/Relation/Binary/BagAndSetEquality.agda @@ -15,7 +15,7 @@ open import Data.Empty open import Data.Fin.Base open import Data.List.Base open import Data.List.Effectful using (monad; module Applicative; module MonadProperties) -import Data.List.Properties as LP +import Data.List.Properties as List open import Data.List.Relation.Unary.Any using (Any; here; there) open import Data.List.Relation.Unary.Any.Properties hiding (++-comm) open import Data.List.Membership.Propositional using (_∈_) @@ -232,7 +232,7 @@ commutativeMonoid {a} k A = record ; ∙-cong = ++-cong } ; assoc = λ xs ys zs → - Eq.reflexive (LP.++-assoc xs ys zs) + Eq.reflexive (List.++-assoc xs ys zs) } ; identityˡ = λ xs → K-refl ; comm = λ xs ys → ↔⇒ (++↔++ xs ys) diff --git a/src/Data/List/Relation/Binary/Infix/Heterogeneous/Properties.agda b/src/Data/List/Relation/Binary/Infix/Heterogeneous/Properties.agda index e833ade444..7e85ae8661 100644 --- a/src/Data/List/Relation/Binary/Infix/Heterogeneous/Properties.agda +++ b/src/Data/List/Relation/Binary/Infix/Heterogeneous/Properties.agda @@ -27,7 +27,7 @@ open import Data.List.Relation.Binary.Pointwise.Base as Pointwise using (Pointwi open import Data.List.Relation.Binary.Infix.Heterogeneous open import Data.List.Relation.Binary.Prefix.Heterogeneous as Prefix using (Prefix; []; _∷_) -import Data.List.Relation.Binary.Prefix.Heterogeneous.Properties as Prefixₚ +import Data.List.Relation.Binary.Prefix.Heterogeneous.Properties as Prefix open import Data.List.Relation.Binary.Suffix.Heterogeneous as Suffix using (Suffix; here; there) @@ -43,7 +43,7 @@ private -- Conversion functions fromPointwise : ∀ {as bs} → Pointwise R as bs → Infix R as bs -fromPointwise pw = here (Prefixₚ.fromPointwise pw) +fromPointwise pw = here (Prefix.fromPointwise pw) fromSuffix : ∀ {as bs} → Suffix R as bs → Infix R as bs fromSuffix (here pw) = fromPointwise pw @@ -52,11 +52,11 @@ fromSuffix (there p) = there (fromSuffix p) module _ {c t} {C : Set c} {T : REL A C t} where fromPrefixSuffix : Trans R S T → Trans (Prefix R) (Suffix S) (Infix T) - fromPrefixSuffix tr p (here q) = here (Prefixₚ.trans tr p (Prefixₚ.fromPointwise q)) + fromPrefixSuffix tr p (here q) = here (Prefix.trans tr p (Prefix.fromPointwise q)) fromPrefixSuffix tr p (there q) = there (fromPrefixSuffix tr p q) fromSuffixPrefix : Trans R S T → Trans (Suffix R) (Prefix S) (Infix T) - fromSuffixPrefix tr (here p) q = here (Prefixₚ.trans tr (Prefixₚ.fromPointwise p) q) + fromSuffixPrefix tr (here p) q = here (Prefix.trans tr (Prefix.fromPointwise p) q) fromSuffixPrefix tr (there p) (_ ∷ q) = there (fromSuffixPrefix tr p q) ∷⁻ : ∀ {as b bs} → Infix R as (b ∷ bs) → Prefix R as (b ∷ bs) ⊎ Infix R as bs @@ -67,7 +67,7 @@ module _ {c t} {C : Set c} {T : REL A C t} where -- length length-mono : ∀ {as bs} → Infix R as bs → length as ≤ length bs -length-mono (here pref) = Prefixₚ.length-mono pref +length-mono (here pref) = Prefix.length-mono pref length-mono (there p) = ℕ.m≤n⇒m≤1+n (length-mono p) ------------------------------------------------------------------------ @@ -76,11 +76,11 @@ length-mono (there p) = ℕ.m≤n⇒m≤1+n (length-mono p) module _ {c t} {C : Set c} {T : REL A C t} where Prefix-Infix-trans : Trans R S T → Trans (Prefix R) (Infix S) (Infix T) - Prefix-Infix-trans tr p (here q) = here (Prefixₚ.trans tr p q) + Prefix-Infix-trans tr p (here q) = here (Prefix.trans tr p q) Prefix-Infix-trans tr p (there q) = there (Prefix-Infix-trans tr p q) Infix-Prefix-trans : Trans R S T → Trans (Infix R) (Prefix S) (Infix T) - Infix-Prefix-trans tr (here p) q = here (Prefixₚ.trans tr p q) + Infix-Prefix-trans tr (here p) q = here (Prefix.trans tr p q) Infix-Prefix-trans tr (there p) (_ ∷ q) = there (Infix-Prefix-trans tr p q) Suffix-Infix-trans : Trans R S T → Trans (Suffix R) (Infix S) (Infix T) @@ -88,7 +88,7 @@ module _ {c t} {C : Set c} {T : REL A C t} where Suffix-Infix-trans tr p (there q) = there (Suffix-Infix-trans tr p q) Infix-Suffix-trans : Trans R S T → Trans (Infix R) (Suffix S) (Infix T) - Infix-Suffix-trans tr p (here q) = Infix-Prefix-trans tr p (Prefixₚ.fromPointwise q) + Infix-Suffix-trans tr p (here q) = Infix-Prefix-trans tr p (Prefix.fromPointwise q) Infix-Suffix-trans tr p (there q) = there (Infix-Suffix-trans tr p q) trans : Trans R S T → Trans (Infix R) (Infix S) (Infix T) @@ -96,7 +96,7 @@ module _ {c t} {C : Set c} {T : REL A C t} where trans tr p (there q) = there (trans tr p q) antisym : Antisym R S T → Antisym (Infix R) (Infix S) (Pointwise T) - antisym asym (here p) (here q) = Prefixₚ.antisym asym p q + antisym asym (here p) (here q) = Prefix.antisym asym p q antisym asym {i = a ∷ as} {j = bs} p@(here _) (there q) = ⊥-elim $′ ℕ.<-irrefl refl $′ begin-strict length as <⟨ length-mono p ⟩ @@ -121,14 +121,14 @@ module _ {c d r} {C : Set c} {D : Set d} {R : REL C D r} where map⁺ : ∀ {as bs} (f : A → C) (g : B → D) → Infix (λ a b → R (f a) (g b)) as bs → Infix R (List.map f as) (List.map g bs) - map⁺ f g (here p) = here (Prefixₚ.map⁺ f g p) + map⁺ f g (here p) = here (Prefix.map⁺ f g p) map⁺ f g (there p) = there (map⁺ f g p) map⁻ : ∀ {as bs} (f : A → C) (g : B → D) → Infix R (List.map f as) (List.map g bs) → Infix (λ a b → R (f a) (g b)) as bs - map⁻ {bs = []} f g (here p) = here (Prefixₚ.map⁻ f g p) - map⁻ {bs = b ∷ bs} f g (here p) = here (Prefixₚ.map⁻ f g p) + map⁻ {bs = []} f g (here p) = here (Prefix.map⁻ f g p) + map⁻ {bs = b ∷ bs} f g (here p) = here (Prefix.map⁻ f g p) map⁻ {bs = b ∷ bs} f g (there p) = there (map⁻ f g p) ------------------------------------------------------------------------ @@ -139,7 +139,7 @@ module _ {p q} {P : Pred A p} {Q : Pred B q} (P? : U.Decidable P) (Q? : U.Decida where filter⁺ : ∀ {as bs} → Infix R as bs → Infix R (filter P? as) (filter Q? bs) - filter⁺ (here p) = here (Prefixₚ.filter⁺ P? Q? (λ _ → P⇒Q) (λ _ → Q⇒P) p) + filter⁺ (here p) = here (Prefix.filter⁺ P? Q? (λ _ → P⇒Q) (λ _ → Q⇒P) p) filter⁺ {bs = b ∷ bs} (there p) with does (Q? b) ... | true = there (filter⁺ p) ... | false = filter⁺ p @@ -149,12 +149,12 @@ module _ {p q} {P : Pred A p} {Q : Pred B q} (P? : U.Decidable P) (Q? : U.Decida replicate⁺ : ∀ {m n a b} → m ≤ n → R a b → Infix R (replicate m a) (replicate n b) -replicate⁺ m≤n r = here (Prefixₚ.replicate⁺ m≤n r) +replicate⁺ m≤n r = here (Prefix.replicate⁺ m≤n r) replicate⁻ : ∀ {m n a b} → m ≢ 0 → Infix R (replicate m a) (replicate n b) → R a b -replicate⁻ {m = m} {n = zero} m≢0 (here p) = Prefixₚ.replicate⁻ m≢0 p -replicate⁻ {m = m} {n = suc n} m≢0 (here p) = Prefixₚ.replicate⁻ m≢0 p +replicate⁻ {m = m} {n = zero} m≢0 (here p) = Prefix.replicate⁻ m≢0 p +replicate⁻ {m = m} {n = suc n} m≢0 (here p) = Prefix.replicate⁻ m≢0 p replicate⁻ {m = m} {n = suc n} m≢0 (there p) = replicate⁻ m≢0 p ------------------------------------------------------------------------ @@ -165,4 +165,4 @@ infix? R? [] [] = yes (here []) infix? R? (a ∷ as) [] = no (λ where (here ())) infix? R? as bbs@(_ ∷ bs) = map′ [ here , there ]′ ∷⁻ - (Prefixₚ.prefix? R? as bbs ⊎-dec infix? R? as bs) + (Prefix.prefix? R? as bbs ⊎-dec infix? R? as bs) diff --git a/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda b/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda index 5e44480bc3..3184ca4420 100644 --- a/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda +++ b/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda @@ -15,13 +15,13 @@ open import Data.Empty open import Data.List.Relation.Unary.All using (Null; []; _∷_) open import Data.List.Relation.Unary.Any using (Any; here; there) open import Data.List.Base as List hiding (map; _∷ʳ_) -import Data.List.Properties as Lₚ +import Data.List.Properties as List open import Data.List.Relation.Unary.Any.Properties using (here-injective; there-injective) open import Data.List.Relation.Binary.Pointwise as Pw using (Pointwise; []; _∷_) open import Data.List.Relation.Binary.Sublist.Heterogeneous -open import Data.Maybe.Relation.Unary.All as MAll using (nothing; just) +open import Data.Maybe.Relation.Unary.All as Maybe using (nothing; just) open import Data.Nat.Base using (ℕ; _≤_; _≥_); open ℕ; open _≤_ import Data.Nat.Properties as ℕ open import Data.Product.Base using (∃₂; _×_; _,_; <_,_>; proj₂; uncurry) @@ -90,9 +90,9 @@ module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where tail-Sublist : ∀ {as bs} → Sublist R as bs → - MAll.All (λ as → Sublist R as bs) (tail as) + Maybe.All (λ as → Sublist R as bs) (tail as) tail-Sublist [] = nothing - tail-Sublist (b ∷ʳ ps) = MAll.map (b ∷ʳ_) (tail-Sublist ps) + tail-Sublist (b ∷ʳ ps) = Maybe.map (b ∷ʳ_) (tail-Sublist ps) tail-Sublist (p ∷ ps) = just (_ ∷ʳ ps) take-Sublist : ∀ {as bs} n → Sublist R as bs → Sublist R (take n as) bs @@ -308,7 +308,7 @@ module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where reverse⁻ : ∀ {as bs} → Sublist R (reverse as) (reverse bs) → Sublist R as bs reverse⁻ {as} {bs} p = cast (reverse⁺ p) where - cast = P.subst₂ (Sublist R) (Lₚ.reverse-involutive as) (Lₚ.reverse-involutive bs) + cast = P.subst₂ (Sublist R) (List.reverse-involutive as) (List.reverse-involutive bs) ------------------------------------------------------------------------ -- Inversion lemmas diff --git a/src/Data/List/Relation/Binary/Subset/Propositional/Properties.agda b/src/Data/List/Relation/Binary/Subset/Propositional/Properties.agda index 71313d087e..908897f4dc 100644 --- a/src/Data/List/Relation/Binary/Subset/Propositional/Properties.agda +++ b/src/Data/List/Relation/Binary/Subset/Propositional/Properties.agda @@ -21,7 +21,7 @@ open import Data.List.Effectful open import Data.List.Relation.Unary.Any using (Any) open import Data.List.Membership.Propositional open import Data.List.Membership.Propositional.Properties -import Data.List.Relation.Binary.Subset.Setoid.Properties as Setoidₚ +import Data.List.Relation.Binary.Subset.Setoid.Properties as Subset open import Data.List.Relation.Binary.Subset.Propositional open import Data.List.Relation.Binary.Permutation.Propositional import Data.List.Relation.Binary.Permutation.Propositional.Properties as Permutation @@ -79,7 +79,7 @@ module _ (A : Set a) where ------------------------------------------------------------------------ -- Relational properties with _↭_ (permutation) ------------------------------------------------------------------------ --- See issue #1354 for why these proofs can't be taken from `Setoidₚ` +-- See issue #1354 for why these proofs can't be taken from `Subset` ⊆-reflexive-↭ : _↭_ {A = A} ⇒ _⊆_ ⊆-reflexive-↭ xs↭ys = Permutation.∈-resp-↭ xs↭ys @@ -109,7 +109,7 @@ module _ (A : Set a) where ------------------------------------------------------------------------ module ⊆-Reasoning (A : Set a) where - open Setoidₚ.⊆-Reasoning (setoid A) public + open Subset.⊆-Reasoning (setoid A) public hiding (step-≋; step-≋˘) ------------------------------------------------------------------------ @@ -117,10 +117,10 @@ module ⊆-Reasoning (A : Set a) where ------------------------------------------------------------------------ Any-resp-⊆ : ∀ {P : Pred A p} → (Any P) Respects _⊆_ -Any-resp-⊆ = Setoidₚ.Any-resp-⊆ (setoid _) (subst _) +Any-resp-⊆ = Subset.Any-resp-⊆ (setoid _) (subst _) All-resp-⊇ : ∀ {P : Pred A p} → (All P) Respects _⊇_ -All-resp-⊇ = Setoidₚ.All-resp-⊇ (setoid _) (subst _) +All-resp-⊇ = Subset.All-resp-⊇ (setoid _) (subst _) ------------------------------------------------------------------------ -- Properties relating _⊆_ to various list functions @@ -137,31 +137,31 @@ map⁺ f xs⊆ys = -- ∷ xs⊆x∷xs : ∀ (xs : List A) x → xs ⊆ x ∷ xs -xs⊆x∷xs = Setoidₚ.xs⊆x∷xs (setoid _) +xs⊆x∷xs = Subset.xs⊆x∷xs (setoid _) ∷⁺ʳ : ∀ x → xs ⊆ ys → x ∷ xs ⊆ x ∷ ys -∷⁺ʳ = Setoidₚ.∷⁺ʳ (setoid _) +∷⁺ʳ = Subset.∷⁺ʳ (setoid _) ∈-∷⁺ʳ : ∀ {x} → x ∈ ys → xs ⊆ ys → x ∷ xs ⊆ ys -∈-∷⁺ʳ = Setoidₚ.∈-∷⁺ʳ (setoid _) +∈-∷⁺ʳ = Subset.∈-∷⁺ʳ (setoid _) ------------------------------------------------------------------------ -- _++_ xs⊆xs++ys : ∀ (xs ys : List A) → xs ⊆ xs ++ ys -xs⊆xs++ys = Setoidₚ.xs⊆xs++ys (setoid _) +xs⊆xs++ys = Subset.xs⊆xs++ys (setoid _) xs⊆ys++xs : ∀ (xs ys : List A) → xs ⊆ ys ++ xs -xs⊆ys++xs = Setoidₚ.xs⊆ys++xs (setoid _) +xs⊆ys++xs = Subset.xs⊆ys++xs (setoid _) ++⁺ʳ : ∀ zs → xs ⊆ ys → zs ++ xs ⊆ zs ++ ys -++⁺ʳ = Setoidₚ.++⁺ʳ (setoid _) +++⁺ʳ = Subset.++⁺ʳ (setoid _) ++⁺ˡ : ∀ zs → xs ⊆ ys → xs ++ zs ⊆ ys ++ zs -++⁺ˡ = Setoidₚ.++⁺ˡ (setoid _) +++⁺ˡ = Subset.++⁺ˡ (setoid _) ++⁺ : ws ⊆ xs → ys ⊆ zs → ws ++ ys ⊆ xs ++ zs -++⁺ = Setoidₚ.++⁺ (setoid _) +++⁺ = Subset.++⁺ (setoid _) ------------------------------------------------------------------------ -- concat @@ -178,7 +178,7 @@ module _ {xss yss : List (List A)} where -- applyUpTo applyUpTo⁺ : ∀ (f : ℕ → A) {m n} → m ≤ n → applyUpTo f m ⊆ applyUpTo f n -applyUpTo⁺ = Setoidₚ.applyUpTo⁺ (setoid _) +applyUpTo⁺ = Subset.applyUpTo⁺ (setoid _) ------------------------------------------------------------------------ -- _>>=_ @@ -248,12 +248,12 @@ module _ {xs : List A} {f : ∀ {x} → x ∈ xs → B} module _ {P : Pred A p} (P? : Decidable P) where filter-⊆ : ∀ xs → filter P? xs ⊆ xs - filter-⊆ = Setoidₚ.filter-⊆ (setoid A) P? + filter-⊆ = Subset.filter-⊆ (setoid A) P? module _ {Q : Pred A q} (Q? : Decidable Q) where filter⁺′ : P ⋐ Q → ∀ {xs ys} → xs ⊆ ys → filter P? xs ⊆ filter Q? ys - filter⁺′ = Setoidₚ.filter⁺′ (setoid A) P? (resp P) Q? (resp Q) + filter⁺′ = Subset.filter⁺′ (setoid A) P? (resp P) Q? (resp Q) ------------------------------------------------------------------------ diff --git a/src/Data/List/Relation/Binary/Suffix/Heterogeneous/Properties.agda b/src/Data/List/Relation/Binary/Suffix/Heterogeneous/Properties.agda index 3ea10495e6..17a0c25c77 100644 --- a/src/Data/List/Relation/Binary/Suffix/Heterogeneous/Properties.agda +++ b/src/Data/List/Relation/Binary/Suffix/Heterogeneous/Properties.agda @@ -30,8 +30,8 @@ open import Relation.Binary.Definitions as B open import Relation.Binary.PropositionalEquality.Core as P using (_≡_; _≢_; refl; sym; subst; subst₂) -import Data.List.Properties as Listₚ -import Data.List.Relation.Binary.Prefix.Heterogeneous.Properties as Prefixₚ +import Data.List.Properties as List +import Data.List.Relation.Binary.Prefix.Heterogeneous.Properties as Prefix ------------------------------------------------------------------------ -- Suffix and Prefix are linked via reverse @@ -43,15 +43,15 @@ module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where fromPrefix {as} {bs} p with Prefix.toView p ... | Prefix._++_ {cs} rs ds = subst (Suffix R (reverse as)) - (sym (Listₚ.reverse-++ cs ds)) + (sym (List.reverse-++ cs ds)) (Suffix.fromView (reverse ds Suffix.++ Pw.reverse⁺ rs)) fromPrefix-rev : ∀ {as bs} → Prefix R (reverse as) (reverse bs) → Suffix R as bs fromPrefix-rev pre = subst₂ (Suffix R) - (Listₚ.reverse-involutive _) - (Listₚ.reverse-involutive _) + (List.reverse-involutive _) + (List.reverse-involutive _) (fromPrefix pre) toPrefix-rev : ∀ {as bs} → Suffix R as bs → @@ -59,15 +59,15 @@ module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where toPrefix-rev {as} {bs} s with Suffix.toView s ... | Suffix._++_ cs {ds} rs = subst (Prefix R (reverse as)) - (sym (Listₚ.reverse-++ cs ds)) + (sym (List.reverse-++ cs ds)) (Prefix.fromView (Pw.reverse⁺ rs Prefix.++ reverse cs)) toPrefix : ∀ {as bs} → Suffix R (reverse as) (reverse bs) → Prefix R as bs toPrefix suf = subst₂ (Prefix R) - (Listₚ.reverse-involutive _) - (Listₚ.reverse-involutive _) + (List.reverse-involutive _) + (List.reverse-involutive _) (toPrefix-rev suf) ------------------------------------------------------------------------ @@ -139,7 +139,7 @@ module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where ds; uncurry) open import Data.Sum.Base using ([_,_]′) open import Data.Sum.Properties using ([,]-map) @@ -689,7 +689,7 @@ map-<,>-zip f g [] = refl map-<,>-zip f g (x ∷ xs) = cong (_ ∷_) (map-<,>-zip f g xs) map-zip : ∀ (f : A → B) (g : C → D) (xs : Vec A n) (ys : Vec C n) → - map (Prod.map f g) (zip xs ys) ≡ zip (map f xs) (map g ys) + map (Product.map f g) (zip xs ys) ≡ zip (map f xs) (map g ys) map-zip f g [] [] = refl map-zip f g (x ∷ xs) (y ∷ ys) = cong (_ ∷_) (map-zip f g xs ys) @@ -705,10 +705,10 @@ lookup-unzip (suc i) ((x , y) ∷ xys) = lookup-unzip i xys map-unzip : ∀ (f : A → B) (g : C → D) (xys : Vec (A × C) n) → let xs , ys = unzip xys - in (map f xs , map g ys) ≡ unzip (map (Prod.map f g) xys) + in (map f xs , map g ys) ≡ unzip (map (Product.map f g) xys) map-unzip f g [] = refl map-unzip f g ((x , y) ∷ xys) = - cong (Prod.map (f x ∷_) (g y ∷_)) (map-unzip f g xys) + cong (Product.map (f x ∷_) (g y ∷_)) (map-unzip f g xys) -- Products of vectors are isomorphic to vectors of products. @@ -716,7 +716,7 @@ unzip∘zip : ∀ (xs : Vec A n) (ys : Vec B n) → unzip (zip xs ys) ≡ (xs , ys) unzip∘zip [] [] = refl unzip∘zip (x ∷ xs) (y ∷ ys) = - cong (Prod.map (x ∷_) (y ∷_)) (unzip∘zip xs ys) + cong (Product.map (x ∷_) (y ∷_)) (unzip∘zip xs ys) zip∘unzip : ∀ (xys : Vec (A × B) n) → uncurry zip (unzip xys) ≡ xys zip∘unzip [] = refl @@ -869,7 +869,7 @@ unfold-∷ʳ eq x (y ∷ xs) = cong (y ∷_) (unfold-∷ʳ (cong pred eq) x xs) ∷ʳ-injective : ∀ (xs ys : Vec A n) → xs ∷ʳ x ≡ ys ∷ʳ y → xs ≡ ys × x ≡ y ∷ʳ-injective [] [] refl = (refl , refl) ∷ʳ-injective (x ∷ xs) (y ∷ ys) eq with ∷-injective eq -... | refl , eq′ = Prod.map₁ (cong (x ∷_)) (∷ʳ-injective xs ys eq′) +... | refl , eq′ = Product.map₁ (cong (x ∷_)) (∷ʳ-injective xs ys eq′) ∷ʳ-injectiveˡ : ∀ (xs ys : Vec A n) → xs ∷ʳ x ≡ ys ∷ʳ y → xs ≡ ys ∷ʳ-injectiveˡ xs ys eq = proj₁ (∷ʳ-injective xs ys eq) @@ -1294,29 +1294,29 @@ cast-fromList : ∀ {xs ys : List A} (eq : xs ≡ ys) → cast (cong List.length eq) (fromList xs) ≡ fromList ys cast-fromList {xs = List.[]} {ys = List.[]} eq = refl cast-fromList {xs = x List.∷ xs} {ys = y List.∷ ys} eq = - let x≡y , xs≡ys = Listₚ.∷-injective eq in begin + let x≡y , xs≡ys = List.∷-injective eq in begin x ∷ cast (cong (pred ∘ List.length) eq) (fromList xs) ≡⟨ cong (_ ∷_) (cast-fromList xs≡ys) ⟩ x ∷ fromList ys ≡⟨ cong (_∷ _) x≡y ⟩ y ∷ fromList ys ∎ where open ≡-Reasoning fromList-map : ∀ (f : A → B) (xs : List A) → - cast (Listₚ.length-map f xs) (fromList (List.map f xs)) ≡ map f (fromList xs) + cast (List.length-map f xs) (fromList (List.map f xs)) ≡ map f (fromList xs) fromList-map f List.[] = refl fromList-map f (x List.∷ xs) = cong (f x ∷_) (fromList-map f xs) fromList-++ : ∀ (xs : List A) {ys : List A} → - cast (Listₚ.length-++ xs) (fromList (xs List.++ ys)) ≡ fromList xs ++ fromList ys + cast (List.length-++ xs) (fromList (xs List.++ ys)) ≡ fromList xs ++ fromList ys fromList-++ List.[] {ys} = cast-is-id refl (fromList ys) fromList-++ (x List.∷ xs) {ys} = cong (x ∷_) (fromList-++ xs) -fromList-reverse : (xs : List A) → cast (Listₚ.length-reverse xs) (fromList (List.reverse xs)) ≡ reverse (fromList xs) +fromList-reverse : (xs : List A) → cast (List.length-reverse xs) (fromList (List.reverse xs)) ≡ reverse (fromList xs) fromList-reverse List.[] = refl fromList-reverse (x List.∷ xs) = begin - fromList (List.reverse (x List.∷ xs)) ≈⟨ cast-fromList (Listₚ.ʳ++-defn xs) ⟩ + fromList (List.reverse (x List.∷ xs)) ≈⟨ cast-fromList (List.ʳ++-defn xs) ⟩ fromList (List.reverse xs List.++ List.[ x ]) ≈⟨ fromList-++ (List.reverse xs) ⟩ fromList (List.reverse xs) ++ [ x ] ≈⟨ unfold-∷ʳ (+-comm 1 _) x (fromList (List.reverse xs)) ⟨ - fromList (List.reverse xs) ∷ʳ x ≈⟨ ≈-cong (_∷ʳ x) (cast-∷ʳ (cong suc (Listₚ.length-reverse xs)) _ _) + fromList (List.reverse xs) ∷ʳ x ≈⟨ ≈-cong (_∷ʳ x) (cast-∷ʳ (cong suc (List.length-reverse xs)) _ _) (fromList-reverse xs) ⟩ reverse (fromList xs) ∷ʳ x ≂⟨ reverse-∷ x (fromList xs) ⟨ reverse (x ∷ fromList xs) ≈⟨⟩ diff --git a/src/Data/Vec/Relation/Unary/All/Properties.agda b/src/Data/Vec/Relation/Unary/All/Properties.agda index 4b8951ff9d..3c2a126230 100644 --- a/src/Data/Vec/Relation/Unary/All/Properties.agda +++ b/src/Data/Vec/Relation/Unary/All/Properties.agda @@ -12,9 +12,8 @@ open import Data.Nat.Base using (ℕ; zero; suc; _+_) open import Data.Fin.Base using (Fin; zero; suc) open import Data.List.Base using ([]; _∷_) open import Data.List.Relation.Unary.All as List using ([]; _∷_) -open import Data.Product.Base as Prod using (_×_; _,_; uncurry; uncurry′) +open import Data.Product.Base as Product using (_×_; _,_; uncurry; uncurry′) open import Data.Vec.Base as Vec -import Data.Vec.Properties as Vecₚ open import Data.Vec.Relation.Unary.All as All using (All; []; _∷_) open import Level using (Level) open import Function.Base using (_∘_; id) @@ -82,7 +81,7 @@ gmap g = map⁺ ∘ All.map g ++⁻ : (xs : Vec A m) {ys : Vec A n} → All P (xs ++ ys) → All P xs × All P ys ++⁻ [] p = [] , p -++⁻ (x ∷ xs) (px ∷ pxs) = Prod.map₁ (px ∷_) (++⁻ _ pxs) +++⁻ (x ∷ xs) (px ∷ pxs) = Product.map₁ (px ∷_) (++⁻ _ pxs) ++⁺∘++⁻ : (xs : Vec A m) {ys : Vec A n} → (p : All P (xs ++ ys)) → diff --git a/src/Data/Vec/Relation/Unary/AllPairs/Properties.agda b/src/Data/Vec/Relation/Unary/AllPairs/Properties.agda index ffc0ec6c4c..b13962b750 100644 --- a/src/Data/Vec/Relation/Unary/AllPairs/Properties.agda +++ b/src/Data/Vec/Relation/Unary/AllPairs/Properties.agda @@ -9,9 +9,9 @@ module Data.Vec.Relation.Unary.AllPairs.Properties where open import Data.Vec -import Data.Vec.Properties as Vecₚ +import Data.Vec.Properties as Vec open import Data.Vec.Relation.Unary.All as All using (All; []; _∷_) -import Data.Vec.Relation.Unary.All.Properties as Allₚ +import Data.Vec.Relation.Unary.All.Properties as All open import Data.Vec.Relation.Unary.AllPairs as AllPairs using (AllPairs; []; _∷_) open import Data.Bool.Base using (true; false) open import Data.Fin.Base using (Fin) @@ -39,7 +39,7 @@ module _ {R : Rel A ℓ} {f : B → A} where map⁺ : ∀ {n xs} → AllPairs (λ x y → R (f x) (f y)) {n} xs → AllPairs R {n} (map f xs) map⁺ [] = [] - map⁺ (x∉xs ∷ xs!) = Allₚ.map⁺ x∉xs ∷ map⁺ xs! + map⁺ (x∉xs ∷ xs!) = All.map⁺ x∉xs ∷ map⁺ xs! ------------------------------------------------------------------------ -- ++ @@ -49,7 +49,7 @@ module _ {R : Rel A ℓ} where ++⁺ : ∀ {n m xs ys} → AllPairs R {n} xs → AllPairs R {m} ys → All (λ x → All (R x) ys) xs → AllPairs R (xs ++ ys) ++⁺ [] Rys _ = Rys - ++⁺ (px ∷ Rxs) Rys (Rxys ∷ Rxsys) = Allₚ.++⁺ px Rxys ∷ ++⁺ Rxs Rys Rxsys + ++⁺ (px ∷ Rxs) Rys (Rxys ∷ Rxsys) = All.++⁺ px Rxys ∷ ++⁺ Rxs Rys Rxsys ------------------------------------------------------------------------ -- concat @@ -61,7 +61,7 @@ module _ {R : Rel A ℓ} where AllPairs R (concat xss) concat⁺ [] [] = [] concat⁺ (pxs ∷ pxss) (Rxsxss ∷ Rxss) = ++⁺ pxs (concat⁺ pxss Rxss) - (All.map Allₚ.concat⁺ (Allₚ.All-swap Rxsxss)) + (All.map All.concat⁺ (All.All-swap Rxsxss)) ------------------------------------------------------------------------ -- take and drop @@ -70,7 +70,7 @@ module _ {R : Rel A ℓ} where take⁺ : ∀ {n} m {xs} → AllPairs R {m + n} xs → AllPairs R {m} (take m xs) take⁺ zero pxs = [] - take⁺ (suc m) {x ∷ xs} (px ∷ pxs) = Allₚ.take⁺ m px ∷ take⁺ m pxs + take⁺ (suc m) {x ∷ xs} (px ∷ pxs) = All.take⁺ m px ∷ take⁺ m pxs drop⁺ : ∀ {n} m {xs} → AllPairs R {m + n} xs → AllPairs R {n} (drop m xs) drop⁺ zero pxs = pxs @@ -85,5 +85,5 @@ module _ {R : Rel A ℓ} where AllPairs R (tabulate f) tabulate⁺ {zero} fᵢ~fⱼ = [] tabulate⁺ {suc n} fᵢ~fⱼ = - Allₚ.tabulate⁺ (λ j → fᵢ~fⱼ λ()) ∷ + All.tabulate⁺ (λ j → fᵢ~fⱼ λ()) ∷ tabulate⁺ (fᵢ~fⱼ ∘ (_∘ suc-injective)) diff --git a/src/Data/Vec/Relation/Unary/Linked/Properties.agda b/src/Data/Vec/Relation/Unary/Linked/Properties.agda index 8ff5a4d2e3..e49cda76f6 100644 --- a/src/Data/Vec/Relation/Unary/Linked/Properties.agda +++ b/src/Data/Vec/Relation/Unary/Linked/Properties.agda @@ -10,7 +10,7 @@ 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ₚ +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; _<_) @@ -43,7 +43,7 @@ module _ (trans : Transitive R) where 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