diff --git a/CHANGELOG.md b/CHANGELOG.md index d5ba31beaf..4b9ed1e14d 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}) ``` @@ -3079,14 +3079,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 ∎ + ``` diff --git a/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda index dd7638bc5f..5600339c7b 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 @@ -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 ------------------------------------------------------------------------ diff --git a/src/Data/List/Relation/Unary/Sorted/TotalOrder/Properties.agda b/src/Data/List/Relation/Unary/Sorted/TotalOrder/Properties.agda index 69654ef242..89582d2f88 100644 --- a/src/Data/List/Relation/Unary/Sorted/TotalOrder/Properties.agda +++ b/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,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 @@ -109,22 +114,33 @@ 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 + -- 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