New property merge-is-superlist (#1950)

Author: andreasabel

CHANGELOG.md

@@ -606,7 +606,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`
@@ -623,11 +623,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`.
 
@@ -773,7 +773,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
@@ -1073,7 +1073,7 @@ Deprecated names
 
 * In `Data.Fin.Induction`:
   ```
-  ≺-Rec 
+  ≺-Rec
   ≺-wellFounded
   ≺-recBuilder
   ≺-rec
@@ -1082,7 +1082,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`:
   ```
@@ -1163,14 +1163,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
@@ -1661,7 +1661,7 @@ New modules
   ```
   Algebra.Properties.Quasigroup
   ```
-  
+
 * Properties of MiddleBolLoop
   ```
   Algebra.Properties.MiddleBolLoop
@@ -1828,7 +1828,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 _
@@ -1864,7 +1864,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`:
@@ -2046,7 +2046,7 @@ Other minor changes
 * Added new functions in `Data.Integer.Base`:
   ```
   _^_ : ℤ → ℕ → ℤ
- 
+
   +-0-rawGroup  : Rawgroup 0ℓ 0ℓ
 
   *-rawMagma    : RawMagma 0ℓ 0ℓ
@@ -2164,7 +2164,7 @@ Other minor changes
   _! : ℕ → ℕ
 
   parity : ℕ → Parity
-  
+
   +-rawMagma          : RawMagma 0ℓ 0ℓ
   +-0-rawMonoid       : RawMonoid 0ℓ 0ℓ
   *-rawMagma          : RawMagma 0ℓ 0ℓ
@@ -2409,10 +2409,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 _<ₗₑₓ_
   ```
 
@@ -2565,7 +2565,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})
 ```
 
@@ -3184,14 +3184,21 @@ This is a full list of proofs that have changed form to use irrelevant instance
   ↭-reverse : (xs : List A) → reverse xs ↭ xs
   ```
 
-* Added new file `Relation.Binary.Reasoning.Base.Apartness`
-
-This is how to use it:
+* Added new proofs to `Data.List.Relation.Binary.Sublist.Setoid.Properties`
+  and `Data.List.Relation.Unary.Sorted.TotalOrder.Properties`.
   ```agda
-  _ : a # d
-  _ = begin-apartness
-    a ≈⟨ a≈b ⟩
-    b #⟨ b#c ⟩
-    c ≈⟨ c≈d ⟩
-    d ∎
+  ⊆-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:
+    ```agda
+    _ : a # d
+    _ = begin-apartness
+      a ≈⟨ a≈b ⟩
+      b #⟨ b#c ⟩
+      c ≈⟨ c≈d ⟩
+      d ∎
+    ```

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
@@ -20,10 +20,12 @@ 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)
 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
@@ -203,6 +205,29 @@ module _ {as bs : List A} where
   reverse⁻ : reverse as ⊆ reverse bs → as ⊆ bs
   reverse⁻ = HeteroProperties.reverse⁻
 
+------------------------------------------------------------------------
+-- merge
+
+module _ {ℓ′} {_≤_ : Rel A ℓ′} (_≤?_ : Decidable₂ _≤_) where
+
+  ⊆-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ʳ : ∀ 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
+
 ------------------------------------------------------------------------
 -- Inversion lemmas
 ------------------------------------------------------------------------

src/Data/List/Relation/Unary/Sorted/TotalOrder/Properties.agda

@@ -14,15 +14,20 @@ 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)
+
 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.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
@@ -101,30 +106,41 @@ 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
     merge-con : ∀ {v xs ys} →
                 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
 
+  -- Reexport ⊆-mergeˡʳ
+
+  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