Rectifies the negated equality symbol in Data.Rational.Unnormalised.* (#2118)

Author: jamesmckinna

CHANGELOG.md

@@ -892,7 +892,7 @@ Non-backwards compatible changes
   (issue #1437) to conform with the defined setoid equality `_≃_` on `Rational`s:
   ```agda
   step-≈  ↦  step-≃
-  step-≃˘ ↦  step-≃˘
+  step-≈˘ ↦  step-≃˘
   ```
   with corresponding associated syntax:
   ```agda
@@ -1399,6 +1399,13 @@ Deprecated names
   <-step          ↦  m<n⇒m<1+n
   ```
 
+* In `Data.Rational.Unnormalised.Base`:
+  ```
+  _≠_  ↦  _≄_
+  +-rawMonoid ↦ +-0-rawMonoid
+  *-rawMonoid ↦ *-1-rawMonoid
+  ```
+
 * In `Data.Rational.Unnormalised.Properties`:
   ```
   ↥[p/q]≡p         ↦  ↥[n/d]≡n

src/Data/Rational/Base.agda

@@ -19,8 +19,8 @@ open import Data.Rational.Unnormalised.Base as ℚᵘ using (ℚᵘ; mkℚᵘ)
 open import Data.Sum.Base using (inj₂)
 open import Function.Base using (id)
 open import Level using (0ℓ)
-open import Relation.Nullary using (¬_; recompute)
-open import Relation.Nullary.Negation using (contradiction)
+open import Relation.Nullary.Decidable.Core using (recompute)
+open import Relation.Nullary.Negation.Core using (¬_; contradiction)
 open import Relation.Unary using (Pred)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.PropositionalEquality.Core

src/Data/Rational/Properties.agda

@@ -59,9 +59,9 @@ open import Relation.Binary.Definitions
 open import Relation.Binary.PropositionalEquality
 open import Relation.Binary.Morphism.Structures
 import Relation.Binary.Morphism.OrderMonomorphism as OrderMonomorphisms
-open import Relation.Nullary.Decidable as Dec
-  using (True; False; fromWitness; fromWitnessFalse; toWitnessFalse; yes; no; recompute; map′; _×-dec_)
-open import Relation.Nullary.Negation using (¬_; contradiction; contraposition)
+open import Relation.Nullary.Decidable.Core as Dec
+  using (yes; no; recompute; map′; _×-dec_)
+open import Relation.Nullary.Negation.Core using (¬_; contradiction)
 
 open import Algebra.Definitions {A = ℚ} _≡_
 open import Algebra.Structures  {A = ℚ} _≡_

src/Data/Rational/Unnormalised/Base.agda

@@ -14,8 +14,7 @@ open import Data.Integer.Base as ℤ
   using (ℤ; +_; +0; +[1+_]; -[1+_]; +<+; +≤+)
 open import Data.Nat.Base as ℕ using (ℕ; zero; suc)
 open import Level using (0ℓ)
-open import Relation.Nullary.Negation using (¬_)
-open import Relation.Nullary.Negation using (contradiction)
+open import Relation.Nullary.Negation.Core using (¬_; contradiction)
 open import Relation.Unary using (Pred)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.PropositionalEquality.Core
@@ -66,8 +65,8 @@ infix 4 _≃_ _≠_
 data _≃_ : Rel ℚᵘ 0ℓ where
   *≡* : ∀ {p q} → (↥ p ℤ.* ↧ q) ≡ (↥ q ℤ.* ↧ p) → p ≃ q
 
-_≠_ : Rel ℚᵘ 0ℓ
-p ≠ q = ¬ (p ≃ q)
+_≄_ : Rel ℚᵘ 0ℓ
+p ≄ q = ¬ (p ≃ q)
 
 ------------------------------------------------------------------------
 -- Ordering of rationals
@@ -156,7 +155,7 @@ NonNegative p = ℤ.NonNegative (↥ p)
 -- from ℤ but it requires importing `Data.Integer.Properties` which
 -- we would like to avoid doing.
 
-≢-nonZero : ∀ {p} → p ≠ 0ℚᵘ → NonZero p
+≢-nonZero : ∀ {p} → p ≄ 0ℚᵘ → NonZero p
 ≢-nonZero {mkℚᵘ -[1+ _ ] _      } _   = _
 ≢-nonZero {mkℚᵘ +[1+ _ ] _      } _   = _
 ≢-nonZero {mkℚᵘ +0       zero   } p≢0 = contradiction (*≡* refl) p≢0
@@ -378,3 +377,8 @@ Please use +-0-rawMonoid instead."
 "Warning: *-rawMonoid was deprecated in v2.0
 Please use *-1-rawMonoid instead."
 #-}
+_≠_ = _≄_
+{-# WARNING_ON_USAGE _≠_
+"Warning: _≠_ was deprecated in v2.0
+Please use _≄_ instead."
+#-}

src/Data/Rational/Unnormalised/Properties.agda

@@ -30,9 +30,8 @@ open import Data.Sum.Base using (_⊎_; [_,_]′; inj₁; inj₂)
 import Data.Sign as Sign
 open import Function.Base using (_on_; _$_; _∘_; flip)
 open import Level using (0ℓ)
-open import Relation.Nullary using (¬_; yes; no)
-import Relation.Nullary.Decidable as Dec
-open import Relation.Nullary.Negation using (contradiction; contraposition)
+open import Relation.Nullary.Decidable.Core as Dec using (yes; no)
+open import Relation.Nullary.Negation.Core using (¬_; contradiction)
 open import Relation.Binary.Core using (_⇒_; _Preserves_⟶_; _Preserves₂_⟶_⟶_)
 open import Relation.Binary.Bundles
   using (Setoid; DecSetoid; Preorder; TotalPreorder; Poset; TotalOrder; DecTotalOrder; StrictPartialOrder; StrictTotalOrder; DenseLinearOrder)
@@ -43,7 +42,6 @@ open import Relation.Binary.Definitions
 import Relation.Binary.Consequences as BC
 open import Relation.Binary.PropositionalEquality
 import Relation.Binary.Properties.Poset as PosetProperties
-open import Relation.Nullary using (yes; no)
 import Relation.Binary.Reasoning.Setoid as SetoidReasoning
 
 open import Algebra.Properties.CommutativeSemigroup ℤ.*-commutativeSemigroup
@@ -105,20 +103,20 @@ infix 4 _≃?_
 _≃?_ : Decidable _≃_
 p ≃? q = Dec.map′ *≡* drop-*≡* (↥ p ℤ.* ↧ q ℤ.≟ ↥ q ℤ.* ↧ p)
 
-0≠1 : 0ℚᵘ ≠ 1ℚᵘ
-0≠1 = Dec.from-no (0ℚᵘ ≃? 1ℚᵘ)
+0≄1 : 0ℚᵘ ≄ 1ℚᵘ
+0≄1 = Dec.from-no (0ℚᵘ ≃? 1ℚᵘ)
 
-≃-≠-irreflexive : Irreflexive _≃_ _≠_
-≃-≠-irreflexive x≃y x≠y = x≠y x≃y
+≃-≄-irreflexive : Irreflexive _≃_ _≄_
+≃-≄-irreflexive x≃y x≄y = x≄y x≃y
 
-≠-symmetric : Symmetric _≠_
-≠-symmetric x≠y y≃x = x≠y (≃-sym y≃x)
+≄-symmetric : Symmetric _≄_
+≄-symmetric x≄y y≃x = x≄y (≃-sym y≃x)
 
-≠-cotransitive : Cotransitive _≠_
-≠-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 = contradiction (≃-trans x≃z z≃y) x≠y
+≄-cotransitive : Cotransitive _≄_
+≄-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 = contradiction (≃-trans x≃z z≃y) x≄y
 
 ≃-isEquivalence : IsEquivalence _≃_
 ≃-isEquivalence = record
@@ -133,16 +131,16 @@ p ≃? q = Dec.map′ *≡* drop-*≡* (↥ p ℤ.* ↧ q ℤ.≟ ↥ q ℤ.* 
   ; _≟_           = _≃?_
   }
 
-≠-isApartnessRelation : IsApartnessRelation _≃_ _≠_
-≠-isApartnessRelation = record
-  { irrefl  = ≃-≠-irreflexive
-  ; sym     = ≠-symmetric
-  ; cotrans = ≠-cotransitive
+≄-isApartnessRelation : IsApartnessRelation _≃_ _≄_
+≄-isApartnessRelation = record
+  { irrefl  = ≃-≄-irreflexive
+  ; sym     = ≄-symmetric
+  ; cotrans = ≄-cotransitive
   }
 
-≠-tight : Tight _≃_ _≠_
-proj₁ (≠-tight p q) ¬p≠q = Dec.decidable-stable (p ≃? q) ¬p≠q
-proj₂ (≠-tight p q) p≃q p≠q = p≠q p≃q
+≄-tight : Tight _≃_ _≄_
+proj₁ (≄-tight p q) ¬p≄q = Dec.decidable-stable (p ≃? q) ¬p≄q
+proj₂ (≄-tight p q) p≃q p≄q = p≄q p≃q
 
 ≃-setoid : Setoid 0ℓ 0ℓ
 ≃-setoid = record
@@ -1127,11 +1125,11 @@ p≤q⇒0≤q-p {p} {q} p≤q = begin
 *-inverseʳ : ∀ p .{{_ : NonZero p}} → p * 1/ p ≃ 1ℚᵘ
 *-inverseʳ p = ≃-trans (*-comm p (1/ p)) (*-inverseˡ p)
 
-≠⇒invertible : p ≠ q → Invertible _≃_ 1ℚᵘ _*_ (p - q)
-≠⇒invertible {p} {q} p≠q = _ , *-inverseˡ (p - q) , *-inverseʳ (p - q)
+≄⇒invertible : p ≄ q → Invertible _≃_ 1ℚᵘ _*_ (p - q)
+≄⇒invertible {p} {q} p≄q = _ , *-inverseˡ (p - q) , *-inverseʳ (p - q)
   where instance
   _ : NonZero (p - q)
-  _ = ≢-nonZero (p≠q ∘ p-q≃0⇒p≃q p q)
+  _ = ≢-nonZero (p≄q ∘ p-q≃0⇒p≃q p q)
 
 *-zeroˡ : LeftZero _≃_ 0ℚᵘ _*_
 *-zeroˡ p@record{} = *≡* refl
@@ -1142,8 +1140,8 @@ p≤q⇒0≤q-p {p} {q} p≤q = begin
 *-zero : Zero _≃_ 0ℚᵘ _*_
 *-zero = *-zeroˡ , *-zeroʳ
 
-invertible⇒≠ : Invertible _≃_ 1ℚᵘ _*_ (p - q) → p ≠ q
-invertible⇒≠ {p} {q} (1/p-q , 1/x*x≃1 , x*1/x≃1) p≃q = 0≠1 (begin
+invertible⇒≄ : Invertible _≃_ 1ℚᵘ _*_ (p - q) → p ≄ q
+invertible⇒≄ {p} {q} (1/p-q , 1/x*x≃1 , x*1/x≃1) p≃q = 0≄1 (begin
   0ℚᵘ             ≈˘⟨ *-zeroˡ 1/p-q ⟩
   0ℚᵘ * 1/p-q     ≈˘⟨ *-congʳ (p≃q⇒p-q≃0 p q p≃q) ⟩
   (p - q) * 1/p-q ≈⟨ x*1/x≃1 ⟩
@@ -1390,18 +1388,18 @@ nonNeg*nonNeg⇒nonNeg p q = nonNegative
   ; *-comm = *-comm
   }
 
-+-*-isHeytingCommutativeRing : IsHeytingCommutativeRing _≃_ _≠_ _+_ _*_ -_ 0ℚᵘ 1ℚᵘ
++-*-isHeytingCommutativeRing : IsHeytingCommutativeRing _≃_ _≄_ _+_ _*_ -_ 0ℚᵘ 1ℚᵘ
 +-*-isHeytingCommutativeRing = record
   { isCommutativeRing   = +-*-isCommutativeRing
-  ; isApartnessRelation = ≠-isApartnessRelation
-  ; #⇒invertible        = ≠⇒invertible
-  ; invertible⇒#        = invertible⇒≠
+  ; isApartnessRelation = ≄-isApartnessRelation
+  ; #⇒invertible        = ≄⇒invertible
+  ; invertible⇒#        = invertible⇒≄
   }
 
-+-*-isHeytingField : IsHeytingField _≃_ _≠_ _+_ _*_ -_ 0ℚᵘ 1ℚᵘ
++-*-isHeytingField : IsHeytingField _≃_ _≄_ _+_ _*_ -_ 0ℚᵘ 1ℚᵘ
 +-*-isHeytingField = record
   { isHeytingCommutativeRing = +-*-isHeytingCommutativeRing
-  ; tight                    = ≠-tight
+  ; tight                    = ≄-tight
   }
 
 ------------------------------------------------------------------------