From e32aee54893301a285747423f459a7c8f8615fa4 Mon Sep 17 00:00:00 2001 From: Guillaume Allais Date: Tue, 3 May 2022 20:47:24 +0100 Subject: [PATCH] [ fix #1354 ] Refactoring Permutation.Propositional --- .../List/Relation/Binary/Permutation.agda | 2 - .../Relation/Binary/BagAndSetEquality.agda | 26 ++-- .../Binary/Permutation/Homogeneous.agda | 58 ++++---- .../Binary/Permutation/Propositional.agda | 41 +++--- .../Permutation/Propositional/Properties.agda | 127 ++++++++++-------- .../Relation/Binary/Permutation/Setoid.agda | 39 +++--- .../Binary/Permutation/Setoid/Properties.agda | 45 +++++-- .../Subset/Propositional/Properties.agda | 9 +- 8 files changed, 185 insertions(+), 162 deletions(-) diff --git a/doc/README/Data/List/Relation/Binary/Permutation.agda b/doc/README/Data/List/Relation/Binary/Permutation.agda index e9141d89c7..9e702de285 100644 --- a/doc/README/Data/List/Relation/Binary/Permutation.agda +++ b/doc/README/Data/List/Relation/Binary/Permutation.agda @@ -9,8 +9,6 @@ module README.Data.List.Relation.Binary.Permutation where open import Algebra.Structures using (IsCommutativeMonoid) open import Data.List.Base open import Data.Nat using (ℕ; _+_) -open import Relation.Binary.PropositionalEquality - using (_≡_; refl; sym; cong; setoid) ------------------------------------------------------------------------ -- Permutations diff --git a/src/Data/List/Relation/Binary/BagAndSetEquality.agda b/src/Data/List/Relation/Binary/BagAndSetEquality.agda index 389721d4c5..6aa3f673f3 100644 --- a/src/Data/List/Relation/Binary/BagAndSetEquality.agda +++ b/src/Data/List/Relation/Binary/BagAndSetEquality.agda @@ -23,6 +23,7 @@ open import Data.List.Membership.Propositional.Properties open import Data.List.Relation.Binary.Subset.Propositional.Properties using (⊆-preorder) open import Data.List.Relation.Binary.Permutation.Propositional + using (_↭_; ↭-refl; ↭-sym; module PermutationReasoning) open import Data.List.Relation.Binary.Permutation.Propositional.Properties open import Data.Product.Base as Prod hiding (map) import Data.Product.Function.Dependent.Propositional as Σ @@ -54,6 +55,7 @@ private x y : A ws xs ys zs : List A + ------------------------------------------------------------------------ -- Definitions @@ -142,8 +144,8 @@ module _ {k} {f g : A → B} {xs ys} where helper y = mk↔ₛ′ (λ x≡fy → ≡.trans x≡fy ( f≗g y)) (λ x≡gy → ≡.trans x≡gy (≡.sym $ f≗g y)) - (λ { ≡.refl → ≡.trans-symˡ (f≗g y) }) - λ { ≡.refl → ≡.trans-symʳ (f≗g y) } + (λ { refl → ≡.trans-symˡ (f≗g y) }) + λ { refl → ≡.trans-symʳ (f≗g y) } ------------------------------------------------------------------------ -- _++_ @@ -282,7 +284,6 @@ empty-unique {xs = _ ∷ _} ∷∼[] with ⇒→ ∷∼[] (here refl) MP.right-distributive xs₁ xs₂ (pure ∘ f)) ⟩ (fs >>= λ f → (xs₁ >>= pure ∘ f) ++ (xs₂ >>= pure ∘ f)) ≈⟨ >>=-left-distributive fs ⟩ - (fs >>= λ f → xs₁ >>= pure ∘ f) ++ (fs >>= λ f → xs₂ >>= pure ∘ f) ≡⟨ ≡.cong₂ _++_ (Applicative.unfold-⊛ fs xs₁) (Applicative.unfold-⊛ fs xs₂) ⟨ @@ -296,7 +297,8 @@ private ¬-drop-cons : ∀ {x : A} → ¬ (∀ {xs ys} → x ∷ xs ∼[ set ] x ∷ ys → xs ∼[ set ] ys) - ¬-drop-cons {x = x} drop-cons with Equivalence.to x∼[] (here refl) + ¬-drop-cons {x = x} drop-cons + with Equivalence.to x∼[] (here refl) where x,x≈x : (x ∷ x ∷ []) ∼[ set ] [ x ] x,x≈x = ++-idempotent [ x ] @@ -357,7 +359,7 @@ drop-cons {x = x} {xs} {ys} x∷xs≈x∷ys = (∃ λ z → z ∈ xs) ↔⟨ Σ.cong K-refl (∈-index xs) ⟩ (∃ λ z → ∃ λ i → z ≡ lookup xs i) ↔⟨ ∃∃↔∃∃ _ ⟩ (∃ λ i → ∃ λ z → z ≡ lookup xs i) ↔⟨ Σ.cong K-refl (mk↔ₛ′ _ (λ _ → _ , refl) (λ _ → refl) (λ { (_ , refl) → refl })) ⟩ - (Fin (length xs) × ⊤) ↔⟨ ×-identityʳ _ _ ⟩ + (Fin (length xs) × ⊤) ↔⟨ ×-identityʳ _ _ ⟩ Fin (length xs) ∎ where open Related.EquationalReasoning @@ -571,15 +573,7 @@ drop-cons {x = x} {xs} {ys} x∷xs≈x∷ys = from xs↭ys = Any-resp-↭ (↭-sym xs↭ys) from∘to : ∀ {xs ys} (p : xs ↭ ys) (q : v ∈ xs) → from p (to p q) ≡ q - from∘to refl v∈xs = refl - from∘to (prep _ _) (here refl) = refl - from∘to (prep _ p) (there v∈xs) = ≡.cong there (from∘to p v∈xs) - from∘to (swap x y p) (here refl) = refl - from∘to (swap x y p) (there (here refl)) = refl - from∘to (swap x y p) (there (there v∈xs)) = ≡.cong (there ∘ there) (from∘to p v∈xs) - from∘to (trans p₁ p₂) v∈xs - rewrite from∘to p₂ (Any-resp-↭ p₁ v∈xs) - | from∘to p₁ v∈xs = refl + from∘to = Any-resp-[σ⁻¹∘σ] to∘from : ∀ {xs ys} (p : xs ↭ ys) (q : v ∈ ys) → to p (from p q) ≡ q to∘from p with from∘to (↭-sym p) @@ -587,8 +581,8 @@ drop-cons {x = x} {xs} {ys} x∷xs≈x∷ys = ∼bag⇒↭ : _∼[ bag ]_ ⇒ _↭_ {A = A} ∼bag⇒↭ {A = A} {[]} eq with empty-unique (↔-sym eq) -... | refl = refl -∼bag⇒↭ {A = A} {x ∷ xs} eq with ∈-∃++ (Inverse.to (eq {x}) (here ≡.refl)) +... | refl = ↭-refl +∼bag⇒↭ {A = A} {x ∷ xs} eq with ∈-∃++ (Inverse.to (eq {x}) (here refl)) ... | zs₁ , zs₂ , p rewrite p = begin x ∷ xs <⟨ ∼bag⇒↭ (drop-cons (↔-trans eq (comm zs₁ (x ∷ zs₂)))) ⟩ x ∷ (zs₂ ++ zs₁) <⟨ ++-comm zs₂ zs₁ ⟩ diff --git a/src/Data/List/Relation/Binary/Permutation/Homogeneous.agda b/src/Data/List/Relation/Binary/Permutation/Homogeneous.agda index 12015b3076..77583c730c 100644 --- a/src/Data/List/Relation/Binary/Permutation/Homogeneous.agda +++ b/src/Data/List/Relation/Binary/Permutation/Homogeneous.agda @@ -9,10 +9,6 @@ module Data.List.Relation.Binary.Permutation.Homogeneous where open import Data.List.Base using (List; _∷_) -open import Data.List.Relation.Binary.Pointwise.Base as Pointwise - using (Pointwise) -open import Data.List.Relation.Binary.Pointwise.Properties as Pointwise - using (symmetric) open import Level using (Level; _⊔_) open import Relation.Binary.Core using (Rel; _⇒_) open import Relation.Binary.Bundles using (Setoid) @@ -21,41 +17,45 @@ open import Relation.Binary.Definitions using (Reflexive; Symmetric) private variable - a r s : Level + a pr r ps s : Level A : Set a -data Permutation {A : Set a} (R : Rel A r) : Rel (List A) (a ⊔ r) where - refl : ∀ {xs ys} → Pointwise R xs ys → Permutation R xs ys - prep : ∀ {xs ys x y} (eq : R x y) → Permutation R xs ys → Permutation R (x ∷ xs) (y ∷ ys) - swap : ∀ {xs ys x y x′ y′} (eq₁ : R x x′) (eq₂ : R y y′) → Permutation R xs ys → Permutation R (x ∷ y ∷ xs) (y′ ∷ x′ ∷ ys) - trans : ∀ {xs ys zs} → Permutation R xs ys → Permutation R ys zs → Permutation R xs zs +-- PR is morally the pointwise lifting of R to lists but it need not be intensionally +data Permutation {A : Set a} (PR : Rel (List A) pr) (R : Rel A r) : Rel (List A) (a ⊔ pr ⊔ r) where + refl : ∀ {xs ys} → PR xs ys → Permutation PR R xs ys + prep : ∀ {xs ys x y} (eq : R x y) → Permutation PR R xs ys → Permutation PR R (x ∷ xs) (y ∷ ys) + swap : ∀ {xs ys x y x′ y′} (eq₁ : R x x′) (eq₂ : R y y′) → Permutation PR R xs ys → Permutation PR R (x ∷ y ∷ xs) (y′ ∷ x′ ∷ ys) + trans : ∀ {xs ys zs} → Permutation PR R xs ys → Permutation PR R ys zs → Permutation PR R xs zs ------------------------------------------------------------------------ -- The Permutation relation is an equivalence -module _ {R : Rel A r} where +module _ {PR : Rel (List A) pr} {R : Rel A r} where - sym : Symmetric R → Symmetric (Permutation R) - sym R-sym (refl xs∼ys) = refl (Pointwise.symmetric R-sym xs∼ys) - sym R-sym (prep x∼x′ xs↭ys) = prep (R-sym x∼x′) (sym R-sym xs↭ys) - sym R-sym (swap x∼x′ y∼y′ xs↭ys) = swap (R-sym y∼y′) (R-sym x∼x′) (sym R-sym xs↭ys) - sym R-sym (trans xs↭ys ys↭zs) = trans (sym R-sym ys↭zs) (sym R-sym xs↭ys) + sym : Symmetric PR → Symmetric R → Symmetric (Permutation PR R) + sym PR-sym R-sym (refl xs∼ys) = refl (PR-sym xs∼ys) + sym PR-sym R-sym (prep x∼x′ xs↭ys) = prep (R-sym x∼x′) (sym PR-sym R-sym xs↭ys) + sym PR-sym R-sym (swap x∼x′ y∼y′ xs↭ys) = swap (R-sym y∼y′) (R-sym x∼x′) (sym PR-sym R-sym xs↭ys) + sym PR-sym R-sym (trans xs↭ys ys↭zs) = trans (sym PR-sym R-sym ys↭zs) (sym PR-sym R-sym xs↭ys) - isEquivalence : Reflexive R → Symmetric R → IsEquivalence (Permutation R) - isEquivalence R-refl R-sym = record - { refl = refl (Pointwise.refl R-refl) - ; sym = sym R-sym + isEquivalence : Reflexive PR → + Symmetric PR → Symmetric R → + IsEquivalence (Permutation PR R) + isEquivalence PR-refl PR-sym R-sym = record + { refl = refl PR-refl + ; sym = sym PR-sym R-sym ; trans = trans } - setoid : Reflexive R → Symmetric R → Setoid _ _ - setoid R-refl R-sym = record - { isEquivalence = isEquivalence R-refl R-sym + setoid : Reflexive PR → Symmetric PR → Symmetric R → Setoid _ _ + setoid PR-refl PR-sym R-sym = record + { isEquivalence = isEquivalence PR-refl PR-sym R-sym } -map : ∀ {R : Rel A r} {S : Rel A s} → - (R ⇒ S) → (Permutation R ⇒ Permutation S) -map R⇒S (refl xs∼ys) = refl (Pointwise.map R⇒S xs∼ys) -map R⇒S (prep e xs∼ys) = prep (R⇒S e) (map R⇒S xs∼ys) -map R⇒S (swap e₁ e₂ xs∼ys) = swap (R⇒S e₁) (R⇒S e₂) (map R⇒S xs∼ys) -map R⇒S (trans xs∼ys ys∼zs) = trans (map R⇒S xs∼ys) (map R⇒S ys∼zs) +map : ∀ {PR : Rel (List A) pr} {PS : Rel (List A) ps} → + {R : Rel A r} {S : Rel A s} → + (PR ⇒ PS) → (R ⇒ S) → (Permutation PR R ⇒ Permutation PS S) +map PR⇒PS R⇒S (refl xs∼ys) = refl (PR⇒PS xs∼ys) +map PR⇒PS R⇒S (prep e xs∼ys) = prep (R⇒S e) (map PR⇒PS R⇒S xs∼ys) +map PR⇒PS R⇒S (swap e₁ e₂ xs∼ys) = swap (R⇒S e₁) (R⇒S e₂) (map PR⇒PS R⇒S xs∼ys) +map PR⇒PS R⇒S (trans xs∼ys ys∼zs) = trans (map PR⇒PS R⇒S xs∼ys) (map PR⇒PS R⇒S ys∼zs) diff --git a/src/Data/List/Relation/Binary/Permutation/Propositional.agda b/src/Data/List/Relation/Binary/Permutation/Propositional.agda index c41793d28a..4e3802af47 100644 --- a/src/Data/List/Relation/Binary/Permutation/Propositional.agda +++ b/src/Data/List/Relation/Binary/Permutation/Propositional.agda @@ -14,41 +14,38 @@ open import Relation.Binary.Core using (Rel; _⇒_) open import Relation.Binary.Bundles using (Setoid) open import Relation.Binary.Structures using (IsEquivalence) open import Relation.Binary.Definitions using (Reflexive; Transitive) -open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl) -import Relation.Binary.Reasoning.Setoid as EqReasoning +open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_) +import Data.List.Relation.Binary.Permutation.Homogeneous as Homogeneous +import Relation.Binary.Reasoning.Setoid as ≈-Reasoning open import Relation.Binary.Reasoning.Syntax ------------------------------------------------------------------------- --- An inductive definition of permutation --- Note that one would expect that this would be defined in terms of --- `Permutation.Setoid`. This is not currently the case as it involves --- adding in a bunch of trivial `_≡_` proofs to the constructors which --- a) adds noise and b) prevents easy access to the variables `x`, `y`. --- This may be changed in future when a better solution is found. +------------------------------------------------------------------------ +-- Definition infix 3 _↭_ -data _↭_ : Rel (List A) a where - refl : ∀ {xs} → xs ↭ xs - prep : ∀ {xs ys} x → xs ↭ ys → x ∷ xs ↭ x ∷ ys - swap : ∀ {xs ys} x y → xs ↭ ys → x ∷ y ∷ xs ↭ y ∷ x ∷ ys - trans : ∀ {xs ys zs} → xs ↭ ys → ys ↭ zs → xs ↭ zs +_↭_ : Rel (List A) a +_↭_ = Homogeneous.Permutation _≡_ _≡_ + +pattern refl = Homogeneous.refl ≡.refl +pattern prep {xs} {ys} x tl = Homogeneous.prep {xs = xs} {ys = ys} {x = x} ≡.refl tl +pattern swap {xs} {ys} x y tl = Homogeneous.swap {xs = xs} {ys = ys} {x = x} {y = y} ≡.refl ≡.refl tl + +open Homogeneous public + using (trans) ------------------------------------------------------------------------ -- _↭_ is an equivalence ↭-reflexive : _≡_ ⇒ _↭_ -↭-reflexive refl = refl +↭-reflexive ≡.refl = refl ↭-refl : Reflexive _↭_ ↭-refl = refl ↭-sym : ∀ {xs ys} → xs ↭ ys → ys ↭ xs -↭-sym refl = refl -↭-sym (prep x xs↭ys) = prep x (↭-sym xs↭ys) -↭-sym (swap x y xs↭ys) = swap y x (↭-sym xs↭ys) -↭-sym (trans xs↭ys ys↭zs) = trans (↭-sym ys↭zs) (↭-sym xs↭ys) +↭-sym = Homogeneous.sym ≡.sym ≡.sym -- A smart version of trans that avoids unnecessary `refl`s (see #1113). ↭-trans : Transitive _↭_ @@ -74,7 +71,7 @@ data _↭_ : Rel (List A) a where module PermutationReasoning where - private module Base = EqReasoning ↭-setoid + private module Base = ≈-Reasoning ↭-setoid open Base public hiding (step-≈; step-≈˘; step-≈-⟩; step-≈-⟨) @@ -89,12 +86,12 @@ module PermutationReasoning where -- Skip reasoning on the first element step-prep : ∀ x xs {ys zs : List A} → (x ∷ ys) IsRelatedTo zs → xs ↭ ys → (x ∷ xs) IsRelatedTo zs - step-prep x xs rel xs↭ys = relTo (trans (prep x xs↭ys) (begin rel)) + step-prep x xs rel xs↭ys = ↭-go (prep x xs↭ys) rel -- Skip reasoning about the first two elements step-swap : ∀ x y xs {ys zs : List A} → (y ∷ x ∷ ys) IsRelatedTo zs → xs ↭ ys → (x ∷ y ∷ xs) IsRelatedTo zs - step-swap x y xs rel xs↭ys = relTo (trans (swap x y xs↭ys) (begin rel)) + step-swap x y xs rel xs↭ys = ↭-go (swap x y xs↭ys) rel syntax step-prep x xs y↭z x↭y = x ∷ xs <⟨ x↭y ⟩ y↭z syntax step-swap x y xs y↭z x↭y = x ∷ y ∷ xs <<⟨ x↭y ⟩ y↭z diff --git a/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda b/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda index d56bdb7fb3..fe908faa55 100644 --- a/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda +++ b/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda @@ -12,8 +12,8 @@ open import Algebra.Bundles open import Algebra.Definitions open import Algebra.Structures open import Data.Bool.Base using (Bool; true; false) -open import Data.Nat.Base using (suc; _*_) -open import Data.Nat.Properties using (*-assoc; *-comm) +open import Data.Nat.Base using (suc) +open import Data.Nat.Properties using (*-1-commutativeMonoid) open import Data.Product.Base using (-,_; proj₂) open import Data.List.Base as List open import Data.List.Relation.Binary.Permutation.Propositional @@ -29,13 +29,14 @@ open import Relation.Unary using (Pred) open import Relation.Binary.Core using (Rel; _Preserves_⟶_; _Preserves₂_⟶_⟶_) open import Relation.Binary.Definitions using (_Respects_; Decidable) open import Relation.Binary.PropositionalEquality.Core as ≡ - using (_≡_ ; refl ; cong; cong₂; _≢_) + using (_≡_ ; cong; cong₂; _≢_) open import Relation.Binary.PropositionalEquality.Properties using (module ≡-Reasoning) +import Relation.Binary.Reasoning.Setoid as ≈-Reasoning open import Relation.Nullary private variable - a b p : Level + a b p r : Level A : Set a B : Set b @@ -43,23 +44,22 @@ private -- Permutations of empty and singleton lists ↭-empty-inv : ∀ {xs : List A} → xs ↭ [] → xs ≡ [] -↭-empty-inv refl = refl -↭-empty-inv (trans p q) with refl ← ↭-empty-inv q = ↭-empty-inv p +↭-empty-inv refl = ≡.refl +↭-empty-inv (trans p q) with ≡.refl ← ↭-empty-inv q = ↭-empty-inv p ¬x∷xs↭[] : ∀ {x} {xs : List A} → ¬ ((x ∷ xs) ↭ []) -¬x∷xs↭[] (trans s₁ s₂) with ↭-empty-inv s₂ -... | refl = ¬x∷xs↭[] s₁ +¬x∷xs↭[] (trans s₁ s₂) with ≡.refl ← ↭-empty-inv s₂ = ¬x∷xs↭[] s₁ ↭-singleton-inv : ∀ {x} {xs : List A} → xs ↭ [ x ] → xs ≡ [ x ] -↭-singleton-inv refl = refl -↭-singleton-inv (prep _ ρ) with refl ← ↭-empty-inv ρ = refl -↭-singleton-inv (trans ρ₁ ρ₂) with refl ← ↭-singleton-inv ρ₂ = ↭-singleton-inv ρ₁ +↭-singleton-inv refl = ≡.refl +↭-singleton-inv (prep _ ρ) with ≡.refl ← ↭-empty-inv ρ = ≡.refl +↭-singleton-inv (trans ρ₁ ρ₂) with ≡.refl ← ↭-singleton-inv ρ₂ = ↭-singleton-inv ρ₁ ------------------------------------------------------------------------ -- sym ↭-sym-involutive : ∀ {xs ys : List A} (p : xs ↭ ys) → ↭-sym (↭-sym p) ≡ p -↭-sym-involutive refl = refl +↭-sym-involutive refl = ≡.refl ↭-sym-involutive (prep x ↭) = cong (prep x) (↭-sym-involutive ↭) ↭-sym-involutive (swap x y ↭) = cong (swap x y) (↭-sym-involutive ↭) ↭-sym-involutive (trans ↭₁ ↭₂) = @@ -90,20 +90,20 @@ Any-resp-[σ⁻¹∘σ] : {xs ys : List A} {P : Pred A p} → (σ : xs ↭ ys) → (ix : Any P xs) → Any-resp-↭ (trans σ (↭-sym σ)) ix ≡ ix -Any-resp-[σ⁻¹∘σ] refl ix = refl -Any-resp-[σ⁻¹∘σ] (prep _ _) (here _) = refl -Any-resp-[σ⁻¹∘σ] (swap _ _ _) (here _) = refl -Any-resp-[σ⁻¹∘σ] (swap _ _ _) (there (here _)) = refl +Any-resp-[σ⁻¹∘σ] refl ix = ≡.refl +Any-resp-[σ⁻¹∘σ] (prep _ _) (here _) = ≡.refl +Any-resp-[σ⁻¹∘σ] (swap _ _ _) (here _) = ≡.refl +Any-resp-[σ⁻¹∘σ] (swap _ _ _) (there (here _)) = ≡.refl Any-resp-[σ⁻¹∘σ] (trans σ₁ σ₂) ix rewrite Any-resp-[σ⁻¹∘σ] σ₂ (Any-resp-↭ σ₁ ix) rewrite Any-resp-[σ⁻¹∘σ] σ₁ ix - = refl + = ≡.refl Any-resp-[σ⁻¹∘σ] (prep _ σ) (there ix) rewrite Any-resp-[σ⁻¹∘σ] σ ix - = refl + = ≡.refl Any-resp-[σ⁻¹∘σ] (swap _ _ σ) (there (there ix)) rewrite Any-resp-[σ⁻¹∘σ] σ ix - = refl + = ≡.refl ∈-resp-[σ⁻¹∘σ] : {xs ys : List A} {x : A} → (σ : xs ↭ ys) → @@ -126,17 +126,17 @@ module _ (f : A → B) where ↭-map-inv : ∀ {xs ys} → map f xs ↭ ys → ∃ λ ys′ → ys ≡ map f ys′ × xs ↭ ys′ ↭-map-inv {[]} ρ = -, ↭-empty-inv (↭-sym ρ) , ↭-refl ↭-map-inv {x ∷ []} ρ = -, ↭-singleton-inv (↭-sym ρ) , ↭-refl - ↭-map-inv {_ ∷ _ ∷ _} refl = -, refl , ↭-refl - ↭-map-inv {_ ∷ _ ∷ _} (prep _ ρ) with _ , refl , ρ′ ← ↭-map-inv ρ = -, refl , prep _ ρ′ - ↭-map-inv {_ ∷ _ ∷ _} (swap _ _ ρ) with _ , refl , ρ′ ← ↭-map-inv ρ = -, refl , swap _ _ ρ′ - ↭-map-inv {_ ∷ _ ∷ _} (trans ρ₁ ρ₂) with _ , refl , ρ₃ ← ↭-map-inv ρ₁ - with _ , refl , ρ₄ ← ↭-map-inv ρ₂ = -, refl , trans ρ₃ ρ₄ + ↭-map-inv {_ ∷ _ ∷ _} refl = -, ≡.refl , ↭-refl + ↭-map-inv {_ ∷ _ ∷ _} (prep _ ρ) with _ , ≡.refl , ρ′ ← ↭-map-inv ρ = -, ≡.refl , prep _ ρ′ + ↭-map-inv {_ ∷ _ ∷ _} (swap _ _ ρ) with _ , ≡.refl , ρ′ ← ↭-map-inv ρ = -, ≡.refl , swap _ _ ρ′ + ↭-map-inv {_ ∷ _ ∷ _} (trans ρ₁ ρ₂) with _ , ≡.refl , ρ₃ ← ↭-map-inv ρ₁ + with _ , ≡.refl , ρ₄ ← ↭-map-inv ρ₂ = -, ≡.refl , trans ρ₃ ρ₄ ------------------------------------------------------------------------ -- length ↭-length : ∀ {xs ys : List A} → xs ↭ ys → length xs ≡ length ys -↭-length refl = refl +↭-length refl = ≡.refl ↭-length (prep x lr) = cong suc (↭-length lr) ↭-length (swap x y lr) = cong (suc ∘ suc) (↭-length lr) ↭-length (trans lr₁ lr₂) = ≡.trans (↭-length lr₁) (↭-length lr₂) @@ -178,55 +178,55 @@ drop-mid-≡ : ∀ {x : A} ws xs {ys} {zs} → ws ++ [ x ] ++ ys ≡ xs ++ [ x ] ++ zs → ws ++ ys ↭ xs ++ zs drop-mid-≡ [] [] eq with cong tail eq -drop-mid-≡ [] [] eq | refl = refl -drop-mid-≡ [] (x ∷ xs) refl = shift _ xs _ -drop-mid-≡ (w ∷ ws) [] refl = ↭-sym (shift _ ws _) +drop-mid-≡ [] [] eq | ≡.refl = refl +drop-mid-≡ [] (x ∷ xs) ≡.refl = shift _ xs _ +drop-mid-≡ (w ∷ ws) [] ≡.refl = ↭-sym (shift _ ws _) drop-mid-≡ (w ∷ ws) (x ∷ xs) eq with Lₚ.∷-injective eq -... | refl , eq′ = prep w (drop-mid-≡ ws xs eq′) +... | ≡.refl , eq′ = prep w (drop-mid-≡ ws xs eq′) drop-mid : ∀ {x : A} ws xs {ys zs} → ws ++ [ x ] ++ ys ↭ xs ++ [ x ] ++ zs → ws ++ ys ↭ xs ++ zs -drop-mid {A = A} {x} ws xs p = drop-mid′ p ws xs refl refl +drop-mid {A = A} {x} ws xs p = drop-mid′ p ws xs ≡.refl ≡.refl where drop-mid′ : ∀ {l′ l″ : List A} → l′ ↭ l″ → ∀ ws xs {ys zs} → ws ++ [ x ] ++ ys ≡ l′ → xs ++ [ x ] ++ zs ≡ l″ → ws ++ ys ↭ xs ++ zs - drop-mid′ refl ws xs refl eq = drop-mid-≡ ws xs (≡.sym eq) - drop-mid′ (prep x p) [] [] refl eq with cong tail eq - drop-mid′ (prep x p) [] [] refl eq | refl = p - drop-mid′ (prep x p) [] (x ∷ xs) refl refl = trans p (shift _ _ _) - drop-mid′ (prep x p) (w ∷ ws) [] refl refl = trans (↭-sym (shift _ _ _)) p - drop-mid′ (prep x p) (w ∷ ws) (x ∷ xs) refl refl = prep _ (drop-mid′ p ws xs refl refl) - drop-mid′ (swap y z p) [] [] refl refl = prep _ p - drop-mid′ (swap y z p) [] (x ∷ []) refl eq with cong {B = List _} + drop-mid′ refl ws xs ≡.refl eq = drop-mid-≡ ws xs (≡.sym eq) + drop-mid′ (prep x p) [] [] ≡.refl eq with cong tail eq + drop-mid′ (prep x p) [] [] ≡.refl eq | ≡.refl = p + drop-mid′ (prep x p) [] (x ∷ xs) ≡.refl ≡.refl = trans p (shift _ _ _) + drop-mid′ (prep x p) (w ∷ ws) [] ≡.refl ≡.refl = trans (↭-sym (shift _ _ _)) p + drop-mid′ (prep x p) (w ∷ ws) (x ∷ xs) ≡.refl ≡.refl = prep _ (drop-mid′ p ws xs ≡.refl ≡.refl) + drop-mid′ (swap y z p) [] [] ≡.refl ≡.refl = prep _ p + drop-mid′ (swap y z p) [] (x ∷ []) ≡.refl eq with cong {B = List _} (λ { (x ∷ _ ∷ xs) → x ∷ xs ; _ → [] }) eq - drop-mid′ (swap y z p) [] (x ∷ []) refl eq | refl = prep _ p - drop-mid′ (swap y z p) [] (x ∷ _ ∷ xs) refl refl = prep _ (trans p (shift _ _ _)) - drop-mid′ (swap y z p) (w ∷ []) [] refl eq with cong tail eq - drop-mid′ (swap y z p) (w ∷ []) [] refl eq | refl = prep _ p - drop-mid′ (swap y z p) (w ∷ x ∷ ws) [] refl refl = prep _ (trans (↭-sym (shift _ _ _)) p) - drop-mid′ (swap y y p) (y ∷ []) (y ∷ []) refl refl = prep _ p - drop-mid′ (swap y z p) (y ∷ []) (z ∷ y ∷ xs) refl refl = begin + drop-mid′ (swap y z p) [] (x ∷ []) ≡.refl eq | ≡.refl = prep _ p + drop-mid′ (swap y z p) [] (x ∷ _ ∷ xs) ≡.refl ≡.refl = prep _ (trans p (shift _ _ _)) + drop-mid′ (swap y z p) (w ∷ []) [] ≡.refl eq with cong tail eq + drop-mid′ (swap y z p) (w ∷ []) [] ≡.refl eq | ≡.refl = prep _ p + drop-mid′ (swap y z p) (w ∷ x ∷ ws) [] ≡.refl ≡.refl = prep _ (trans (↭-sym (shift _ _ _)) p) + drop-mid′ (swap y y p) (y ∷ []) (y ∷ []) ≡.refl ≡.refl = prep _ p + drop-mid′ (swap y z p) (y ∷ []) (z ∷ y ∷ xs) ≡.refl ≡.refl = begin _ ∷ _ <⟨ p ⟩ _ ∷ (xs ++ _ ∷ _) <⟨ shift _ _ _ ⟩ _ ∷ _ ∷ xs ++ _ <<⟨ refl ⟩ _ ∷ _ ∷ xs ++ _ ∎ where open PermutationReasoning - drop-mid′ (swap y z p) (y ∷ z ∷ ws) (z ∷ []) refl refl = begin + drop-mid′ (swap y z p) (y ∷ z ∷ ws) (z ∷ []) ≡.refl ≡.refl = begin _ ∷ _ ∷ ws ++ _ <<⟨ refl ⟩ _ ∷ (_ ∷ ws ++ _) <⟨ ↭-sym (shift _ _ _) ⟩ _ ∷ (ws ++ _ ∷ _) <⟨ p ⟩ _ ∷ _ ∎ where open PermutationReasoning - drop-mid′ (swap y z p) (y ∷ z ∷ ws) (z ∷ y ∷ xs) refl refl = swap y z (drop-mid′ p _ _ refl refl) - drop-mid′ (trans p₁ p₂) ws xs refl refl with ∈-∃++ (∈-resp-↭ p₁ (∈-insert ws)) - ... | (h , t , refl) = trans (drop-mid′ p₁ ws h refl refl) (drop-mid′ p₂ h xs refl refl) + drop-mid′ (swap y z p) (y ∷ z ∷ ws) (z ∷ y ∷ xs) ≡.refl ≡.refl = swap y z (drop-mid′ p _ _ ≡.refl ≡.refl) + drop-mid′ (trans p₁ p₂) ws xs ≡.refl ≡.refl with ∈-∃++ (∈-resp-↭ p₁ (∈-insert ws)) + ... | (h , t , ≡.refl) = trans (drop-mid′ p₁ ws h ≡.refl ≡.refl) (drop-mid′ p₂ h xs ≡.refl ≡.refl) -- Algebraic properties @@ -360,16 +360,27 @@ module _ {ℓ} {R : Rel A ℓ} (R? : Decidable R) where x ∷ xs ++ y ∷ ys ∎ where open PermutationReasoning +------------------------------------------------------------------------ +-- foldr of Commutative Monoid + +module _ (commutativeMonoid : CommutativeMonoid a r) where + + open module CM = CommutativeMonoid commutativeMonoid + + foldr-commMonoid : ∀ {xs ys} → xs ↭ ys → List.foldr _∙_ ε xs ≈ List.foldr _∙_ ε ys + foldr-commMonoid refl = CM.refl + foldr-commMonoid (prep x xs↭ys) = ∙-congˡ (foldr-commMonoid xs↭ys) + foldr-commMonoid (swap {xs} {ys} x y xs↭ys) = begin + x ∙ (y ∙ foldr _∙_ ε xs) ≈⟨ ∙-congˡ (∙-congˡ (foldr-commMonoid xs↭ys)) ⟩ + x ∙ (y ∙ foldr _∙_ ε ys) ≈⟨ assoc x y (foldr _∙_ ε ys) ⟨ + (x ∙ y) ∙ foldr _∙_ ε ys ≈⟨ ∙-congʳ (comm x y) ⟩ + (y ∙ x) ∙ foldr _∙_ ε ys ≈⟨ assoc y x (foldr _∙_ ε ys) ⟩ + y ∙ (x ∙ foldr _∙_ ε ys) ∎ + where open ≈-Reasoning CM.setoid + foldr-commMonoid (trans xs↭ys ys↭zs) = CM.trans (foldr-commMonoid xs↭ys) (foldr-commMonoid ys↭zs) + ------------------------------------------------------------------------ -- product product-↭ : product Preserves _↭_ ⟶ _≡_ -product-↭ refl = refl -product-↭ (prep x r) = cong (x *_) (product-↭ r) -product-↭ (trans r s) = ≡.trans (product-↭ r) (product-↭ s) -product-↭ (swap {xs} {ys} x y r) = begin - x * (y * product xs) ≡˘⟨ *-assoc x y (product xs) ⟩ - (x * y) * product xs ≡⟨ cong₂ _*_ (*-comm x y) (product-↭ r) ⟩ - (y * x) * product ys ≡⟨ *-assoc y x (product ys) ⟩ - y * (x * product ys) ∎ - where open ≡-Reasoning +product-↭ = foldr-commMonoid *-1-commutativeMonoid diff --git a/src/Data/List/Relation/Binary/Permutation/Setoid.agda b/src/Data/List/Relation/Binary/Permutation/Setoid.agda index 4409e78cc4..f630f546f4 100644 --- a/src/Data/List/Relation/Binary/Permutation/Setoid.agda +++ b/src/Data/List/Relation/Binary/Permutation/Setoid.agda @@ -19,16 +19,16 @@ module Data.List.Relation.Binary.Permutation.Setoid open import Data.List.Base using (List; _∷_) import Data.List.Relation.Binary.Permutation.Homogeneous as Homogeneous -import Data.List.Relation.Binary.Pointwise.Properties as Pointwise using (refl) -open import Data.List.Relation.Binary.Equality.Setoid S +open import Data.List.Relation.Binary.Pointwise as Pointwise using (Pointwise) +open import Data.List.Relation.Binary.Equality.Setoid S using (_≋_; ≋-refl; ≋-sym) open import Data.Nat.Base using (ℕ; zero; suc; _+_) open import Level using (_⊔_) open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl) import Relation.Binary.Reasoning.Setoid as ≈-Reasoning -private - module Eq = Setoid S -open Eq using (_≈_) renaming (Carrier to A) +open Setoid S + using (_≈_) + renaming (Carrier to A; refl to ≈-refl; sym to ≈-sym ; trans to ≈-trans) ------------------------------------------------------------------------ -- Definition @@ -39,7 +39,7 @@ open Homogeneous public infix 3 _↭_ _↭_ : Rel (List A) (a ⊔ ℓ) -_↭_ = Homogeneous.Permutation _≈_ +_↭_ = Homogeneous.Permutation _≋_ _≈_ ------------------------------------------------------------------------ -- Constructor aliases @@ -48,10 +48,10 @@ _↭_ = Homogeneous.Permutation _≈_ -- swapped or prepended are propositionally equal ↭-prep : ∀ x {xs ys} → xs ↭ ys → x ∷ xs ↭ x ∷ ys -↭-prep x xs↭ys = prep Eq.refl xs↭ys +↭-prep x xs↭ys = prep ≈-refl xs↭ys ↭-swap : ∀ x y {xs ys} → xs ↭ ys → x ∷ y ∷ xs ↭ y ∷ x ∷ ys -↭-swap x y xs↭ys = swap Eq.refl Eq.refl xs↭ys +↭-swap x y xs↭ys = swap ≈-refl ≈-refl xs↭ys ------------------------------------------------------------------------ -- Functions over permutations @@ -65,23 +65,26 @@ steps (trans xs↭ys ys↭zs) = steps xs↭ys + steps ys↭zs ------------------------------------------------------------------------ -- _↭_ is an equivalence -↭-reflexive : _≡_ ⇒ _↭_ -↭-reflexive refl = refl (Pointwise.refl Eq.refl) +↭-pointwise : _≋_ ⇒ _↭_ +↭-pointwise = refl ↭-refl : Reflexive _↭_ -↭-refl = ↭-reflexive refl +↭-refl = ↭-pointwise ≋-refl + +↭-reflexive : _≡_ ⇒ _↭_ +↭-reflexive refl = ↭-refl ↭-sym : Symmetric _↭_ -↭-sym = Homogeneous.sym Eq.sym +↭-sym = Homogeneous.sym ≋-sym ≈-sym ↭-trans : Transitive _↭_ -↭-trans = trans +↭-trans = Homogeneous.trans ↭-isEquivalence : IsEquivalence _↭_ -↭-isEquivalence = Homogeneous.isEquivalence Eq.refl Eq.sym +↭-isEquivalence = Homogeneous.isEquivalence ≋-refl ≋-sym ≈-sym ↭-setoid : Setoid _ _ -↭-setoid = Homogeneous.setoid {R = _≈_} Eq.refl Eq.sym +↭-setoid = Homogeneous.setoid {PR = Pointwise _≈_} {R = _≈_} ≋-refl ≋-sym ≈-sym ------------------------------------------------------------------------ -- A reasoning API to chain permutation proofs @@ -95,7 +98,7 @@ module PermutationReasoning where renaming (≈-go to ↭-go) open ↭-syntax _IsRelatedTo_ _IsRelatedTo_ ↭-go ↭-sym public - open ≋-syntax _IsRelatedTo_ _IsRelatedTo_ (↭-go ∘′ refl) ≋-sym public + open ≋-syntax _IsRelatedTo_ _IsRelatedTo_ (↭-go ∘′ ↭-pointwise) ≋-sym public -- Some extra combinators that allow us to skip certain elements @@ -104,12 +107,12 @@ module PermutationReasoning where -- Skip reasoning on the first element step-prep : ∀ x xs {ys zs : List A} → (x ∷ ys) IsRelatedTo zs → xs ↭ ys → (x ∷ xs) IsRelatedTo zs - step-prep x xs rel xs↭ys = relTo (trans (prep Eq.refl xs↭ys) (begin rel)) + step-prep x xs rel xs↭ys = ↭-go (↭-prep x xs↭ys) rel -- Skip reasoning about the first two elements step-swap : ∀ x y xs {ys zs : List A} → (y ∷ x ∷ ys) IsRelatedTo zs → xs ↭ ys → (x ∷ y ∷ xs) IsRelatedTo zs - step-swap x y xs rel xs↭ys = relTo (trans (swap Eq.refl Eq.refl xs↭ys) (begin rel)) + step-swap x y xs rel xs↭ys = ↭-go (↭-swap x y xs↭ys) rel syntax step-prep x xs y↭z x↭y = x ∷ xs <⟨ x↭y ⟩ y↭z syntax step-swap x y xs y↭z x↭y = x ∷ y ∷ xs <<⟨ x↭y ⟩ y↭z diff --git a/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda index 3af753e826..60c46df7cd 100644 --- a/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda +++ b/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda @@ -37,7 +37,7 @@ open import Data.Product.Base using (_,_; _×_; ∃; ∃₂; proj₁; proj₂) open import Function.Base using (_∘_; _⟨_⟩_; flip) open import Level using (Level; _⊔_) open import Relation.Unary using (Pred; Decidable) -import Relation.Binary.Reasoning.Setoid as RelSetoid +import Relation.Binary.Reasoning.Setoid as ≈-Reasoning open import Relation.Binary.Properties.Setoid S using (≉-resp₂) open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_ ; refl; sym; cong; cong₂; subst; _≢_) @@ -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-≋) -open PermutationReasoning + ------------------------------------------------------------------------ -- Relationships to other predicates @@ -98,7 +98,7 @@ Unique-resp-↭ = AllPairs-resp-↭ (_∘ ≈-sym) ≉-resp₂ ------------------------------------------------------------------------ ≋⇒↭ : _≋_ ⇒ _↭_ -≋⇒↭ = refl +≋⇒↭ = ↭-pointwise ↭-respʳ-≋ : _↭_ Respectsʳ _≋_ ↭-respʳ-≋ xs≋ys (refl zs≋xs) = refl (≋-trans zs≋xs xs≋ys) @@ -165,6 +165,7 @@ shift {v} {w} v≈w (x ∷ xs) ys = begin x ∷ (xs ++ [ v ] ++ ys) <⟨ shift v≈w xs ys ⟩ x ∷ w ∷ xs ++ ys <<⟨ ↭-refl ⟩ w ∷ x ∷ xs ++ ys ∎ + where open PermutationReasoning ↭-shift : ∀ {v} (xs ys : List A) → xs ++ [ v ] ++ ys ↭ v ∷ xs ++ ys ↭-shift = shift ≈-refl @@ -202,6 +203,7 @@ shift {v} {w} v≈w (x ∷ xs) ys = begin x ∷ xs ++ ys <⟨ ++-comm xs ys ⟩ x ∷ ys ++ xs ↭⟨ ↭-shift ys xs ⟨ ys ++ (x ∷ xs) ∎ + where open PermutationReasoning -- Structures @@ -266,6 +268,7 @@ shifts xs ys {zs} = begin (xs ++ ys) ++ zs ↭⟨ ++⁺ʳ zs (++-comm xs ys) ⟩ (ys ++ xs) ++ zs ↭⟨ ++-assoc ys xs zs ⟩ ys ++ xs ++ zs ∎ + where open PermutationReasoning dropMiddleElement-≋ : ∀ {x} ws xs {ys} {zs} → ws ++ [ x ] ++ ys ≋ xs ++ [ x ] ++ zs → @@ -460,6 +463,12 @@ module _ {ℓ} {R : Rel A ℓ} (R? : B.Decidable R) where x ∷ xs ++ y ∷ ys ∎ where open PermutationReasoning +------------------------------------------------------------------------ +-- _∷_ + +drop-∷ : ∀ {x : A} {xs ys} → x ∷ xs ↭ x ∷ ys → xs ↭ ys +drop-∷ = dropMiddleElement [] [] + ------------------------------------------------------------------------ -- _∷ʳ_ @@ -477,6 +486,18 @@ module _ {ℓ} {R : Rel A ℓ} (R? : B.Decidable R) where ++↭ʳ++ [] ys = ↭-refl ++↭ʳ++ (x ∷ xs) ys = ↭-trans (↭-sym (↭-shift xs ys)) (++↭ʳ++ xs (x ∷ ys)) +------------------------------------------------------------------------ +-- reverse + +↭-reverse : (xs : List A) → reverse xs ↭ xs +↭-reverse [] = ↭-refl +↭-reverse (x ∷ xs) = begin + reverse (x ∷ xs) ≡⟨ Lₚ.unfold-reverse x xs ⟩ + reverse xs ∷ʳ x ↭⟨ ∷↭∷ʳ x (reverse xs) ⟨ + x ∷ reverse xs <⟨ ↭-reverse xs ⟩ + x ∷ xs ∎ + where open PermutationReasoning + ------------------------------------------------------------------------ -- foldr of Commutative Monoid @@ -484,22 +505,20 @@ module _ {_∙_ : Op₂ A} {ε : A} (isCmonoid : IsCommutativeMonoid _≈_ _∙_ open module CM = IsCommutativeMonoid isCmonoid private - module S = RelSetoid setoid cmonoid : CommutativeMonoid _ _ cmonoid = record { isCommutativeMonoid = isCmonoid } - open ACM cmonoid - foldr-commMonoid : ∀ {xs ys} → xs ↭ ys → foldr _∙_ ε xs ≈ foldr _∙_ ε ys foldr-commMonoid (refl []) = CM.refl foldr-commMonoid (refl (x≈y ∷ xs≈ys)) = ∙-cong x≈y (foldr-commMonoid (Permutation.refl xs≈ys)) foldr-commMonoid (prep x≈y xs↭ys) = ∙-cong x≈y (foldr-commMonoid xs↭ys) - foldr-commMonoid (swap {xs} {ys} {x} {y} {x′} {y′} x≈x′ y≈y′ xs↭ys) = S.begin - x ∙ (y ∙ foldr _∙_ ε xs) S.≈⟨ ∙-congˡ (∙-congˡ (foldr-commMonoid xs↭ys)) ⟩ - x ∙ (y ∙ foldr _∙_ ε ys) S.≈⟨ assoc x y (foldr _∙_ ε ys) ⟨ - (x ∙ y) ∙ foldr _∙_ ε ys S.≈⟨ ∙-congʳ (comm x y) ⟩ - (y ∙ x) ∙ foldr _∙_ ε ys S.≈⟨ ∙-congʳ (∙-cong y≈y′ x≈x′) ⟩ - (y′ ∙ x′) ∙ foldr _∙_ ε ys S.≈⟨ assoc y′ x′ (foldr _∙_ ε ys) ⟩ - y′ ∙ (x′ ∙ foldr _∙_ ε ys) S.∎ + foldr-commMonoid (swap {xs} {ys} {x} {y} {x′} {y′} x≈x′ y≈y′ xs↭ys) = begin + x ∙ (y ∙ foldr _∙_ ε xs) ≈⟨ ∙-congˡ (∙-congˡ (foldr-commMonoid xs↭ys)) ⟩ + x ∙ (y ∙ foldr _∙_ ε ys) ≈⟨ assoc x y (foldr _∙_ ε ys) ⟨ + (x ∙ y) ∙ foldr _∙_ ε ys ≈⟨ ∙-congʳ (comm x y) ⟩ + (y ∙ x) ∙ foldr _∙_ ε ys ≈⟨ ∙-congʳ (∙-cong y≈y′ x≈x′) ⟩ + (y′ ∙ x′) ∙ foldr _∙_ ε ys ≈⟨ assoc y′ x′ (foldr _∙_ ε ys) ⟩ + y′ ∙ (x′ ∙ foldr _∙_ ε ys) ∎ + where open ≈-Reasoning setoid foldr-commMonoid (trans xs↭ys ys↭zs) = CM.trans (foldr-commMonoid xs↭ys) (foldr-commMonoid ys↭zs) diff --git a/src/Data/List/Relation/Binary/Subset/Propositional/Properties.agda b/src/Data/List/Relation/Binary/Subset/Propositional/Properties.agda index 3e91679bb2..7fcb72ed58 100644 --- a/src/Data/List/Relation/Binary/Subset/Propositional/Properties.agda +++ b/src/Data/List/Relation/Binary/Subset/Propositional/Properties.agda @@ -24,6 +24,7 @@ open import Data.List.Membership.Propositional.Properties 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 + using (_↭_; ↭-sym; ↭-isEquivalence) import Data.List.Relation.Binary.Permutation.Propositional.Properties as Permutation open import Data.Nat using (ℕ; _≤_) import Data.Product.Base as Product @@ -36,8 +37,8 @@ open import Relation.Nullary using (¬_; yes; no) open import Relation.Unary using (Decidable; Pred) renaming (_⊆_ to _⋐_) open import Relation.Binary.Core using (_⇒_) open import Relation.Binary.Bundles using (Preorder) -open import Relation.Binary.PropositionalEquality - using (_≡_; _≗_; isEquivalence; subst; resp; refl; setoid; module ≡-Reasoning) +open import Relation.Binary.PropositionalEquality as ≡ + using (_≡_; _≗_; isEquivalence; resp; refl; setoid; module ≡-Reasoning) import Relation.Binary.Reasoning.Preorder as ≲-Reasoning private @@ -117,10 +118,10 @@ module ⊆-Reasoning (A : Set a) where ------------------------------------------------------------------------ Any-resp-⊆ : ∀ {P : Pred A p} → (Any P) Respects _⊆_ -Any-resp-⊆ = Subset.Any-resp-⊆ (setoid _) (subst _) +Any-resp-⊆ = Subset.Any-resp-⊆ (setoid _) (resp _) All-resp-⊇ : ∀ {P : Pred A p} → (All P) Respects _⊇_ -All-resp-⊇ = Subset.All-resp-⊇ (setoid _) (subst _) +All-resp-⊇ = Subset.All-resp-⊇ (setoid _) (resp _) ------------------------------------------------------------------------ -- Properties relating _⊆_ to various list functions