diff --git a/CHANGELOG.md b/CHANGELOG.md index e56fc6dcd8..1c23ceb055 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -344,7 +344,7 @@ Non-backwards compatible changes ### Change in reduction behaviour of rationals * Currently arithmetic expressions involving rationals (both normalised and - unnormalised) undergo disastorous exponential normalisation. For example, + unnormalised) undergo disastrous exponential normalisation. For example, `p + q` would often be normalised by Agda to `(↥ p ℤ.* ↧ q ℤ.+ ↥ q ℤ.* ↧ p) / (↧ₙ p ℕ.* ↧ₙ q)`. While the normalised form of `p + q + r + s + t + u + v` would be ~700 lines long. This behaviour @@ -677,6 +677,22 @@ Non-backwards compatible changes exported by `Data.Rational.Base`. You will have to open `Data.Integer(.Base)` directly to use them. +* The names of the (in)equational reasoning combinators defined in the internal + modules `Data.Rational(.Unnormalised).Properties.≤-Reasoning` have been renamed + (issue #1437) to conform with the defined setoid equality `_≃_` on `Rational`s: + ```agda + step-≈ ↦ step-≃ + step-≃˘ ↦ step-≃˘ + ``` + with corresponding associated syntax: + ```agda + _≈⟨_⟩_ ↦ _≃⟨_⟩_ + _≈˘⟨_⟩_ ↦ _≃˘⟨_⟩_ + ``` + NB. It is not possible to rename or deprecate `syntax` declarations, so Agda will + only issue a "Could not parse the application `begin ...` when scope checking" + warning if the old combinators are used. + * The types of the proofs `pos⇒1/pos`/`1/pos⇒pos` and `neg⇒1/neg`/`1/neg⇒neg` in `Data.Rational(.Unnormalised).Properties` have been switched, as the previous naming scheme didn't correctly generalise to e.g. `pos+pos⇒pos`. For example diff --git a/src/Data/Rational/Properties.agda b/src/Data/Rational/Properties.agda index cdae93364b..805b2786a8 100644 --- a/src/Data/Rational/Properties.agda +++ b/src/Data/Rational/Properties.agda @@ -429,9 +429,9 @@ toℚᵘ-cong refl = *≡* refl fromℚᵘ-cong : fromℚᵘ Preserves _≃ᵘ_ ⟶ _≡_ fromℚᵘ-cong {p} {q} p≃q = toℚᵘ-injective (begin-equality - toℚᵘ (fromℚᵘ p) ≈⟨ toℚᵘ-fromℚᵘ p ⟩ - p ≈⟨ p≃q ⟩ - q ≈˘⟨ toℚᵘ-fromℚᵘ q ⟩ + toℚᵘ (fromℚᵘ p) ≃⟨ toℚᵘ-fromℚᵘ p ⟩ + p ≃⟨ p≃q ⟩ + q ≃˘⟨ toℚᵘ-fromℚᵘ q ⟩ toℚᵘ (fromℚᵘ q) ∎) where open ℚᵘ.≤-Reasoning @@ -705,15 +705,24 @@ _>?_ = flip __ *-monoˡ-<-neg r {p} {q} p q *-cancelˡ-<-nonPos {p} {q} r rp?_ = flip __ *-monoˡ-<-neg r {p} {q} p0}} p0 = positive (neg-mono-< (negative⁻¹ r)) @@ -1215,9 +1225,9 @@ private *-cancelˡ-<-nonPos : ∀ r .{{_ : NonPositive r}} → r * p < r * q → q < p *-cancelˡ-<-nonPos {p} {q} r rp1⇒1/p<1 {p} p>1 = lemma′ p (p>1⇒p≢0 p>1) p>1 1/-antimono-≤-pos : ∀ {p q} .{{_ : Positive p}} .{{_ : Positive q}} → p ≤ q → (1/ q) {{pos⇒nonZero q}} ≤ (1/ p) {{pos⇒nonZero p}} 1/-antimono-≤-pos {p} {q} p≤q = begin - 1/q ≈˘⟨ *-identityˡ 1/q ⟩ - 1ℚᵘ * 1/q ≈˘⟨ *-congʳ (*-inverseˡ p) ⟩ + 1/q ≃˘⟨ *-identityˡ 1/q ⟩ + 1ℚᵘ * 1/q ≃˘⟨ *-congʳ (*-inverseˡ p) ⟩ (1/p * p) * 1/q ≤⟨ *-monoˡ-≤-nonNeg 1/q (*-monoʳ-≤-nonNeg 1/p p≤q) ⟩ - (1/p * q) * 1/q ≈⟨ *-assoc 1/p q 1/q ⟩ - 1/p * (q * 1/q) ≈⟨ *-congˡ {1/p} (*-inverseʳ q) ⟩ - 1/p * 1ℚᵘ ≈⟨ *-identityʳ (1/p) ⟩ + (1/p * q) * 1/q ≃⟨ *-assoc 1/p q 1/q ⟩ + 1/p * (q * 1/q) ≃⟨ *-congˡ {1/p} (*-inverseʳ q) ⟩ + 1/p * 1ℚᵘ ≃⟨ *-identityʳ (1/p) ⟩ 1/p ∎ where open ≤-Reasoning