Merge branch 'master' into refinement-value-injective

CHANGELOG.md

@@ -11,6 +11,10 @@ Bug-fixes
 
 * Removed unnecessary parameter `#-trans : Transitive _#_` from
   `Relation.Binary.Reasoning.Base.Apartness`.
+* Relax the types for `≡-syntax` in `Relation.Binary.HeterogeneousEquality`.
+  These operators are used for equational reasoning of heterogeneous equality
+  `x ≅ y`, but previously the three operators in `≡-syntax` unnecessarily require
+  `x` and `y` to have the same type, making them unusable in most situations.
 
 Non-backwards compatible changes
 --------------------------------
@@ -318,11 +322,31 @@ Additions to existing modules
   m≤pred[n]⇒suc[m]≤n : .{{NonZero n}} → m ≤ pred n → suc m ≤ n
   ```
 
+* New lemmas in `Data.Rational.Properties`:
+  ```agda
+  nonNeg+nonNeg⇒nonNeg : ∀ p .{{_ : NonNegative p}} q .{{_ : NonNegative q}} → NonNegative (p + q)
+  nonPos+nonPos⇒nonPos : ∀ p .{{_ : NonPositive p}} q .{{_ : NonPositive q}} → NonPositive (p + q)
+  pos+nonNeg⇒pos : ∀ p .{{_ : Positive p}} q .{{_ : NonNegative q}} → Positive (p + q)
+  nonNeg+pos⇒pos : ∀ p .{{_ : NonNegative p}} q .{{_ : Positive q}} → Positive (p + q)
+  pos+pos⇒pos : ∀ p .{{_ : Positive p}} q .{{_ : Positive q}} → Positive (p + q)
+  neg+nonPos⇒neg : ∀ p .{{_ : Negative p}} q .{{_ : NonPositive q}} → Negative (p + q)
+  nonPos+neg⇒neg : ∀ p .{{_ : NonPositive p}} q .{{_ : Negative q}} → Negative (p + q)
+  neg+neg⇒neg : ∀ p .{{_ : Negative p}} q .{{_ : Negative q}} → Negative (p + q)
+  nonNeg*nonNeg⇒nonNeg : ∀ p .{{_ : NonNegative p}} q .{{_ : NonNegative q}} → NonNegative (p * q)
+  nonPos*nonNeg⇒nonPos : ∀ p .{{_ : NonPositive p}} q .{{_ : NonNegative q}} → NonPositive (p * q)
+  nonNeg*nonPos⇒nonPos : ∀ p .{{_ : NonNegative p}} q .{{_ : NonPositive q}} → NonPositive (p * q)
+  nonPos*nonPos⇒nonPos : ∀ p .{{_ : NonPositive p}} q .{{_ : NonPositive q}} → NonNegative (p * q)
+  pos*pos⇒pos : ∀ p .{{_ : Positive p}} q .{{_ : Positive q}} → Positive (p * q)
+  neg*pos⇒neg : ∀ p .{{_ : Negative p}} q .{{_ : Positive q}} → Negative (p * q)
+  pos*neg⇒neg : ∀ p .{{_ : Positive p}} q .{{_ : Negative q}} → Negative (p * q)
+  neg*neg⇒pos : ∀ p .{{_ : Negative p}} q .{{_ : Negative q}} → Positive (p * q)
+  ```
+
 * New properties re-exported from `Data.Refinement`:
   ```agda
   value-injective : value v ≡ value w → v ≡ w
   _≟_             : DecidableEquality A → DecidableEquality [ x ∈ A ∣ P x ]
-  ```
+ ```
 
 * New lemma in `Data.Vec.Properties`:
   ```agda
@@ -334,17 +358,35 @@ Additions to existing modules
   _≡?_ : DecidableEquality (Vec A n)
   ```
 
+* In `Relation.Binary.Bundles`:
+  ```agda
+  record DecPreorder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂))
+  ```
+  plus associated sub-bundles.
+
 * In `Relation.Binary.Construct.Interior.Symmetric`:
   ```agda
   decidable         : Decidable R → Decidable (SymInterior R)
   ```
   and for `Reflexive` and `Transitive` relations `R`:
   ```agda
   isDecEquivalence  : Decidable R → IsDecEquivalence (SymInterior R)
+  isDecPreorder     : Decidable R → IsDecPreorder (SymInterior R) R
   isDecPartialOrder : Decidable R → IsDecPartialOrder (SymInterior R) R
+  decPreorder       : Decidable R → DecPreorder _ _ _
   decPoset          : Decidable R → DecPoset _ _ _
   ```
 
+* In `Relation.Binary.Structures`:
+  ```agda
+  record IsDecPreorder (_≲_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where
+    field
+      isPreorder : IsPreorder _≲_
+      _≟_        : Decidable _≈_
+      _≲?_       : Decidable _≲_
+  ```
+  plus associated `isDecPreorder` fields in each higher `IsDec*Order` structure.
+
 * In `Relation.Nullary.Decidable`:
   ```agda
   does-⇔  : A ⇔ B → (a? : Dec A) → (b? : Dec B) → does a? ≡ does b?

src/Data/List/Relation/Binary/Equality/DecSetoid.agda

@@ -7,33 +7,25 @@
 {-# OPTIONS --cubical-compatible --safe #-}
 
 open import Relation.Binary.Bundles using (DecSetoid)
-open import Relation.Binary.Structures using (IsDecEquivalence)
-open import Relation.Binary.Definitions using (Decidable)
 
 module Data.List.Relation.Binary.Equality.DecSetoid
   {a ℓ} (DS : DecSetoid a ℓ) where
 
 import Data.List.Relation.Binary.Equality.Setoid as SetoidEquality
-import Data.List.Relation.Binary.Pointwise as PW
-open import Level
-open import Relation.Binary.Definitions using (Decidable)
-open DecSetoid DS
-
-------------------------------------------------------------------------
--- Make all definitions from setoid equality available
-
-open SetoidEquality setoid public
+open import Data.List.Relation.Binary.Pointwise using (decSetoid)
+open DecSetoid DS using (setoid)
 
 ------------------------------------------------------------------------
 -- Additional properties
 
-infix 4 _≋?_
+≋-decSetoid : DecSetoid _ _
+≋-decSetoid = decSetoid DS
 
-_≋?_ : Decidable _≋_
-_≋?_ = PW.decidable _≟_
+open DecSetoid ≋-decSetoid public
+  using ()
+  renaming (isDecEquivalence to ≋-isDecEquivalence; _≟_ to _≋?_)
 
-≋-isDecEquivalence : IsDecEquivalence _≋_
-≋-isDecEquivalence = PW.isDecEquivalence isDecEquivalence
+------------------------------------------------------------------------
+-- Make all definitions from setoid equality available
 
-≋-decSetoid : DecSetoid a (a ⊔ ℓ)
-≋-decSetoid = PW.decSetoid DS
+open SetoidEquality setoid public

src/Data/List/Relation/Binary/Equality/Setoid.agda

@@ -48,24 +48,17 @@ open PW public
 -- Relational properties
 ------------------------------------------------------------------------
 
-≋-refl : Reflexive _≋_
-≋-refl = PW.refl refl
-
-≋-reflexive : _≡_ ⇒ _≋_
-≋-reflexive ≡.refl = ≋-refl
-
-≋-sym : Symmetric _≋_
-≋-sym = PW.symmetric sym
-
-≋-trans : Transitive _≋_
-≋-trans = PW.transitive trans
-
-≋-isEquivalence : IsEquivalence _≋_
-≋-isEquivalence = PW.isEquivalence isEquivalence
-
 ≋-setoid : Setoid _ _
 ≋-setoid = PW.setoid S
 
+open Setoid ≋-setoid public
+  using ()
+  renaming ( refl to ≋-refl
+           ; reflexive to ≋-reflexive
+           ; sym to ≋-sym
+           ; trans to ≋-trans
+           ; isEquivalence to ≋-isEquivalence)
+
 ------------------------------------------------------------------------
 -- Relationships to predicates
 ------------------------------------------------------------------------

src/Data/List/Relation/Binary/Subset/DecSetoid.agda

@@ -14,10 +14,10 @@ open import Function.Base using (_∘_)
 open import Data.List.Base using ([]; _∷_)
 open import Data.List.Relation.Unary.Any using (here; there; map)
 open import Relation.Binary.Definitions using (Decidable)
-open import Relation.Nullary using (yes; no)
-open DecSetoid S
-open import Data.List.Relation.Binary.Equality.DecSetoid S
-open import Data.List.Membership.DecSetoid S
+open import Relation.Nullary.Decidable.Core using (yes; no)
+
+open DecSetoid S using (setoid; refl; trans)
+open import Data.List.Membership.DecSetoid S using (_∈?_)
 
 -- Re-export definitions
 open import Data.List.Relation.Binary.Subset.Setoid setoid public

src/Data/Rational/Properties.agda

@@ -1012,6 +1012,12 @@ neg-distrib-+ = +-Monomorphism.⁻¹-distrib-∙ ℚᵘ.+-0-isAbelianGroup (ℚ
 +-monoʳ-≤ : ∀ r → (_+_ r) Preserves _≤_ ⟶ _≤_
 +-monoʳ-≤ r p≤q = +-mono-≤ (≤-refl {r}) p≤q
 
+nonNeg+nonNeg⇒nonNeg : ∀ p .{{_ : NonNegative p}} q .{{_ : NonNegative q}} → NonNegative (p + q)
+nonNeg+nonNeg⇒nonNeg p q = nonNegative $ +-mono-≤ (nonNegative⁻¹ p) (nonNegative⁻¹ q)
+
+nonPos+nonPos⇒nonPos : ∀ p .{{_ : NonPositive p}} q .{{_ : NonPositive q}} → NonPositive (p + q)
+nonPos+nonPos⇒nonPos p q = nonPositive $ +-mono-≤ (nonPositive⁻¹ p) (nonPositive⁻¹ q)
+
 ------------------------------------------------------------------------
 -- Properties of _+_ and _<_
 
@@ -1035,6 +1041,24 @@ neg-distrib-+ = +-Monomorphism.⁻¹-distrib-∙ ℚᵘ.+-0-isAbelianGroup (ℚ
 +-monoʳ-< : ∀ r → (_+_ r) Preserves _<_ ⟶ _<_
 +-monoʳ-< r p<q = +-mono-≤-< (≤-refl {r}) p<q
 
+pos+nonNeg⇒pos : ∀ p .{{_ : Positive p}} q .{{_ : NonNegative q}} → Positive (p + q)
+pos+nonNeg⇒pos p q = positive $ +-mono-<-≤ (positive⁻¹ p) (nonNegative⁻¹ q)
+
+nonNeg+pos⇒pos : ∀ p .{{_ : NonNegative p}} q .{{_ : Positive q}} → Positive (p + q)
+nonNeg+pos⇒pos p q = positive $ +-mono-≤-< (nonNegative⁻¹ p) (positive⁻¹ q)
+
+pos+pos⇒pos : ∀ p .{{_ : Positive p}} q .{{_ : Positive q}} → Positive (p + q)
+pos+pos⇒pos p q = positive $ +-mono-< (positive⁻¹ p) (positive⁻¹ q)
+
+neg+nonPos⇒neg : ∀ p .{{_ : Negative p}} q .{{_ : NonPositive q}} → Negative (p + q)
+neg+nonPos⇒neg p q = negative $ +-mono-<-≤ (negative⁻¹ p) (nonPositive⁻¹ q)
+
+nonPos+neg⇒neg : ∀ p .{{_ : NonPositive p}} q .{{_ : Negative q}} → Negative (p + q)
+nonPos+neg⇒neg p q = negative $ +-mono-≤-< (nonPositive⁻¹ p) (negative⁻¹ q)
+
+neg+neg⇒neg : ∀ p .{{_ : Negative p}} q .{{_ : Negative q}} → Negative (p + q)
+neg+neg⇒neg p q = negative $ +-mono-< (negative⁻¹ p) (negative⁻¹ q)
+
 ------------------------------------------------------------------------
 -- Properties of _*_
 ------------------------------------------------------------------------
@@ -1340,6 +1364,34 @@ module _ where
 *-cancelˡ-≤-neg : ∀ r .{{_ : Negative r}} → r * p ≤ r * q → p ≥ q
 *-cancelˡ-≤-neg {p} {q} r rewrite *-comm r p | *-comm r q = *-cancelʳ-≤-neg r
 
+nonNeg*nonNeg⇒nonNeg : ∀ p .{{_ : NonNegative p}} q .{{_ : NonNegative q}} → NonNegative (p * q)
+nonNeg*nonNeg⇒nonNeg p q = nonNegative $ begin
+  0ℚ     ≡⟨ *-zeroʳ p ⟨
+  p * 0ℚ ≤⟨ *-monoˡ-≤-nonNeg p (nonNegative⁻¹ q) ⟩
+  p * q  ∎
+  where open ≤-Reasoning
+
+nonPos*nonNeg⇒nonPos : ∀ p .{{_ : NonPositive p}} q .{{_ : NonNegative q}} → NonPositive (p * q)
+nonPos*nonNeg⇒nonPos p q = nonPositive $ begin
+  p * q  ≤⟨ *-monoˡ-≤-nonPos p (nonNegative⁻¹ q) ⟩
+  p * 0ℚ ≡⟨ *-zeroʳ p ⟩
+  0ℚ     ∎
+  where open ≤-Reasoning
+
+nonNeg*nonPos⇒nonPos : ∀ p .{{_ : NonNegative p}} q .{{_ : NonPositive q}} → NonPositive (p * q)
+nonNeg*nonPos⇒nonPos p q = nonPositive $ begin
+  p * q  ≤⟨ *-monoˡ-≤-nonNeg p (nonPositive⁻¹ q) ⟩
+  p * 0ℚ ≡⟨ *-zeroʳ p ⟩
+  0ℚ     ∎
+  where open ≤-Reasoning
+
+nonPos*nonPos⇒nonPos : ∀ p .{{_ : NonPositive p}} q .{{_ : NonPositive q}} → NonNegative (p * q)
+nonPos*nonPos⇒nonPos p q = nonNegative $ begin
+  0ℚ     ≡⟨ *-zeroʳ p ⟨
+  p * 0ℚ ≤⟨ *-monoˡ-≤-nonPos p (nonPositive⁻¹ q) ⟩
+  p * q  ∎
+  where open ≤-Reasoning
+
 ------------------------------------------------------------------------
 -- Properties of _*_ and _<_
 
@@ -1387,6 +1439,34 @@ module _ where
 *-cancelʳ-<-nonPos : ∀ r .{{_ : NonPositive r}} → p * r < q * r → p > q
 *-cancelʳ-<-nonPos {p} {q} r rewrite *-comm p r | *-comm q r = *-cancelˡ-<-nonPos r
 
+pos*pos⇒pos : ∀ p .{{_ : Positive p}} q .{{_ : Positive q}} → Positive (p * q)
+pos*pos⇒pos p q = positive $ begin-strict
+  0ℚ     ≡⟨ *-zeroʳ p ⟨
+  p * 0ℚ <⟨ *-monoʳ-<-pos p (positive⁻¹ q) ⟩
+  p * q  ∎
+  where open ≤-Reasoning
+
+neg*pos⇒neg : ∀ p .{{_ : Negative p}} q .{{_ : Positive q}} → Negative (p * q)
+neg*pos⇒neg p q = negative $ begin-strict
+  p * q  <⟨ *-monoʳ-<-neg p (positive⁻¹ q) ⟩
+  p * 0ℚ ≡⟨ *-zeroʳ p ⟩
+  0ℚ     ∎
+  where open ≤-Reasoning
+
+pos*neg⇒neg : ∀ p .{{_ : Positive p}} q .{{_ : Negative q}} → Negative (p * q)
+pos*neg⇒neg p q = negative $ begin-strict
+  p * q  <⟨ *-monoʳ-<-pos p (negative⁻¹ q) ⟩
+  p * 0ℚ ≡⟨ *-zeroʳ p ⟩
+  0ℚ     ∎
+  where open ≤-Reasoning
+
+neg*neg⇒pos : ∀ p .{{_ : Negative p}} q .{{_ : Negative q}} → Positive (p * q)
+neg*neg⇒pos p q = positive $ begin-strict
+  0ℚ     ≡⟨ *-zeroʳ p ⟨
+  p * 0ℚ <⟨ *-monoʳ-<-neg p (negative⁻¹ q) ⟩
+  p * q  ∎
+  where open ≤-Reasoning
+
 ------------------------------------------------------------------------
 -- Properties of _⊓_
 ------------------------------------------------------------------------

src/Relation/Binary/Bundles.agda

@@ -132,6 +132,36 @@ record TotalPreorder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
   open Preorder preorder public
     hiding (Carrier; _≈_; _≲_; isPreorder)
 
+
+record DecPreorder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
+  field
+    Carrier         : Set c
+    _≈_             : Rel Carrier ℓ₁  -- The underlying equality.
+    _≲_             : Rel Carrier ℓ₂  -- The relation.
+    isDecPreorder   : IsDecPreorder _≈_ _≲_
+
+  private module DPO = IsDecPreorder isDecPreorder
+
+  open DPO public
+    using (_≟_; _≲?_; isPreorder)
+
+  preorder : Preorder c ℓ₁ ℓ₂
+  preorder = record
+    { isPreorder = isPreorder
+    }
+
+  open Preorder preorder public
+    hiding (Carrier; _≈_; _≲_; isPreorder; module Eq)
+
+  module Eq where
+    decSetoid : DecSetoid c ℓ₁
+    decSetoid = record
+      { isDecEquivalence = DPO.Eq.isDecEquivalence
+      }
+
+    open DecSetoid decSetoid public
+
+
 ------------------------------------------------------------------------
 -- Partial orders
 ------------------------------------------------------------------------
@@ -173,7 +203,7 @@ record DecPoset c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
   private module DPO = IsDecPartialOrder isDecPartialOrder
 
   open DPO public
-    using (_≟_; _≤?_; isPartialOrder)
+    using (_≟_; _≤?_; isPartialOrder; isDecPreorder)
 
   poset : Poset c ℓ₁ ℓ₂
   poset = record
@@ -183,13 +213,11 @@ record DecPoset c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
   open Poset poset public
     hiding (Carrier; _≈_; _≤_; isPartialOrder; module Eq)
 
-  module Eq where
-    decSetoid : DecSetoid c ℓ₁
-    decSetoid = record
-      { isDecEquivalence = DPO.Eq.isDecEquivalence
-      }
+  decPreorder : DecPreorder c ℓ₁ ℓ₂
+  decPreorder = record { isDecPreorder = isDecPreorder }
 
-    open DecSetoid decSetoid public
+  open DecPreorder decPreorder public
+    using (module Eq)
 
 
 record StrictPartialOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where

src/Relation/Binary/Construct/Interior/Symmetric.agda

@@ -100,12 +100,6 @@ module _ {R : Rel A ℓ} (refl : Reflexive R) (trans : Transitive R) where
 
   module _ (R? : Decidable R) where
 
-    isDecEquivalence : IsDecEquivalence (SymInterior R)
-    isDecEquivalence = record
-      { isEquivalence = isEquivalence
-      ; _≟_ = decidable R?
-      }
-
     isDecPartialOrder : IsDecPartialOrder (SymInterior R) R
     isDecPartialOrder = record
       { isPartialOrder = isPartialOrder
@@ -115,3 +109,10 @@ module _ {R : Rel A ℓ} (refl : Reflexive R) (trans : Transitive R) where
 
     decPoset : DecPoset _ ℓ ℓ
     decPoset = record { isDecPartialOrder = isDecPartialOrder }
+
+    open DecPoset public
+      using (isDecPreorder; decPreorder)
+
+    isDecEquivalence : IsDecEquivalence (SymInterior R)
+    isDecEquivalence = DecPoset.Eq.isDecEquivalence decPoset
+

src/Relation/Binary/HeterogeneousEquality.agda

@@ -234,22 +234,22 @@ module ≅-Reasoning where
 
   infix 4 _IsRelatedTo_
 
-  data _IsRelatedTo_ {A : Set ℓ} {B : Set ℓ} (x : A) (y : B) : Set ℓ where
+  data _IsRelatedTo_ {A : Set a} {B : Set b} (x : A) (y : B) : Set a where
     relTo : (x≅y : x ≅ y) → x IsRelatedTo y
 
   start : ∀ {x : A} {y : B} → x IsRelatedTo y → x ≅ y
   start (relTo x≅y) = x≅y
 
-  ≡-go : ∀ {A : Set a} → Trans {A = A} {C = A} _≡_ _IsRelatedTo_ _IsRelatedTo_
+  ≡-go : ∀ {A : Set a} {B : Set b} → Trans {A = A} {C = B} _≡_ _IsRelatedTo_ _IsRelatedTo_
   ≡-go x≡y (relTo y≅z) = relTo (trans (reflexive x≡y) y≅z)
 
   -- Combinators with one heterogeneous relation
-  module _ {A : Set ℓ} {B : Set ℓ} where
+  module _ {A : Set a} {B : Set b} where
     open begin-syntax (_IsRelatedTo_ {A = A} {B}) start public
+    open ≡-syntax (_IsRelatedTo_ {A = A} {B}) ≡-go public
 
   -- Combinators with homogeneous relations
-  module _ {A : Set ℓ} where
-    open ≡-syntax (_IsRelatedTo_ {A = A}) ≡-go public
+  module _ {A : Set a} where
     open end-syntax (_IsRelatedTo_ {A = A}) (relTo refl) public
 
   -- Can't create syntax in the standard `Syntax` module for