#453: added Dense relations and DenseLinearOrder (#2111)

Author: jamesmckinna

CHANGELOG.md

@@ -308,7 +308,7 @@ Non-backwards compatible changes
   Data.Sum.Function.Setoid
   Data.Sum.Function.Propositional
   ```
-  
+
 * Additionally the following proofs now use the new definitions instead of the old ones:
   * `Algebra.Lattice.Properties.BooleanAlgebra`
   * `Algebra.Properties.CommutativeMonoid.Sum`
@@ -388,8 +388,8 @@ Non-backwards compatible changes
 * The module `Function.Definitions` no longer has two equalities as module arguments, as
   they did not interact as intended with the re-exports from `Function.Definitions.(Core1/Core2)`.
   The latter have been removed and their definitions folded into `Function.Definitions`.
-  
-* In `Function.Definitions` the types of `Surjective`, `Injective` and `Surjective` 
+
+* In `Function.Definitions` the types of `Surjective`, `Injective` and `Surjective`
   have been changed from:
   ```
   Surjective f = ∀ y → ∃ λ x → f x ≈₂ y
@@ -404,16 +404,16 @@ Non-backwards compatible changes
   ```
   This is for several reasons: i) the new definitions compose much more easily, ii) Agda
   can better infer the equalities used.
-  
+
   To ease backwards compatibility:
-   - the old definitions have been moved to the new names  `StrictlySurjective`, 
-	 `StrictlyInverseˡ` and `StrictlyInverseʳ`. 
-   - The records in  `Function.Structures` and `Function.Bundles` export proofs 
-	 of these under the names `strictlySurjective`, `strictlyInverseˡ` and 
-	 `strictlyInverseʳ`,
+   - the old definitions have been moved to the new names  `StrictlySurjective`,
+         `StrictlyInverseˡ` and `StrictlyInverseʳ`.
+   - The records in  `Function.Structures` and `Function.Bundles` export proofs
+         of these under the names `strictlySurjective`, `strictlyInverseˡ` and
+         `strictlyInverseʳ`,
    - Conversion functions have been added in both directions to
-	 `Function.Consequences(.Propositional)`. 
-  
+         `Function.Consequences(.Propositional)`.
+
 #### Proofs of non-zeroness/positivity/negativity as instance arguments
 
 * Many numeric operations in the library require their arguments to be non-zero,
@@ -800,14 +800,14 @@ Non-backwards compatible changes
 ### Changes to triple reasoning interface
 
 * The module `Relation.Binary.Reasoning.Base.Triple` now takes an extra proof that the strict
-  relation is irreflexive. 
-  
+  relation is irreflexive.
+
 * This allows the following new proof combinator:
   ```agda
   begin-contradiction : (r : x IsRelatedTo x) → {s : True (IsStrict? r)} → A
   ```
   that takes a proof that a value is strictly less than itself and then applies the principle of explosion.
-  
+
 * Specialised versions of this combinator are available in the following derived modules:
   ```
   Data.Nat.Properties
@@ -1442,6 +1442,11 @@ Deprecated names
   *-rawMonoid ↦ *-1-rawMonoid
   ```
 
+* In `Data.Rational.Unnormalised.Properties`:
+  ```
+  ≤-steps  ↦  p≤q⇒p≤r+q
+  ```
+
 * In `Data.Sum.Properties`:
   ```agda
   [,]-∘-distr      ↦  [,]-∘
@@ -1491,7 +1496,7 @@ Deprecated names
   take-distr-map     ↦  take-map
   drop-distr-zipWith ↦  drop-zipWith
   drop-distr-map     ↦  drop-map
-  
+
   updateAt-id-relative      ↦  updateAt-id-local
   updateAt-compose-relative ↦  updateAt-∘-local
   updateAt-compose          ↦  updateAt-∘
@@ -2375,7 +2380,7 @@ Additions to existing modules
 
   length-isMagmaHomomorphism  : (A : Set a) → IsMagmaHomomorphism (++-rawMagma A) +-rawMagma length
   length-isMonoidHomomorphism : (A : Set a) → IsMonoidHomomorphism (++-[]-rawMonoid A) +-0-rawMonoid length
-  
+
   take-map : take n (map f xs) ≡ map f (take n xs)
   drop-map : drop n (map f xs) ≡ map f (drop n xs)
   head-map : head (map f xs) ≡ Maybe.map f (head xs)
@@ -3058,6 +3063,7 @@ Additions to existing modules
 
 * Added new definitions in `Relation.Binary.Definitions`:
   ```
+  Dense        _<_ = ∀ {x y} → x < y → ∃[ z ] x < z × z < y
   Cotransitive _#_ = ∀ {x y} → x # y → ∀ z → (x # z) ⊎ (z # y)
   Tight    _≈_ _#_ = ∀ x y → (¬ x # y → x ≈ y) × (x ≈ y → ¬ x # y)
 
@@ -3072,11 +3078,13 @@ Additions to existing modules
 
 * Added new definitions in `Relation.Binary.Bundles`:
   ```
+  record DenseLinearOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
   record ApartnessRelation c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
   ```
 
 * Added new definitions in `Relation.Binary.Structures`:
   ```
+  record IsDenseLinearOrder (_<_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where
   record IsApartnessRelation (_#_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where
   ```
 
@@ -3310,7 +3318,6 @@ This is a full list of proofs that have changed form to use irrelevant instance
   negative<positive    : ∀ {p q} → .(Negative p) → .(Positive q) → p < q
   nonNeg∧nonPos⇒0      : ∀ {p} → .(NonNegative p) → .(NonPositive p) → p ≃ 0ℚᵘ
 
-  ≤-steps : ∀ {p q r} → NonNegative r → p ≤ q → p ≤ r + q
   p≤p+q   : ∀ {p q} → NonNegative q → p ≤ p + q
   p≤q+p   : ∀ {p} → NonNegative p → ∀ {q} → q ≤ p + q
 
@@ -3468,6 +3475,13 @@ This is a full list of proofs that have changed form to use irrelevant instance
   foldr-commMonoid : xs ↭ ys → foldr _∙_ ε xs ≈ foldr _∙_ ε ys
   ```
 
+* Added new proof, structure, and bundle to `Data.Rational.Properties`
+  ```agda
+  <-dense              : Dense _<_
+  <-isDenseLinearOrder : IsDenseLinearOrder _≡_ _<_
+  <-denseLinearOrder   : DenseLinearOrder 0ℓ 0ℓ 0ℓ
+  ```
+
 * Added new module to `Data.Rational.Unnormalised.Properties`
   ```agda
   module ≃-Reasoning = SetoidReasoning ≃-setoid
@@ -3480,16 +3494,20 @@ This is a full list of proofs that have changed form to use irrelevant instance
   ≠-symmetric : Symmetric _≠_
   ≠-cotransitive : Cotransitive _≠_
   ≠⇒invertible : p ≠ q → Invertible _≃_ 1ℚᵘ _*_ (p - q)
+
+  <-dense : Dense _<_
   ```
 
 * Added new structures to `Data.Rational.Unnormalised.Properties`
   ```agda
+  <-isDenseLinearOrder : IsDenseLinearOrder _≃_ _<_
   +-*-isHeytingCommutativeRing : IsHeytingCommutativeRing _≃_ _≠_ _+_ _*_ -_ 0ℚᵘ 1ℚᵘ
   +-*-isHeytingField : IsHeytingField _≃_ _≠_ _+_ _*_ -_ 0ℚᵘ 1ℚᵘ
   ```
 
 * Added new bundles to `Data.Rational.Unnormalised.Properties`
   ```agda
+  <-denseLinearOrder : DenseLinearOrder 0ℓ 0ℓ 0ℓ
   +-*-heytingCommutativeRing : HeytingCommutativeRing 0ℓ 0ℓ 0ℓ
   +-*-heytingField : HeytingField 0ℓ 0ℓ 0ℓ
   ```

src/Data/Rational/Properties.agda

@@ -51,11 +51,11 @@ open import Function.Definitions using (Injective)
 open import Level using (0ℓ)
 open import Relation.Binary.Core using (_⇒_; _Preserves_⟶_; _Preserves₂_⟶_⟶_)
 open import Relation.Binary.Bundles
-  using (Setoid; DecSetoid; TotalPreorder; DecTotalOrder; StrictPartialOrder; StrictTotalOrder)
+  using (Setoid; DecSetoid; TotalPreorder; DecTotalOrder; StrictPartialOrder; StrictTotalOrder; DenseLinearOrder)
 open import Relation.Binary.Structures
-  using (IsPreorder; IsTotalOrder; IsTotalPreorder; IsPartialOrder; IsDecTotalOrder; IsStrictPartialOrder; IsStrictTotalOrder)
+  using (IsPreorder; IsTotalOrder; IsTotalPreorder; IsPartialOrder; IsDecTotalOrder; IsStrictPartialOrder; IsStrictTotalOrder; IsDenseLinearOrder)
 open import Relation.Binary.Definitions
-  using (DecidableEquality; Reflexive; Transitive; Antisymmetric; Total; Decidable; Irrelevant; Irreflexive; Asymmetric; Trans; Trichotomous; tri<; tri>; tri≈; _Respectsʳ_; _Respectsˡ_; _Respects₂_)
+  using (DecidableEquality; Reflexive; Transitive; Antisymmetric; Total; Decidable; Irrelevant; Irreflexive; Asymmetric; Dense; Trans; Trichotomous; tri<; tri>; tri≈; _Respectsʳ_; _Respectsˡ_; _Respects₂_)
 open import Relation.Binary.PropositionalEquality
 open import Relation.Binary.Morphism.Structures
 import Relation.Binary.Morphism.OrderMonomorphism as OrderMonomorphisms
@@ -614,6 +614,20 @@ toℚᵘ-isOrderMonomorphism-< = record
 <-asym : Asymmetric _<_
 <-asym (*<* p<q) (*<* q<p) = ℤ.<-asym p<q q<p
 
+<-dense : Dense _<_
+<-dense {p} {q} p<q = let
+    m , p<ᵘm , m<ᵘq = ℚᵘ.<-dense (toℚᵘ-mono-< p<q)
+
+    m≃m : m ≃ᵘ toℚᵘ (fromℚᵘ m)
+    m≃m = ℚᵘ.≃-sym (toℚᵘ-fromℚᵘ m)
+
+    p<m : p < fromℚᵘ m
+    p<m = toℚᵘ-cancel-< (ℚᵘ.<-respʳ-≃ m≃m p<ᵘm)
+
+    m<q : fromℚᵘ m < q
+    m<q = toℚᵘ-cancel-< (ℚᵘ.<-respˡ-≃ m≃m m<ᵘq)
+  in fromℚᵘ m , p<m , m<q
+
 <-≤-trans : Trans _<_ _≤_ _<_
 <-≤-trans {p} {q} {r} (*<* p<q) (*≤* q≤r) = *<*
   (ℤ.*-cancelʳ-<-nonNeg _ (begin-strict
@@ -693,6 +707,12 @@ _>?_ = flip _<?_
   ; compare       = <-cmp
   }
 
+<-isDenseLinearOrder : IsDenseLinearOrder _≡_ _<_
+<-isDenseLinearOrder = record
+  { isStrictTotalOrder = <-isStrictTotalOrder
+  ; dense              = <-dense
+  }
+
 ------------------------------------------------------------------------
 -- Bundles
 
@@ -706,6 +726,11 @@ _>?_ = flip _<?_
   { isStrictTotalOrder = <-isStrictTotalOrder
   }
 
+<-denseLinearOrder : DenseLinearOrder 0ℓ 0ℓ 0ℓ
+<-denseLinearOrder = record
+  { isDenseLinearOrder = <-isDenseLinearOrder
+  }
+
 ------------------------------------------------------------------------
 -- A specialised module for reasoning about the _≤_ and _<_ relations
 ------------------------------------------------------------------------

src/Data/Rational/Unnormalised/Properties.agda

@@ -1,4 +1,4 @@
-------------------------------------------------------------------------
+-----------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Properties of unnormalized Rational numbers
@@ -17,7 +17,6 @@ open import Algebra.Consequences.Propositional
 open import Algebra.Construct.NaturalChoice.Base
 import Algebra.Construct.NaturalChoice.MinMaxOp as MinMaxOp
 import Algebra.Lattice.Construct.NaturalChoice.MinMaxOp as LatticeMinMaxOp
-open import Data.Empty using (⊥-elim)
 open import Data.Bool.Base using (T; true; false)
 open import Data.Nat.Base as ℕ using (suc; pred)
 import Data.Nat.Properties as ℕ
@@ -36,11 +35,11 @@ import Relation.Nullary.Decidable as Dec
 open import Relation.Nullary.Negation using (contradiction; contraposition)
 open import Relation.Binary.Core using (_⇒_; _Preserves_⟶_; _Preserves₂_⟶_⟶_)
 open import Relation.Binary.Bundles
-  using (Setoid; DecSetoid; Preorder; TotalPreorder; Poset; TotalOrder; DecTotalOrder; StrictPartialOrder; StrictTotalOrder)
+  using (Setoid; DecSetoid; Preorder; TotalPreorder; Poset; TotalOrder; DecTotalOrder; StrictPartialOrder; StrictTotalOrder; DenseLinearOrder)
 open import Relation.Binary.Structures
-  using (IsEquivalence; IsDecEquivalence; IsApartnessRelation; IsTotalPreorder; IsPreorder; IsPartialOrder; IsTotalOrder; IsDecTotalOrder; IsStrictPartialOrder; IsStrictTotalOrder)
+  using (IsEquivalence; IsDecEquivalence; IsApartnessRelation; IsTotalPreorder; IsPreorder; IsPartialOrder; IsTotalOrder; IsDecTotalOrder; IsStrictPartialOrder; IsStrictTotalOrder; IsDenseLinearOrder)
 open import Relation.Binary.Definitions
-  using (Reflexive; Symmetric; Transitive; Cotransitive; Tight; Decidable; Antisymmetric; Asymmetric; Total; Trans; Trichotomous; Irreflexive; Irrelevant; _Respectsˡ_; _Respectsʳ_; _Respects₂_; tri≈; tri<; tri>)
+  using (Reflexive; Symmetric; Transitive; Cotransitive; Tight; Decidable; Antisymmetric; Asymmetric; Dense; Total; Trans; Trichotomous; Irreflexive; Irrelevant; _Respectsˡ_; _Respectsʳ_; _Respects₂_; tri≈; tri<; tri>)
 import Relation.Binary.Consequences as BC
 open import Relation.Binary.PropositionalEquality
 import Relation.Binary.Properties.Poset as PosetProperties
@@ -119,7 +118,7 @@ p ≃? q = Dec.map′ *≡* drop-*≡* (↥ p ℤ.* ↧ q ℤ.≟ ↥ q ℤ.* 
 ≠-cotransitive {x} {y} x≠y z with x ≃? z | z ≃? y
 ... | no  x≠z | _       = inj₁ x≠z
 ... | yes _   | no z≠y  = inj₂ z≠y
-... | yes x≃z | yes z≃y = ⊥-elim (x≠y (≃-trans x≃z z≃y))
+... | yes x≃z | yes z≃y = contradiction (≃-trans x≃z z≃y) x≠y
 
 ≃-isEquivalence : IsEquivalence _≃_
 ≃-isEquivalence = record
@@ -412,6 +411,39 @@ drop-*<* (*<* pq<qp) = pq<qp
 <-asym : Asymmetric _<_
 <-asym (*<* x<y) = ℤ.<-asym x<y ∘ drop-*<*
 
+<-dense : Dense _<_
+<-dense {p} {q} (*<* p<q) = m , p<m , m<q
+  where
+  open ℤ.≤-Reasoning
+  m : ℚᵘ
+  m = mkℚᵘ (↥ p ℤ.+ ↥ q) (pred (↧ₙ p ℕ.+ ↧ₙ q))
+
+  p<m : p < m
+  p<m = *<* (begin-strict
+    ↥ p ℤ.* ↧ m
+      ≡⟨⟩
+    ↥ p ℤ.* (↧ p ℤ.+ ↧ q)
+      ≡⟨ ℤ.*-distribˡ-+ (↥ p) (↧ p) (↧ q) ⟩
+    ↥ p ℤ.* ↧ p ℤ.+ ↥ p ℤ.* ↧ q
+      <⟨ ℤ.+-monoʳ-< (↥ p ℤ.* ↧ p) p<q ⟩
+    ↥ p ℤ.* ↧ p ℤ.+ ↥ q ℤ.* ↧ p
+      ≡˘⟨ ℤ.*-distribʳ-+ (↧ p) (↥ p) (↥ q) ⟩
+    (↥ p ℤ.+ ↥ q) ℤ.* ↧ p
+      ≡⟨⟩
+    ↥ m ℤ.* ↧ p ∎)
+
+  m<q : m < q
+  m<q = *<* (begin-strict
+    ↥ m ℤ.* ↧ q
+      ≡⟨ ℤ.*-distribʳ-+ (↧ q) (↥ p) (↥ q) ⟩
+    ↥ p ℤ.* ↧ q ℤ.+ ↥ q ℤ.* ↧ q
+      <⟨ ℤ.+-monoˡ-< (↥ q ℤ.* ↧ q) p<q ⟩
+    ↥ q ℤ.* ↧ p ℤ.+ ↥ q ℤ.* ↧ q
+      ≡˘⟨ ℤ.*-distribˡ-+ (↥ q) (↧ p) (↧ q) ⟩
+    ↥ q ℤ.* (↧ p ℤ.+ ↧ q)
+      ≡⟨⟩
+    ↥ q ℤ.* ↧ m ∎)
+
 ≤-<-trans : Trans _≤_ _<_ _<_
 ≤-<-trans {p} {q} {r} (*≤* p≤q) (*<* q<r) = *<* $
   ℤ.*-cancelʳ-<-nonNeg _ $ begin-strict
@@ -517,6 +549,12 @@ _>?_ = flip _<?_
   ; compare       = <-cmp
   }
 
+<-isDenseLinearOrder : IsDenseLinearOrder _≃_ _<_
+<-isDenseLinearOrder = record
+  { isStrictTotalOrder = <-isStrictTotalOrder
+  ; dense              = <-dense
+  }
+
 ------------------------------------------------------------------------
 -- Bundles
 
@@ -535,6 +573,11 @@ _>?_ = flip _<?_
   { isStrictTotalOrder = <-isStrictTotalOrder
   }
 
+<-denseLinearOrder : DenseLinearOrder 0ℓ 0ℓ 0ℓ
+<-denseLinearOrder = record
+  { isDenseLinearOrder = <-isDenseLinearOrder
+  }
+
 ------------------------------------------------------------------------
 -- A specialised module for reasoning about the _≤_ and _<_ relations
 ------------------------------------------------------------------------

src/Data/Tree/AVL/Indexed/WithK.agda

@@ -15,6 +15,7 @@ module Data.Tree.AVL.Indexed.WithK
        {k r} (Key : Set k) {_<_ : Rel Key r}
        (isStrictTotalOrder : IsStrictTotalOrder _≡_ _<_) where
 
+strictTotalOrder : StrictTotalOrder _ _ _
 strictTotalOrder = record { isStrictTotalOrder = isStrictTotalOrder }
 
 open import Data.Tree.AVL.Indexed strictTotalOrder as AVL hiding (Value)

src/Data/Tree/AVL/NonEmpty/Propositional.agda

@@ -17,7 +17,9 @@ module Data.Tree.AVL.NonEmpty.Propositional
 
 open import Level
 
-private strictTotalOrder = record { isStrictTotalOrder = isStrictTotalOrder}
+private
+  strictTotalOrder : StrictTotalOrder _ _ _
+  strictTotalOrder = record { isStrictTotalOrder = isStrictTotalOrder}
 open import Data.Tree.AVL.Value (StrictTotalOrder.Eq.setoid strictTotalOrder)
 import Data.Tree.AVL.NonEmpty strictTotalOrder as AVL⁺
 

src/Relation/Binary/Bundles.agda

@@ -299,6 +299,24 @@ record StrictTotalOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) wh
   Please use Eq.decSetoid instead."
   #-}
 
+record DenseLinearOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
+  infix 4 _≈_ _<_
+  field
+    Carrier            : Set c
+    _≈_                : Rel Carrier ℓ₁
+    _<_                : Rel Carrier ℓ₂
+    isDenseLinearOrder : IsDenseLinearOrder _≈_ _<_
+
+  open IsDenseLinearOrder isDenseLinearOrder public
+    using (isStrictTotalOrder; dense)
+
+  strictTotalOrder : StrictTotalOrder c ℓ₁ ℓ₂
+  strictTotalOrder = record
+    { isStrictTotalOrder = isStrictTotalOrder
+    }
+
+  open StrictTotalOrder strictTotalOrder public
+
 
 ------------------------------------------------------------------------
 -- Apartness relations

src/Relation/Binary/Definitions.agda

@@ -13,7 +13,7 @@ module Relation.Binary.Definitions where
 open import Agda.Builtin.Equality using (_≡_)
 
 open import Data.Maybe.Base using (Maybe)
-open import Data.Product.Base using (_×_)
+open import Data.Product.Base using (_×_; ∃-syntax)
 open import Data.Sum.Base using (_⊎_)
 open import Function.Base using (_on_; flip)
 open import Level
@@ -88,6 +88,11 @@ Irreflexive _≈_ _<_ = ∀ {x y} → x ≈ y → ¬ (x < y)
 Asymmetric : Rel A ℓ → Set _
 Asymmetric _<_ = ∀ {x y} → x < y → ¬ (y < x)
 
+-- Density
+
+Dense : Rel A ℓ → Set _
+Dense _<_ = ∀ {x y} → x < y → ∃[ z ] x < z × z < y
+
 -- Generalised connex - exactly one of the two relations holds.
 
 Connex : REL A B ℓ₁ → REL B A ℓ₂ → Set _