From 47b6a2843d2ddca47b444d6c8cccededa3a90091 Mon Sep 17 00:00:00 2001 From: Andreas Abel Date: Wed, 25 Sep 2024 20:55:05 +0200 Subject: [PATCH 1/5] CI: use v2-install for happy (#2484) `cabal v1-install happy` does not work any longer: https://github.com/haskell/happy/issues/315 --- .github/workflows/ci-ubuntu.yml | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) diff --git a/.github/workflows/ci-ubuntu.yml b/.github/workflows/ci-ubuntu.yml index 93c23f6fe7..56b4c88637 100644 --- a/.github/workflows/ci-ubuntu.yml +++ b/.github/workflows/ci-ubuntu.yml @@ -32,7 +32,7 @@ on: ## To be experimented with again in the future to see if things have ## gotten better. ## -## We use `v1-install` rather than `install` as Agda as a community +## We mostly use `v1-install` rather than `install` as Agda as a community ## hasn't figured out how to manage dependencies with the new local ## style builds (see agda/agda#4627 for details). Once this is resolved ## we should upgrade to `install`. @@ -50,8 +50,8 @@ on: env: GHC_VERSION: 9.8.2 CABAL_VERSION: 3.10.3.0 - CABAL_INSTALL: cabal v1-install --ghc-options='-O1 +RTS -M6G -RTS' - # CABAL_INSTALL: cabal install --overwrite-policy=always --ghc-options='-O1 +RTS -M6G -RTS' + CABAL_V1_INSTALL: cabal v1-install --ghc-options='-O1 +RTS -M6G -RTS' + CABAL_INSTALL: cabal install --overwrite-policy=always --ghc-options='-O1 +RTS -M6G -RTS' AGDA: agda -Werror +RTS -M5G -H3.5G -A128M -RTS -i. -isrc -idoc jobs: @@ -121,13 +121,15 @@ jobs: cabal-update: true - name: Put cabal programs in PATH - run: echo "~/.cabal/bin" >> "${GITHUB_PATH}" + run: echo ~/.cabal/bin >> "${GITHUB_PATH}" - name: Install alex & happy if: steps.cache-cabal.outputs.cache-hit != 'true' run: | ${{ env.CABAL_INSTALL }} alex ${{ env.CABAL_INSTALL }} happy + # happy>=2.0 cannot be v1-installed: https://github.com/haskell/happy/issues/315 + # Since we only need the executable, it is fine to use v2-install here. - name: Download and install Agda from github if: steps.cache-cabal.outputs.cache-hit != 'true' @@ -137,7 +139,7 @@ jobs: git checkout ${{ env.AGDA_COMMIT }} mkdir -p doc touch doc/user-manual.pdf - ${{ env.CABAL_INSTALL }} + ${{ env.CABAL_V1_INSTALL }} cd .. ######################################################################## @@ -167,7 +169,7 @@ jobs: - name: Golden testing run: | - ${{ env.CABAL_INSTALL }} clock + ${{ env.CABAL_V1_INSTALL }} clock make testsuite INTERACTIVE='' AGDA_EXEC='~/.cabal/bin/agda' From 7273c6e06618ba3b284fc3e60490c2104f671a9c Mon Sep 17 00:00:00 2001 From: Orestis Melkonian Date: Wed, 25 Sep 2024 21:53:30 +0100 Subject: [PATCH 2/5] Lists: porting several lemmas from other libraries (#2479) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * Lists: irrelevance of membership (in unique lists) * Lists: the empty list is always a sublist of another * Lists: lookupMaybe (unsafe version of lookup) * List: `concatMap⁺` for the subset relation * Lists: memberhsip lemma for AllPairs * Lists: membership lemmas for map∘filter * Lists: lemmas about concatMap * Lists: lemmas about deduplicate * Lists: membership lemmas about nested lists * Lists: extra subset lemmas about _∷_ * Lists: extra lemmas about _∷_/Unique * Lists: incorporate feedback from James * Lists: incorporate feedback from Guillaume --- CHANGELOG.md | 104 +++++++++++++++- .../Membership/Propositional/Properties.agda | 112 ++++++++++++++---- .../Propositional/Properties/Core.agda | 8 +- .../Propositional/Properties/WithK.agda | 20 +++- .../List/Membership/Setoid/Properties.agda | 69 +++++++++-- src/Data/List/Properties.agda | 8 ++ .../Disjoint/Propositional/Properties.agda | 65 ++++++++++ .../Binary/Disjoint/Setoid/Properties.agda | 48 ++++---- .../Propositional/Properties/WithK.agda | 54 +++++++++ .../Sublist/Heterogeneous/Properties.agda | 6 +- .../Binary/Sublist/Setoid/Properties.agda | 7 +- .../Subset/Propositional/Properties.agda | 33 +++++- .../Binary/Subset/Setoid/Properties.agda | 45 ++++++- .../List/Relation/Unary/Any/Properties.agda | 11 ++ .../Unique/Propositional/Properties.agda | 18 ++- .../Unary/Unique/Setoid/Properties.agda | 20 ++++ 16 files changed, 558 insertions(+), 70 deletions(-) create mode 100644 src/Data/List/Relation/Binary/Disjoint/Propositional/Properties.agda create mode 100644 src/Data/List/Relation/Binary/Permutation/Propositional/Properties/WithK.agda diff --git a/CHANGELOG.md b/CHANGELOG.md index 62f9b4b8e5..a513e4978f 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -98,6 +98,11 @@ New modules Data.List.Relation.Unary.All.Properties.Core ``` +* `Data.List.Relation.Binary.Disjoint.Propositional.Properties`: + Propositional counterpart to `Data.List.Relation.Binary.Disjoint.Setoid.Properties` + +* `Data.List.Relation.Binary.Permutation.Propositional.Properties.WithK` + Additions to existing modules ----------------------------- @@ -120,14 +125,44 @@ Additions to existing modules * In `Data.List.Membership.Setoid.Properties`: ```agda - Any-∈-swap : Any (_∈ ys) xs → Any (_∈ xs) ys - All-∉-swap : All (_∉ ys) xs → All (_∉ xs) ys + Any-∈-swap : Any (_∈ ys) xs → Any (_∈ xs) ys + All-∉-swap : All (_∉ ys) xs → All (_∉ xs) ys + ∈-map∘filter⁻ : y ∈₂ map f (filter P? xs) → ∃[ x ] x ∈₁ xs × y ≈₂ f x × P x + ∈-map∘filter⁺ : f Preserves _≈₁_ ⟶ _≈₂_ → + ∃[ x ] x ∈₁ xs × y ≈₂ f x × P x → + y ∈₂ map f (filter P? xs) + ∈-concatMap⁺ : Any ((y ∈_) ∘ f) xs → y ∈ concatMap f xs + ∈-concatMap⁻ : y ∈ concatMap f xs → Any ((y ∈_) ∘ f) xs + ∉[] : x ∉ [] + deduplicate-∈⇔ : _≈_ Respectsʳ (flip R) → z ∈ xs ⇔ z ∈ deduplicate R? xs + ``` + +* In `Data.List.Membership.Propositional.Properties`: + ```agda + ∈-AllPairs₂ : AllPairs R xs → x ∈ xs → y ∈ xs → x ≡ y ⊎ R x y ⊎ R y x + ∈-map∘filter⁻ : y ∈ map f (filter P? xs) → (∃[ x ] x ∈ xs × y ≡ f x × P x) + ∈-map∘filter⁺ : (∃[ x ] x ∈ xs × y ≡ f x × P x) → y ∈ map f (filter P? xs) + ∈-concatMap⁺ : Any ((y ∈_) ∘ f) xs → y ∈ concatMap f xs + ∈-concatMap⁻ : y ∈ concatMap f xs → Any ((y ∈_) ∘ f) xs + ++-∈⇔ : v ∈ xs ++ ys ⇔ (v ∈ xs ⊎ v ∈ ys) + []∉map∷ : [] ∉ map (x ∷_) xss + map∷-decomp∈ : (x ∷ xs) ∈ map (y ∷_) xss → x ≡ y × xs ∈ xss + map∷-decomp : xs ∈ map (y ∷_) xss → ∃[ ys ] ys ∈ xss × y ∷ ys ≡ xs + ∈-map∷⁻ : xs ∈ map (x ∷_) xss → x ∈ xs + ∉[] : x ∉ [] + deduplicate-∈⇔ : z ∈ xs ⇔ z ∈ deduplicate _≈?_ xs + ``` + +* In `Data.List.Membership.Propositional.Properties.WithK`: + ```agda + unique∧set⇒bag : Unique xs → Unique ys → xs ∼[ set ] ys → xs ∼[ bag ] ys ``` * In `Data.List.Properties`: ```agda - product≢0 : All NonZero ns → NonZero (product ns) - ∈⇒≤product : All NonZero ns → n ∈ ns → n ≤ product ns + product≢0 : All NonZero ns → NonZero (product ns) + ∈⇒≤product : All NonZero ns → n ∈ ns → n ≤ product ns + concatMap-++ : concatMap f (xs ++ ys) ≡ concatMap f xs ++ concatMap f ys ``` * In `Data.List.Relation.Unary.All`: @@ -135,6 +170,22 @@ Additions to existing modules search : Decidable P → ∀ xs → All (∁ P) xs ⊎ Any P xs ``` +* In `Data.List.Relation.Unary.Any.Properties`: + ```agda + concatMap⁺ : Any (Any P ∘ f) xs → Any P (concatMap f xs) + concatMap⁻ : Any P (concatMap f xs) → Any (Any P ∘ f) xs + ``` + +* In `Data.List.Relation.Unary.Unique.Setoid.Properties`: + ```agda + Unique[x∷xs]⇒x∉xs : Unique S (x ∷ xs) → x ∉ xs + ``` + +* In `Data.List.Relation.Unary.Unique.Propositional.Properties`: + ```agda + Unique[x∷xs]⇒x∉xs : Unique (x ∷ xs) → x ∉ xs + ``` + * In `Data.List.Relation.Binary.Equality.Setoid`: ```agda ++⁺ʳ : ∀ xs → ys ≋ zs → xs ++ ys ≋ xs ++ zs @@ -147,6 +198,51 @@ Additions to existing modules ++⁺ˡ : Reflexive R → ∀ zs → (_++ zs) Preserves (Pointwise R) ⟶ (Pointwise R) ``` +* In `Data.List.Relation.Binary.Subset.Setoid.Properties`: + ```agda + ∷⊈[] : x ∷ xs ⊈ [] + ⊆∷⇒∈∨⊆ : xs ⊆ y ∷ ys → y ∈ xs ⊎ xs ⊆ ys + ⊆∷∧∉⇒⊆ : xs ⊆ y ∷ ys → y ∉ xs → xs ⊆ ys + ``` + +* In `Data.List.Relation.Binary.Subset.Propositional.Properties`: + ```agda + ∷⊈[] : x ∷ xs ⊈ [] + ⊆∷⇒∈∨⊆ : xs ⊆ y ∷ ys → y ∈ xs ⊎ xs ⊆ ys + ⊆∷∧∉⇒⊆ : xs ⊆ y ∷ ys → y ∉ xs → xs ⊆ ys + ``` + +* In `Data.List.Relation.Binary.Subset.Propositional.Properties`: + ```agda + concatMap⁺ : xs ⊆ ys → concatMap f xs ⊆ concatMap f ys + ``` + +* In `Data.List.Relation.Binary.Sublist.Heterogeneous.Properties`: + ```agda + Sublist-[]-universal : Universal (Sublist R []) + ``` + +* In `Data.List.Relation.Binary.Sublist.Setoid.Properties`: + ```agda + []⊆-universal : Universal ([] ⊆_) + ``` + +* In `Data.List.Relation.Binary.Disjoint.Setoid.Properties`: + ```agda + deduplicate⁺ : Disjoint S xs ys → Disjoint S (deduplicate _≟_ xs) (deduplicate _≟_ ys) + ``` + +* In `Data.List.Relation.Binary.Disjoint.Propositional.Properties`: + ```agda + deduplicate⁺ : Disjoint xs ys → Disjoint (deduplicate _≟_ xs) (deduplicate _≟_ ys) + ``` + +* In `Data.List.Relation.Binary.Permutation.Propositional.Properties.WithK`: + ```agda + dedup-++-↭ : Disjoint xs ys → + deduplicate _≟_ (xs ++ ys) ↭ deduplicate _≟_ xs ++ deduplicate _≟_ ys + ``` + * In `Data.Maybe.Properties`: ```agda maybe′-∘ : ∀ f g → f ∘ (maybe′ g b) ≗ maybe′ (f ∘ g) (f b) diff --git a/src/Data/List/Membership/Propositional/Properties.agda b/src/Data/List/Membership/Propositional/Properties.agda index 03e31d8aae..39204f19e2 100644 --- a/src/Data/List/Membership/Propositional/Properties.agda +++ b/src/Data/List/Membership/Propositional/Properties.agda @@ -24,16 +24,16 @@ open import Data.List.Relation.Unary.Any.Properties open import Data.Nat.Base using (ℕ; suc; s≤s; _≤_; _<_; _≰_) open import Data.Nat.Properties using (suc-injective; m≤n⇒m≤1+n; _≤?_; <⇒≢; ≰⇒>) -open import Data.Product.Base using (∃; ∃₂; _×_; _,_) +open import Data.Product.Base using (∃; ∃₂; _×_; _,_; ∃-syntax; -,_; map₂) open import Data.Product.Properties using (×-≡,≡↔≡) open import Data.Product.Function.NonDependent.Propositional using (_×-cong_) import Data.Product.Function.Dependent.Propositional as Σ open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂) open import Effect.Monad using (RawMonad) -open import Function.Base using (_∘_; _∘′_; _$_; id; flip; _⟨_⟩_) +open import Function.Base using (_∘_; _∘′_; _$_; id; flip; _⟨_⟩_; _∋_) open import Function.Definitions using (Injective) import Function.Related.Propositional as Related -open import Function.Bundles using (_↔_; _↣_; Injection) +open import Function.Bundles using (_↔_; _↣_; Injection; _⇔_; mk⇔) open import Function.Related.TypeIsomorphisms using (×-comm; ∃∃↔∃∃) open import Function.Construct.Identity using (↔-id) open import Level using (Level) @@ -55,6 +55,9 @@ private variable ℓ : Level A B C : Set ℓ + x y v : A + xs ys : List A + xss : List (List A) ------------------------------------------------------------------------ -- Publicly re-export properties from Core @@ -64,10 +67,10 @@ open import Data.List.Membership.Propositional.Properties.Core public ------------------------------------------------------------------------ -- Equality -∈-resp-≋ : ∀ {x : A} → (x ∈_) Respects _≋_ +∈-resp-≋ : (x ∈_) Respects _≋_ ∈-resp-≋ = Membership.∈-resp-≋ (≡.setoid _) -∉-resp-≋ : ∀ {x : A} → (x ∉_) Respects _≋_ +∉-resp-≋ : (x ∉_) Respects _≋_ ∉-resp-≋ = Membership.∉-resp-≋ (≡.setoid _) ------------------------------------------------------------------------ @@ -96,14 +99,14 @@ map-mapWith∈ = Membership.map-mapWith∈ (≡.setoid _) module _ (f : A → B) where - ∈-map⁺ : ∀ {x xs} → x ∈ xs → f x ∈ map f xs + ∈-map⁺ : x ∈ xs → f x ∈ map f xs ∈-map⁺ = Membership.∈-map⁺ (≡.setoid A) (≡.setoid B) (cong f) - ∈-map⁻ : ∀ {y xs} → y ∈ map f xs → ∃ λ x → x ∈ xs × y ≡ f x + ∈-map⁻ : y ∈ map f xs → ∃ λ x → x ∈ xs × y ≡ f x ∈-map⁻ = Membership.∈-map⁻ (≡.setoid A) (≡.setoid B) - map-∈↔ : ∀ {y xs} → (∃ λ x → x ∈ xs × y ≡ f x) ↔ y ∈ map f xs - map-∈↔ {y} {xs} = + map-∈↔ : (∃ λ x → x ∈ xs × y ≡ f x) ↔ y ∈ map f xs + map-∈↔ {xs} {y} = (∃ λ x → x ∈ xs × y ≡ f x) ↔⟨ Any↔ ⟩ Any (λ x → y ≡ f x) xs ↔⟨ map↔ ⟩ y ∈ List.map f xs ∎ @@ -114,7 +117,7 @@ module _ (f : A → B) where module _ {v : A} where - ∈-++⁺ˡ : ∀ {xs ys} → v ∈ xs → v ∈ xs ++ ys + ∈-++⁺ˡ : v ∈ xs → v ∈ xs ++ ys ∈-++⁺ˡ = Membership.∈-++⁺ˡ (≡.setoid A) ∈-++⁺ʳ : ∀ xs {ys} → v ∈ ys → v ∈ xs ++ ys @@ -123,10 +126,13 @@ module _ {v : A} where ∈-++⁻ : ∀ xs {ys} → v ∈ xs ++ ys → (v ∈ xs) ⊎ (v ∈ ys) ∈-++⁻ = Membership.∈-++⁻ (≡.setoid A) + ++-∈⇔ : v ∈ xs ++ ys ⇔ (v ∈ xs ⊎ v ∈ ys) + ++-∈⇔ = mk⇔ (∈-++⁻ _) Sum.[ ∈-++⁺ˡ , ∈-++⁺ʳ _ ] + ∈-insert : ∀ xs {ys} → v ∈ xs ++ [ v ] ++ ys ∈-insert xs = Membership.∈-insert (≡.setoid A) xs refl - ∈-∃++ : ∀ {xs} → v ∈ xs → ∃₂ λ ys zs → xs ≡ ys ++ [ v ] ++ zs + ∈-∃++ : v ∈ xs → ∃₂ λ ys zs → xs ≡ ys ++ [ v ] ++ zs ∈-∃++ v∈xs with ys , zs , _ , refl , eq ← Membership.∈-∃++ (≡.setoid A) v∈xs = ys , zs , ≋⇒≡ eq @@ -136,7 +142,7 @@ module _ {v : A} where module _ {v : A} where - ∈-concat⁺ : ∀ {xss} → Any (v ∈_) xss → v ∈ concat xss + ∈-concat⁺ : Any (v ∈_) xss → v ∈ concat xss ∈-concat⁺ = Membership.∈-concat⁺ (≡.setoid A) ∈-concat⁻ : ∀ xss → v ∈ concat xss → Any (v ∈_) xss @@ -151,8 +157,7 @@ module _ {v : A} where let xs , v∈xs , xs∈xss = Membership.∈-concat⁻′ (≡.setoid A) xss v∈c in xs , v∈xs , Any.map ≋⇒≡ xs∈xss - concat-∈↔ : ∀ {xss : List (List A)} → - (∃ λ xs → v ∈ xs × xs ∈ xss) ↔ v ∈ concat xss + concat-∈↔ : (∃ λ xs → v ∈ xs × xs ∈ xss) ↔ v ∈ concat xss concat-∈↔ {xss} = (∃ λ xs → v ∈ xs × xs ∈ xss) ↔⟨ Σ.cong (↔-id _) $ ×-comm _ _ ⟩ (∃ λ xs → xs ∈ xss × v ∈ xs) ↔⟨ Any↔ ⟩ @@ -160,6 +165,19 @@ module _ {v : A} where v ∈ concat xss ∎ where open Related.EquationalReasoning +------------------------------------------------------------------------ +-- concatMap + +module _ (f : A → List B) {xs y} where + + private Sᴬ = ≡.setoid A; Sᴮ = ≡.setoid B + + ∈-concatMap⁺ : Any ((y ∈_) ∘ f) xs → y ∈ concatMap f xs + ∈-concatMap⁺ = Membership.∈-concatMap⁺ Sᴬ Sᴮ + + ∈-concatMap⁻ : y ∈ concatMap f xs → Any ((y ∈_) ∘ f) xs + ∈-concatMap⁻ = Membership.∈-concatMap⁻ Sᴬ Sᴮ + ------------------------------------------------------------------------ -- cartesianProductWith @@ -246,12 +264,25 @@ module _ {n} {f : Fin n → A} where module _ {p} {P : A → Set p} (P? : Decidable P) where - ∈-filter⁺ : ∀ {x xs} → x ∈ xs → P x → x ∈ filter P? xs + ∈-filter⁺ : x ∈ xs → P x → x ∈ filter P? xs ∈-filter⁺ = Membership.∈-filter⁺ (≡.setoid A) P? (≡.resp P) - ∈-filter⁻ : ∀ {v xs} → v ∈ filter P? xs → v ∈ xs × P v + ∈-filter⁻ : v ∈ filter P? xs → v ∈ xs × P v ∈-filter⁻ = Membership.∈-filter⁻ (≡.setoid A) P? (≡.resp P) +------------------------------------------------------------------------ +-- map∘filter + +module _ (f : A → B) {p} {P : A → Set p} (P? : Decidable P) {f xs y} where + + private Sᴬ = ≡.setoid A; Sᴮ = ≡.setoid B; respP = ≡.resp P + + ∈-map∘filter⁻ : y ∈ map f (filter P? xs) → (∃[ x ] x ∈ xs × y ≡ f x × P x) + ∈-map∘filter⁻ = Membership.∈-map∘filter⁻ Sᴬ Sᴮ P? respP + + ∈-map∘filter⁺ : (∃[ x ] x ∈ xs × y ≡ f x × P x) → y ∈ map f (filter P? xs) + ∈-map∘filter⁺ = Membership.∈-map∘filter⁺ Sᴬ Sᴮ P? respP (cong f) + ------------------------------------------------------------------------ -- derun and deduplicate @@ -268,8 +299,13 @@ module _ (_≈?_ : DecidableEquality A) where ∈-derun⁺ : ∀ {xs z} → z ∈ xs → z ∈ derun _≈?_ xs ∈-derun⁺ z∈xs = Membership.∈-derun⁺ (≡.setoid A) _≈?_ (flip trans) z∈xs + private resp≈ = λ {c b a : A} (c≡b : c ≡ b) (a≡b : a ≡ b) → trans a≡b (sym c≡b) + ∈-deduplicate⁺ : ∀ {xs z} → z ∈ xs → z ∈ deduplicate _≈?_ xs - ∈-deduplicate⁺ z∈xs = Membership.∈-deduplicate⁺ (≡.setoid A) _≈?_ (λ c≡b a≡b → trans a≡b (sym c≡b)) z∈xs + ∈-deduplicate⁺ z∈xs = Membership.∈-deduplicate⁺ (≡.setoid A) _≈?_ resp≈ z∈xs + + deduplicate-∈⇔ : ∀ {xs z} → z ∈ xs ⇔ z ∈ deduplicate _≈?_ xs + deduplicate-∈⇔ = Membership.deduplicate-∈⇔ (≡.setoid A) _≈?_ resp≈ ------------------------------------------------------------------------ -- _>>=_ @@ -310,13 +346,13 @@ module _ (_≈?_ : DecidableEquality A) where ------------------------------------------------------------------------ -- length -∈-length : ∀ {x : A} {xs} → x ∈ xs → 0 < length xs +∈-length : x ∈ xs → 0 < length xs ∈-length = Membership.∈-length (≡.setoid _) ------------------------------------------------------------------------ -- lookup -∈-lookup : ∀ {xs : List A} i → lookup xs i ∈ xs +∈-lookup : ∀ i → lookup xs i ∈ xs ∈-lookup {xs = xs} i = Membership.∈-lookup (≡.setoid _) xs i ------------------------------------------------------------------------ @@ -337,7 +373,7 @@ module _ {_•_ : Op₂ A} where ------------------------------------------------------------------------ -- inits -[]∈inits : ∀ {a} {A : Set a} (as : List A) → [] ∈ inits as +[]∈inits : (as : List A) → [] ∈ inits as []∈inits _ = here refl ------------------------------------------------------------------------ @@ -401,3 +437,39 @@ there-injective-≢∈ : ∀ {xs} {x y z : A} {x∈xs : x ∈ xs} {y∈xs : y there {x = z} x∈xs ≢∈ there y∈xs → x∈xs ≢∈ y∈xs there-injective-≢∈ neq refl eq = neq refl (≡.cong there eq) + +------------------------------------------------------------------------ +-- AllPairs + +open import Data.List.Relation.Unary.AllPairs using (AllPairs; []; _∷_) +import Data.List.Relation.Unary.All as All + +module _ {R : A → A → Set ℓ} where + ∈-AllPairs₂ : ∀ {xs x y} → AllPairs R xs → x ∈ xs → y ∈ xs → x ≡ y ⊎ R x y ⊎ R y x + ∈-AllPairs₂ (_ ∷ _) (here refl) (here refl) = inj₁ refl + ∈-AllPairs₂ (p ∷ _) (here refl) (there y∈) = inj₂ $ inj₁ $ All.lookup p y∈ + ∈-AllPairs₂ (p ∷ _) (there x∈) (here refl) = inj₂ $ inj₂ $ All.lookup p x∈ + ∈-AllPairs₂ (_ ∷ ps) (there x∈) (there y∈) = ∈-AllPairs₂ ps x∈ y∈ + +------------------------------------------------------------------------ +-- nested lists + +[]∉map∷ : (List A ∋ []) ∉ map (x ∷_) xss +[]∉map∷ {xss = _ ∷ _} (there p) = []∉map∷ p + +map∷-decomp∈ : (List A ∋ x ∷ xs) ∈ map (y ∷_) xss → x ≡ y × xs ∈ xss +map∷-decomp∈ {xss = _ ∷ _} = λ where + (here refl) → refl , here refl + (there p) → map₂ there $ map∷-decomp∈ p + +map∷-decomp : xs ∈ map (y ∷_) xss → ∃[ ys ] ys ∈ xss × y ∷ ys ≡ xs +map∷-decomp {xss = _ ∷ _} (here refl) = -, here refl , refl +map∷-decomp {xs = []} {xss = _ ∷ _} (there xs∈) = contradiction xs∈ []∉map∷ +map∷-decomp {xs = x ∷ xs} {xss = _ ∷ _} (there xs∈) = + let eq , p = map∷-decomp∈ xs∈ + in -, there p , cong (_∷ _) (sym eq) + +∈-map∷⁻ : xs ∈ map (x ∷_) xss → x ∈ xs +∈-map∷⁻ {xss = _ ∷ _} = λ where + (here refl) → here refl + (there p) → ∈-map∷⁻ p diff --git a/src/Data/List/Membership/Propositional/Properties/Core.agda b/src/Data/List/Membership/Propositional/Properties/Core.agda index 5c77e40b96..65485abb0e 100644 --- a/src/Data/List/Membership/Propositional/Properties/Core.agda +++ b/src/Data/List/Membership/Propositional/Properties/Core.agda @@ -12,7 +12,7 @@ module Data.List.Membership.Propositional.Properties.Core where -open import Data.List.Base using (List) +open import Data.List.Base using (List; []) open import Data.List.Membership.Propositional open import Data.List.Relation.Unary.Any as Any using (Any; here; there) open import Data.Product.Base as Product using (_,_; ∃; _×_) @@ -30,6 +30,12 @@ private x : A xs : List A +------------------------------------------------------------------------ +-- Basics + +∉[] : x ∉ [] +∉[] () + ------------------------------------------------------------------------ -- find satisfies a simple equality when the predicate is a -- propositional equality. diff --git a/src/Data/List/Membership/Propositional/Properties/WithK.agda b/src/Data/List/Membership/Propositional/Properties/WithK.agda index a86f23a8ea..656ec11dae 100644 --- a/src/Data/List/Membership/Propositional/Properties/WithK.agda +++ b/src/Data/List/Membership/Propositional/Properties/WithK.agda @@ -9,17 +9,31 @@ module Data.List.Membership.Propositional.Properties.WithK where +open import Level using (Level) +open import Function.Bundles using (Equivalence) open import Data.List.Base open import Data.List.Relation.Unary.Unique.Propositional open import Data.List.Membership.Propositional import Data.List.Membership.Setoid.Properties as Membership +open import Data.List.Relation.Binary.BagAndSetEquality using (_∼[_]_; set; bag) +open import Data.Product using (_,_) open import Relation.Unary using (Irrelevant) open import Relation.Binary.PropositionalEquality.Properties as ≡ -open import Relation.Binary.PropositionalEquality.WithK +open import Relation.Binary.PropositionalEquality.WithK using (≡-irrelevant) + +private + variable + a : Level + A : Set a + xs ys : List A ------------------------------------------------------------------------ -- Irrelevance -unique⇒irrelevant : ∀ {a} {A : Set a} {xs : List A} → - Unique xs → Irrelevant (_∈ xs) +unique⇒irrelevant : Unique xs → Irrelevant (_∈ xs) unique⇒irrelevant = Membership.unique⇒irrelevant (≡.setoid _) ≡-irrelevant + +unique∧set⇒bag : Unique xs → Unique ys → xs ∼[ set ] ys → xs ∼[ bag ] ys +unique∧set⇒bag p p′ eq = record + { Equivalence eq + ; inverse = (λ _ → unique⇒irrelevant p′ _ _) , (λ _ → unique⇒irrelevant p _ _) } diff --git a/src/Data/List/Membership/Setoid/Properties.agda b/src/Data/List/Membership/Setoid/Properties.agda index 76bbd8beaf..c17fa15b98 100644 --- a/src/Data/List/Membership/Setoid/Properties.agda +++ b/src/Data/List/Membership/Setoid/Properties.agda @@ -1,4 +1,4 @@ ------------------------------------------------------------------------- +----------------------------------------------------------------------- -- The Agda standard library -- -- Properties related to setoid list membership @@ -21,11 +21,11 @@ import Data.List.Relation.Unary.All.Properties.Core as All import Data.List.Relation.Unary.Any.Properties as Any import Data.List.Relation.Unary.Unique.Setoid as Unique open import Data.Nat.Base using (suc; z>=-∈↔; ⊛-∈↔; ⊗-∈↔) import Data.List.Relation.Binary.Subset.Setoid.Properties as Subset open import Data.List.Relation.Binary.Subset.Propositional - using (_⊆_; _⊇_) + using (_⊆_; _⊇_; _⊈_) 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.Base using (ℕ; _≤_) import Data.Product.Base as Product -import Data.Sum.Base as Sum +open import Data.Sum.Base as Sum using (_⊎_) open import Effect.Monad open import Function.Base using (_∘_; _∘′_; id; _$_) open import Function.Bundles using (_↔_; Inverse; Equivalence) @@ -52,8 +52,19 @@ private a b p q : Level A : Set a B : Set b + x y : A ws xs ys zs : List A +------------------------------------------------------------------------ +-- Basics +------------------------------------------------------------------------ + +∷⊈[] : x ∷ xs ⊈ [] +∷⊈[] = Subset.∷⊈[] (setoid _) + +⊆[]⇒≡[] : ∀ {A : Set a} → (_⊆ []) ⋐ (_≡ []) +⊆[]⇒≡[] {A = A} = Subset.⊆[]⇒≡[] (setoid A) + ------------------------------------------------------------------------ -- Relational properties with _≋_ (pointwise equality) ------------------------------------------------------------------------ @@ -150,6 +161,12 @@ xs⊆x∷xs = Subset.xs⊆x∷xs (setoid _) ∈-∷⁺ʳ : ∀ {x} → x ∈ ys → xs ⊆ ys → x ∷ xs ⊆ ys ∈-∷⁺ʳ = Subset.∈-∷⁺ʳ (setoid _) +⊆∷⇒∈∨⊆ : xs ⊆ y ∷ ys → y ∈ xs ⊎ xs ⊆ ys +⊆∷⇒∈∨⊆ = Subset.⊆∷⇒∈∨⊆ (setoid _) + +⊆∷∧∉⇒⊆ : xs ⊆ y ∷ ys → y ∉ xs → xs ⊆ ys +⊆∷∧∉⇒⊆ = Subset.⊆∷∧∉⇒⊆ (setoid _) + ------------------------------------------------------------------------ -- _++_ @@ -179,6 +196,12 @@ module _ {xss yss : List (List A)} where Product.map₂ (Product.map₂ xss⊆yss) ∘ Inverse.from concat-∈↔ +------------------------------------------------------------------------ +-- concatMap + +concatMap⁺ : ∀ (f : A → List B) → xs ⊆ ys → concatMap f xs ⊆ concatMap f ys +concatMap⁺ _ = concat⁺ ∘ map⁺ _ + ------------------------------------------------------------------------ -- applyUpTo diff --git a/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda index 0d0d685a27..901ee8b942 100644 --- a/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda +++ b/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda @@ -22,7 +22,8 @@ import Data.List.Relation.Binary.Equality.Setoid as Equality import Data.List.Relation.Binary.Permutation.Setoid as Permutation import Data.List.Relation.Binary.Permutation.Setoid.Properties as Permutationₚ open import Data.Product.Base using (_,_) -open import Function.Base using (_∘_; _∘₂_; _$_) +open import Data.Sum.Base using (_⊎_; inj₁; inj₂) +open import Function.Base using (_∘_; _∘₂_; _$_; case_of_) open import Level using (Level) open import Relation.Nullary using (¬_; does; yes; no) open import Relation.Nullary.Negation using (contradiction) @@ -34,6 +35,7 @@ open import Relation.Binary.Bundles using (Setoid; Preorder) open import Relation.Binary.Structures using (IsPreorder) import Relation.Binary.Reasoning.Preorder as ≲-Reasoning open import Relation.Binary.Reasoning.Syntax +open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_) open Setoid using (Carrier) @@ -41,6 +43,22 @@ private variable a b p q r ℓ : Level +------------------------------------------------------------------------ +-- Basics +------------------------------------------------------------------------ + +module _ (S : Setoid a ℓ) where + + open Setoid S using (refl) + open Subset S + + ∷⊈[] : ∀ {x xs} → x ∷ xs ⊈ [] + ∷⊈[] p = Membershipₚ.∉[] S $ p (here refl) + + ⊆[]⇒≡[] : (_⊆ []) ⋐ (_≡ []) + ⊆[]⇒≡[] {x = []} _ = ≡.refl + ⊆[]⇒≡[] {x = _ ∷ _} p with () ← ∷⊈[] p + ------------------------------------------------------------------------ -- Relational properties with _≋_ (pointwise equality) ------------------------------------------------------------------------ @@ -161,12 +179,14 @@ module _ (S : Setoid a ℓ) where ------------------------------------------------------------------------ -- Properties of list functions +------------------------------------------------------------------------ + ------------------------------------------------------------------------ -- ∷ module _ (S : Setoid a ℓ) where - open Setoid S + open Setoid S renaming (Carrier to A) open Subset S open Membership S open Membershipₚ @@ -174,14 +194,31 @@ module _ (S : Setoid a ℓ) where xs⊆x∷xs : ∀ xs x → xs ⊆ x ∷ xs xs⊆x∷xs xs x = there - ∷⁺ʳ : ∀ {xs ys} x → xs ⊆ ys → x ∷ xs ⊆ x ∷ ys + private variable + x y : A + xs ys : List A + + ∷⁺ʳ : ∀ x → xs ⊆ ys → x ∷ xs ⊆ x ∷ ys ∷⁺ʳ x xs⊆ys (here p) = here p ∷⁺ʳ x xs⊆ys (there p) = there (xs⊆ys p) - ∈-∷⁺ʳ : ∀ {xs ys x} → x ∈ ys → xs ⊆ ys → x ∷ xs ⊆ ys + ∈-∷⁺ʳ : x ∈ ys → xs ⊆ ys → x ∷ xs ⊆ ys ∈-∷⁺ʳ x∈ys _ (here v≈x) = ∈-resp-≈ S (sym v≈x) x∈ys ∈-∷⁺ʳ _ xs⊆ys (there x∈xs) = xs⊆ys x∈xs + ⊆∷⇒∈∨⊆ : xs ⊆ y ∷ ys → y ∈ xs ⊎ xs ⊆ ys + ⊆∷⇒∈∨⊆ {xs = []} []⊆y∷ys = inj₂ λ () + ⊆∷⇒∈∨⊆ {xs = _ ∷ _} x∷xs⊆y∷ys with ⊆∷⇒∈∨⊆ $ x∷xs⊆y∷ys ∘ there + ... | inj₁ y∈xs = inj₁ $ there y∈xs + ... | inj₂ xs⊆ys with x∷xs⊆y∷ys (here refl) + ... | here x≈y = inj₁ $ here (sym x≈y) + ... | there x∈ys = inj₂ (∈-∷⁺ʳ x∈ys xs⊆ys) + + ⊆∷∧∉⇒⊆ : xs ⊆ y ∷ ys → y ∉ xs → xs ⊆ ys + ⊆∷∧∉⇒⊆ xs⊆y∷ys y∉xs with ⊆∷⇒∈∨⊆ xs⊆y∷ys + ... | inj₁ y∈xs = contradiction y∈xs y∉xs + ... | inj₂ xs⊆ys = xs⊆ys + ------------------------------------------------------------------------ -- ++ diff --git a/src/Data/List/Relation/Unary/Any/Properties.agda b/src/Data/List/Relation/Unary/Any/Properties.agda index 836e73d4a4..6f1df8cbcc 100644 --- a/src/Data/List/Relation/Unary/Any/Properties.agda +++ b/src/Data/List/Relation/Unary/Any/Properties.agda @@ -461,6 +461,17 @@ module _ {P : A → Set p} where concat↔ : ∀ {xss} → Any (Any P) xss ↔ Any P (concat xss) concat↔ {xss} = mk↔ₛ′ concat⁺ (concat⁻ xss) (concat⁺∘concat⁻ xss) concat⁻∘concat⁺ +------------------------------------------------------------------------ +-- concatMap + +module _ (f : A → List B) {p} {P : Pred B p} where + + concatMap⁺ : Any (Any P ∘ f) xs → Any P (concatMap f xs) + concatMap⁺ = concat⁺ ∘ map⁺ + + concatMap⁻ : Any P (concatMap f xs) → Any (Any P ∘ f) xs + concatMap⁻ = map⁻ ∘ concat⁻ _ + ------------------------------------------------------------------------ -- cartesianProductWith diff --git a/src/Data/List/Relation/Unary/Unique/Propositional/Properties.agda b/src/Data/List/Relation/Unary/Unique/Propositional/Properties.agda index bcd7df1176..8852bdd704 100644 --- a/src/Data/List/Relation/Unary/Unique/Propositional/Properties.agda +++ b/src/Data/List/Relation/Unary/Unique/Propositional/Properties.agda @@ -8,9 +8,12 @@ module Data.List.Relation.Unary.Unique.Propositional.Properties where -open import Data.List.Base using (map; _++_; concat; cartesianProductWith; - cartesianProduct; drop; take; applyUpTo; upTo; applyDownFrom; downFrom; - tabulate; allFin; filter) +open import Data.List.Base + using ( List; _∷_; map; _++_; concat; cartesianProductWith + ; cartesianProduct; drop; take; applyUpTo; upTo; applyDownFrom; downFrom + ; tabulate; allFin; filter + ) +open import Data.List.Membership.Propositional using (_∉_) open import Data.List.Relation.Binary.Disjoint.Propositional using (Disjoint) open import Data.List.Relation.Unary.All as All using (All; []; _∷_) @@ -35,6 +38,9 @@ open import Relation.Nullary.Negation using (¬_) private variable a b c p : Level + A : Set a + x y : A + xs : List A ------------------------------------------------------------------------ -- Introduction (⁺) and elimination (⁻) rules for list operations @@ -154,3 +160,9 @@ module _ {A : Set a} {P : Pred _ p} (P? : Decidable P) where filter⁺ : ∀ {xs} → Unique xs → Unique (filter P? xs) filter⁺ = Setoid.filter⁺ (setoid A) P? + +------------------------------------------------------------------------ +-- ∷ + +Unique[x∷xs]⇒x∉xs : Unique (x ∷ xs) → x ∉ xs +Unique[x∷xs]⇒x∉xs = Setoid.Unique[x∷xs]⇒x∉xs (setoid _) diff --git a/src/Data/List/Relation/Unary/Unique/Setoid/Properties.agda b/src/Data/List/Relation/Unary/Unique/Setoid/Properties.agda index ffb587018a..0dc7027c79 100644 --- a/src/Data/List/Relation/Unary/Unique/Setoid/Properties.agda +++ b/src/Data/List/Relation/Unary/Unique/Setoid/Properties.agda @@ -9,9 +9,11 @@ module Data.List.Relation.Unary.Unique.Setoid.Properties where open import Data.List.Base +import Data.List.Membership.Setoid as Membership open import Data.List.Membership.Setoid.Properties open import Data.List.Relation.Binary.Disjoint.Setoid open import Data.List.Relation.Binary.Disjoint.Setoid.Properties +open import Data.List.Relation.Unary.Any using (here; there) open import Data.List.Relation.Unary.All as All using (All; []; _∷_) open import Data.List.Relation.Unary.All.Properties using (All¬⇒¬Any) open import Data.List.Relation.Unary.AllPairs as AllPairs using (AllPairs) @@ -156,3 +158,21 @@ module _ (S : Setoid a ℓ) {P : Pred _ p} (P? : Decidable P) where filter⁺ : ∀ {xs} → Unique S xs → Unique S (filter P? xs) filter⁺ = AllPairs.filter⁺ P? + +------------------------------------------------------------------------ +-- ∷ + +module _ (S : Setoid a ℓ) where + + open Setoid S renaming (Carrier to A) + open Membership S using (_∉_) + + private + variable + x y : A + xs : List A + + Unique[x∷xs]⇒x∉xs : Unique S (x ∷ xs) → x ∉ xs + Unique[x∷xs]⇒x∉xs ((x≉ ∷ x∉) ∷ _ ∷ uniq) = λ where + (here x≈) → x≉ x≈ + (there x∈) → Unique[x∷xs]⇒x∉xs (x∉ AllPairs.∷ uniq) x∈ From fc54cfbbb7ccb75a6478905706b766c307b43a86 Mon Sep 17 00:00:00 2001 From: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com> Date: Sat, 28 Sep 2024 06:50:10 +0100 Subject: [PATCH 3/5] add properties/structures/bundles related to decidability (#2481) --- CHANGELOG.md | 11 +++ .../Binary/Construct/Interior/Symmetric.agda | 80 +++++++++++++------ 2 files changed, 68 insertions(+), 23 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index a513e4978f..304ff75e5a 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -270,6 +270,17 @@ Additions to existing modules _≡?_ : DecidableEquality (Vec A n) ``` +* In `Relation.Binary.Construct.Interior.Symmetric`: + ```agda + decidable : Decidable R → Decidable (SymInterior R) + ``` + and for `Reflexive` and `Transitive` relations `R`: + ```agda + isDecEquivalence : Decidable R → IsDecEquivalence (SymInterior R) + isDecPartialOrder : Decidable R → IsDecPartialOrder (SymInterior R) R + decPoset : Decidable R → DecPoset _ _ _ + ``` + * In `Relation.Nullary.Decidable`: ```agda does-⇔ : A ⇔ B → (a? : Dec A) → (b? : Dec B) → does a? ≡ does b? diff --git a/src/Relation/Binary/Construct/Interior/Symmetric.agda b/src/Relation/Binary/Construct/Interior/Symmetric.agda index a954dc99ec..50b75b309d 100644 --- a/src/Relation/Binary/Construct/Interior/Symmetric.agda +++ b/src/Relation/Binary/Construct/Interior/Symmetric.agda @@ -8,15 +8,18 @@ module Relation.Binary.Construct.Interior.Symmetric where -open import Function.Base using (flip) -open import Level +open import Data.Bool.Base using (_∧_) +open import Function.Base using (flip; _∘_) +open import Level using (Level) open import Relation.Binary +open import Relation.Nullary.Decidable.Core +open import Relation.Nullary.Reflects private variable - a b c ℓ r s t : Level + a ℓ : Level A : Set a - R S T : Rel A r + R S T : Rel A ℓ ------------------------------------------------------------------------ -- Definition @@ -56,28 +59,59 @@ transitive tr = trans tr tr asymmetric⇒empty : Asymmetric R → Empty (SymInterior R) asymmetric⇒empty asym (r , r′) = asym r r′ +-- Decidability +decidable : Decidable R → Decidable (SymInterior R) +does (decidable R? x y) = does (R? x y) ∧ does (R? y x) +proof (decidable R? x y) = proof (R? x y) reflects proof (R? y x) + where + _reflects_ : ∀ {bxy byx} → Reflects (R x y) bxy → Reflects (R y x) byx → + Reflects (SymInterior R x y) (bxy ∧ byx) + ofʸ rxy reflects ofʸ ryx = of (rxy , ryx) + ofʸ rxy reflects ofⁿ ¬ryx = of (¬ryx ∘ rhs≤lhs) + ofⁿ ¬rxy reflects _ = of (¬rxy ∘ lhs≤rhs) + -- A reflexive transitive relation _≤_ gives rise to a poset in which the -- equivalence relation is SymInterior _≤_. -isEquivalence : Reflexive R → Transitive R → IsEquivalence (SymInterior R) -isEquivalence refl trans = record - { refl = reflexive refl - ; sym = symmetric - ; trans = transitive trans - } - -isPartialOrder : Reflexive R → Transitive R → IsPartialOrder (SymInterior R) R -isPartialOrder refl trans = record - { isPreorder = record - { isEquivalence = isEquivalence refl trans +module _ {R : Rel A ℓ} (refl : Reflexive R) (trans : Transitive R) where + + isEquivalence : IsEquivalence (SymInterior R) + isEquivalence = record + { refl = reflexive refl + ; sym = symmetric + ; trans = transitive trans + } + + isPreorder : IsPreorder (SymInterior R) R + isPreorder = record + { isEquivalence = isEquivalence ; reflexive = lhs≤rhs ; trans = trans } - ; antisym = _,_ - } - -poset : ∀ {a} {A : Set a} {R : Rel A ℓ} → Reflexive R → Transitive R → Poset a ℓ ℓ -poset {R = R} refl trans = record - { _≤_ = R - ; isPartialOrder = isPartialOrder refl trans - } + + isPartialOrder : IsPartialOrder (SymInterior R) R + isPartialOrder = record + { isPreorder = isPreorder + ; antisym = _,_ + } + + poset : Poset _ ℓ ℓ + poset = record { isPartialOrder = isPartialOrder } + + module _ (R? : Decidable R) where + + isDecEquivalence : IsDecEquivalence (SymInterior R) + isDecEquivalence = record + { isEquivalence = isEquivalence + ; _≟_ = decidable R? + } + + isDecPartialOrder : IsDecPartialOrder (SymInterior R) R + isDecPartialOrder = record + { isPartialOrder = isPartialOrder + ; _≟_ = decidable R? + ; _≤?_ = R? + } + + decPoset : DecPoset _ ℓ ℓ + decPoset = record { isDecPartialOrder = isDecPartialOrder } From d13d1ef00af23fc0b55a90870437ff28c860e6c0 Mon Sep 17 00:00:00 2001 From: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com> Date: Sat, 28 Sep 2024 07:29:01 +0100 Subject: [PATCH 4/5] fixes #2466 (#2478) Co-authored-by: MatthewDaggitt --- CHANGELOG.md | 2 ++ src/Data/List/Membership/Setoid/Properties.agda | 10 +++++++++- 2 files changed, 11 insertions(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 304ff75e5a..5e52a3ae66 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -125,6 +125,8 @@ Additions to existing modules * In `Data.List.Membership.Setoid.Properties`: ```agda + ∉⇒All[≉] : x ∉ xs → All (x ≉_) xs + All[≉]⇒∉ : All (x ≉_) xs → x ∉ xs Any-∈-swap : Any (_∈ ys) xs → Any (_∈ xs) ys All-∉-swap : All (_∉ ys) xs → All (_∉ xs) ys ∈-map∘filter⁻ : y ∈₂ map f (filter P? xs) → ∃[ x ] x ∈₁ xs × y ≈₂ f x × P x diff --git a/src/Data/List/Membership/Setoid/Properties.agda b/src/Data/List/Membership/Setoid/Properties.agda index c17fa15b98..988c01a07e 100644 --- a/src/Data/List/Membership/Setoid/Properties.agda +++ b/src/Data/List/Membership/Setoid/Properties.agda @@ -75,6 +75,14 @@ module _ (S : Setoid c ℓ) where ∉-resp-≋ : ∀ {x} → (x ∉_) Respects _≋_ ∉-resp-≋ xs≋ys v∉xs v∈ys = v∉xs (∈-resp-≋ (≋-sym xs≋ys) v∈ys) + -- x ∉_ is equivalent to All (x ≉_) + + ∉⇒All[≉] : ∀ {x xs} → x ∉ xs → All (x ≉_) xs + ∉⇒All[≉] = All.¬Any⇒All¬ _ + + All[≉]⇒∉ : ∀ {x xs} → All (x ≉_) xs → x ∉ xs + All[≉]⇒∉ = All.All¬⇒¬Any + -- index is injective in its first argument. index-injective : ∀ {x₁ x₂ xs} (x₁∈xs : x₁ ∈ xs) (x₂∈xs : x₂ ∈ xs) → @@ -93,7 +101,7 @@ module _ (S : Setoid c ℓ) where private ∉×∈⇒≉ : ∀ {x y xs} → All (y ≉_) xs → x ∈ xs → x ≉ y - ∉×∈⇒≉ = All.lookupWith λ y≉z x≈z x≈y → y≉z (trans (sym x≈y) x≈z) + ∉×∈⇒≉ ≉s x∈xs x≈y = All[≉]⇒∉ S ≉s (∈-resp-≈ S x≈y x∈xs) unique⇒irrelevant : Binary.Irrelevant _≈_ → ∀ {xs} → Unique xs → Unary.Irrelevant (_∈ xs) unique⇒irrelevant ≈-irr _ (here p) (here q) = From 45a46f7691c328364856eeda8b042bf6f389d8a8 Mon Sep 17 00:00:00 2001 From: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com> Date: Sat, 28 Sep 2024 07:34:04 +0100 Subject: [PATCH 5/5] Refactor `Data.List.Relation.Binary.Permutation.*`, part I (#2333) * move `steps` towards deprecation in `Homogeneous` * deprecate `steps`; refactor `Setoid` proofs and equaiotnal reasoning combinators * extensive refactoring * tidy up * add equivalence with `Setoid` representation * removed buggy `PermutationReasoning` syntax * refactored; removed buggy `PermutationReasoning` syntax * `CHANGELOG` * final fix-ups * tighten `import`s * tighten `import`s * redundant constructor aliases * fix-up `Reasoning` steps with the alias * use aliases * more `import` tightening * refactor: encapsulate and tighten up * avoid `PermutationReasoning` custom combinators * fix up `CHANGELOG` * encapsulate helper function * revert changes * review comments * `fix-whitespace` * toned down the comment on `steps` * remove use of infix `insert` * revert other deprecation * no need for qualification * remove deprecation banner * three paras of commentary on the new transitivity proofs * missing entry * missing terminator * response to review comments * `with` to `let` * fixed `BagAndSetEquality` * fixed qualified `import` bug introduced during merge conflict resolution * Update CHANGELOG.md Deleted spurious attribution of the lemmas in `Data.List.Properties` about `product` to `Data.List.Relation.Unary.All.Properties`. Hope this fixes things now! --------- Co-authored-by: MatthewDaggitt --- CHANGELOG.md | 60 +- .../Relation/Binary/BagAndSetEquality.agda | 29 +- .../Binary/Permutation/Homogeneous.agda | 12 +- .../Binary/Permutation/Propositional.agda | 65 ++- .../Permutation/Propositional/Properties.agda | 181 +++--- .../Relation/Binary/Permutation/Setoid.agda | 105 ++-- .../Binary/Permutation/Setoid/Properties.agda | 530 +++++++++--------- 7 files changed, 551 insertions(+), 431 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 5e52a3ae66..443c8de9b3 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -59,6 +59,13 @@ Deprecated names normalise-correct ↦ Algebra.Solver.Monoid.Normal.correct ``` +* In `Data.List.Relation.Binary.Permutation.Setoid.Properties`: + ```agda + split ↦ ↭-split + ``` + with a more informative type (see below). + ``` + * In `Data.Vec.Properties`: ```agda ++-assoc _ ↦ ++-assoc-eqFree @@ -167,11 +174,6 @@ Additions to existing modules concatMap-++ : concatMap f (xs ++ ys) ≡ concatMap f xs ++ concatMap f ys ``` -* In `Data.List.Relation.Unary.All`: - ```agda - search : Decidable P → ∀ xs → All (∁ P) xs ⊎ Any P xs - ``` - * In `Data.List.Relation.Unary.Any.Properties`: ```agda concatMap⁺ : Any (Any P ∘ f) xs → Any P (concatMap f xs) @@ -194,12 +196,60 @@ Additions to existing modules ++⁺ˡ : ∀ zs → ws ≋ xs → ws ++ zs ≋ xs ++ zs ``` +* In `Data.List.Relation.Binary.Permutation.Homogeneous`: + ```agda + steps : Permutation R xs ys → ℕ + ``` + +* In `Data.List.Relation.Binary.Permutation.Propositional`: + constructor aliases + ```agda + ↭-refl : Reflexive _↭_ + ↭-prep : ∀ x → xs ↭ ys → x ∷ xs ↭ x ∷ ys + ↭-swap : ∀ x y → xs ↭ ys → x ∷ y ∷ xs ↭ y ∷ x ∷ ys + ``` + and properties + ```agda + ↭-reflexive-≋ : _≋_ ⇒ _↭_ + ↭⇒↭ₛ : _↭_ ⇒ _↭ₛ_ + ↭ₛ⇒↭ : _↭ₛ_ ⇒ _↭_ + ``` + where `_↭ₛ_` is the `Setoid (setoid _)` instance of `Permutation` + +* In `Data.List.Relation.Binary.Permutation.Propositional.Properties`: + ```agda + Any-resp-[σ∘σ⁻¹] : (σ : xs ↭ ys) (iy : Any P ys) → + Any-resp-↭ (trans (↭-sym σ) σ) iy ≡ iy + ∈-resp-[σ∘σ⁻¹] : (σ : xs ↭ ys) (iy : y ∈ ys) → + ∈-resp-↭ (trans (↭-sym σ) σ) iy ≡ iy + product-↭ : product Preserves _↭_ ⟶ _≡_ + ``` + +* In `Data.List.Relation.Binary.Permutation.Setoid`: + ```agda + ↭-reflexive-≋ : _≋_ ⇒ _↭_ + ↭-transˡ-≋ : LeftTrans _≋_ _↭_ + ↭-transʳ-≋ : RightTrans _↭_ _≋_ + ↭-trans′ : Transitive _↭_ + ``` + +* In `Data.List.Relation.Binary.Permutation.Setoid.Properties`: + ```agda + ↭-split : xs ↭ (as ++ [ v ] ++ bs) → + ∃₂ λ ps qs → xs ≋ (ps ++ [ v ] ++ qs) × (ps ++ qs) ↭ (as ++ bs) + drop-∷ : x ∷ xs ↭ x ∷ ys → xs ↭ ys + ``` + * In `Data.List.Relation.Binary.Pointwise`: ```agda ++⁺ʳ : Reflexive R → ∀ xs → (xs ++_) Preserves (Pointwise R) ⟶ (Pointwise R) ++⁺ˡ : Reflexive R → ∀ zs → (_++ zs) Preserves (Pointwise R) ⟶ (Pointwise R) ``` +* In `Data.List.Relation.Unary.All`: + ```agda + search : Decidable P → ∀ xs → All (∁ P) xs ⊎ Any P xs + * In `Data.List.Relation.Binary.Subset.Setoid.Properties`: ```agda ∷⊈[] : x ∷ xs ⊈ [] diff --git a/src/Data/List/Relation/Binary/BagAndSetEquality.agda b/src/Data/List/Relation/Binary/BagAndSetEquality.agda index 815b27db89..b27e45d585 100644 --- a/src/Data/List/Relation/Binary/BagAndSetEquality.agda +++ b/src/Data/List/Relation/Binary/BagAndSetEquality.agda @@ -27,9 +27,9 @@ 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 (_↭_; ↭-sym; refl; module PermutationReasoning) + using (_↭_; ↭-refl; ↭-sym; ↭-prep; module PermutationReasoning) open import Data.List.Relation.Binary.Permutation.Propositional.Properties - using (∈-resp-↭; ∈-resp-[σ⁻¹∘σ]; ↭-sym-involutive; shift; ++-comm) + using (∈-resp-↭; ∈-resp-[σ⁻¹∘σ]; ∈-resp-[σ∘σ⁻¹]; shift; ++-comm) open import Data.Product.Base as Product using (∃; _,_; proj₁; proj₂; _×_) import Data.Product.Function.Dependent.Propositional as Σ open import Data.Sum.Base as Sum using (_⊎_; [_,_]′; inj₁; inj₂) @@ -574,29 +574,18 @@ drop-cons {x = x} {xs} {ys} x∷xs≈x∷ys = ------------------------------------------------------------------------ --- Relationships to other relations +-- Relationships to propositional permutation ↭⇒∼bag : _↭_ {A = A} ⇒ _∼[ bag ]_ -↭⇒∼bag xs↭ys {v} = mk↔ₛ′ (to xs↭ys) (from xs↭ys) (to∘from xs↭ys) (from∘to xs↭ys) - where - to : ∀ {xs ys} → xs ↭ ys → v ∈ xs → v ∈ ys - to xs↭ys = ∈-resp-↭ xs↭ys - - from : ∀ {xs ys} → xs ↭ ys → v ∈ ys → v ∈ xs - from xs↭ys = ∈-resp-↭ (↭-sym xs↭ys) - - from∘to : ∀ {xs ys} (p : xs ↭ ys) (q : v ∈ xs) → from p (to p q) ≡ q - from∘to = ∈-resp-[σ⁻¹∘σ] - - to∘from : ∀ {xs ys} (p : xs ↭ ys) (q : v ∈ ys) → to p (from p q) ≡ q - to∘from p with res ← from∘to (↭-sym p) rewrite ↭-sym-involutive p = res +↭⇒∼bag xs↭ys {v} = + mk↔ₛ′ (∈-resp-↭ xs↭ys) (∈-resp-↭ (↭-sym xs↭ys)) (∈-resp-[σ∘σ⁻¹] xs↭ys) (∈-resp-[σ⁻¹∘σ] xs↭ys) ∼bag⇒↭ : _∼[ bag ]_ ⇒ _↭_ {A = A} -∼bag⇒↭ {A = A} {[]} eq with refl ← empty-unique (↔-sym eq) = refl +∼bag⇒↭ {A = A} {[]} eq with refl ← empty-unique (↔-sym eq) = ↭-refl ∼bag⇒↭ {A = A} {x ∷ xs} eq - with zs₁ , zs₂ , p ← ∈-∃++ (Inverse.to (eq {x}) (here ≡.refl)) rewrite p = begin - x ∷ xs <⟨ ∼bag⇒↭ (drop-cons (↔-trans eq (comm zs₁ (x ∷ zs₂)))) ⟩ - x ∷ (zs₂ ++ zs₁) <⟨ ++-comm zs₂ zs₁ ⟩ + with zs₁ , zs₂ , refl ← ∈-∃++ (Inverse.to (eq {x}) (here refl)) = begin + x ∷ xs ↭⟨ ↭-prep x (∼bag⇒↭ (drop-cons (↔-trans eq (comm zs₁ (x ∷ zs₂))))) ⟩ + x ∷ (zs₂ ++ zs₁) ↭⟨ ↭-prep x (++-comm zs₂ zs₁) ⟩ x ∷ (zs₁ ++ zs₂) ↭⟨ shift x zs₁ zs₂ ⟨ zs₁ ++ x ∷ zs₂ ∎ where diff --git a/src/Data/List/Relation/Binary/Permutation/Homogeneous.agda b/src/Data/List/Relation/Binary/Permutation/Homogeneous.agda index 12015b3076..686c569423 100644 --- a/src/Data/List/Relation/Binary/Permutation/Homogeneous.agda +++ b/src/Data/List/Relation/Binary/Permutation/Homogeneous.agda @@ -11,8 +11,8 @@ 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) +import Data.List.Relation.Binary.Pointwise.Properties as Pointwise +open import Data.Nat.Base using (ℕ; suc; _+_) open import Level using (Level; _⊔_) open import Relation.Binary.Core using (Rel; _⇒_) open import Relation.Binary.Bundles using (Setoid) @@ -59,3 +59,11 @@ 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) + +-- Measures the number of constructors, can be useful for termination proofs + +steps : ∀ {R : Rel A r} {xs ys} → Permutation R xs ys → ℕ +steps (refl _) = 1 +steps (prep _ xs↭ys) = suc (steps xs↭ys) +steps (swap _ _ xs↭ys) = suc (steps xs↭ys) +steps (trans xs↭ys ys↭zs) = steps xs↭ys + steps ys↭zs diff --git a/src/Data/List/Relation/Binary/Permutation/Propositional.agda b/src/Data/List/Relation/Binary/Permutation/Propositional.agda index c41793d28a..0e13a5e3ba 100644 --- a/src/Data/List/Relation/Binary/Permutation/Propositional.agda +++ b/src/Data/List/Relation/Binary/Permutation/Propositional.agda @@ -10,14 +10,22 @@ module Data.List.Relation.Binary.Permutation.Propositional {a} {A : Set a} where open import Data.List.Base using (List; []; _∷_) +open import Data.List.Relation.Binary.Equality.Propositional using (_≋_; ≋⇒≡) 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) +open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; refl) import Relation.Binary.Reasoning.Setoid as EqReasoning open import Relation.Binary.Reasoning.Syntax +import Data.List.Relation.Binary.Permutation.Setoid as Permutation + +private + variable + x y z v w : A + ws xs ys zs : List A + ------------------------------------------------------------------------ -- An inductive definition of permutation @@ -30,21 +38,32 @@ open import Relation.Binary.Reasoning.Syntax 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 + refl : xs ↭ xs + prep : ∀ x → xs ↭ ys → x ∷ xs ↭ x ∷ ys + swap : ∀ x y → xs ↭ ys → x ∷ y ∷ xs ↭ y ∷ x ∷ ys + trans : xs ↭ ys → ys ↭ zs → xs ↭ zs + +-- Constructor aliases + +↭-refl : Reflexive _↭_ +↭-refl = refl + +↭-prep : ∀ x → xs ↭ ys → x ∷ xs ↭ x ∷ ys +↭-prep = prep + +↭-swap : ∀ x y → xs ↭ ys → x ∷ y ∷ xs ↭ y ∷ x ∷ ys +↭-swap = swap ------------------------------------------------------------------------ -- _↭_ is an equivalence ↭-reflexive : _≡_ ⇒ _↭_ -↭-reflexive refl = refl +↭-reflexive refl = ↭-refl -↭-refl : Reflexive _↭_ -↭-refl = refl +↭-reflexive-≋ : _≋_ ⇒ _↭_ +↭-reflexive-≋ xs≋ys = ↭-reflexive (≋⇒≡ xs≋ys) -↭-sym : ∀ {xs ys} → xs ↭ ys → ys ↭ xs +↭-sym : 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) @@ -58,7 +77,7 @@ data _↭_ : Rel (List A) a where ↭-isEquivalence : IsEquivalence _↭_ ↭-isEquivalence = record - { refl = refl + { refl = ↭-refl ; sym = ↭-sym ; trans = ↭-trans } @@ -68,6 +87,28 @@ data _↭_ : Rel (List A) a where { isEquivalence = ↭-isEquivalence } +------------------------------------------------------------------------ +-- _↭_ is equivalent to `Setoid`-based permutation + +private + open module ↭ₛ = Permutation (≡.setoid A) + using () + renaming (_↭_ to _↭ₛ_) + +↭⇒↭ₛ : xs ↭ ys → xs ↭ₛ ys +↭⇒↭ₛ refl = ↭ₛ.↭-refl +↭⇒↭ₛ (prep x p) = ↭ₛ.↭-prep x (↭⇒↭ₛ p) +↭⇒↭ₛ (swap x y p) = ↭ₛ.↭-swap x y (↭⇒↭ₛ p) +↭⇒↭ₛ (trans p q) = ↭ₛ.↭-trans′ (↭⇒↭ₛ p) (↭⇒↭ₛ q) + + +↭ₛ⇒↭ : _↭ₛ_ ⇒ _↭_ +↭ₛ⇒↭ (↭ₛ.refl xs≋ys) = ↭-reflexive-≋ xs≋ys +↭ₛ⇒↭ (↭ₛ.prep refl p) = ↭-prep _ (↭ₛ⇒↭ p) +↭ₛ⇒↭ (↭ₛ.swap refl refl p) = ↭-swap _ _ (↭ₛ⇒↭ p) +↭ₛ⇒↭ (↭ₛ.trans p q) = ↭-trans (↭ₛ⇒↭ p) (↭ₛ⇒↭ q) + + ------------------------------------------------------------------------ -- A reasoning API to chain permutation proofs and allow "zooming in" -- to localised reasoning. @@ -89,12 +130,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 6fe439ed03..30cd2bdcc0 100644 --- a/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda +++ b/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda @@ -12,16 +12,16 @@ 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.Product.Base using (-,_; proj₂) +open import Data.Nat.Base using (ℕ; suc) +import Data.Nat.Properties as ℕ +open import Data.Product.Base using (-,_) open import Data.List.Base as List open import Data.List.Relation.Binary.Permutation.Propositional open import Data.List.Relation.Unary.Any using (Any; here; there) open import Data.List.Relation.Unary.All using (All; []; _∷_) open import Data.List.Membership.Propositional open import Data.List.Membership.Propositional.Properties -import Data.List.Properties as Lₚ +import Data.List.Properties as List open import Data.Product.Base using (_,_; _×_; ∃; ∃₂) open import Data.Maybe.Base using (Maybe; just; nothing) open import Function.Base using (_∘_; _⟨_⟩_; _$_) @@ -34,6 +34,8 @@ open import Relation.Binary.PropositionalEquality.Core as ≡ open import Relation.Binary.PropositionalEquality.Properties using (module ≡-Reasoning) open import Relation.Nullary +import Data.List.Relation.Binary.Permutation.Setoid.Properties as Permutation + private variable a b p : Level @@ -70,49 +72,58 @@ private ------------------------------------------------------------------------ -- Relationships to other predicates -All-resp-↭ : ∀ {P : Pred A p} → (All P) Respects _↭_ -All-resp-↭ refl wit = wit -All-resp-↭ (prep x p) (px ∷ wit) = px ∷ All-resp-↭ p wit -All-resp-↭ (swap x y p) (px ∷ py ∷ wit) = py ∷ px ∷ All-resp-↭ p wit -All-resp-↭ (trans p₁ p₂) wit = All-resp-↭ p₂ (All-resp-↭ p₁ wit) - -Any-resp-↭ : ∀ {P : Pred A p} → (Any P) Respects _↭_ -Any-resp-↭ refl wit = wit -Any-resp-↭ (prep x p) (here px) = here px -Any-resp-↭ (prep x p) (there wit) = there (Any-resp-↭ p wit) -Any-resp-↭ (swap x y p) (here px) = there (here px) -Any-resp-↭ (swap x y p) (there (here px)) = here px -Any-resp-↭ (swap x y p) (there (there wit)) = there (there (Any-resp-↭ p wit)) -Any-resp-↭ (trans p p₁) wit = Any-resp-↭ p₁ (Any-resp-↭ p wit) +module _ {P : Pred A p} where + + All-resp-↭ : (All P) Respects _↭_ + All-resp-↭ refl wit = wit + All-resp-↭ (prep x p) (px ∷ wit) = px ∷ All-resp-↭ p wit + All-resp-↭ (swap x y p) (px ∷ py ∷ wit) = py ∷ px ∷ All-resp-↭ p wit + All-resp-↭ (trans p₁ p₂) wit = All-resp-↭ p₂ (All-resp-↭ p₁ wit) + + Any-resp-↭ : (Any P) Respects _↭_ + Any-resp-↭ refl wit = wit + Any-resp-↭ (prep x p) (here px) = here px + Any-resp-↭ (prep x p) (there wit) = there (Any-resp-↭ p wit) + Any-resp-↭ (swap x y p) (here px) = there (here px) + Any-resp-↭ (swap x y p) (there (here px)) = here px + Any-resp-↭ (swap x y p) (there (there wit)) = there (there (Any-resp-↭ p wit)) + Any-resp-↭ (trans p p₁) wit = Any-resp-↭ p₁ (Any-resp-↭ p wit) + + Any-resp-[σ⁻¹∘σ] : ∀ {xs ys} (σ : 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-[σ⁻¹∘σ] (trans σ₁ σ₂) ix + rewrite Any-resp-[σ⁻¹∘σ] σ₂ (Any-resp-↭ σ₁ ix) + rewrite Any-resp-[σ⁻¹∘σ] σ₁ ix + = refl + Any-resp-[σ⁻¹∘σ] (prep _ σ) (there ix) + rewrite Any-resp-[σ⁻¹∘σ] σ ix + = refl + Any-resp-[σ⁻¹∘σ] (swap _ _ σ) (there (there ix)) + rewrite Any-resp-[σ⁻¹∘σ] σ ix + = refl + + Any-resp-[σ∘σ⁻¹] : ∀ {xs ys} (σ : xs ↭ ys) (iy : Any P ys) → + Any-resp-↭ (trans (↭-sym σ) σ) iy ≡ iy + Any-resp-[σ∘σ⁻¹] p + with res ← Any-resp-[σ⁻¹∘σ] (↭-sym p) + rewrite ↭-sym-involutive p + = res ∈-resp-↭ : ∀ {x : A} → (x ∈_) Respects _↭_ ∈-resp-↭ = Any-resp-↭ -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-[σ⁻¹∘σ] (trans σ₁ σ₂) ix - rewrite Any-resp-[σ⁻¹∘σ] σ₂ (Any-resp-↭ σ₁ ix) - rewrite Any-resp-[σ⁻¹∘σ] σ₁ ix - = refl -Any-resp-[σ⁻¹∘σ] (prep _ σ) (there ix) - rewrite Any-resp-[σ⁻¹∘σ] σ ix - = refl -Any-resp-[σ⁻¹∘σ] (swap _ _ σ) (there (there ix)) - rewrite Any-resp-[σ⁻¹∘σ] σ ix - = refl - -∈-resp-[σ⁻¹∘σ] : {xs ys : List A} {x : A} → - (σ : xs ↭ ys) → - (ix : x ∈ xs) → +∈-resp-[σ⁻¹∘σ] : ∀ {xs ys} {x : A} (σ : xs ↭ ys) (ix : x ∈ xs) → ∈-resp-↭ (trans σ (↭-sym σ)) ix ≡ ix ∈-resp-[σ⁻¹∘σ] = Any-resp-[σ⁻¹∘σ] +∈-resp-[σ∘σ⁻¹] : ∀ {xs ys} {y : A} (σ : xs ↭ ys) (iy : y ∈ ys) → + ∈-resp-↭ (trans (↭-sym σ) σ) iy ≡ iy +∈-resp-[σ∘σ⁻¹] = Any-resp-[σ∘σ⁻¹] + ------------------------------------------------------------------------ -- map @@ -171,64 +182,63 @@ inject v ws↭ys xs↭zs = trans (++⁺ˡ _ (prep v xs↭zs)) (++⁺ʳ _ ws↭ys shift : ∀ v (xs ys : List A) → xs ++ [ v ] ++ ys ↭ v ∷ xs ++ ys shift v [] ys = refl shift v (x ∷ xs) ys = begin - x ∷ (xs ++ [ v ] ++ ys) <⟨ shift v xs ys ⟩ - x ∷ v ∷ xs ++ ys <<⟨ refl ⟩ + x ∷ (xs ++ [ v ] ++ ys) ↭⟨ prep _ (shift v xs ys) ⟩ + x ∷ v ∷ xs ++ ys ↭⟨ swap _ _ refl ⟩ v ∷ x ∷ xs ++ ys ∎ where open PermutationReasoning 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-≡ [] [] eq + with refl ← List.∷-injectiveʳ eq = 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′) +drop-mid-≡ (w ∷ ws) (x ∷ xs) eq + with refl , eq′ ← List.∷-injective 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 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″ → + drop-mid′ : ∀ {as bs} → as ↭ bs → + ∀ {x : A} ws xs {ys zs} → + as ≡ ws ++ [ x ] ++ ys → + bs ≡ xs ++ [ x ] ++ zs → 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′ refl ws xs refl eq = drop-mid-≡ ws xs eq + drop-mid′ (trans p q) ws xs refl refl + with h , t , refl ← ∈-∃++ (∈-resp-↭ p (∈-insert ws)) + = trans (drop-mid ws h p) (drop-mid h xs q) + drop-mid′ (prep x p) [] [] refl eq + with refl ← List.∷-injectiveʳ eq = 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′ (prep x p) (w ∷ ws) (x ∷ xs) refl refl = prep _ (drop-mid ws xs p) 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 ∷ []) refl eq + with refl , eq′ ← List.∷-injective eq + with refl ← List.∷-injectiveʳ eq′ = 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 ∷ []) [] refl eq + with refl ← List.∷-injectiveʳ eq = 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 ⟩ + _ ∷ _ ↭⟨ prep _ p ⟩ + _ ∷ (xs ++ _ ∷ _) ↭⟨ prep _ (shift _ _ _) ⟩ + _ ∷ _ ∷ xs ++ _ ↭⟨ swap _ _ refl ⟩ _ ∷ _ ∷ xs ++ _ ∎ where open PermutationReasoning drop-mid′ (swap y z p) (y ∷ z ∷ ws) (z ∷ []) refl refl = begin - _ ∷ _ ∷ ws ++ _ <<⟨ refl ⟩ - _ ∷ (_ ∷ ws ++ _) <⟨ ↭-sym (shift _ _ _) ⟩ - _ ∷ (ws ++ _ ∷ _) <⟨ p ⟩ + _ ∷ _ ∷ ws ++ _ ↭⟨ swap _ _ refl ⟩ + _ ∷ (_ ∷ ws ++ _) ↭⟨ prep _ (shift _ _ _) ⟨ + _ ∷ (ws ++ _ ∷ _) ↭⟨ prep _ 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) + -- Algebraic properties @@ -236,18 +246,18 @@ drop-mid {A = A} {x} ws xs p = drop-mid′ p ws xs refl refl ++-identityˡ xs = refl ++-identityʳ : RightIdentity {A = List A} _↭_ [] _++_ -++-identityʳ xs = ↭-reflexive (Lₚ.++-identityʳ xs) +++-identityʳ xs = ↭-reflexive (List.++-identityʳ xs) ++-identity : Identity {A = List A} _↭_ [] _++_ ++-identity = ++-identityˡ , ++-identityʳ ++-assoc : Associative {A = List A} _↭_ _++_ -++-assoc xs ys zs = ↭-reflexive (Lₚ.++-assoc xs ys zs) +++-assoc xs ys zs = ↭-reflexive (List.++-assoc xs ys zs) ++-comm : Commutative {A = List A} _↭_ _++_ ++-comm [] ys = ↭-sym (++-identityʳ ys) ++-comm (x ∷ xs) ys = begin - x ∷ xs ++ ys <⟨ ++-comm xs ys ⟩ + x ∷ xs ++ ys ↭⟨ prep _ (++-comm xs ys) ⟩ x ∷ ys ++ xs ↭⟨ shift x ys xs ⟨ ys ++ (x ∷ xs) ∎ where open PermutationReasoning @@ -320,7 +330,7 @@ drop-∷ = drop-mid [] [] ∷↭∷ʳ : ∀ (x : A) xs → x ∷ xs ↭ xs ∷ʳ x ∷↭∷ʳ x xs = ↭-sym (begin xs ++ [ x ] ↭⟨ shift x xs [] ⟩ - x ∷ xs ++ [] ≡⟨ Lₚ.++-identityʳ _ ⟩ + x ∷ xs ++ [] ≡⟨ List.++-identityʳ _ ⟩ x ∷ xs ∎) where open PermutationReasoning @@ -337,7 +347,7 @@ drop-∷ = drop-mid [] [] ↭-reverse : (xs : List A) → reverse xs ↭ xs ↭-reverse [] = ↭-refl ↭-reverse (x ∷ xs) = begin - reverse (x ∷ xs) ≡⟨ Lₚ.unfold-reverse x xs ⟩ + reverse (x ∷ xs) ≡⟨ List.unfold-reverse x xs ⟩ reverse xs ∷ʳ x ↭⟨ ∷↭∷ʳ x (reverse xs) ⟨ x ∷ reverse xs ↭⟨ prep x (↭-reverse xs) ⟩ x ∷ xs ∎ @@ -356,9 +366,9 @@ module _ {ℓ} {R : Rel A ℓ} (R? : Decidable R) where with does (R? x y) | merge-↭ xs (y ∷ ys) | merge-↭ (x ∷ xs) ys ... | true | rec | _ = prep x rec ... | false | _ | rec = begin - y ∷ merge R? (x ∷ xs) ys <⟨ rec ⟩ + y ∷ merge R? (x ∷ xs) ys ↭⟨ prep _ rec ⟩ y ∷ x ∷ xs ++ ys ↭⟨ shift y (x ∷ xs) ys ⟨ - (x ∷ xs) ++ y ∷ ys ≡⟨ Lₚ.++-assoc [ x ] xs (y ∷ ys) ⟨ + (x ∷ xs) ++ y ∷ ys ≡⟨ List.++-assoc [ x ] xs (y ∷ ys) ⟨ x ∷ xs ++ y ∷ ys ∎ where open PermutationReasoning @@ -366,15 +376,10 @@ module _ {ℓ} {R : Rel A ℓ} (R? : Decidable R) where -- 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-↭ p = foldr-commMonoid ℕ-*-1.isCommutativeMonoid (↭⇒↭ₛ p) + where + module ℕ-*-1 = CommutativeMonoid ℕ.*-1-commutativeMonoid + open Permutation ℕ-*-1.setoid ------------------------------------------------------------------------ -- catMaybes diff --git a/src/Data/List/Relation/Binary/Permutation/Setoid.agda b/src/Data/List/Relation/Binary/Permutation/Setoid.agda index 4409e78cc4..5c81eb6999 100644 --- a/src/Data/List/Relation/Binary/Permutation/Setoid.agda +++ b/src/Data/List/Relation/Binary/Permutation/Setoid.agda @@ -6,32 +6,29 @@ {-# OPTIONS --cubical-compatible --safe #-} -open import Function.Base using (_∘′_) -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; Symmetric; Transitive) -open import Relation.Binary.Reasoning.Syntax module Data.List.Relation.Binary.Permutation.Setoid {a ℓ} (S : Setoid a ℓ) where 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.Nat.Base using (ℕ; zero; suc; _+_) +import Data.List.Relation.Binary.Equality.Setoid as ≋ +open import Function.Base using (_∘′_) open import Level using (_⊔_) +open import Relation.Binary.Core using (Rel; _⇒_) +open import Relation.Binary.Definitions + using (Reflexive; Symmetric; Transitive; LeftTrans; RightTrans) open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl) import Relation.Binary.Reasoning.Setoid as ≈-Reasoning +open import Relation.Binary.Reasoning.Syntax +open import Relation.Binary.Structures using (IsEquivalence) -private - module Eq = Setoid S -open Eq using (_≈_) renaming (Carrier to A) +open module ≈ = Setoid S using (_≈_) renaming (Carrier to A) +open ≋ S using (_≋_; _∷_; ≋-refl; ≋-sym; ≋-trans) ------------------------------------------------------------------------ --- Definition +-- Definition, based on `Homogeneous` open Homogeneous public using (refl; prep; swap; trans) @@ -41,47 +38,89 @@ infix 3 _↭_ _↭_ : Rel (List A) (a ⊔ ℓ) _↭_ = Homogeneous.Permutation _≈_ +steps = Homogeneous.steps {R = _≈_} + ------------------------------------------------------------------------ -- Constructor aliases +-- Constructor alias + +↭-reflexive-≋ : _≋_ ⇒ _↭_ +↭-reflexive-≋ = refl + +↭-trans : Transitive _↭_ +↭-trans = trans + -- These provide aliases for `swap` and `prep` when the elements being -- 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 - ------------------------------------------------------------------------- --- Functions over permutations - -steps : ∀ {xs ys} → xs ↭ ys → ℕ -steps (refl _) = 1 -steps (prep _ xs↭ys) = suc (steps xs↭ys) -steps (swap _ _ xs↭ys) = suc (steps xs↭ys) -steps (trans xs↭ys ys↭zs) = steps xs↭ys + steps ys↭zs +↭-swap x y xs↭ys = swap ≈.refl ≈.refl xs↭ys ------------------------------------------------------------------------ -- _↭_ is an equivalence ↭-reflexive : _≡_ ⇒ _↭_ -↭-reflexive refl = refl (Pointwise.refl Eq.refl) +↭-reflexive refl = ↭-reflexive-≋ ≋-refl ↭-refl : Reflexive _↭_ ↭-refl = ↭-reflexive refl ↭-sym : Symmetric _↭_ -↭-sym = Homogeneous.sym Eq.sym +↭-sym = Homogeneous.sym ≈.sym -↭-trans : Transitive _↭_ -↭-trans = trans +-- As with the existing proofs `↭-respʳ-≋` and `↭-respˡ-≋` in `Setoid.Properties` +-- (which appeal to symmetry of the underlying equality, and its effect on the +-- proofs of symmetry for both pointwise equality and permutation) to the effect +-- that _↭_ respects _≋_ on the left and right, such arguments can be both +-- streamlined, and used to define a 'smart' constructor `↭-trans′` for transitivity. +-- +-- The arguments below show how proofs of permutation can have all transitive +-- compositions with instances of `refl` pushed to the leaves of derivations, +-- thereby addressing the inefficiencies analysed in issue #1113 +-- +-- Conjecture: these transformations are `steps` invariant, but that is moot, +-- given their use here, and in `Setoid.Properties.↭-split` (without requiring +-- WF-induction on `steps`) to enable a new, sharper, analysis of lists `xs` +-- such that `xs ↭ ys ++ [ x ] ++ zs` in terms of `x`, `ys`, and `zs`. + +↭-transˡ-≋ : LeftTrans _≋_ _↭_ +↭-transˡ-≋ xs≋ys (refl ys≋zs) + = refl (≋-trans xs≋ys ys≋zs) +↭-transˡ-≋ (x≈y ∷ xs≋ys) (prep y≈z ys↭zs) + = prep (≈.trans x≈y y≈z) (↭-transˡ-≋ xs≋ys ys↭zs) +↭-transˡ-≋ (x≈y ∷ w≈z ∷ xs≋ys) (swap eq₁ eq₂ ys↭zs) + = swap (≈.trans x≈y eq₁) (≈.trans w≈z eq₂) (↭-transˡ-≋ xs≋ys ys↭zs) +↭-transˡ-≋ xs≋ys (trans ys↭ws ws↭zs) + = trans (↭-transˡ-≋ xs≋ys ys↭ws) ws↭zs + +↭-transʳ-≋ : RightTrans _↭_ _≋_ +↭-transʳ-≋ (refl xs≋ys) ys≋zs + = refl (≋-trans xs≋ys ys≋zs) +↭-transʳ-≋ (prep x≈y xs↭ys) (y≈z ∷ ys≋zs) + = prep (≈.trans x≈y y≈z) (↭-transʳ-≋ xs↭ys ys≋zs) +↭-transʳ-≋ (swap eq₁ eq₂ xs↭ys) (x≈w ∷ y≈z ∷ ys≋zs) + = swap (≈.trans eq₁ y≈z) (≈.trans eq₂ x≈w) (↭-transʳ-≋ xs↭ys ys≋zs) +↭-transʳ-≋ (trans xs↭ws ws↭ys) ys≋zs + = trans xs↭ws (↭-transʳ-≋ ws↭ys ys≋zs) + +↭-trans′ : Transitive _↭_ +↭-trans′ (refl xs≋ys) ys↭zs = ↭-transˡ-≋ xs≋ys ys↭zs +↭-trans′ xs↭ys (refl ys≋zs) = ↭-transʳ-≋ xs↭ys ys≋zs +↭-trans′ xs↭ys ys↭zs = trans xs↭ys ys↭zs ↭-isEquivalence : IsEquivalence _↭_ -↭-isEquivalence = Homogeneous.isEquivalence Eq.refl Eq.sym +↭-isEquivalence = record + { refl = ↭-refl + ; sym = ↭-sym + ; trans = ↭-trans + } ↭-setoid : Setoid _ _ -↭-setoid = Homogeneous.setoid {R = _≈_} Eq.refl Eq.sym +↭-setoid = record { isEquivalence = ↭-isEquivalence } ------------------------------------------------------------------------ -- A reasoning API to chain permutation proofs @@ -95,7 +134,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 ∘′ ↭-reflexive-≋) ≋-sym public -- Some extra combinators that allow us to skip certain elements @@ -104,12 +143,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 0440e3a3b6..d82178dd8b 100644 --- a/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda +++ b/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda @@ -16,7 +16,6 @@ module Data.List.Relation.Binary.Permutation.Setoid.Properties where open import Algebra -import Algebra.Properties.CommutativeMonoid as ACM open import Data.Bool.Base using (true; false) open import Data.List.Base as List hiding (head; tail) open import Data.List.Relation.Binary.Pointwise as Pointwise @@ -29,7 +28,7 @@ open import Data.List.Relation.Unary.AllPairs using (AllPairs; []; _∷_) import Data.List.Relation.Unary.Unique.Setoid as Unique import Data.List.Membership.Setoid as Membership open import Data.List.Membership.Setoid.Properties using (∈-∃++; ∈-insert) -import Data.List.Properties as Lₚ +import Data.List.Properties as List open import Data.Nat.Base using (ℕ; suc; _<_; z