Skip to content

Ob #453: added Dense relations and DenseLinearOrder #2111

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 9 commits into from
Oct 2, 2023
Merged
Show file tree
Hide file tree
Changes from 3 commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
45 changes: 28 additions & 17 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -280,7 +280,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`
Expand Down Expand Up @@ -360,8 +360,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
Expand All @@ -376,16 +376,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,
Expand Down Expand Up @@ -772,14 +772,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
Expand Down Expand Up @@ -1414,6 +1414,11 @@ Deprecated names
*-rawMonoid ↦ *-1-rawMonoid
```

* In `Data.Rational.Unnormalised.Properties`:
```
≤-steps ↦ p≤q⇒p≤r+q
```

* In `Data.Sum.Properties`:
```agda
[,]-∘-distr ↦ [,]-∘
Expand Down Expand Up @@ -1463,7 +1468,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-∘
Expand Down Expand Up @@ -2336,7 +2341,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)
Expand Down Expand Up @@ -3019,6 +3024,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)

Expand All @@ -3033,11 +3039,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
```

Expand Down Expand Up @@ -3271,7 +3279,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

Expand Down Expand Up @@ -3441,18 +3448,22 @@ 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
+-*-isHeytingCommutativeRing : IsHeytingCommutativeRing _≃_ _≠_ _+_ _*_ -_ 0ℚᵘ 1ℚᵘ
+-*-isHeytingField : IsHeytingField _≃_ _≠_ _+_ _*_ -_ 0ℚᵘ 1ℚᵘ
<-isDenseLinearOrder : IsDenseLinearOrder _≃_ _<_
```

* Added new bundles to `Data.Rational.Unnormalised.Properties`
```agda
+-*-heytingCommutativeRing : HeytingCommutativeRing 0ℓ 0ℓ 0ℓ
+-*-heytingField : HeytingField 0ℓ 0ℓ 0ℓ
<-denseLinearOrder : DenseLinearOrder 0ℓ 0ℓ 0ℓ
```

* Added new function to `Data.Vec.Relation.Binary.Pointwise.Inductive`
Expand Down
48 changes: 45 additions & 3 deletions src/Data/Rational/Unnormalised/Properties.agda
Original file line number Diff line number Diff line change
Expand Up @@ -36,11 +36,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
Expand Down Expand Up @@ -412,6 +412,37 @@ drop-*<* (*<* pq<qp) = pq<qp
<-asym : Asymmetric _<_
<-asym (*<* x<y) = ℤ.<-asym x<y ∘ drop-*<*

<-dense : Dense _<_
<-dense {p} {q} (*<* p<q) = mid , p<r , r<q
where
open ℤ.≤-Reasoning
mid : ℚᵘ
mid = mkℚᵘ ((↥ p) ℤ.+ (↥ q)) (pred ((↧ₙ p) ℕ.+ (↧ₙ q)))
p<r : p < mid
p<r = *<* (begin-strict
(↥ p) ℤ.* (↧ mid)
≡⟨⟩
(↥ 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)
≡⟨⟩
(↥ mid) ℤ.* (↧ p) ∎)
r<q : mid < q
r<q = *<* (begin-strict
(↥ mid) ℤ.* (↧ 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) ℤ.* (↧ mid) ∎)

≤-<-trans : Trans _≤_ _<_ _<_
≤-<-trans {p} {q} {r} (*≤* p≤q) (*<* q<r) = *<* $
ℤ.*-cancelʳ-<-nonNeg _ $ begin-strict
Expand Down Expand Up @@ -517,6 +548,12 @@ _>?_ = flip _<?_
; compare = <-cmp
}

<-isDenseLinearOrder : IsDenseLinearOrder _≃_ _<_
<-isDenseLinearOrder = record
{ isStrictTotalOrder = <-isStrictTotalOrder
; dense = <-dense
}

------------------------------------------------------------------------
-- Bundles

Expand All @@ -535,6 +572,11 @@ _>?_ = flip _<?_
{ isStrictTotalOrder = <-isStrictTotalOrder
}

<-denseLinearOrder : DenseLinearOrder 0ℓ 0ℓ 0ℓ
<-denseLinearOrder = record
{ isDenseLinearOrder = <-isDenseLinearOrder
}

------------------------------------------------------------------------
-- A specialised module for reasoning about the _≤_ and _<_ relations
------------------------------------------------------------------------
Expand Down
1 change: 1 addition & 0 deletions src/Data/Tree/AVL/Indexed/WithK.agda
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
4 changes: 3 additions & 1 deletion src/Data/Tree/AVL/NonEmpty/Propositional.agda
Original file line number Diff line number Diff line change
Expand Up @@ -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⁺

Expand Down
17 changes: 17 additions & 0 deletions src/Relation/Binary/Bundles.agda
Original file line number Diff line number Diff line change
Expand Up @@ -299,6 +299,23 @@ 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

strictTotalOrder : StrictTotalOrder c ℓ₁ ℓ₂
strictTotalOrder = record
{ isStrictTotalOrder = isStrictTotalOrder
}

--open StrictTotalOrder strictTotalOrder public


------------------------------------------------------------------------
-- Apartness relations
Expand Down
7 changes: 6 additions & 1 deletion src/Relation/Binary/Definitions.agda
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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 _
Expand Down
8 changes: 8 additions & 0 deletions src/Relation/Binary/Structures.agda
Original file line number Diff line number Diff line change
Expand Up @@ -280,6 +280,14 @@ record IsStrictTotalOrder (_<_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) wher
using (irrefl; asym; <-respʳ-≈; <-respˡ-≈; <-resp-≈)


record IsDenseLinearOrder (_<_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where
field
isStrictTotalOrder : IsStrictTotalOrder _<_
dense : Dense _<_

open IsStrictTotalOrder isStrictTotalOrder public


------------------------------------------------------------------------
-- Apartness relations
------------------------------------------------------------------------
Expand Down