From 0a5e9cc4fbaa0e26f1f1e331bdb4688e724061b8 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sun, 1 Oct 2023 11:12:34 +0100 Subject: [PATCH 1/4] renamed negated equality symbol; knock-on deprecation --- CHANGELOG.md | 9 ++++++++- src/Data/Rational/Unnormalised/Base.agda | 11 ++++++++--- 2 files changed, 16 insertions(+), 4 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 3ba0274349..3ff7bac3d0 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -864,7 +864,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 @@ -1371,6 +1371,13 @@ Deprecated names <-step ↦ m Date: Sun, 1 Oct 2023 11:19:02 +0100 Subject: [PATCH 2/4] knock-on consequences; simplified `import`s --- src/Data/Rational/Properties.agda | 4 +- .../Rational/Unnormalised/Properties.agda | 67 +++++++++---------- 2 files changed, 34 insertions(+), 37 deletions(-) diff --git a/src/Data/Rational/Properties.agda b/src/Data/Rational/Properties.agda index 959573218a..21bc3823f4 100644 --- a/src/Data/Rational/Properties.agda +++ b/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 +open import Relation.Nullary.Decidable.Core 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.Negation.Core using (¬_; contradiction) open import Algebra.Definitions {A = ℚ} _≡_ open import Algebra.Structures {A = ℚ} _≡_ diff --git a/src/Data/Rational/Unnormalised/Properties.agda b/src/Data/Rational/Unnormalised/Properties.agda index 2ede5bb44c..cf4d2265e8 100644 --- a/src/Data/Rational/Unnormalised/Properties.agda +++ b/src/Data/Rational/Unnormalised/Properties.agda @@ -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 ℕ @@ -31,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) @@ -44,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 @@ -106,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 = ⊥-elim (x≠y (≃-trans x≃z z≃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 @@ -134,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 @@ -1084,11 +1081,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 @@ -1099,8 +1096,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 ⟩ @@ -1347,18 +1344,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 } ------------------------------------------------------------------------ From 4047297302405161401b8858bba8f4a4d988a2c8 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sun, 1 Oct 2023 11:46:48 +0100 Subject: [PATCH 3/4] more simplified `import`s --- src/Data/Rational/Base.agda | 4 ++-- src/Data/Rational/Unnormalised/Base.agda | 3 +-- 2 files changed, 3 insertions(+), 4 deletions(-) diff --git a/src/Data/Rational/Base.agda b/src/Data/Rational/Base.agda index 53739b8571..5f5a35e6f9 100644 --- a/src/Data/Rational/Base.agda +++ b/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 diff --git a/src/Data/Rational/Unnormalised/Base.agda b/src/Data/Rational/Unnormalised/Base.agda index 4f5186211d..dc5bd144dc 100644 --- a/src/Data/Rational/Unnormalised/Base.agda +++ b/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 From ab139d40f96b367649254ff659885e2d91e1b730 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 2 Oct 2023 08:17:44 +0100 Subject: [PATCH 4/4] another simplification --- src/Data/Rational/Properties.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/Rational/Properties.agda b/src/Data/Rational/Properties.agda index 21bc3823f4..5a87b4ef65 100644 --- a/src/Data/Rational/Properties.agda +++ b/src/Data/Rational/Properties.agda @@ -60,7 +60,7 @@ open import Relation.Binary.PropositionalEquality open import Relation.Binary.Morphism.Structures import Relation.Binary.Morphism.OrderMonomorphism as OrderMonomorphisms open import Relation.Nullary.Decidable.Core as Dec - using (True; False; fromWitness; fromWitnessFalse; toWitnessFalse; yes; no; recompute; map′; _×-dec_) + using (yes; no; recompute; map′; _×-dec_) open import Relation.Nullary.Negation.Core using (¬_; contradiction) open import Algebra.Definitions {A = ℚ} _≡_