From cd8bba0ac0187ac25bc631ef2fdd7c14325d5f97 Mon Sep 17 00:00:00 2001 From: Github Actions Date: Wed, 14 Aug 2024 01:07:26 +0000 Subject: [PATCH] =?UTF-8?q?Deploying=20to=20gh-pages=20from=20@=20agda/agd?= =?UTF-8?q?a-stdlib@a6da449732a92cbe1d4525e97ba2de9c324e5580=20?= =?UTF-8?q?=F0=9F=9A=80?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- master/Codata.Sized.Colist.Properties.html | 4 +- master/Codata.Sized.Stream.Properties.html | 4 +- ...t.Membership.Propositional.Properties.html | 6 +- ...ata.List.Membership.Setoid.Properties.html | 20 +- ...st.Relation.Binary.Equality.DecSetoid.html | 8 +- ...elation.Binary.Equality.Propositional.html | 6 +- ...ion.Binary.Equality.Setoid.Properties.html | 12 +- ....List.Relation.Binary.Equality.Setoid.html | 186 ++++--- ...n.Binary.Infix.Homogeneous.Properties.html | 2 +- .../Data.List.Relation.Binary.Lex.Strict.html | 4 +- ....Binary.Permutation.Setoid.Properties.html | 68 +-- ...st.Relation.Binary.Permutation.Setoid.html | 2 +- .../Data.List.Relation.Binary.Pointwise.html | 506 +++++++++--------- ....Binary.Prefix.Homogeneous.Properties.html | 2 +- ...ist.Relation.Binary.Sublist.DecSetoid.html | 2 +- ...nary.Sublist.Heterogeneous.Properties.html | 2 +- ...tion.Binary.Sublist.Setoid.Properties.html | 14 +- ...a.List.Relation.Binary.Sublist.Setoid.html | 10 +- ...ation.Binary.Subset.Setoid.Properties.html | 12 +- ...inary.Suffix.Heterogeneous.Properties.html | 24 +- ....Binary.Suffix.Homogeneous.Properties.html | 2 +- ...ry.Appending.Propositional.Properties.html | 8 +- ...ation.Ternary.Appending.Propositional.html | 8 +- ...ernary.Interleaving.Setoid.Properties.html | 4 +- ...ta.List.Relation.Unary.All.Properties.html | 2 +- master/Data.String.Properties.html | 4 +- master/Data.Trie.NonEmpty.html | 6 +- master/Data.Trie.html | 2 +- ...ME.Data.List.Relation.Binary.Equality.html | 6 +- ...E.Data.List.Relation.Binary.Pointwise.html | 2 +- master/README.Text.Regex.html | 4 +- master/Text.Regex.Derivative.Brzozowski.html | 8 +- master/Text.Regex.Search.html | 2 +- 33 files changed, 484 insertions(+), 468 deletions(-) diff --git a/master/Codata.Sized.Colist.Properties.html b/master/Codata.Sized.Colist.Properties.html index c65996b3ee..1311a3b4b3 100644 --- a/master/Codata.Sized.Colist.Properties.html +++ b/master/Codata.Sized.Colist.Properties.html @@ -24,7 +24,7 @@ open import Data.List.Base as List using (List; []; _∷_) open import Data.List.NonEmpty as List⁺ using (List⁺; _∷_) import Data.List.Scans.Base as Scans -open import Data.List.Relation.Binary.Equality.Propositional using (≋-refl) +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 open import Data.Maybe.Relation.Unary.All using (All; nothing; just) @@ -318,7 +318,7 @@ i ⊢ concat (fromStream ass) ≈ fromStream (Stream.concat ass) fromStream-concat (as@(a ∷ _) ∷ ass) = begin concat (fromStream (as ∷ ass)) - ≈⟨ ≡.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 diff --git a/master/Codata.Sized.Stream.Properties.html b/master/Codata.Sized.Stream.Properties.html index e8c3e82d52..5f7bad31fe 100644 --- a/master/Codata.Sized.Stream.Properties.html +++ b/master/Codata.Sized.Stream.Properties.html @@ -59,7 +59,7 @@ cycle-replicate : ∀ {i} (n : ℕ) (n≢0 : n ≢ 0) (a : A) → i ⊢ cycle (List⁺.replicate n n≢0 a) ≈ repeat a cycle-replicate {i} n n≢0 a = let as = List⁺.replicate n n≢0 a in begin cycle as ≡⟨⟩ - as ⁺++ _ ≈⟨ ⁺++⁺ ≋.≋-refl (λ where .force → cycle-replicate n n≢0 a) ⟩ + as ⁺++ _ ≈⟨ ⁺++⁺ ≋.≋-refl (λ where .force → cycle-replicate n n≢0 a) ⟩ as ⁺++ (λ where .force → repeat a) ≈⟨ ≡.refl ∷ (λ where .force → replicate-repeat (pred n) a) ⟩ repeat a ∎ where open ≈-Reasoning @@ -87,7 +87,7 @@ map-cycle : ∀ {i} (f : A → B) as → i ⊢ map f (cycle as) ≈ cycle (List⁺.map f as) map-cycle f as = begin map f (cycle as) ≈⟨ map-⁺++ f as _ ⟩ - List⁺.map f as ⁺++ _ ≈⟨ ⁺++⁺ ≋.≋-refl (λ where .force → map-cycle f as) ⟩ + List⁺.map f as ⁺++ _ ≈⟨ ⁺++⁺ ≋.≋-refl (λ where .force → map-cycle f as) ⟩ cycle (List⁺.map f as) ∎ where open ≈-Reasoning ------------------------------------------------------------------------ diff --git a/master/Data.List.Membership.Propositional.Properties.html b/master/Data.List.Membership.Propositional.Properties.html index 0dac8debe0..ea974b818f 100644 --- a/master/Data.List.Membership.Propositional.Properties.html +++ b/master/Data.List.Membership.Propositional.Properties.html @@ -18,7 +18,7 @@ using (_∈_; _∉_; mapWith∈; _≢∈_) import Data.List.Membership.Setoid.Properties as Membership open import Data.List.Relation.Binary.Equality.Propositional - using (_≋_; ≡⇒≋; ≋⇒≡) + using (_≋_; ≡⇒≋; ≋⇒≡) open import Data.List.Relation.Unary.Any as Any using (Any; here; there) open import Data.List.Relation.Unary.Any.Properties using (map↔; concat↔; >>=↔; ⊛↔; Any-cong; ⊗↔′; ¬Any[]) @@ -65,10 +65,10 @@ ------------------------------------------------------------------------ -- Equality -∈-resp-≋ : ∀ {x : A} → (x ∈_) Respects _≋_ +∈-resp-≋ : ∀ {x : A} → (x ∈_) Respects _≋_ ∈-resp-≋ = Membership.∈-resp-≋ (≡.setoid _) -∉-resp-≋ : ∀ {x : A} → (x ∉_) Respects _≋_ +∉-resp-≋ : ∀ {x : A} → (x ∉_) Respects _≋_ ∉-resp-≋ = Membership.∉-resp-≋ (≡.setoid _) ------------------------------------------------------------------------ diff --git a/master/Data.List.Membership.Setoid.Properties.html b/master/Data.List.Membership.Setoid.Properties.html index 5da484b4c1..f1c85354f9 100644 --- a/master/Data.List.Membership.Setoid.Properties.html +++ b/master/Data.List.Membership.Setoid.Properties.html @@ -59,11 +59,11 @@ ∉-resp-≈ : ∀ {xs} → (_∉ xs) Respects _≈_ ∉-resp-≈ v≈w v∉xs w∈xs = v∉xs (∈-resp-≈ (sym v≈w) w∈xs) - ∈-resp-≋ : ∀ {x} → (x ∈_) Respects _≋_ + ∈-resp-≋ : ∀ {x} → (x ∈_) Respects _≋_ ∈-resp-≋ = Any.lift-resp (flip trans) - ∉-resp-≋ : ∀ {x} → (x ∉_) Respects _≋_ - ∉-resp-≋ xs≋ys v∉xs v∈ys = v∉xs (∈-resp-≋ (≋-sym xs≋ys) v∈ys) + ∉-resp-≋ : ∀ {x} → (x ∉_) Respects _≋_ + ∉-resp-≋ xs≋ys v∉xs v∈ys = v∉xs (∈-resp-≋ (≋-sym xs≋ys) v∈ys) -- index is injective in its first argument. @@ -102,8 +102,8 @@ open Setoid S₁ renaming (Carrier to A₁; _≈_ to _≈₁_; refl to refl₁) open Setoid S₂ renaming (Carrier to A₂; _≈_ to _≈₂_; refl to refl₂) - open Equality S₁ using ([]; _∷_) renaming (_≋_ to _≋₁_) - open Equality S₂ using () renaming (_≋_ to _≋₂_) + open Equality S₁ using ([]; _∷_) renaming (_≋_ to _≋₁_) + open Equality S₂ using () renaming (_≋_ to _≋₂_) open Membership S₁ mapWith∈-cong : ∀ {xs ys} → xs ≋₁ ys → @@ -174,7 +174,7 @@ open Membership S using (_∈_) open Setoid S - open Equality S using (_≋_; _∷_; ≋-refl) + open Equality S using (_≋_; _∷_; ≋-refl) ∈-++⁺ˡ : ∀ {v xs ys} → v ∈ xs → v ∈ xs ++ ys ∈-++⁺ˡ = Any.++⁺ˡ @@ -210,8 +210,8 @@ ∈-insert xs = Any.++-insert xs ∈-∃++ : ∀ {v xs} → v ∈ xs → ∃₂ λ ys zs → ∃ λ w → - v ≈ w × xs ≋ ys ++ [ w ] ++ zs - ∈-∃++ (here px) = [] , _ , _ , px , ≋-refl + v ≈ w × xs ≋ ys ++ [ w ] ++ zs + ∈-∃++ (here px) = [] , _ , _ , px , ≋-refl ∈-∃++ (there {d} v∈xs) = let hs , _ , _ , v≈v′ , eq = ∈-∃++ v∈xs in d ∷ hs , _ , _ , v≈v′ , refl ∷ eq @@ -223,8 +223,8 @@ open Setoid S using (_≈_) open Membership S using (_∈_) - open Equality S using (≋-setoid) - open Membership ≋-setoid using (find) renaming (_∈_ to _∈ₗ_) + open Equality S using (≋-setoid) + open Membership ≋-setoid using (find) renaming (_∈_ to _∈ₗ_) ∈-concat⁺ : ∀ {v xss} → Any (v ∈_) xss → v ∈ concat xss ∈-concat⁺ = Any.concat⁺ diff --git a/master/Data.List.Relation.Binary.Equality.DecSetoid.html b/master/Data.List.Relation.Binary.Equality.DecSetoid.html index c09cb83e8f..0e5ef6c76e 100644 --- a/master/Data.List.Relation.Binary.Equality.DecSetoid.html +++ b/master/Data.List.Relation.Binary.Equality.DecSetoid.html @@ -30,12 +30,12 @@ infix 4 _≋?_ -_≋?_ : Decidable _≋_ +_≋?_ : Decidable _≋_ _≋?_ = PW.decidable _≟_ -≋-isDecEquivalence : IsDecEquivalence _≋_ -≋-isDecEquivalence = PW.isDecEquivalence isDecEquivalence +≋-isDecEquivalence : IsDecEquivalence _≋_ +≋-isDecEquivalence = PW.isDecEquivalence isDecEquivalence ≋-decSetoid : DecSetoid a (a ⊔ ℓ) -≋-decSetoid = PW.decSetoid DS +≋-decSetoid = PW.decSetoid DS \ No newline at end of file diff --git a/master/Data.List.Relation.Binary.Equality.Propositional.html b/master/Data.List.Relation.Binary.Equality.Propositional.html index 03a72b8c46..6ab3e5744c 100644 --- a/master/Data.List.Relation.Binary.Equality.Propositional.html +++ b/master/Data.List.Relation.Binary.Equality.Propositional.html @@ -28,10 +28,10 @@ ------------------------------------------------------------------------ -- ≋ is propositional -≋⇒≡ : _≋_ ⇒ _≡_ +≋⇒≡ : _≋_ ⇒ _≡_ ≋⇒≡ [] = refl ≋⇒≡ (refl ∷ xs≈ys) = cong (_ ∷_) (≋⇒≡ xs≈ys) -≡⇒≋ : _≡_ ⇒ _≋_ -≡⇒≋ refl = ≋-refl +≡⇒≋ : _≡_ ⇒ _≋_ +≡⇒≋ refl = ≋-refl \ No newline at end of file diff --git a/master/Data.List.Relation.Binary.Equality.Setoid.Properties.html b/master/Data.List.Relation.Binary.Equality.Setoid.Properties.html index d06f7a502f..ddc4e9f02d 100644 --- a/master/Data.List.Relation.Binary.Equality.Setoid.Properties.html +++ b/master/Data.List.Relation.Binary.Equality.Setoid.Properties.html @@ -22,8 +22,8 @@ open import Function.Base using (_∘_) open import Level using (_⊔_) -open ≋ S using (_≋_; ≋-refl; ≋-reflexive; ≋-isEquivalence; ++⁺) -open Structures _≋_ using (IsMagma; IsSemigroup; IsMonoid) +open ≋ S using (_≋_; ≋-refl; ≋-reflexive; ≋-isEquivalence; ++⁺) +open Structures _≋_ using (IsMagma; IsSemigroup; IsMonoid) ------------------------------------------------------------------------ -- The []-++-Monoid @@ -32,20 +32,20 @@ isMagma : IsMagma _++_ isMagma = record - { isEquivalence = ≋-isEquivalence - ; ∙-cong = ++⁺ + { isEquivalence = ≋-isEquivalence + ; ∙-cong = ++⁺ } isSemigroup : IsSemigroup _++_ isSemigroup = record { isMagma = isMagma - ; assoc = λ xs ys zs → ≋-reflexive (List.++-assoc xs ys zs) + ; assoc = λ xs ys zs → ≋-reflexive (List.++-assoc xs ys zs) } isMonoid : IsMonoid _++_ [] isMonoid = record { isSemigroup = isSemigroup - ; identity = (λ _ → ≋-refl) , ≋-reflexive ∘ List.++-identityʳ + ; identity = (λ _ → ≋-refl) , ≋-reflexive ∘ List.++-identityʳ } -- Bundles diff --git a/master/Data.List.Relation.Binary.Equality.Setoid.html b/master/Data.List.Relation.Binary.Equality.Setoid.html index f3e6bbc2cd..40ae7aa588 100644 --- a/master/Data.List.Relation.Binary.Equality.Setoid.html +++ b/master/Data.List.Relation.Binary.Equality.Setoid.html @@ -30,132 +30,140 @@ private variable p q : Level + ws xs xs′ ys ys′ zs : List A + xss yss : List (List A) ------------------------------------------------------------------------- --- Definition of equality ------------------------------------------------------------------------- +------------------------------------------------------------------------ +-- Definition of equality +------------------------------------------------------------------------ -infix 4 _≋_ +infix 4 _≋_ -_≋_ : Rel₂ (List A) (a ⊔ ℓ) -_≋_ = Pointwise _≈_ +_≋_ : Rel₂ (List A) (a ⊔ ℓ) +_≋_ = Pointwise _≈_ -open PW public - using ([]; _∷_) +open PW public + using ([]; _∷_) ------------------------------------------------------------------------- --- Relational properties ------------------------------------------------------------------------- +------------------------------------------------------------------------ +-- Relational properties +------------------------------------------------------------------------ -≋-refl : Reflexive _≋_ -≋-refl = PW.refl refl +≋-refl : Reflexive _≋_ +≋-refl = PW.refl refl -≋-reflexive : _≡_ ⇒ _≋_ -≋-reflexive ≡.refl = ≋-refl +≋-reflexive : _≡_ ⇒ _≋_ +≋-reflexive ≡.refl = ≋-refl -≋-sym : Symmetric _≋_ -≋-sym = PW.symmetric sym +≋-sym : Symmetric _≋_ +≋-sym = PW.symmetric sym -≋-trans : Transitive _≋_ -≋-trans = PW.transitive trans +≋-trans : Transitive _≋_ +≋-trans = PW.transitive trans -≋-isEquivalence : IsEquivalence _≋_ -≋-isEquivalence = PW.isEquivalence isEquivalence +≋-isEquivalence : IsEquivalence _≋_ +≋-isEquivalence = PW.isEquivalence isEquivalence -≋-setoid : Setoid _ _ -≋-setoid = PW.setoid S +≋-setoid : Setoid _ _ +≋-setoid = PW.setoid S ------------------------------------------------------------------------- --- Relationships to predicates ------------------------------------------------------------------------- +------------------------------------------------------------------------ +-- 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-≋ - ) +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₂ +Unique-resp-≋ : Unique Respects _≋_ +Unique-resp-≋ = AllPairs-resp-≋ ≉-resp₂ ------------------------------------------------------------------------- --- List operations ------------------------------------------------------------------------- +------------------------------------------------------------------------ +-- List operations +------------------------------------------------------------------------ ------------------------------------------------------------------------- --- length +------------------------------------------------------------------------ +-- length -≋-length : ∀ {xs ys} → xs ≋ ys → length xs ≡ length ys -≋-length = PW.Pointwise-length +≋-length : ∀ {xs ys} → xs ≋ ys → length xs ≡ length ys +≋-length = PW.Pointwise-length ------------------------------------------------------------------------- --- map +------------------------------------------------------------------------ +-- map -module _ {b ℓ₂} (T : Setoid b ℓ₂) where +module _ {b ℓ₂} (T : Setoid b ℓ₂) where - open Setoid T using () renaming (_≈_ to _≈′_) - private - _≋′_ = Pointwise _≈′_ + 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) + 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 -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 +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.++⁺ +++⁺ : ws ≋ xs → ys ≋ zs → ws ++ ys ≋ xs ++ zs +++⁺ = PW.++⁺ -++-cancelˡ : ∀ xs {ys zs} → xs ++ ys ≋ xs ++ zs → ys ≋ zs -++-cancelˡ xs = PW.++-cancelˡ xs +++⁺ʳ : ∀ xs → ys ≋ zs → xs ++ ys ≋ xs ++ zs +++⁺ʳ xs = PW.++⁺ʳ refl xs -++-cancelʳ : ∀ {xs} ys zs → ys ++ xs ≋ zs ++ xs → ys ≋ zs -++-cancelʳ = PW.++-cancelʳ +++⁺ˡ : ∀ zs → ws ≋ xs → ws ++ zs ≋ xs ++ zs +++⁺ˡ zs = PW.++⁺ˡ refl zs ------------------------------------------------------------------------- --- concat +++-cancelˡ : ∀ xs {ys zs} → xs ++ ys ≋ xs ++ zs → ys ≋ zs +++-cancelˡ xs = PW.++-cancelˡ xs -concat⁺ : ∀ {xss yss} → Pointwise _≋_ xss yss → concat xss ≋ concat yss -concat⁺ = PW.concat⁺ +++-cancelʳ : ∀ {xs} ys zs → ys ++ xs ≋ zs ++ xs → ys ≋ zs +++-cancelʳ = PW.++-cancelʳ ------------------------------------------------------------------------- --- tabulate +------------------------------------------------------------------------ +-- concat -module _ {n} {f g : Fin n → A} - where +concat⁺ : Pointwise _≋_ xss yss → concat xss ≋ concat yss +concat⁺ = PW.concat⁺ - tabulate⁺ : (∀ i → f i ≈ g i) → tabulate f ≋ tabulate g - tabulate⁺ = PW.tabulate⁺ +------------------------------------------------------------------------ +-- tabulate - tabulate⁻ : tabulate f ≋ tabulate g → (∀ i → f i ≈ g i) - tabulate⁻ = PW.tabulate⁻ +module _ {n} {f g : Fin n → A} + where ------------------------------------------------------------------------- --- filter + tabulate⁺ : (∀ i → f i ≈ g i) → tabulate f ≋ tabulate g + tabulate⁺ = PW.tabulate⁺ -module _ {P : Pred A p} (P? : U.Decidable P) (resp : P Respects _≈_) - where + tabulate⁻ : tabulate f ≋ tabulate g → (∀ i → f i ≈ g i) + tabulate⁻ = PW.tabulate⁻ - filter⁺ : ∀ {xs ys} → xs ≋ ys → filter P? xs ≋ filter P? ys - filter⁺ xs≋ys = PW.filter⁺ P? P? resp (resp ∘ sym) xs≋ys +------------------------------------------------------------------------ +-- filter ------------------------------------------------------------------------- --- reverse +module _ {P : Pred A p} (P? : U.Decidable P) (resp : P Respects _≈_) + where -ʳ++⁺ : ∀{xs xs′ ys ys′} → xs ≋ xs′ → ys ≋ ys′ → xs ʳ++ ys ≋ xs′ ʳ++ ys′ -ʳ++⁺ = PW.ʳ++⁺ + filter⁺ : xs ≋ ys → filter P? xs ≋ filter P? ys + filter⁺ xs≋ys = PW.filter⁺ P? P? resp (resp ∘ sym) xs≋ys -reverse⁺ : ∀ {xs ys} → xs ≋ ys → reverse xs ≋ reverse ys -reverse⁺ = PW.reverse⁺ +------------------------------------------------------------------------ +-- reverse + +ʳ++⁺ : xs ≋ xs′ → ys ≋ ys′ → xs ʳ++ ys ≋ xs′ ʳ++ ys′ +ʳ++⁺ = PW.ʳ++⁺ + +reverse⁺ : xs ≋ ys → reverse xs ≋ reverse ys +reverse⁺ = PW.reverse⁺ \ No newline at end of file diff --git a/master/Data.List.Relation.Binary.Infix.Homogeneous.Properties.html b/master/Data.List.Relation.Binary.Infix.Homogeneous.Properties.html index f260e0b838..ec1eebad5f 100644 --- a/master/Data.List.Relation.Binary.Infix.Homogeneous.Properties.html +++ b/master/Data.List.Relation.Binary.Infix.Homogeneous.Properties.html @@ -29,7 +29,7 @@ isPreorder : IsPreorder R S → IsPreorder (Pointwise R) (Infix S) isPreorder po = record - { isEquivalence = Pointwise.isEquivalence PO.isEquivalence + { isEquivalence = Pointwise.isEquivalence PO.isEquivalence ; reflexive = fromPointwise ∘′ Pointwise.map PO.reflexive ; trans = trans PO.trans } where module PO = IsPreorder po diff --git a/master/Data.List.Relation.Binary.Lex.Strict.html b/master/Data.List.Relation.Binary.Lex.Strict.html index dca4f2b069..34f80215ef 100644 --- a/master/Data.List.Relation.Binary.Lex.Strict.html +++ b/master/Data.List.Relation.Binary.Lex.Strict.html @@ -113,7 +113,7 @@ <-isStrictPartialOrder : IsStrictPartialOrder _≈_ _≺_ → IsStrictPartialOrder _≋_ _<_ <-isStrictPartialOrder spo = record - { isEquivalence = Pointwise.isEquivalence isEquivalence + { isEquivalence = Pointwise.isEquivalence isEquivalence ; irrefl = <-irreflexive irrefl ; trans = Core.transitive isEquivalence <-resp-≈ trans ; <-resp-≈ = Core.respects₂ isEquivalence <-resp-≈ @@ -189,7 +189,7 @@ ≤-isPreorder : IsEquivalence _≈_ → Transitive _≺_ → _≺_ Respects₂ _≈_ → IsPreorder _≋_ _≤_ ≤-isPreorder eq tr resp = record - { isEquivalence = Pointwise.isEquivalence eq + { isEquivalence = Pointwise.isEquivalence eq ; reflexive = ≤-reflexive _≈_ _≺_ ; trans = Core.transitive eq resp tr } diff --git a/master/Data.List.Relation.Binary.Permutation.Setoid.Properties.html b/master/Data.List.Relation.Binary.Permutation.Setoid.Properties.html index 25c794648b..f40ce71bbe 100644 --- a/master/Data.List.Relation.Binary.Permutation.Setoid.Properties.html +++ b/master/Data.List.Relation.Binary.Permutation.Setoid.Properties.html @@ -54,7 +54,7 @@ open Membership S open Unique S using (Unique) open module ≋ = Equality S - using (_≋_; []; _∷_; ≋-refl; ≋-sym; ≋-trans; All-resp-≋; Any-resp-≋; AllPairs-resp-≋) + using (_≋_; []; _∷_; ≋-refl; ≋-sym; ≋-trans; All-resp-≋; Any-resp-≋; AllPairs-resp-≋) open PermutationReasoning ------------------------------------------------------------------------ @@ -62,13 +62,13 @@ ------------------------------------------------------------------------ All-resp-↭ : ∀ {P : Pred A p} → P Respects _≈_ → (All P) Respects _↭_ -All-resp-↭ resp (refl xs≋ys) pxs = All-resp-≋ resp xs≋ys pxs +All-resp-↭ resp (refl xs≋ys) pxs = All-resp-≋ resp xs≋ys pxs All-resp-↭ resp (prep x≈y p) (px ∷ pxs) = resp x≈y px ∷ All-resp-↭ resp p pxs All-resp-↭ resp (swap ≈₁ ≈₂ p) (px ∷ py ∷ pxs) = resp ≈₂ py ∷ resp ≈₁ px ∷ All-resp-↭ resp p pxs All-resp-↭ resp (trans p₁ p₂) pxs = All-resp-↭ resp p₂ (All-resp-↭ resp p₁ pxs) Any-resp-↭ : ∀ {P : Pred A p} → P Respects _≈_ → (Any P) Respects _↭_ -Any-resp-↭ resp (refl xs≋ys) pxs = Any-resp-≋ resp xs≋ys pxs +Any-resp-↭ resp (refl xs≋ys) pxs = Any-resp-≋ resp xs≋ys pxs Any-resp-↭ resp (prep x≈y p) (here px) = here (resp x≈y px) Any-resp-↭ resp (prep x≈y p) (there pxs) = there (Any-resp-↭ resp p pxs) Any-resp-↭ resp (swap x y p) (here px) = there (here (resp x px)) @@ -77,7 +77,7 @@ Any-resp-↭ resp (trans p₁ p₂) pxs = Any-resp-↭ resp p₂ (Any-resp-↭ resp p₁ pxs) AllPairs-resp-↭ : ∀ {R : Rel A r} → Symmetric R → R Respects₂ _≈_ → (AllPairs R) Respects _↭_ -AllPairs-resp-↭ sym resp (refl xs≋ys) pxs = AllPairs-resp-≋ resp xs≋ys pxs +AllPairs-resp-↭ sym resp (refl xs≋ys) pxs = AllPairs-resp-≋ resp xs≋ys pxs AllPairs-resp-↭ sym resp (prep x≈y p) (∼ ∷ pxs) = All-resp-↭ (proj₁ resp) p (All.map (proj₂ resp x≈y) ∼) ∷ AllPairs-resp-↭ sym resp p pxs @@ -98,17 +98,17 @@ -- Relationships to other relations ------------------------------------------------------------------------ -≋⇒↭ : _≋_ ⇒ _↭_ +≋⇒↭ : _≋_ ⇒ _↭_ ≋⇒↭ = refl -↭-respʳ-≋ : _↭_ Respectsʳ _≋_ -↭-respʳ-≋ xs≋ys (refl zs≋xs) = refl (≋-trans zs≋xs xs≋ys) +↭-respʳ-≋ : _↭_ Respectsʳ _≋_ +↭-respʳ-≋ xs≋ys (refl zs≋xs) = refl (≋-trans zs≋xs xs≋ys) ↭-respʳ-≋ (x≈y ∷ xs≋ys) (prep eq zs↭xs) = prep (≈-trans eq x≈y) (↭-respʳ-≋ xs≋ys zs↭xs) ↭-respʳ-≋ (x≈y ∷ w≈z ∷ xs≋ys) (swap eq₁ eq₂ zs↭xs) = swap (≈-trans eq₁ w≈z) (≈-trans eq₂ x≈y) (↭-respʳ-≋ xs≋ys zs↭xs) ↭-respʳ-≋ xs≋ys (trans ws↭zs zs↭xs) = trans ws↭zs (↭-respʳ-≋ xs≋ys zs↭xs) -↭-respˡ-≋ : _↭_ Respectsˡ _≋_ -↭-respˡ-≋ xs≋ys (refl ys≋zs) = refl (≋-trans (≋-sym xs≋ys) ys≋zs) +↭-respˡ-≋ : _↭_ Respectsˡ _≋_ +↭-respˡ-≋ xs≋ys (refl ys≋zs) = refl (≋-trans (≋-sym xs≋ys) ys≋zs) ↭-respˡ-≋ (x≈y ∷ xs≋ys) (prep eq zs↭xs) = prep (≈-trans (≈-sym x≈y) eq) (↭-respˡ-≋ xs≋ys zs↭xs) ↭-respˡ-≋ (x≈y ∷ w≈z ∷ xs≋ys) (swap eq₁ eq₂ zs↭xs) = swap (≈-trans (≈-sym x≈y) eq₁) (≈-trans (≈-sym w≈z) eq₂) (↭-respˡ-≋ xs≋ys zs↭xs) ↭-respˡ-≋ xs≋ys (trans ws↭zs zs↭xs) = trans (↭-respˡ-≋ xs≋ys ws↭zs) zs↭xs @@ -124,14 +124,14 @@ 0<steps (trans xs↭ys xs↭ys₁) = <-≤-trans (0<steps xs↭ys) (m≤m+n (steps xs↭ys) (steps xs↭ys₁)) -steps-respˡ : ∀ {xs ys zs} (ys≋xs : ys ≋ xs) (ys↭zs : ys ↭ zs) → +steps-respˡ : ∀ {xs ys zs} (ys≋xs : ys ≋ xs) (ys↭zs : ys ↭ zs) → steps (↭-respˡ-≋ ys≋xs ys↭zs) ≡ steps ys↭zs steps-respˡ _ (refl _) = refl steps-respˡ (_ ∷ ys≋xs) (prep _ ys↭zs) = cong suc (steps-respˡ ys≋xs ys↭zs) steps-respˡ (_ ∷ _ ∷ ys≋xs) (swap _ _ ys↭zs) = cong suc (steps-respˡ ys≋xs ys↭zs) steps-respˡ ys≋xs (trans ys↭ws ws↭zs) = cong (_+ steps ws↭zs) (steps-respˡ ys≋xs ys↭ws) -steps-respʳ : ∀ {xs ys zs} (xs≋ys : xs ≋ ys) (zs↭xs : zs ↭ xs) → +steps-respʳ : ∀ {xs ys zs} (xs≋ys : xs ≋ ys) (zs↭xs : zs ↭ xs) → steps (↭-respʳ-≋ xs≋ys zs↭xs) ≡ steps zs↭xs steps-respʳ _ (refl _) = refl steps-respʳ (_ ∷ ys≋xs) (prep _ ys↭zs) = cong suc (steps-respʳ ys≋xs ys↭zs) @@ -152,7 +152,7 @@ map⁺ : ∀ {f} → f Preserves _≈_ ⟶ _≈′_ → ∀ {xs ys} → xs ↭ ys → map f xs ↭′ map f ys - map⁺ pres (refl xs≋ys) = refl (Pointwise.map⁺ _ _ (Pointwise.map pres xs≋ys)) + map⁺ pres (refl xs≋ys) = refl (Pointwise.map⁺ _ _ (Pointwise.map pres xs≋ys)) map⁺ pres (prep x p) = prep (pres x) (map⁺ pres p) map⁺ pres (swap x y p) = swap (pres x) (pres y) (map⁺ pres p) map⁺ pres (trans p₁ p₂) = trans (map⁺ pres p₁) (map⁺ pres p₂) @@ -175,7 +175,7 @@ ++⁺ˡ (x ∷ xs) ys↭zs = ↭-prep _ (++⁺ˡ xs ys↭zs) ++⁺ʳ : ∀ {xs ys : List A} zs → xs ↭ ys → xs ++ zs ↭ ys ++ zs -++⁺ʳ zs (refl xs≋ys) = refl (Pointwise.++⁺ xs≋ys ≋-refl) +++⁺ʳ zs (refl xs≋ys) = refl (Pointwise.++⁺ xs≋ys ≋-refl) ++⁺ʳ zs (prep x ↭) = prep x (++⁺ʳ zs ↭) ++⁺ʳ zs (swap x y ↭) = swap x y (++⁺ʳ zs ↭) ++⁺ʳ zs (trans ↭₁ ↭₂) = trans (++⁺ʳ zs ↭₁) (++⁺ʳ zs ↭₂) @@ -269,17 +269,17 @@ ys ++ xs ++ zs ∎ dropMiddleElement-≋ : ∀ {x} ws xs {ys} {zs} → - ws ++ [ x ] ++ ys ≋ xs ++ [ x ] ++ zs → + ws ++ [ x ] ++ ys ≋ xs ++ [ x ] ++ zs → ws ++ ys ↭ xs ++ zs dropMiddleElement-≋ [] [] (_ ∷ eq) = ≋⇒↭ eq -dropMiddleElement-≋ [] (x ∷ xs) (w≈v ∷ eq) = ↭-respˡ-≋ (≋-sym eq) (shift w≈v xs _) +dropMiddleElement-≋ [] (x ∷ xs) (w≈v ∷ eq) = ↭-respˡ-≋ (≋-sym eq) (shift w≈v xs _) dropMiddleElement-≋ (w ∷ ws) [] (w≈x ∷ eq) = ↭-respʳ-≋ eq (↭-sym (shift (≈-sym w≈x) ws _)) dropMiddleElement-≋ (w ∷ ws) (x ∷ xs) (w≈x ∷ eq) = prep w≈x (dropMiddleElement-≋ ws xs eq) dropMiddleElement : ∀ {v} ws xs {ys zs} → ws ++ [ v ] ++ ys ↭ xs ++ [ v ] ++ zs → ws ++ ys ↭ xs ++ zs -dropMiddleElement {v} ws xs {ys} {zs} p = helper p ws xs ≋-refl ≋-refl +dropMiddleElement {v} ws xs {ys} {zs} p = helper p ws xs ≋-refl ≋-refl where lemma : ∀ {w x y z} → w ≈ x → x ≈ y → z ≈ y → w ≈ z lemma w≈x x≈y z≈y = ≈-trans (≈-trans w≈x x≈y) (≈-sym z≈y) @@ -290,11 +290,11 @@ -- much more difficult to prove. At the very least would require using `Acc`. helper : ∀ {l′ l″ : List A} → l′ ↭ l″ → ∀ ws xs {ys zs : List A} → - ws ++ [ v ] ++ ys ≋ l′ → - xs ++ [ v ] ++ zs ≋ l″ → + ws ++ [ v ] ++ ys ≋ l′ → + xs ++ [ v ] ++ zs ≋ l″ → ws ++ ys ↭ xs ++ zs helper {as} {bs} (refl eq3) ws xs {ys} {zs} eq1 eq2 = - dropMiddleElement-≋ ws xs (≋-trans (≋-trans eq1 eq3) (≋-sym eq2)) + dropMiddleElement-≋ ws xs (≋-trans (≋-trans eq1 eq3) (≋-sym eq2)) helper {_ ∷ as} {_ ∷ bs} (prep _ as↭bs) [] [] {ys} {zs} (_ ∷ ys≋as) (_ ∷ zs≋bs) = begin ys ≋⟨ ys≋as ⟩ as ↭⟨ as↭bs ⟩ @@ -328,29 +328,29 @@ helper {_ ∷ a ∷ as} {_ ∷ b ∷ bs} (swap v≈w y≈x p) [] (x ∷ w ∷ xs) {ys} {zs} (≈₁ ∷ ≋₁) (≈₂ ∷ ≋₂) = begin ys ≋⟨ ≋₁ ⟩ a ∷ as ↭⟨ prep y≈x p ⟩ - _ ∷ bs ≋⟨ ≋-sym (≈₂ ∷ tail ≋₂) ⟩ + _ ∷ bs ≋⟨ ≋-sym (≈₂ ∷ tail ≋₂) ⟩ x ∷ xs ++ v ∷ zs ↭⟨ prep ≈-refl (shift (lemma ≈₁ v≈w (head ≋₂)) xs zs) ⟩ x ∷ w ∷ xs ++ zs ∎ helper {_ ∷ a ∷ as} {_ ∷ b ∷ bs} (swap w≈x _ p) (w ∷ []) [] {ys} {zs} (≈₁ ∷ ≋₁) (≈₂ ∷ ≋₂) = begin w ∷ ys ≋⟨ ≈₁ ∷ tail (≋₁) ⟩ _ ∷ as ↭⟨ prep w≈x p ⟩ - b ∷ bs ≋⟨ ≋-sym ≋₂ ⟩ + b ∷ bs ≋⟨ ≋-sym ≋₂ ⟩ zs ∎ helper {_ ∷ a ∷ as} {_ ∷ b ∷ bs} (swap w≈y x≈v p) (w ∷ x ∷ ws) [] {ys} {zs} (≈₁ ∷ ≋₁) (≈₂ ∷ ≋₂) = begin w ∷ x ∷ ws ++ ys ↭⟨ prep ≈-refl (↭-sym (shift (lemma ≈₂ (≈-sym x≈v) (head ≋₁)) ws ys)) ⟩ w ∷ ws ++ v ∷ ys ≋⟨ ≈₁ ∷ tail ≋₁ ⟩ _ ∷ as ↭⟨ prep w≈y p ⟩ - b ∷ bs ≋⟨ ≋-sym ≋₂ ⟩ + b ∷ bs ≋⟨ ≋-sym ≋₂ ⟩ zs ∎ helper {_ ∷ a ∷ as} {_ ∷ b ∷ bs} (swap x≈v v≈y p) (x ∷ []) (y ∷ []) {ys} {zs} (≈₁ ∷ ≋₁) (≈₂ ∷ ≋₂) = begin x ∷ ys ≋⟨ ≈₁ ∷ tail ≋₁ ⟩ _ ∷ as ↭⟨ prep (≈-trans x≈v (≈-trans (≈-sym (head ≋₂)) (≈-trans (head ≋₁) v≈y))) p ⟩ - _ ∷ bs ≋⟨ ≋-sym (≈₂ ∷ tail ≋₂) ⟩ + _ ∷ bs ≋⟨ ≋-sym (≈₂ ∷ tail ≋₂) ⟩ y ∷ zs ∎ helper {_ ∷ a ∷ as} {_ ∷ b ∷ bs} (swap y≈w v≈z p) (y ∷ []) (z ∷ w ∷ xs) {ys} {zs} (≈₁ ∷ ≋₁) (≈₂ ∷ ≋₂) = begin y ∷ ys ≋⟨ ≈₁ ∷ tail ≋₁ ⟩ _ ∷ as ↭⟨ prep y≈w p ⟩ - _ ∷ bs ≋⟨ ≋-sym ≋₂ ⟩ + _ ∷ bs ≋⟨ ≋-sym ≋₂ ⟩ w ∷ xs ++ v ∷ zs ↭⟨ ↭-prep w (↭-shift xs zs) ⟩ w ∷ v ∷ xs ++ zs ↭⟨ swap ≈-refl (lemma (head ≋₁) v≈z ≈₂) ↭-refl ⟩ z ∷ w ∷ xs ++ zs ∎ @@ -359,16 +359,16 @@ w ∷ v ∷ ws ++ ys ↭⟨ ↭-prep w (↭-sym (↭-shift ws ys)) ⟩ w ∷ ws ++ v ∷ ys ≋⟨ ≋₁ ⟩ _ ∷ as ↭⟨ prep w≈z p ⟩ - _ ∷ bs ≋⟨ ≋-sym (≈₂ ∷ tail ≋₂) ⟩ + _ ∷ bs ≋⟨ ≋-sym (≈₂ ∷ tail ≋₂) ⟩ z ∷ zs ∎ helper (swap x≈z y≈w p) (x ∷ y ∷ ws) (w ∷ z ∷ xs) {ys} {zs} (≈₁ ∷ ≈₃ ∷ ≋₁) (≈₂ ∷ ≈₄ ∷ ≋₂) = begin x ∷ y ∷ ws ++ ys ↭⟨ swap (lemma ≈₁ x≈z ≈₄) (lemma ≈₃ y≈w ≈₂) (helper p ws xs ≋₁ ≋₂) ⟩ w ∷ z ∷ xs ++ zs ∎ helper {as} {bs} (trans p₁ p₂) ws xs eq1 eq2 - with ∈-∃++ S (∈-resp-↭ (↭-respˡ-≋ (≋-sym eq1) p₁) (∈-insert S ws ≈-refl)) + with ∈-∃++ S (∈-resp-↭ (↭-respˡ-≋ (≋-sym eq1) p₁) (∈-insert S ws ≈-refl)) ... | (h , t , w , v≈w , eq) = trans - (helper p₁ ws h eq1 (≋-trans (≋.++⁺ ≋-refl (v≈w ∷ ≋-refl)) (≋-sym eq))) - (helper p₂ h xs (≋-trans (≋.++⁺ ≋-refl (v≈w ∷ ≋-refl)) (≋-sym eq)) eq2) + (helper p₁ ws h eq1 (≋-trans (≋.++⁺ ≋-refl (v≈w ∷ ≋-refl)) (≋-sym eq))) + (helper p₂ h xs (≋-trans (≋.++⁺ ≋-refl (v≈w ∷ ≋-refl)) (≋-sym eq)) eq2) dropMiddle : ∀ {vs} ws xs {ys zs} → ws ++ vs ++ ys ↭ xs ++ vs ++ zs → @@ -376,19 +376,19 @@ dropMiddle {[]} ws xs p = p dropMiddle {v ∷ vs} ws xs p = dropMiddle ws xs (dropMiddleElement ws xs p) -split : ∀ (v : A) as bs {xs} → xs ↭ as ++ [ v ] ++ bs → ∃₂ λ ps qs → xs ≋ ps ++ [ v ] ++ qs +split : ∀ (v : A) as bs {xs} → xs ↭ as ++ [ v ] ++ bs → ∃₂ λ ps qs → xs ≋ ps ++ [ v ] ++ qs split v as bs p = helper as bs p (<-wellFounded (steps p)) where helper : ∀ as bs {xs} (p : xs ↭ as ++ [ v ] ++ bs) → Acc _<_ (steps p) → - ∃₂ λ ps qs → xs ≋ ps ++ [ v ] ++ qs + ∃₂ λ ps qs → xs ≋ ps ++ [ v ] ++ qs helper [] bs (refl eq) _ = [] , bs , eq helper (a ∷ []) bs (refl eq) _ = [ a ] , bs , eq helper (a ∷ b ∷ as) bs (refl eq) _ = a ∷ b ∷ as , bs , eq - helper [] bs (prep v≈x _) _ = [] , _ , v≈x ∷ ≋-refl + helper [] bs (prep v≈x _) _ = [] , _ , v≈x ∷ ≋-refl helper (a ∷ as) bs (prep eq as↭xs) (acc rec) with helper as bs as↭xs (rec ≤-refl) ... | (ps , qs , eq₂) = a ∷ ps , qs , eq ∷ eq₂ - helper [] (b ∷ bs) (swap x≈b y≈v _) _ = [ b ] , _ , x≈b ∷ y≈v ∷ ≋-refl - helper (a ∷ []) bs (swap x≈v y≈a ↭) _ = [] , a ∷ _ , x≈v ∷ y≈a ∷ ≋-refl + helper [] (b ∷ bs) (swap x≈b y≈v _) _ = [ b ] , _ , x≈b ∷ y≈v ∷ ≋-refl + helper (a ∷ []) bs (swap x≈v y≈a ↭) _ = [] , a ∷ _ , x≈v ∷ y≈a ∷ ≋-refl helper (a ∷ b ∷ as) bs (swap x≈b y≈a as↭xs) (acc rec) with helper as bs as↭xs (rec ≤-refl) ... | (ps , qs , eq) = b ∷ a ∷ ps , qs , x≈b ∷ y≈a ∷ eq helper as bs (trans ↭₁ ↭₂) (acc rec) with helper as bs ↭₂ (rec (m<n+m (steps ↭₂) (0<steps ↭₁))) @@ -401,7 +401,7 @@ module _ {p} {P : Pred A p} (P? : Decidable P) (P≈ : P Respects _≈_) where filter⁺ : ∀ {xs ys : List A} → xs ↭ ys → filter P? xs ↭ filter P? ys - filter⁺ (refl xs≋ys) = refl (≋.filter⁺ P? P≈ xs≋ys) + filter⁺ (refl xs≋ys) = refl (≋.filter⁺ P? P≈ xs≋ys) filter⁺ (trans xs↭zs zs↭ys) = trans (filter⁺ xs↭zs) (filter⁺ zs↭ys) filter⁺ {x ∷ xs} {y ∷ ys} (prep x≈y xs↭ys) with P? x | P? y ... | yes _ | yes _ = prep x≈y (filter⁺ xs↭ys) diff --git a/master/Data.List.Relation.Binary.Permutation.Setoid.html b/master/Data.List.Relation.Binary.Permutation.Setoid.html index b227070a57..5171ed4f37 100644 --- a/master/Data.List.Relation.Binary.Permutation.Setoid.html +++ b/master/Data.List.Relation.Binary.Permutation.Setoid.html @@ -96,7 +96,7 @@ renaming (≈-go to ↭-go) open ↭-syntax _IsRelatedTo_ _IsRelatedTo_ ↭-go ↭-sym public - open ≋-syntax _IsRelatedTo_ _IsRelatedTo_ (↭-go ∘′ refl) ≋-sym public + open ≋-syntax _IsRelatedTo_ _IsRelatedTo_ (↭-go ∘′ refl) ≋-sym public -- Some extra combinators that allow us to skip certain elements diff --git a/master/Data.List.Relation.Binary.Pointwise.html b/master/Data.List.Relation.Binary.Pointwise.html index 5ba09c963e..cf47cc9af4 100644 --- a/master/Data.List.Relation.Binary.Pointwise.html +++ b/master/Data.List.Relation.Binary.Pointwise.html @@ -27,253 +27,261 @@ 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 ℓ - ------------------------------------------------------------------------- --- Re-exporting the definition and basic operations ------------------------------------------------------------------------- - -open import Data.List.Relation.Binary.Pointwise.Base public -open import Data.List.Relation.Binary.Pointwise.Properties public - ------------------------------------------------------------------------- --- Structures - -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 - ------------------------------------------------------------------------- --- Bundles - -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) - } - ------------------------------------------------------------------------- --- Relationships to other list predicates ------------------------------------------------------------------------- - -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) - ------------------------------------------------------------------------- --- Relationship to functions over lists ------------------------------------------------------------------------- --- length - -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 - -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) --- Impossible cases -++-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 - -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) - ------------------------------------------------------------------------- --- reverse - -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 - -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 - -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) - ------------------------------------------------------------------------- --- filter - -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 - -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 - -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 - ------------------------------------------------------------------------- --- Properties of propositional pointwise ------------------------------------------------------------------------- - -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-≡ - } +open import Relation.Binary.Definitions using (Reflexive; _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 ℓ + +------------------------------------------------------------------------ +-- Re-exporting the definition and basic operations +------------------------------------------------------------------------ + +open import Data.List.Relation.Binary.Pointwise.Base public +open import Data.List.Relation.Binary.Pointwise.Properties public + +------------------------------------------------------------------------ +-- Structures + +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 + +------------------------------------------------------------------------ +-- Bundles + +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) + } + +------------------------------------------------------------------------ +-- Relationships to other list predicates +------------------------------------------------------------------------ + +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) + +------------------------------------------------------------------------ +-- Relationship to functions over lists +------------------------------------------------------------------------ +-- length + +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 + +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) +-- Impossible cases +++-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) + +module _ (rfl : Reflexive R) where + + ++⁺ʳ : ∀ xs → (xs ++_) Preserves (Pointwise R) ⟶ (Pointwise R) + ++⁺ʳ xs = ++⁺ (refl rfl) + + ++⁺ˡ : ∀ zs → (_++ zs) Preserves (Pointwise R) ⟶ (Pointwise R) + ++⁺ˡ zs rs = ++⁺ rs (refl rfl) + + +------------------------------------------------------------------------ +-- concat + +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) + +------------------------------------------------------------------------ +-- reverse + +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 + +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 + +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) + +------------------------------------------------------------------------ +-- filter + +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 + +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 + +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 + +------------------------------------------------------------------------ +-- Properties of propositional pointwise +------------------------------------------------------------------------ + +Pointwise-≡⇒≡ : Pointwise {A = A} _≡_ ⇒ _≡_ +Pointwise-≡⇒≡ [] = ≡.refl +Pointwise-≡⇒≡ (≡.refl ∷ xs∼ys) = ≡.cong (_ ∷_) (Pointwise-≡⇒≡ xs∼ys) + +≡⇒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-≡ + } \ No newline at end of file diff --git a/master/Data.List.Relation.Binary.Prefix.Homogeneous.Properties.html b/master/Data.List.Relation.Binary.Prefix.Homogeneous.Properties.html index e1b346a0ab..f81b2985e9 100644 --- a/master/Data.List.Relation.Binary.Prefix.Homogeneous.Properties.html +++ b/master/Data.List.Relation.Binary.Prefix.Homogeneous.Properties.html @@ -29,7 +29,7 @@ isPreorder : IsPreorder R S → IsPreorder (Pointwise R) (Prefix S) isPreorder po = record - { isEquivalence = Pointwise.isEquivalence PO.isEquivalence + { isEquivalence = Pointwise.isEquivalence PO.isEquivalence ; reflexive = fromPointwise ∘′ Pointwise.map PO.reflexive ; trans = trans PO.trans } where module PO = IsPreorder po diff --git a/master/Data.List.Relation.Binary.Sublist.DecSetoid.html b/master/Data.List.Relation.Binary.Sublist.DecSetoid.html index 70bbc94b31..d4fdc00dba 100644 --- a/master/Data.List.Relation.Binary.Sublist.DecSetoid.html +++ b/master/Data.List.Relation.Binary.Sublist.DecSetoid.html @@ -39,7 +39,7 @@ _⊆?_ : Decidable _⊆_ _⊆?_ = HeterogeneousProperties.sublist? _≟_ -⊆-isDecPartialOrder : IsDecPartialOrder _≋_ _⊆_ +⊆-isDecPartialOrder : IsDecPartialOrder _≋_ _⊆_ ⊆-isDecPartialOrder = record { isPartialOrder = ⊆-isPartialOrder ; _≟_ = _≋?_ diff --git a/master/Data.List.Relation.Binary.Sublist.Heterogeneous.Properties.html b/master/Data.List.Relation.Binary.Sublist.Heterogeneous.Properties.html index b67a37140f..3a0047a577 100644 --- a/master/Data.List.Relation.Binary.Sublist.Heterogeneous.Properties.html +++ b/master/Data.List.Relation.Binary.Sublist.Heterogeneous.Properties.html @@ -433,7 +433,7 @@ isPreorder : IsPreorder E R → IsPreorder (Pointwise E) (Sublist R) isPreorder ER-isPreorder = record - { isEquivalence = Pw.isEquivalence ER.isEquivalence + { isEquivalence = Pw.isEquivalence ER.isEquivalence ; reflexive = fromPointwise ∘ Pw.map ER.reflexive ; trans = trans ER.trans } where module ER = IsPreorder ER-isPreorder diff --git a/master/Data.List.Relation.Binary.Sublist.Setoid.Properties.html b/master/Data.List.Relation.Binary.Sublist.Setoid.Properties.html index 1fd98d55e3..67cbe06b50 100644 --- a/master/Data.List.Relation.Binary.Sublist.Setoid.Properties.html +++ b/master/Data.List.Relation.Binary.Sublist.Setoid.Properties.html @@ -36,7 +36,7 @@ import Data.List.Membership.Setoid as SetoidMembership open Setoid S using (_≈_; trans) renaming (Carrier to A; refl to ≈-refl) -open SetoidEquality S using (_≋_; ≋-refl) +open SetoidEquality S using (_≋_; ≋-refl) open SetoidSublist S hiding (map) open SetoidMembership S using (_∈_) @@ -124,10 +124,10 @@ module _ (P? : Decidable P) where takeWhile⊆filter : ∀ xs → takeWhile P? xs ⊆ filter P? xs - takeWhile⊆filter xs = HeteroProperties.takeWhile-filter P? {xs} ≋-refl + takeWhile⊆filter xs = HeteroProperties.takeWhile-filter P? {xs} ≋-refl filter⊆dropWhile : ∀ xs → filter P? xs ⊆ dropWhile (¬? ∘ P?) xs - filter⊆dropWhile xs = HeteroProperties.filter-dropWhile P? {xs} ≋-refl + filter⊆dropWhile xs = HeteroProperties.filter-dropWhile P? {xs} ≋-refl ------------------------------------------------------------------------ -- Various list functions are increasing wrt _⊆_ @@ -182,7 +182,7 @@ module _ where take⁺ : m ≤ n → take m xs ⊆ take n xs - take⁺ m≤n = HeteroProperties.take⁺ m≤n ≋-refl + take⁺ m≤n = HeteroProperties.take⁺ m≤n ≋-refl ------------------------------------------------------------------------ -- drop @@ -209,11 +209,11 @@ takeWhile⁺ : ∀ {xs} → (∀ {a b} → a ≈ b → P a → Q b) → takeWhile P? xs ⊆ takeWhile Q? xs - takeWhile⁺ {xs} P⇒Q = HeteroProperties.⊆-takeWhile-Sublist P? Q? {xs} P⇒Q ≋-refl + takeWhile⁺ {xs} P⇒Q = HeteroProperties.⊆-takeWhile-Sublist P? Q? {xs} P⇒Q ≋-refl dropWhile⁺ : ∀ {xs} → (∀ {a b} → a ≈ b → Q b → P a) → dropWhile P? xs ⊆ dropWhile Q? xs - dropWhile⁺ {xs} P⇒Q = HeteroProperties.⊇-dropWhile-Sublist P? Q? {xs} P⇒Q ≋-refl + dropWhile⁺ {xs} P⇒Q = HeteroProperties.⊇-dropWhile-Sublist P? Q? {xs} P⇒Q ≋-refl ------------------------------------------------------------------------ -- filter @@ -290,7 +290,7 @@ ------------------------------------------------------------------------ -- Conversion to and from list equality - to-≋ : length as ≡ length bs → as ⊆ bs → as ≋ bs + to-≋ : length as ≡ length bs → as ⊆ bs → as ≋ bs to-≋ = HeteroProperties.toPointwise ------------------------------------------------------------------------ diff --git a/master/Data.List.Relation.Binary.Sublist.Setoid.html b/master/Data.List.Relation.Binary.Sublist.Setoid.html index 71e64601fa..f3a3d2b399 100644 --- a/master/Data.List.Relation.Binary.Sublist.Setoid.html +++ b/master/Data.List.Relation.Binary.Sublist.Setoid.html @@ -48,7 +48,7 @@ xs ⊇ ys = ys ⊆ xs _⊂_ : Rel (List A) (c ⊔ ℓ) -xs ⊂ ys = xs ⊆ ys × ¬ (xs ≋ ys) +xs ⊂ ys = xs ⊆ ys × ¬ (xs ≋ ys) _⊃_ : Rel (List A) (c ⊔ ℓ) xs ⊃ ys = ys ⊂ xs @@ -87,7 +87,7 @@ ------------------------------------------------------------------------ -- Relational properties holding for Setoid case -⊆-reflexive : _≋_ ⇒ _⊆_ +⊆-reflexive : _≋_ ⇒ _⊆_ ⊆-reflexive = HeterogeneousProperties.fromPointwise open HeterogeneousProperties.Reflexivity {R = _≈_} refl public using () @@ -99,14 +99,14 @@ open HeterogeneousProperties.Antisymmetry {R = _≈_} {S = _≈_} (λ x≈y _ → x≈y) public using () renaming (antisym to ⊆-antisym) -- ⊆-antisym : Antisymmetric _≋_ _⊆_ -⊆-isPreorder : IsPreorder _≋_ _⊆_ +⊆-isPreorder : IsPreorder _≋_ _⊆_ ⊆-isPreorder = record - { isEquivalence = ≋-isEquivalence + { isEquivalence = ≋-isEquivalence ; reflexive = ⊆-reflexive ; trans = ⊆-trans } -⊆-isPartialOrder : IsPartialOrder _≋_ _⊆_ +⊆-isPartialOrder : IsPartialOrder _≋_ _⊆_ ⊆-isPartialOrder = record { isPreorder = ⊆-isPreorder ; antisym = ⊆-antisym diff --git a/master/Data.List.Relation.Binary.Subset.Setoid.Properties.html b/master/Data.List.Relation.Binary.Subset.Setoid.Properties.html index e56758508f..28fa2fa9cc 100644 --- a/master/Data.List.Relation.Binary.Subset.Setoid.Properties.html +++ b/master/Data.List.Relation.Binary.Subset.Setoid.Properties.html @@ -53,7 +53,7 @@ open Membership S open Membershipₚ - ⊆-reflexive : _≋_ ⇒ _⊆_ + ⊆-reflexive : _≋_ ⇒ _⊆_ ⊆-reflexive xs≋ys = ∈-resp-≋ S xs≋ys ⊆-refl : Reflexive _⊆_ @@ -62,15 +62,15 @@ ⊆-trans : Transitive _⊆_ ⊆-trans xs⊆ys ys⊆zs x∈xs = ys⊆zs (xs⊆ys x∈xs) - ⊆-respʳ-≋ : _⊆_ Respectsʳ _≋_ + ⊆-respʳ-≋ : _⊆_ Respectsʳ _≋_ ⊆-respʳ-≋ xs≋ys = ∈-resp-≋ S xs≋ys ∘_ - ⊆-respˡ-≋ : _⊆_ Respectsˡ _≋_ - ⊆-respˡ-≋ xs≋ys = _∘ ∈-resp-≋ S (≋-sym xs≋ys) + ⊆-respˡ-≋ : _⊆_ Respectsˡ _≋_ + ⊆-respˡ-≋ xs≋ys = _∘ ∈-resp-≋ S (≋-sym xs≋ys) - ⊆-isPreorder : IsPreorder _≋_ _⊆_ + ⊆-isPreorder : IsPreorder _≋_ _⊆_ ⊆-isPreorder = record - { isEquivalence = ≋-isEquivalence + { isEquivalence = ≋-isEquivalence ; reflexive = ⊆-reflexive ; trans = ⊆-trans } diff --git a/master/Data.List.Relation.Binary.Suffix.Heterogeneous.Properties.html b/master/Data.List.Relation.Binary.Suffix.Heterogeneous.Properties.html index fb148c5e03..382618ad09 100644 --- a/master/Data.List.Relation.Binary.Suffix.Heterogeneous.Properties.html +++ b/master/Data.List.Relation.Binary.Suffix.Heterogeneous.Properties.html @@ -13,7 +13,7 @@ open import Data.List.Base as List using (List; []; _∷_; _++_; length; filter; replicate; reverse; reverseAcc) open import Data.List.Relation.Binary.Pointwise as Pw - using (Pointwise; []; _∷_; Pointwise-length) + using (Pointwise; []; _∷_; Pointwise-length) open import Data.List.Relation.Binary.Suffix.Heterogeneous as Suffix using (Suffix; here; there; tail) open import Data.List.Relation.Binary.Prefix.Heterogeneous as Prefix @@ -44,7 +44,7 @@ fromPrefix {as} {bs} p with Prefix._++_ {cs} rs ds ← Prefix.toView p = subst (Suffix R (reverse as)) (sym (List.reverse-++ cs ds)) - (Suffix.fromView (reverse ds Suffix.++ Pw.reverse⁺ rs)) + (Suffix.fromView (reverse ds Suffix.++ Pw.reverse⁺ rs)) fromPrefix-rev : ∀ {as bs} → Prefix R (reverse as) (reverse bs) → Suffix R as bs @@ -59,7 +59,7 @@ toPrefix-rev {as} {bs} s with Suffix._++_ cs {ds} rs ← Suffix.toView s = subst (Prefix R (reverse as)) (sym (List.reverse-++ cs ds)) - (Prefix.fromView (Pw.reverse⁺ rs Prefix.++ reverse cs)) + (Prefix.fromView (Pw.reverse⁺ rs Prefix.++ reverse cs)) toPrefix : ∀ {as bs} → Suffix R (reverse as) (reverse bs) → Prefix R as bs @@ -75,7 +75,7 @@ module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where length-mono : ∀ {as bs} → Suffix R as bs → length as ≤ length bs - length-mono (here rs) = ≤-reflexive (Pointwise-length rs) + length-mono (here rs) = ≤-reflexive (Pointwise-length rs) length-mono (there suf) = m≤n⇒m≤1+n (length-mono suf) S[as][bs]⇒∣as∣≢1+∣bs∣ : ∀ {as bs} → Suffix R as bs → @@ -123,7 +123,7 @@ ++⁺ : ∀ {as bs cs ds} → Suffix R as bs → Pointwise R cs ds → Suffix R (as ++ cs) (bs ++ ds) - ++⁺ (here rs) rs′ = here (Pw.++⁺ rs rs′) + ++⁺ (here rs) rs′ = here (Pw.++⁺ rs rs′) ++⁺ (there suf) rs′ = there (++⁺ suf rs′) ++⁻ : ∀ {as bs cs ds} → length cs ≡ length ds → @@ -139,7 +139,7 @@ length ds ≤⟨ m≤n+m (length ds) (length bs) ⟩ length bs + length ds <⟨ ≤-refl ⟩ suc (length bs + length ds) ≡⟨ sym $ List.length-++ (b ∷ bs) ⟩ - length (b ∷ bs ++ ds) ≡⟨ sym $ Pointwise-length rs ⟩ + length (b ∷ bs ++ ds) ≡⟨ sym $ Pointwise-length rs ⟩ length cs ∎ ------------------------------------------------------------------------ @@ -151,13 +151,13 @@ map⁺ : ∀ {as bs} (f : A → C) (g : B → D) → Suffix (λ a b → R (f a) (g b)) as bs → Suffix R (List.map f as) (List.map g bs) - map⁺ f g (here rs) = here (Pw.map⁺ f g rs) + map⁺ f g (here rs) = here (Pw.map⁺ f g rs) map⁺ f g (there suf) = there (map⁺ f g suf) map⁻ : ∀ {as bs} (f : A → C) (g : B → D) → Suffix R (List.map f as) (List.map g bs) → Suffix (λ a b → R (f a) (g b)) as bs - map⁻ {as} {b ∷ bs} f g (here rs) = here (Pw.map⁻ f g rs) + map⁻ {as} {b ∷ bs} f g (here rs) = here (Pw.map⁻ f g rs) map⁻ {as} {b ∷ bs} f g (there suf) = there (map⁻ f g suf) map⁻ {x ∷ as} {[]} f g suf = contradiction (length-mono suf) λ() map⁻ {[]} {[]} f g suf = here [] @@ -174,7 +174,7 @@ filter⁺ : ∀ {as bs} → Suffix R as bs → Suffix R (filter P? as) (filter Q? bs) - filter⁺ (here rs) = here (Pw.filter⁺ P? Q? P⇒Q Q⇒P rs) + filter⁺ (here rs) = here (Pw.filter⁺ P? Q? P⇒Q Q⇒P rs) filter⁺ (there {a} suf) with does (Q? a) ... | true = there (filter⁺ suf) ... | false = filter⁺ suf @@ -189,7 +189,7 @@ replicate⁺ {a = a} {b = b} m≤n r = repl (≤⇒≤′ m≤n) where repl : ∀ {m n} → m ≤′ n → Suffix R (replicate m a) (replicate n b) - repl ≤′-refl = here (Pw.replicate⁺ r _) + repl ≤′-refl = here (Pw.replicate⁺ r _) repl (≤′-step m≤n) = there (repl m≤n) ------------------------------------------------------------------------ @@ -199,8 +199,8 @@ irrelevant : Irrelevant R → Irrelevant (Suffix R) irrelevant irr (here rs) (here rs₁) = cong here $ Pw.irrelevant irr rs rs₁ - irrelevant irr (here rs) (there rsuf) = contradiction (Pointwise-length rs) (S[as][bs]⇒∣as∣≢1+∣bs∣ rsuf) - irrelevant irr (there rsuf) (here rs) = contradiction (Pointwise-length rs) (S[as][bs]⇒∣as∣≢1+∣bs∣ rsuf) + irrelevant irr (here rs) (there rsuf) = contradiction (Pointwise-length rs) (S[as][bs]⇒∣as∣≢1+∣bs∣ rsuf) + irrelevant irr (there rsuf) (here rs) = contradiction (Pointwise-length rs) (S[as][bs]⇒∣as∣≢1+∣bs∣ rsuf) irrelevant irr (there rsuf) (there rsuf₁) = cong there $ irrelevant irr rsuf rsuf₁ ------------------------------------------------------------------------ diff --git a/master/Data.List.Relation.Binary.Suffix.Homogeneous.Properties.html b/master/Data.List.Relation.Binary.Suffix.Homogeneous.Properties.html index e7c86d8800..51c2bf38bb 100644 --- a/master/Data.List.Relation.Binary.Suffix.Homogeneous.Properties.html +++ b/master/Data.List.Relation.Binary.Suffix.Homogeneous.Properties.html @@ -29,7 +29,7 @@ isPreorder : IsPreorder R S → IsPreorder (Pointwise R) (Suffix S) isPreorder po = record - { isEquivalence = Pointwise.isEquivalence PO.isEquivalence + { isEquivalence = Pointwise.isEquivalence PO.isEquivalence ; reflexive = fromPointwise ∘′ Pointwise.map PO.reflexive ; trans = trans PO.trans } where module PO = IsPreorder po diff --git a/master/Data.List.Relation.Ternary.Appending.Propositional.Properties.html b/master/Data.List.Relation.Ternary.Appending.Propositional.Properties.html index c5c364e42f..2974b8c320 100644 --- a/master/Data.List.Relation.Ternary.Appending.Propositional.Properties.html +++ b/master/Data.List.Relation.Ternary.Appending.Propositional.Properties.html @@ -10,8 +10,8 @@ module Data.List.Relation.Ternary.Appending.Propositional.Properties {a} {A : Set a} where open import Data.List.Base as List using (List; []) -import Data.List.Relation.Binary.Pointwise as Pw using (Pointwise-≡⇒≡) -open import Data.List.Relation.Binary.Equality.Propositional using (_≋_) +import Data.List.Relation.Binary.Pointwise as Pw using (Pointwise-≡⇒≡) +open import Data.List.Relation.Binary.Equality.Propositional using (_≋_) open import Data.List.Relation.Ternary.Appending.Propositional {A = A} open import Function.Base using (_∘′_) open import Relation.Binary.PropositionalEquality.Core using (_≡_) @@ -34,8 +34,8 @@ -- Prove propositional-specific ones []++⁻¹ : Appending [] bs cs → bs ≡ cs -[]++⁻¹ = Pw.Pointwise-≡⇒≡ ∘′ Appending.[]++⁻¹ +[]++⁻¹ = Pw.Pointwise-≡⇒≡ ∘′ Appending.[]++⁻¹ ++[]⁻¹ : Appending as [] cs → as ≡ cs -++[]⁻¹ = Pw.Pointwise-≡⇒≡ ∘′ Appending.++[]⁻¹ +++[]⁻¹ = Pw.Pointwise-≡⇒≡ ∘′ Appending.++[]⁻¹ \ No newline at end of file diff --git a/master/Data.List.Relation.Ternary.Appending.Propositional.html b/master/Data.List.Relation.Ternary.Appending.Propositional.html index c49d32f041..f1b4e0be41 100644 --- a/master/Data.List.Relation.Ternary.Appending.Propositional.html +++ b/master/Data.List.Relation.Ternary.Appending.Propositional.html @@ -15,7 +15,7 @@ open import Data.Product.Base using (_,_) import Data.List.Properties as List -import Data.List.Relation.Binary.Pointwise as Pw using (≡⇒Pointwise-≡; Pointwise-≡⇒≡) +import Data.List.Relation.Binary.Pointwise as Pw using (≡⇒Pointwise-≡; Pointwise-≡⇒≡) open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; trans; cong₂) open import Relation.Binary.PropositionalEquality.Properties @@ -37,14 +37,14 @@ infixr 5 _++_ _++[] _++_ : (as bs : List A) → Appending as bs (as List.++ bs) -as ++ bs = Pw.≡⇒Pointwise-≡ refl General.++ Pw.≡⇒Pointwise-≡ refl +as ++ bs = Pw.≡⇒Pointwise-≡ refl General.++ Pw.≡⇒Pointwise-≡ refl _++[] : (as : List A) → Appending as [] as -as ++[] = Appending.respʳ-≋ (as ++ []) (Pw.≡⇒Pointwise-≡ (List.++-identityʳ as)) +as ++[] = Appending.respʳ-≋ (as ++ []) (Pw.≡⇒Pointwise-≡ (List.++-identityʳ as)) break : ∀ {as bs cs} → Appending as bs cs → as List.++ bs ≡ cs break {as} {bs} {cs} lrs = let (cs₁ , cs₂ , eq , acs , bcs) = General.break lrs in begin - as List.++ bs ≡⟨ cong₂ List._++_ (Pw.Pointwise-≡⇒≡ acs) (Pw.Pointwise-≡⇒≡ bcs) ⟩ + as List.++ bs ≡⟨ cong₂ List._++_ (Pw.Pointwise-≡⇒≡ acs) (Pw.Pointwise-≡⇒≡ bcs) ⟩ cs₁ List.++ cs₂ ≡⟨ eq ⟩ cs ∎ where open ≡-Reasoning \ No newline at end of file diff --git a/master/Data.List.Relation.Ternary.Interleaving.Setoid.Properties.html b/master/Data.List.Relation.Ternary.Interleaving.Setoid.Properties.html index f9008aa579..7ea47dda03 100644 --- a/master/Data.List.Relation.Ternary.Interleaving.Setoid.Properties.html +++ b/master/Data.List.Relation.Ternary.Interleaving.Setoid.Properties.html @@ -19,7 +19,7 @@ open import Relation.Nullary.Decidable using (¬?) open import Function.Base using (_∘_) -open import Data.List.Relation.Binary.Equality.Setoid S using (≋-refl) +open import Data.List.Relation.Binary.Equality.Setoid S using (≋-refl) open import Data.List.Relation.Ternary.Interleaving.Setoid S open Setoid S renaming (Carrier to A) @@ -32,7 +32,7 @@ -- _++_ ++-linear : (xs ys : List A) → Interleaving xs ys (xs ++ ys) -++-linear xs ys = ++-disjoint (left ≋-refl) (right ≋-refl) +++-linear xs ys = ++-disjoint (left ≋-refl) (right ≋-refl) ------------------------------------------------------------------------ -- filter diff --git a/master/Data.List.Relation.Unary.All.Properties.html b/master/Data.List.Relation.Unary.All.Properties.html index 7d8240c664..4b28ff4f03 100644 --- a/master/Data.List.Relation.Unary.All.Properties.html +++ b/master/Data.List.Relation.Unary.All.Properties.html @@ -746,7 +746,7 @@ open Setoid S open ≋ S - respects : P B.Respects _≈_ → (All P) B.Respects _≋_ + respects : P B.Respects _≈_ → (All P) B.Respects _≋_ respects p≈ [] [] = [] respects p≈ (x≈y ∷ xs≈ys) (px ∷ pxs) = p≈ x≈y px ∷ respects p≈ xs≈ys pxs diff --git a/master/Data.String.Properties.html b/master/Data.String.Properties.html index 3e84db5597..14176aee90 100644 --- a/master/Data.String.Properties.html +++ b/master/Data.String.Properties.html @@ -40,10 +40,10 @@ ≈⇒≡ : _≈_ ⇒ _≡_ ≈⇒≡ = toList-injective _ _ - ∘ Pointwise.Pointwise-≡⇒≡ + ∘ Pointwise.Pointwise-≡⇒≡ ≈-reflexive : _≡_ ⇒ _≈_ -≈-reflexive = Pointwise.≡⇒Pointwise-≡ +≈-reflexive = Pointwise.≡⇒Pointwise-≡ ∘ cong toList ≈-refl : Reflexive _≈_ diff --git a/master/Data.Trie.NonEmpty.html b/master/Data.Trie.NonEmpty.html index 9e310e6c29..f8a6c2e17f 100644 --- a/master/Data.Trie.NonEmpty.html +++ b/master/Data.Trie.NonEmpty.html @@ -29,7 +29,7 @@ open import Data.List.Relation.Binary.Equality.Setoid Eq.setoid open import Data.Tree.AVL.Value hiding (Value) -open import Data.Tree.AVL.Value ≋-setoid using (Value) +open import Data.Tree.AVL.Value ≋-setoid using (Value) open import Data.Tree.AVL.NonEmpty S as Tree⁺ using (Tree⁺) open Value @@ -46,7 +46,7 @@ eat : ∀ {v} → Value v → Word → Value v family (eat V ks) = family V ∘′ (ks ++_) -respects (eat V ks) = respects V ∘′ ++⁺ ≋-refl +respects (eat V ks) = respects V ∘′ ++⁺ ≋-refl data Trie⁺ {v} (V : Value v) : Size → Set (v ⊔ k ⊔ e ⊔ r) Tries⁺ : ∀ {v} (V : Value v) (i : Size) → Set (v ⊔ k ⊔ e ⊔ r) @@ -59,7 +59,7 @@ node : ∀ {i} → These (family V []) (Tries⁺ V i) → Trie⁺ V (↑ i) Tries⁺ V j = Tree⁺ $ MkValue (λ k → Trie⁺ (eat V (k ∷ [])) j) - $ λ eq → map _ _ (respects V (eq ∷ ≋-refl)) + $ λ eq → map _ _ (respects V (eq ∷ ≋-refl)) map V W f (node t) = node $ These.map f (Tree⁺.map (map _ _ f)) t diff --git a/master/Data.Trie.html b/master/Data.Trie.html index 966daff154..3807f8ced9 100644 --- a/master/Data.Trie.html +++ b/master/Data.Trie.html @@ -30,7 +30,7 @@ renaming (Carrier to Key) open import Data.List.Relation.Binary.Equality.Setoid Eq.setoid -open import Data.Tree.AVL.Value ≋-setoid using (Value) +open import Data.Tree.AVL.Value ≋-setoid using (Value) ------------------------------------------------------------------------ -- Definition diff --git a/master/README.Data.List.Relation.Binary.Equality.html b/master/README.Data.List.Relation.Binary.Equality.html index b8c2cc0762..711c1468a6 100644 --- a/master/README.Data.List.Relation.Binary.Equality.html +++ b/master/README.Data.List.Relation.Binary.Equality.html @@ -93,7 +93,7 @@ -- new equality relation over lists. The type of `lem₃` can therefore -- be rewritten as: -lem₄ : (λ x → x + 1) ∷ [] ≋ (λ x → x + 2 ∸ 1) ∷ [] +lem₄ : (λ x → x + 1) ∷ [] ≋ (λ x → x + 2 ∸ 1) ∷ [] lem₄ = 2x+2≗2[x+1] ∷ [] where 2x+2≗2[x+1] : (λ x → x + 1) ≗ (λ x → x + 2 ∸ 1) @@ -103,8 +103,8 @@ -- setoid in its own right and therefore is reflexive, symmetric, -- transitive: -lem₅ : (λ x → 2 * x + 2) ∷ [] ≋ (λ x → 2 * x + 2) ∷ [] -lem₅ = ≋-refl +lem₅ : (λ x → 2 * x + 2) ∷ [] ≋ (λ x → 2 * x + 2) ∷ [] +lem₅ = ≋-refl -- If we could prove that `_≗_` forms a `DecSetoid` then we could use -- the module `DecSetoidEq` instead. This exports everything from diff --git a/master/README.Data.List.Relation.Binary.Pointwise.html b/master/README.Data.List.Relation.Binary.Pointwise.html index 6524e701b7..15ed2515b5 100644 --- a/master/README.Data.List.Relation.Binary.Pointwise.html +++ b/master/README.Data.List.Relation.Binary.Pointwise.html @@ -50,5 +50,5 @@ -- also included in the module: lem₃ : ∀ {xs ys} → Pointwise _<_ xs ys → length xs ≡ length ys -lem₃ = Pointwise-length +lem₃ = Pointwise-length \ No newline at end of file diff --git a/master/README.Text.Regex.html b/master/README.Text.Regex.html index ce8ee80517..d99208a966 100644 --- a/master/README.Text.Regex.html +++ b/master/README.Text.Regex.html @@ -150,7 +150,7 @@ open import Data.List.Relation.Binary.Infix.Heterogeneous open import Data.List.Relation.Binary.Infix.Heterogeneous.Properties -open import Data.List.Relation.Binary.Pointwise using (≡⇒Pointwise-≡) +open import Data.List.Relation.Binary.Pointwise using (≡⇒Pointwise-≡) open import Relation.Binary.PropositionalEquality -- Here is an example of a match: it gives back the substring, the inductive @@ -167,7 +167,7 @@ proof : Infix _≡_ (toList "agda") (toList "Maria Magdalena") proof = toList "Maria M" - ++ⁱ fromPointwise (≡⇒Pointwise-≡ refl) + ++ⁱ fromPointwise (≡⇒Pointwise-≡ refl) ⁱ++ toList "lena" diff --git a/master/Text.Regex.Derivative.Brzozowski.html b/master/Text.Regex.Derivative.Brzozowski.html index d8a13ca6d4..768ada26e8 100644 --- a/master/Text.Regex.Derivative.Brzozowski.html +++ b/master/Text.Regex.Derivative.Brzozowski.html @@ -72,10 +72,10 @@ ... | prod eq p q = star (sum (inj₂ (prod (refl ∷ eq) (eat-sound x e p) (⋆-sound e q)))) -eat-complete′ : ∀ x {xs w} e → w ≋ (x ∷ xs) → w ∈ e → xs ∈ eat x e +eat-complete′ : ∀ x {xs w} e → w ≋ (x ∷ xs) → w ∈ e → xs ∈ eat x e eat-complete : ∀ x {xs} e → (x ∷ xs) ∈ e → xs ∈ eat x e -eat-complete x e = eat-complete′ x e ≋-refl +eat-complete x e = eat-complete′ x e ≋-refl eat-complete′ x [ rs ] (refl ∷ []) [ p ] with (x ∷ []) ∈?[ rs ] @@ -95,12 +95,12 @@ = ∙-complete (eat x e) f (prod (respʳ-≋ app eq) (eat-complete x e p) q) eat-complete′ x (e R.∙ f) eq (prod ([]++ eq′) p q) | yes []∈e = ∣-complete (eat x e ∙ f) (eat x f) $ sum $ inj₂ - $ eat-complete′ x f (≋-trans eq′ eq) q + $ eat-complete′ x f (≋-trans eq′ eq) q eat-complete′ x (e R.∙ f) (refl ∷ eq) (prod (refl ∷ app) p q) | yes []∈e = ∣-complete (eat x e ∙ f) (eat x f) $ sum $ inj₁ $ ∙-complete (eat x e) f (prod (respʳ-≋ app eq) (eat-complete x e p) q) eat-complete′ x (e R.⋆) eq (star (sum (inj₂ (prod ([]++ app) p q)))) - = eat-complete′ x (e R.⋆) (≋-trans app eq) q + = eat-complete′ x (e R.⋆) (≋-trans app eq) q eat-complete′ x (e R.⋆) (refl ∷ eq) (star (sum (inj₂ (prod (refl ∷ app) p q)))) = ∙-complete (eat x e) (e ⋆) $ prod (respʳ-≋ app eq) (eat-complete x e p) $ ⋆-complete e q diff --git a/master/Text.Regex.Search.html b/master/Text.Regex.Search.html index 5effd2d2c8..8ecbca7bd3 100644 --- a/master/Text.Regex.Search.html +++ b/master/Text.Regex.Search.html @@ -170,7 +170,7 @@ whole xs e p = mkMatch xs p (Pointwise.refl refl) whole⁻¹ : ∀ xs e → Match (Pointwise _≡_) xs e → xs ∈ e - whole⁻¹ xs e (mkMatch ys ys∈e p) with Pointwise.Pointwise-≡⇒≡ p + whole⁻¹ xs e (mkMatch ys ys∈e p) with Pointwise.Pointwise-≡⇒≡ p whole⁻¹ xs e (mkMatch .xs xs∈e p) | refl = xs∈e search : Decidable (Match (Pointwise _≡_))