Address Matthew's comment

Author: andreasabel

src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda

@@ -13,14 +13,14 @@ 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 ℕₚ
 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
 

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 → xs ⊆ merge _≤?_ xs ys
+  ⊆-mergeʳ = SP.⊆-mergeʳ _≤?_
 
 ------------------------------------------------------------------------
 -- filter