From 1bced4442b63c071033e263eaf3b486eabf7921b Mon Sep 17 00:00:00 2001 From: Andreas Abel Date: Mon, 24 Apr 2023 07:38:13 +0200 Subject: [PATCH 1/8] New property merge-is-sublist Proofs that both lists involved in a merge are sublists of the result of the merge. --- .../Binary/Sublist/Setoid/Properties.agda | 39 ++++++++++++++++- .../Unary/Sorted/TotalOrder/Properties.agda | 43 ++++++++++++++++--- 2 files changed, 73 insertions(+), 9 deletions(-) diff --git a/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda index dd7638bc5f..4fbbaaed19 100644 --- a/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda +++ b/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda @@ -6,7 +6,7 @@ {-# OPTIONS --cubical-compatible --safe #-} -open import Relation.Binary using (Setoid; _⇒_; _Preserves_⟶_) +open import Relation.Binary using (Rel; Setoid; _⇒_; _Preserves_⟶_) module Data.List.Relation.Binary.Sublist.Setoid.Properties {c ℓ} (S : Setoid c ℓ) where @@ -21,9 +21,10 @@ open import Function.Base open import Function.Bundles using (_⇔_; _⤖_) open import Level open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong) +open import Relation.Binary.Structures using (IsDecTotalOrder) open import Relation.Unary using (Pred; Decidable; Irrelevant) open import Relation.Nullary.Negation using (¬_) -open import Relation.Nullary.Decidable using (¬?) +open import Relation.Nullary.Decidable using (¬?; yes; no) import Data.List.Relation.Binary.Equality.Setoid as SetoidEquality import Data.List.Relation.Binary.Sublist.Setoid as SetoidSublist @@ -36,6 +37,15 @@ open SetoidEquality S using (_≋_; ≋-refl) open SetoidSublist S hiding (map) open SetoidMembership S using (_∈_) +------------------------------------------------------------------------ +-- Least element + +module _ where + + []⊆ : ∀ xs → [] ⊆ xs + []⊆ [] = [] + []⊆ (x ∷ xs) = x ∷ʳ []⊆ xs + ------------------------------------------------------------------------ -- Injectivity of constructors ------------------------------------------------------------------------ @@ -203,6 +213,31 @@ module _ {as bs : List A} where reverse⁻ : reverse as ⊆ reverse bs → as ⊆ bs reverse⁻ = HeteroProperties.reverse⁻ +------------------------------------------------------------------------ +-- merge + +module _ {ℓ′} (_≤_ : Rel A ℓ′) (dto : IsDecTotalOrder _≈_ _≤_) where + + open IsDecTotalOrder dto using (_≤?_) + + merge-is-sublistˡ : ∀ xs ys → xs ⊆ merge _≤?_ xs ys + merge-is-sublistˡ [] ys = []⊆ ys + merge-is-sublistˡ (x ∷ xs) [] = ⊆-refl + merge-is-sublistˡ (x ∷ xs) (y ∷ ys) + with x ≤? y | merge-is-sublistˡ xs (y ∷ ys) + | merge-is-sublistˡ (x ∷ xs) ys + ... | yes x≤y | rec | _ = ≈-refl ∷ rec + ... | no x≰y | _ | rec = y ∷ʳ rec + + merge-is-sublistʳ : ∀ xs ys → ys ⊆ merge _≤?_ xs ys + merge-is-sublistʳ [] ys = ⊆-refl + merge-is-sublistʳ (x ∷ xs) [] = []⊆ (merge _≤?_ (x ∷ xs) []) + merge-is-sublistʳ (x ∷ xs) (y ∷ ys) + with x ≤? y | merge-is-sublistʳ xs (y ∷ ys) + | merge-is-sublistʳ (x ∷ xs) ys + ... | yes x≤y | rec | _ = x ∷ʳ rec + ... | no x≰y | _ | rec = ≈-refl ∷ rec + ------------------------------------------------------------------------ -- Inversion lemmas ------------------------------------------------------------------------ diff --git a/src/Data/List/Relation/Unary/Sorted/TotalOrder/Properties.agda b/src/Data/List/Relation/Unary/Sorted/TotalOrder/Properties.agda index 69654ef242..ad3909d1fe 100644 --- a/src/Data/List/Relation/Unary/Sorted/TotalOrder/Properties.agda +++ b/src/Data/List/Relation/Unary/Sorted/TotalOrder/Properties.agda @@ -8,21 +8,29 @@ module Data.List.Relation.Unary.Sorted.TotalOrder.Properties where -open import Data.List.Base +open import Data.List.Base hiding (_∷ʳ_) open import Data.List.Relation.Unary.All using (All) open import Data.List.Relation.Unary.AllPairs using (AllPairs) open import Data.List.Relation.Unary.Linked as Linked using (Linked; []; [-]; _∷_; _∷′_; head′; tail) import Data.List.Relation.Unary.Linked.Properties as Linked open import Data.List.Relation.Unary.Sorted.TotalOrder hiding (head) +open import Data.List.Relation.Binary.Sublist.Propositional + using (_⊆_; []; _∷ʳ_; _∷_; ⊆-refl) +open import Data.List.Relation.Binary.Sublist.Propositional.Properties + using ([]⊆) + open import Data.Maybe.Base using (just; nothing) open import Data.Maybe.Relation.Binary.Connected using (Connected; just) open import Data.Nat.Base using (ℕ; zero; suc; _<_) + open import Level using (Level) open import Relation.Binary hiding (Decidable) +import Relation.Binary.PropositionalEquality as ≡ import Relation.Binary.Properties.TotalOrder as TotalOrderProperties open import Relation.Unary using (Pred; Decidable) open import Relation.Nullary.Decidable using (yes; no) + private variable a b p ℓ₁ ℓ₂ ℓ₃ ℓ₄ : Level @@ -109,22 +117,43 @@ module _ (DO : DecTotalOrder a ℓ₁ ℓ₂) where Connected _≤_ (just v) (head xs) → Connected _≤_ (just v) (head ys) → Connected _≤_ (just v) (head (merge _≤?_ xs ys)) - merge-con {xs = []} {[]} cxs cys = cys - merge-con {xs = []} {y ∷ ys} cxs cys = cys + merge-con {xs = []} cxs cys = cys merge-con {xs = x ∷ xs} {[]} cxs cys = cxs merge-con {xs = x ∷ xs} {y ∷ ys} cxs cys with x ≤? y ... | yes x≤y = cxs ... | no x≰y = cys merge⁺ : ∀ {xs ys} → Sorted O xs → Sorted O ys → Sorted O (merge _≤?_ xs ys) - merge⁺ {[]} {[]} rxs rys = [] - merge⁺ {[]} {x ∷ ys} rxs rys = rys + merge⁺ {[]} rxs rys = rys merge⁺ {x ∷ xs} {[]} rxs rys = rxs - merge⁺ {x ∷ xs} {y ∷ ys} rxs rys with x ≤? y | - merge⁺ (Linked.tail rxs) rys | merge⁺ rxs (Linked.tail rys) + merge⁺ {x ∷ xs} {y ∷ ys} rxs rys + with x ≤? y | merge⁺ (Linked.tail rxs) rys + | merge⁺ rxs (Linked.tail rys) ... | yes x≤y | rec | _ = merge-con (head′ rxs) (just x≤y) ∷′ rec ... | no x≰y | _ | rec = merge-con (just (≰⇒≥ x≰y)) (head′ rys) ∷′ rec + merge-is-sublistˡ : ∀ {xs ys} (rxs : Sorted O xs) (rys : Sorted O ys) → + xs ⊆ merge _≤?_ xs ys + merge-is-sublistˡ {xs = []} {ys} rxs rys = []⊆ ys + merge-is-sublistˡ {xs = x ∷ xs} {[]} rxs rys = ⊆-refl + merge-is-sublistˡ {xs = x ∷ xs} {y ∷ ys} rxs rys + with x ≤? y | merge-is-sublistˡ (Linked.tail rxs) rys + | merge-is-sublistˡ rxs (Linked.tail rys) + ... | yes x≤y | rec | _ = ≡.refl ∷ rec + ... | no x≰y | _ | rec = y ∷ʳ rec + + merge-is-sublistʳ : ∀ {xs ys} (rxs : Sorted O xs) (rys : Sorted O ys) → + ys ⊆ merge _≤?_ xs ys + merge-is-sublistʳ {xs = []} {ys} rxs rys = ⊆-refl + merge-is-sublistʳ {xs = x ∷ xs} {[]} rxs rys = []⊆ (merge _≤?_ (x ∷ xs) []) + merge-is-sublistʳ {xs = x ∷ xs} {y ∷ ys} rxs rys + with x ≤? y | merge-is-sublistʳ (Linked.tail rxs) rys + | merge-is-sublistʳ rxs (Linked.tail rys) + ... | yes x≤y | rec | _ = x ∷ʳ rec + ... | no x≰y | _ | rec = ≡.refl ∷ rec + + + ------------------------------------------------------------------------ -- filter From 16f44a97d8305d48ab6150a207a7979e6218e2be Mon Sep 17 00:00:00 2001 From: Andreas Abel Date: Tue, 25 Apr 2023 07:13:12 +0200 Subject: [PATCH 2/8] =?UTF-8?q?Adress=20review:=20import=20[]=E2=8A=86=5F?= =?UTF-8?q?=20from=20Sublist.Heterogeneous.minimum?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- .../Relation/Binary/Sublist/Setoid/Properties.agda | 10 +--------- 1 file changed, 1 insertion(+), 9 deletions(-) diff --git a/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda index 4fbbaaed19..781bfb6546 100644 --- a/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda +++ b/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda @@ -13,6 +13,7 @@ module Data.List.Relation.Binary.Sublist.Setoid.Properties open import Data.List.Base hiding (_∷ʳ_) open import Data.List.Relation.Unary.Any using (Any) +open import Data.List.Relation.Binary.Sublist.Heterogeneous using () renaming (minimum to []⊆_) import Data.Maybe.Relation.Unary.All as Maybe open import Data.Nat.Base using (_≤_; _≥_) import Data.Nat.Properties as ℕₚ @@ -37,15 +38,6 @@ open SetoidEquality S using (_≋_; ≋-refl) open SetoidSublist S hiding (map) open SetoidMembership S using (_∈_) ------------------------------------------------------------------------- --- Least element - -module _ where - - []⊆ : ∀ xs → [] ⊆ xs - []⊆ [] = [] - []⊆ (x ∷ xs) = x ∷ʳ []⊆ xs - ------------------------------------------------------------------------ -- Injectivity of constructors ------------------------------------------------------------------------ From 970d332402d3f16bdff8254c44a7a12bfd596287 Mon Sep 17 00:00:00 2001 From: Andreas Abel Date: Tue, 25 Apr 2023 07:59:40 +0200 Subject: [PATCH 3/8] Address review: sublist -> superlist; deduplicate code --- .../Binary/Sublist/Setoid/Properties.agda | 26 +++++++-------- .../Unary/Sorted/TotalOrder/Properties.agda | 32 +++++-------------- 2 files changed, 21 insertions(+), 37 deletions(-) diff --git a/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda index 781bfb6546..80fe5625ca 100644 --- a/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda +++ b/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda @@ -208,25 +208,25 @@ module _ {as bs : List A} where ------------------------------------------------------------------------ -- merge -module _ {ℓ′} (_≤_ : Rel A ℓ′) (dto : IsDecTotalOrder _≈_ _≤_) where +module Merge {ℓ′} (_≤_ : Rel A ℓ′) (dto : IsDecTotalOrder _≈_ _≤_) where open IsDecTotalOrder dto using (_≤?_) - merge-is-sublistˡ : ∀ xs ys → xs ⊆ merge _≤?_ xs ys - merge-is-sublistˡ [] ys = []⊆ ys - merge-is-sublistˡ (x ∷ xs) [] = ⊆-refl - merge-is-sublistˡ (x ∷ xs) (y ∷ ys) - with x ≤? y | merge-is-sublistˡ xs (y ∷ ys) - | merge-is-sublistˡ (x ∷ xs) ys + merge-is-superlistˡ : ∀ xs ys → xs ⊆ merge _≤?_ xs ys + merge-is-superlistˡ [] ys = []⊆ ys + merge-is-superlistˡ (x ∷ xs) [] = ⊆-refl + merge-is-superlistˡ (x ∷ xs) (y ∷ ys) + with x ≤? y | merge-is-superlistˡ xs (y ∷ ys) + | merge-is-superlistˡ (x ∷ xs) ys ... | yes x≤y | rec | _ = ≈-refl ∷ rec ... | no x≰y | _ | rec = y ∷ʳ rec - merge-is-sublistʳ : ∀ xs ys → ys ⊆ merge _≤?_ xs ys - merge-is-sublistʳ [] ys = ⊆-refl - merge-is-sublistʳ (x ∷ xs) [] = []⊆ (merge _≤?_ (x ∷ xs) []) - merge-is-sublistʳ (x ∷ xs) (y ∷ ys) - with x ≤? y | merge-is-sublistʳ xs (y ∷ ys) - | merge-is-sublistʳ (x ∷ xs) ys + merge-is-superlistʳ : ∀ xs ys → ys ⊆ merge _≤?_ xs ys + merge-is-superlistʳ [] ys = ⊆-refl + merge-is-superlistʳ (x ∷ xs) [] = []⊆ (merge _≤?_ (x ∷ xs) []) + merge-is-superlistʳ (x ∷ xs) (y ∷ ys) + with x ≤? y | merge-is-superlistʳ xs (y ∷ ys) + | merge-is-superlistʳ (x ∷ xs) ys ... | yes x≤y | rec | _ = x ∷ʳ rec ... | no x≰y | _ | rec = ≈-refl ∷ rec diff --git a/src/Data/List/Relation/Unary/Sorted/TotalOrder/Properties.agda b/src/Data/List/Relation/Unary/Sorted/TotalOrder/Properties.agda index ad3909d1fe..18f7dc92f3 100644 --- a/src/Data/List/Relation/Unary/Sorted/TotalOrder/Properties.agda +++ b/src/Data/List/Relation/Unary/Sorted/TotalOrder/Properties.agda @@ -14,11 +14,8 @@ open import Data.List.Relation.Unary.AllPairs using (AllPairs) open import Data.List.Relation.Unary.Linked as Linked using (Linked; []; [-]; _∷_; _∷′_; head′; tail) import Data.List.Relation.Unary.Linked.Properties as Linked +import Data.List.Relation.Binary.Sublist.Setoid.Properties as SublistProperties open import Data.List.Relation.Unary.Sorted.TotalOrder hiding (head) -open import Data.List.Relation.Binary.Sublist.Propositional - using (_⊆_; []; _∷ʳ_; _∷_; ⊆-refl) -open import Data.List.Relation.Binary.Sublist.Propositional.Properties - using ([]⊆) open import Data.Maybe.Base using (just; nothing) open import Data.Maybe.Relation.Binary.Connected using (Connected; just) @@ -132,27 +129,14 @@ module _ (DO : DecTotalOrder a ℓ₁ ℓ₂) where ... | yes x≤y | rec | _ = merge-con (head′ rxs) (just x≤y) ∷′ rec ... | no x≰y | _ | rec = merge-con (just (≰⇒≥ x≰y)) (head′ rys) ∷′ rec - merge-is-sublistˡ : ∀ {xs ys} (rxs : Sorted O xs) (rys : Sorted O ys) → - xs ⊆ merge _≤?_ xs ys - merge-is-sublistˡ {xs = []} {ys} rxs rys = []⊆ ys - merge-is-sublistˡ {xs = x ∷ xs} {[]} rxs rys = ⊆-refl - merge-is-sublistˡ {xs = x ∷ xs} {y ∷ ys} rxs rys - with x ≤? y | merge-is-sublistˡ (Linked.tail rxs) rys - | merge-is-sublistˡ rxs (Linked.tail rys) - ... | yes x≤y | rec | _ = ≡.refl ∷ rec - ... | no x≰y | _ | rec = y ∷ʳ rec - - merge-is-sublistʳ : ∀ {xs ys} (rxs : Sorted O xs) (rys : Sorted O ys) → - ys ⊆ merge _≤?_ xs ys - merge-is-sublistʳ {xs = []} {ys} rxs rys = ⊆-refl - merge-is-sublistʳ {xs = x ∷ xs} {[]} rxs rys = []⊆ (merge _≤?_ (x ∷ xs) []) - merge-is-sublistʳ {xs = x ∷ xs} {y ∷ ys} rxs rys - with x ≤? y | merge-is-sublistʳ (Linked.tail rxs) rys - | merge-is-sublistʳ rxs (Linked.tail rys) - ... | yes x≤y | rec | _ = x ∷ʳ rec - ... | no x≰y | _ | rec = ≡.refl ∷ rec - + -- Reexport merge-is-superlistˡʳ + open + SublistProperties.Merge + (Preorder.Eq.setoid (DecTotalOrder.preorder DO)) + _≤_ + (DecTotalOrder.isDecTotalOrder DO) + public using (merge-is-superlistˡ; merge-is-superlistʳ) ------------------------------------------------------------------------ -- filter From 71a3f505c28b69a6f7d17f7515a50308d186fed1 Mon Sep 17 00:00:00 2001 From: Andreas Abel Date: Tue, 25 Apr 2023 08:02:29 +0200 Subject: [PATCH 4/8] Remove now redundant imports --- src/Data/List/Relation/Unary/Sorted/TotalOrder/Properties.agda | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/Data/List/Relation/Unary/Sorted/TotalOrder/Properties.agda b/src/Data/List/Relation/Unary/Sorted/TotalOrder/Properties.agda index 18f7dc92f3..3b5017f3af 100644 --- a/src/Data/List/Relation/Unary/Sorted/TotalOrder/Properties.agda +++ b/src/Data/List/Relation/Unary/Sorted/TotalOrder/Properties.agda @@ -8,7 +8,7 @@ module Data.List.Relation.Unary.Sorted.TotalOrder.Properties where -open import Data.List.Base hiding (_∷ʳ_) +open import Data.List.Base open import Data.List.Relation.Unary.All using (All) open import Data.List.Relation.Unary.AllPairs using (AllPairs) open import Data.List.Relation.Unary.Linked as Linked @@ -23,7 +23,6 @@ open import Data.Nat.Base using (ℕ; zero; suc; _<_) open import Level using (Level) open import Relation.Binary hiding (Decidable) -import Relation.Binary.PropositionalEquality as ≡ import Relation.Binary.Properties.TotalOrder as TotalOrderProperties open import Relation.Unary using (Pred; Decidable) open import Relation.Nullary.Decidable using (yes; no) From d95c65dea4983938cf1b5987799418d27fe3275f Mon Sep 17 00:00:00 2001 From: Andreas Abel Date: Sat, 6 May 2023 14:40:04 +0200 Subject: [PATCH 5/8] Address Matthew's review comments --- .../Binary/Sublist/Setoid/Properties.agda | 30 +++++++++---------- .../Unary/Sorted/TotalOrder/Properties.agda | 20 ++++++++----- 2 files changed, 26 insertions(+), 24 deletions(-) diff --git a/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda index 80fe5625ca..5600339c7b 100644 --- a/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda +++ b/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda @@ -13,7 +13,6 @@ module Data.List.Relation.Binary.Sublist.Setoid.Properties open import Data.List.Base hiding (_∷ʳ_) open import Data.List.Relation.Unary.Any using (Any) -open import Data.List.Relation.Binary.Sublist.Heterogeneous using () renaming (minimum to []⊆_) import Data.Maybe.Relation.Unary.All as Maybe open import Data.Nat.Base using (_≤_; _≥_) import Data.Nat.Properties as ℕₚ @@ -21,6 +20,7 @@ open import Data.Product using (∃; _,_; proj₂) open import Function.Base open import Function.Bundles using (_⇔_; _⤖_) open import Level +open import Relation.Binary using () renaming (Decidable to Decidable₂) open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong) open import Relation.Binary.Structures using (IsDecTotalOrder) open import Relation.Unary using (Pred; Decidable; Irrelevant) @@ -208,25 +208,23 @@ module _ {as bs : List A} where ------------------------------------------------------------------------ -- merge -module Merge {ℓ′} (_≤_ : Rel A ℓ′) (dto : IsDecTotalOrder _≈_ _≤_) where +module _ {ℓ′} {_≤_ : Rel A ℓ′} (_≤?_ : Decidable₂ _≤_) where - open IsDecTotalOrder dto using (_≤?_) - - merge-is-superlistˡ : ∀ xs ys → xs ⊆ merge _≤?_ xs ys - merge-is-superlistˡ [] ys = []⊆ ys - merge-is-superlistˡ (x ∷ xs) [] = ⊆-refl - merge-is-superlistˡ (x ∷ xs) (y ∷ ys) - with x ≤? y | merge-is-superlistˡ xs (y ∷ ys) - | merge-is-superlistˡ (x ∷ xs) ys + ⊆-mergeˡ : ∀ xs ys → xs ⊆ merge _≤?_ xs ys + ⊆-mergeˡ [] ys = minimum ys + ⊆-mergeˡ (x ∷ xs) [] = ⊆-refl + ⊆-mergeˡ (x ∷ xs) (y ∷ ys) + with x ≤? y | ⊆-mergeˡ xs (y ∷ ys) + | ⊆-mergeˡ (x ∷ xs) ys ... | yes x≤y | rec | _ = ≈-refl ∷ rec ... | no x≰y | _ | rec = y ∷ʳ rec - merge-is-superlistʳ : ∀ xs ys → ys ⊆ merge _≤?_ xs ys - merge-is-superlistʳ [] ys = ⊆-refl - merge-is-superlistʳ (x ∷ xs) [] = []⊆ (merge _≤?_ (x ∷ xs) []) - merge-is-superlistʳ (x ∷ xs) (y ∷ ys) - with x ≤? y | merge-is-superlistʳ xs (y ∷ ys) - | merge-is-superlistʳ (x ∷ xs) ys + ⊆-mergeʳ : ∀ xs ys → ys ⊆ merge _≤?_ xs ys + ⊆-mergeʳ [] ys = ⊆-refl + ⊆-mergeʳ (x ∷ xs) [] = minimum (merge _≤?_ (x ∷ xs) []) + ⊆-mergeʳ (x ∷ xs) (y ∷ ys) + with x ≤? y | ⊆-mergeʳ xs (y ∷ ys) + | ⊆-mergeʳ (x ∷ xs) ys ... | yes x≤y | rec | _ = x ∷ʳ rec ... | no x≰y | _ | rec = ≈-refl ∷ rec diff --git a/src/Data/List/Relation/Unary/Sorted/TotalOrder/Properties.agda b/src/Data/List/Relation/Unary/Sorted/TotalOrder/Properties.agda index 3b5017f3af..89582d2f88 100644 --- a/src/Data/List/Relation/Unary/Sorted/TotalOrder/Properties.agda +++ b/src/Data/List/Relation/Unary/Sorted/TotalOrder/Properties.agda @@ -14,6 +14,7 @@ open import Data.List.Relation.Unary.AllPairs using (AllPairs) open import Data.List.Relation.Unary.Linked as Linked using (Linked; []; [-]; _∷_; _∷′_; head′; tail) import Data.List.Relation.Unary.Linked.Properties as Linked +import Data.List.Relation.Binary.Sublist.Setoid as Sublist import Data.List.Relation.Binary.Sublist.Setoid.Properties as SublistProperties open import Data.List.Relation.Unary.Sorted.TotalOrder hiding (head) @@ -105,7 +106,7 @@ module _ (O : TotalOrder a ℓ₁ ℓ₂) where -- merge module _ (DO : DecTotalOrder a ℓ₁ ℓ₂) where - open DecTotalOrder DO renaming (totalOrder to O) + open DecTotalOrder DO using (_≤_; _≤?_) renaming (totalOrder to O) open TotalOrderProperties O using (≰⇒≥) private @@ -128,14 +129,17 @@ module _ (DO : DecTotalOrder a ℓ₁ ℓ₂) where ... | yes x≤y | rec | _ = merge-con (head′ rxs) (just x≤y) ∷′ rec ... | no x≰y | _ | rec = merge-con (just (≰⇒≥ x≰y)) (head′ rys) ∷′ rec - -- Reexport merge-is-superlistˡʳ + -- Reexport ⊆-mergeˡʳ - open - SublistProperties.Merge - (Preorder.Eq.setoid (DecTotalOrder.preorder DO)) - _≤_ - (DecTotalOrder.isDecTotalOrder DO) - public using (merge-is-superlistˡ; merge-is-superlistʳ) + S = Preorder.Eq.setoid (DecTotalOrder.preorder DO) + open Sublist S using (_⊆_) + module SP = SublistProperties S + + ⊆-mergeˡ : ∀ xs ys → xs ⊆ merge _≤?_ xs ys + ⊆-mergeˡ = SP.⊆-mergeˡ _≤?_ + + ⊆-mergeʳ : ∀ xs ys → ys ⊆ merge _≤?_ xs ys + ⊆-mergeʳ = SP.⊆-mergeʳ _≤?_ ------------------------------------------------------------------------ -- filter From a7f56ab64fd44e2a0880d6e9b8ced8cccc9ec8c5 Mon Sep 17 00:00:00 2001 From: Andreas Abel Date: Sat, 10 Jun 2023 19:21:34 +0200 Subject: [PATCH 6/8] CHANGELOG.md: remove trailing whitespace --- CHANGELOG.md | 36 ++++++++++++++++++------------------ 1 file changed, 18 insertions(+), 18 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index d5ba31beaf..f4c3310ebb 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -528,7 +528,7 @@ Non-backwards compatible changes * It was very difficult to use the `Relation.Nullary` modules, as `Relation.Nullary` contained the basic definitions of negation, decidability etc., and the operations and proofs were smeared over `Relation.Nullary.(Negation/Product/Sum/Implication etc.)`. - + * In order to fix this: - the definition of `Dec` and `recompute` have been moved to `Relation.Nullary.Decidable.Core` - the definition of `Reflects` has been moved to `Relation.Nullary.Reflects` @@ -545,11 +545,11 @@ Non-backwards compatible changes have been deprecated and their contents moved to `Relation.Nullary.(Negation/Reflects/Decidable)` however all their contents is re-exported by `Relation.Nullary` which is the easiest way to access it now. - + * In order to facilitate this reorganisation the following breaking moves have occured: - `¬?` has been moved from `Relation.Nullary.Negation.Core` to `Relation.Nullary.Decidable.Core` - `¬-reflects` has been moved from `Relation.Nullary.Negation.Core` to `Relation.Nullary.Reflects`. - - `decidable-stable`, `excluded-middle` and `¬-drop-Dec` have been moved from `Relation.Nullary.Negation` + - `decidable-stable`, `excluded-middle` and `¬-drop-Dec` have been moved from `Relation.Nullary.Negation` to `Relation.Nullary.Decidable`. - `fromDec` and `toDec` have been mvoed from `Data.Sum.Base` to `Data.Sum`. @@ -695,7 +695,7 @@ Non-backwards compatible changes ``` NB. It is not possible to rename or deprecate `syntax` declarations, so Agda will only issue a "Could not parse the application `begin ...` when scope checking" - warning if the old combinators are used. + warning if the old combinators are used. * The types of the proofs `pos⇒1/pos`/`1/pos⇒pos` and `neg⇒1/neg`/`1/neg⇒neg` in `Data.Rational(.Unnormalised).Properties` have been switched, as the previous @@ -987,7 +987,7 @@ Deprecated names * In `Data.Fin.Induction`: ``` - ≺-Rec + ≺-Rec ≺-wellFounded ≺-recBuilder ≺-rec @@ -996,7 +996,7 @@ Deprecated names As with Issue #1726 above: the deprecation of relation `_≺_` means that these definitions associated with wf-recursion are deprecated in favour of their `_<_` counterparts. But it's not quite sensible to say that these definiton should be *renamed* to *anything*, - least of all those counterparts... the type confusion would be intolerable. + least of all those counterparts... the type confusion would be intolerable. * In `Data.Fin.Properties`: ``` @@ -1077,14 +1077,14 @@ Deprecated names ^-semigroup-morphism ↦ ^-isMagmaHomomorphism ^-monoid-morphism ↦ ^-isMonoidHomomorphism - + pos-distrib-* ↦ pos-* pos-+-commute ↦ pos-+ abs-*-commute ↦ abs-* - + +-isAbelianGroup ↦ +-0-isAbelianGroup ``` - + * In `Data.List.Properties`: ```agda map-id₂ ↦ map-id-local @@ -1575,7 +1575,7 @@ New modules ``` Algebra.Properties.Quasigroup ``` - + * Properties of MiddleBolLoop ``` Algebra.Properties.MiddleBolLoop @@ -1736,7 +1736,7 @@ Other minor changes _MiddleFourExchange_ : Op₂ A → Op₂ A → Set _ SelfInverse : Op₁ A → Set _ - + LeftDividesˡ : Op₂ A → Op₂ A → Set _ LeftDividesʳ : Op₂ A → Op₂ A → Set _ RightDividesˡ : Op₂ A → Op₂ A → Set _ @@ -1772,7 +1772,7 @@ Other minor changes _^ᵗ_ : A → ℕ → A ``` -* `Algebra.Properties.Magma.Divisibility` now re-exports operations +* `Algebra.Properties.Magma.Divisibility` now re-exports operations `_∣ˡ_`, `_∤ˡ_`, `_∣ʳ_`, `_∤ʳ_` from `Algebra.Definitions.Magma`. * Added new proofs to `Algebra.Properties.CommutativeSemigroup`: @@ -1954,7 +1954,7 @@ Other minor changes * Added new functions in `Data.Integer.Base`: ``` _^_ : ℤ → ℕ → ℤ - + +-0-rawGroup : Rawgroup 0ℓ 0ℓ *-rawMagma : RawMagma 0ℓ 0ℓ @@ -2069,7 +2069,7 @@ Other minor changes _! : ℕ → ℕ parity : ℕ → Parity - + +-rawMagma : RawMagma 0ℓ 0ℓ +-0-rawMonoid : RawMonoid 0ℓ 0ℓ *-rawMagma : RawMagma 0ℓ 0ℓ @@ -2314,10 +2314,10 @@ Other minor changes * Added new proof to `Data.Product.Relation.Binary.Lex.Strict` ```agda ×-respectsʳ : Transitive _≈₁_ → - _<₁_ Respectsʳ _≈₁_ → _<₂_ Respectsʳ _≈₂_ → _<ₗₑₓ_ Respectsʳ _≋_ + _<₁_ Respectsʳ _≈₁_ → _<₂_ Respectsʳ _≈₂_ → _<ₗₑₓ_ Respectsʳ _≋_ ×-respectsˡ : Symmetric _≈₁_ → Transitive _≈₁_ → - _<₁_ Respectsˡ _≈₁_ → _<₂_ Respectsˡ _≈₂_ → _<ₗₑₓ_ Respectsˡ _≋_ - ×-wellFounded' : Symmetric _≈₁_ → Transitive _≈₁_ → _<₁_ Respectsʳ _≈₁_ → + _<₁_ Respectsˡ _≈₁_ → _<₂_ Respectsˡ _≈₂_ → _<ₗₑₓ_ Respectsˡ _≋_ + ×-wellFounded' : Symmetric _≈₁_ → Transitive _≈₁_ → _<₁_ Respectsʳ _≈₁_ → WellFounded _<₁_ → WellFounded _<₂_ → WellFounded _<ₗₑₓ_ ``` @@ -2470,7 +2470,7 @@ Other minor changes ∀ {m n} → _Respectsˡ_ (_<_ {m} {n}) _≋_ <-respectsʳ : IsPartialEquivalence _≈_ → _≺_ Respectsʳ _≈_ → ∀ {m n} → _Respectsʳ_ (_<_ {m} {n}) _≋_ - <-wellFounded : Symmetric _≈_ → Transitive _≈_ → _≺_ Respectsʳ _≈_ → WellFounded _≺_ → + <-wellFounded : Symmetric _≈_ → Transitive _≈_ → _≺_ Respectsʳ _≈_ → WellFounded _≺_ → ∀ {n} → WellFounded (_<_ {n}) ``` From e69ee9e8b829f2b44ac81a8cc8720b6ebaa3defc Mon Sep 17 00:00:00 2001 From: Andreas Abel Date: Sat, 10 Jun 2023 19:28:01 +0200 Subject: [PATCH 7/8] CHANGELOG.md: missing indentation --- CHANGELOG.md | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index f4c3310ebb..fa6c8592ea 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -3081,12 +3081,12 @@ This is a full list of proofs that have changed form to use irrelevant instance * Added new file `Relation.Binary.Reasoning.Base.Apartness` -This is how to use it: - ```agda - _ : a # d - _ = begin-apartness - a ≈⟨ a≈b ⟩ - b #⟨ b#c ⟩ - c ≈⟨ c≈d ⟩ - d ∎ - ``` + This is how to use it: + ```agda + _ : a # d + _ = begin-apartness + a ≈⟨ a≈b ⟩ + b #⟨ b#c ⟩ + c ≈⟨ c≈d ⟩ + d ∎ + ``` From 16ea8295262d9ee9ee1862b04269bb889f524fb1 Mon Sep 17 00:00:00 2001 From: Andreas Abel Date: Sat, 10 Jun 2023 19:28:16 +0200 Subject: [PATCH 8/8] CHANGELOG for #1950 --- CHANGELOG.md | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index fa6c8592ea..4b9ed1e14d 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -3079,6 +3079,13 @@ This is a full list of proofs that have changed form to use irrelevant instance ↭-reverse : (xs : List A) → reverse xs ↭ xs ``` +* Added new proofs to `Data.List.Relation.Binary.Sublist.Setoid.Properties` + and `Data.List.Relation.Unary.Sorted.TotalOrder.Properties`. + ```agda + ⊆-mergeˡ : ∀ xs ys → xs ⊆ merge _≤?_ xs ys + ⊆-mergeʳ : ∀ xs ys → ys ⊆ merge _≤?_ xs ys + ``` + * Added new file `Relation.Binary.Reasoning.Base.Apartness` This is how to use it: