Improve reduction behaviour of rationals (#1764)

Author: MatthewDaggitt

CHANGELOG.md

@@ -306,6 +306,39 @@ Non-backwards compatible changes
   ∣↥p∣≢0⇒p≄0 : ∀ p → ℤ.∣ (↥ p) ∣ ≢0 → p ≠ 0ℚᵘ
   ```
 
+### Change in reduction behaviour of rationals
+
+* Currently arithmetic expressions involving rationals (both normalised and 
+  unnormalised) undergo disastorous 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
+  often chokes both type-checking and the display of the expressions in the IDE.
+
+* To avoid this expansion and make non-trivial reasoning about rationals actually feasible:
+  1. the records `ℚᵘ` and `ℚ` have both had the `no-eta-equality` flag enabled
+  2. definition of arithmetic operations have trivial pattern matching added to
+     prevent them reducing, e.g.
+     ```agda
+     p + q = (↥ p ℤ.* ↧ q ℤ.+ ↥ q ℤ.* ↧ p) / (↧ₙ p ℕ.* ↧ₙ q)
+     ```
+     has been changed to
+     ```
+     p@record{} + q@record{} = (↥ p ℤ.* ↧ q ℤ.+ ↥ q ℤ.* ↧ p) / (↧ₙ p ℕ.* ↧ₙ q)
+     ```
+
+* As a consequence of this, some proofs that relied on this reduction behaviour
+  or on eta-equality may no longer go through. There are several ways to fix this:
+  1. The principled way is to not rely on this reduction behaviour in the first place. 
+	 The `Properties` files for rational numbers have been greatly expanded in `v1.7` 
+	 and `v2.0`, and we believe most proofs should be able to be built up from existing
+	 proofs contained within these files.
+  2. Alternatively, annotating any rational arguments to a proof with either
+	 `@record{}` or `@(mkℚ _ _ _)` should restore the old reduction behaviour for any
+	 terms involving those parameters.
+  3. Finally, if the above approaches are not viable then you may be forced to explicitly
+	 use `cong` combined with a lemma that proves the old reduction behaviour.
+
 ### Change in the definition of `Prime`
 
 * The definition of `Prime` in `Data.Nat.Primality` was:
@@ -1306,6 +1339,9 @@ Other minor changes
 
 * Added new definitions and proofs in `Data.Rational.Properties`:
   ```agda
+  ↥ᵘ-toℚᵘ : ↥ᵘ (toℚᵘ p) ≡ ↥ p
+  ↧ᵘ-toℚᵘ : ↧ᵘ (toℚᵘ p) ≡ ↧ p
+  
   +-*-rawNearSemiring                 : RawNearSemiring 0ℓ 0ℓ
   +-*-rawSemiring                     : RawSemiring 0ℓ 0ℓ
   toℚᵘ-isNearSemiringHomomorphism-+-* : IsNearSemiringHomomorphism +-*-rawNearSemiring ℚᵘ.+-*-rawNearSemiring toℚᵘ

src/Data/Rational/Base.agda

@@ -30,6 +30,12 @@ open import Relation.Binary.PropositionalEquality.Core
 -- way to represent every rational number.
 
 record ℚ : Set where
+  -- We add "no-eta-equality; pattern" to the record to stop Agda
+  -- automatically unfolding rationals when arithmetic operations are
+  -- applied to them (see definition of operators below and Issue #1753
+  -- for details).
+  no-eta-equality; pattern
+
   constructor mkℚ
   field
     numerator     : ℤ
@@ -178,41 +184,44 @@ NonNegative p = ℚᵘ.NonNegative (toℚᵘ p)
 ≢-nonZero {mkℚ +0       (suc d) c} p≢0 = contradiction (λ {i} → C.recompute c {i}) ¬0-coprimeTo-2+
 
 >-nonZero : ∀ {p} → p > 0ℚ → NonZero p
->-nonZero {p} (*<* p<q) = ℚᵘ.>-nonZero {toℚᵘ p} (ℚᵘ.*<* p<q)
+>-nonZero {p@(mkℚ _ _ _)} (*<* p<q) = ℚᵘ.>-nonZero {toℚᵘ p} (ℚᵘ.*<* p<q)
 
 <-nonZero : ∀ {p} → p < 0ℚ → NonZero p
-<-nonZero {p} (*<* p<q) = ℚᵘ.<-nonZero {toℚᵘ p} (ℚᵘ.*<* p<q)
+<-nonZero {p@(mkℚ _ _ _)} (*<* p<q) = ℚᵘ.<-nonZero {toℚᵘ p} (ℚᵘ.*<* p<q)
 
 positive : ∀ {p} → p > 0ℚ → Positive p
-positive {p} (*<* p<q) = ℚᵘ.positive {toℚᵘ p} (ℚᵘ.*<* p<q)
+positive {p@(mkℚ _ _ _)} (*<* p<q) = ℚᵘ.positive {toℚᵘ p} (ℚᵘ.*<* p<q)
 
 negative : ∀ {p} → p < 0ℚ → Negative p
-negative {p} (*<* p<q) = ℚᵘ.negative {toℚᵘ p} (ℚᵘ.*<* p<q)
+negative {p@(mkℚ _ _ _)} (*<* p<q) = ℚᵘ.negative {toℚᵘ p} (ℚᵘ.*<* p<q)
 
 nonPositive : ∀ {p} → p ≤ 0ℚ → NonPositive p
-nonPositive {p} (*≤* p≤q) = ℚᵘ.nonPositive {toℚᵘ p} (ℚᵘ.*≤* p≤q)
+nonPositive {p@(mkℚ _ _ _)} (*≤* p≤q) = ℚᵘ.nonPositive {toℚᵘ p} (ℚᵘ.*≤* p≤q)
 
 nonNegative : ∀ {p} → p ≥ 0ℚ → NonNegative p
-nonNegative {p} (*≤* p≤q) = ℚᵘ.nonNegative {toℚᵘ p} (ℚᵘ.*≤* p≤q)
+nonNegative {p@(mkℚ _ _ _)} (*≤* p≤q) = ℚᵘ.nonNegative {toℚᵘ p} (ℚᵘ.*≤* p≤q)
 
 ------------------------------------------------------------------------------
 -- Operations on rationals
 
+-- For explanation of the `@record{}` annotations see notes in the equivalent
+-- place in `Data.Rational.Unnormalised.Base`.
+
 infix  8 -_ 1/_
 infixl 7 _*_ _÷_ _⊓_
 infixl 6 _-_ _+_ _⊔_
 
 -- addition
 _+_ : ℚ → ℚ → ℚ
-p + q = (↥ p ℤ.* ↧ q ℤ.+ ↥ q ℤ.* ↧ p) / (↧ₙ p ℕ.* ↧ₙ q)
+p@record{} + q@record{} = (↥ p ℤ.* ↧ q ℤ.+ ↥ q ℤ.* ↧ p) / (↧ₙ p ℕ.* ↧ₙ q)
 
 -- multiplication
 _*_ : ℚ → ℚ → ℚ
-p * q = (↥ p ℤ.* ↥ q) / (↧ₙ p ℕ.* ↧ₙ q)
+p@record{} * q@record{} = (↥ p ℤ.* ↥ q) / (↧ₙ p ℕ.* ↧ₙ q)
 
 -- subtraction
 _-_ : ℚ → ℚ → ℚ
-p - q = p + (- q)
+p@record{} - q@record{} = p + (- q)
 
 -- reciprocal: requires a proof that the numerator is not zero
 1/_ : (p : ℚ) → .{{_ : NonZero p}} → ℚ
@@ -221,15 +230,15 @@ p - q = p + (- q)
 
 -- division: requires a proof that the denominator is not zero
 _÷_ : (p q : ℚ) → .{{_ : NonZero q}} → ℚ
-p ÷ q = p * (1/ q)
+p@record{} ÷ q@record{} = p * (1/ q)
 
 -- max
 _⊔_ : (p q : ℚ) → ℚ
-p ⊔ q = if p ≤ᵇ q then q else p
+p@record{} ⊔ q@record{} = if p ≤ᵇ q then q else p
 
 -- min
 _⊓_ : (p q : ℚ) → ℚ
-p ⊓ q = if p ≤ᵇ q then p else q
+p@record{} ⊓ q@record{} = if p ≤ᵇ q then p else q
 
 -- absolute value
 ∣_∣ : ℚ → ℚ
@@ -240,11 +249,11 @@ p ⊓ q = if p ≤ᵇ q then p else q
 
 -- Floor (round towards -∞)
 floor : ℚ → ℤ
-floor p = ↥ p ℤ./ ↧ p
+floor p@record{} = ↥ p ℤ./ ↧ p
 
 -- Ceiling (round towards +∞)
 ceiling : ℚ → ℤ
-ceiling p = ℤ.- floor (- p)
+ceiling p@record{} = ℤ.- floor (- p)
 
 -- Truncate  (round towards 0)
 truncate : ℚ → ℤ
@@ -260,7 +269,7 @@ round p with p ≤ᵇ 0ℚ
 
 -- Fractional part (remainder after floor)
 fracPart : ℚ → ℚ
-fracPart p = ∣ p - truncate p / 1 ∣
+fracPart p@record{} = ∣ p - truncate p / 1 ∣
 
 -- Extra notations  ⌊ ⌋ floor,  ⌈ ⌉ ceiling,  [ ] truncate
 syntax floor p = ⌊ p ⌋

src/Data/Rational/Properties.agda

@@ -380,13 +380,18 @@ normalize-injective-≃ m n c d eq = ℕ./-cancelʳ-≡
 /-cong { -[1+ n ]} refl = cong -_ ∘′ normalize-cong {suc n} refl
 
 private
-  /-injective-≃-helper : ∀ {m n c-1 d-1} →
-                         - normalize (suc m) (suc c-1) ≡ normalize n (suc d-1) →
-                          mkℚᵘ -[1+ m ] c-1 ≃ᵘ mkℚᵘ (+ n) d-1
-  /-injective-≃-helper {m} {n} {c-1} {d-1} eq
-    with normalize-pos (suc m) (suc c-1) | normalize-nonNeg n (suc d-1)
-  ... | norm[m,c]-pos | norm[n,d]-nonNeg =
-    contradiction (sym eq) (nonNeg≢neg _ _ {{norm[n,d]-nonNeg}} {{neg-pos norm[m,c]-pos}})
+  /-injective-≃-helper : ∀ {m n c d} .{{_ : ℕ.NonZero c}} .{{_ : ℕ.NonZero d}} →
+                         - normalize (suc m) c ≡ normalize n d →
+                          mkℚᵘ -[1+ m ] (ℕ.pred c) ≃ᵘ mkℚᵘ (+ n) (ℕ.pred d)
+  /-injective-≃-helper {m} {n} {c} {d} -norm≡norm = contradiction
+    (sym -norm≡norm)
+    (nonNeg≢neg (normalize n d) (- normalize (suc m) c))
+    where instance
+      _ : NonNegative (normalize n d)
+      _ = normalize-nonNeg n d
+
+      _ : Negative (- normalize (suc m) c)
+      _ = neg-pos {normalize (suc m) c} (normalize-pos (suc m) c)
 
 /-injective-≃ : ∀ p q → ↥ᵘ p / ↧ₙᵘ p ≡ ↥ᵘ q / ↧ₙᵘ q → p ≃ᵘ q
 /-injective-≃ (mkℚᵘ (+ m)    c-1) (mkℚᵘ (+ n)    d-1) eq =
@@ -402,11 +407,17 @@ private
 -- Properties of toℚ/fromℚ
 ------------------------------------------------------------------------
 
+↥ᵘ-toℚᵘ : ∀ p → ↥ᵘ (toℚᵘ p) ≡ ↥ p
+↥ᵘ-toℚᵘ p@record{} = refl
+
+↧ᵘ-toℚᵘ : ∀ p → ↧ᵘ (toℚᵘ p) ≡ ↧ p
+↧ᵘ-toℚᵘ p@record{} = refl
+
 toℚᵘ-injective : Injective _≡_ _≃ᵘ_ toℚᵘ
-toℚᵘ-injective (*≡* eq) = ≃⇒≡ eq
+toℚᵘ-injective {x@record{}} {y@record{}} (*≡* eq) = ≃⇒≡ eq
 
 fromℚᵘ-injective : Injective _≃ᵘ_ _≡_ fromℚᵘ
-fromℚᵘ-injective {p} {q} = /-injective-≃ p q
+fromℚᵘ-injective {p@record{}} {q@record{}} = /-injective-≃ p q
 
 fromℚᵘ-toℚᵘ : ∀ p → fromℚᵘ (toℚᵘ p) ≡ p
 fromℚᵘ-toℚᵘ (mkℚ (+ n)      d-1 c) = normalize-coprime c
@@ -448,10 +459,10 @@ drop-*≤* (*≤* pq≤qp) = pq≤qp
 -- toℚᵘ is a isomorphism
 
 toℚᵘ-mono-≤ : p ≤ q → toℚᵘ p ≤ᵘ toℚᵘ q
-toℚᵘ-mono-≤ (*≤* p≤q) = *≤* p≤q
+toℚᵘ-mono-≤ {p@record{}} {q@record{}} (*≤* p≤q) = *≤* p≤q
 
 toℚᵘ-cancel-≤ : toℚᵘ p ≤ᵘ toℚᵘ q → p ≤ q
-toℚᵘ-cancel-≤ (*≤* p≤q) = *≤* p≤q
+toℚᵘ-cancel-≤ {p@record{}} {q@record{}} (*≤* p≤q) = *≤* p≤q
 
 toℚᵘ-isOrderHomomorphism-≤ : IsOrderHomomorphism _≡_ _≃ᵘ_ _≤_ _≤ᵘ_ toℚᵘ
 toℚᵘ-isOrderHomomorphism-≤ = record
@@ -556,10 +567,10 @@ drop-*<* (*<* pq<qp) = pq<qp
 -- toℚᵘ is a isomorphism
 
 toℚᵘ-mono-< : p < q → toℚᵘ p <ᵘ toℚᵘ q
-toℚᵘ-mono-< (*<* p<q) = *<* p<q
+toℚᵘ-mono-< {p@record{}} {q@record{}} (*<* p<q) = *<* p<q
 
 toℚᵘ-cancel-< : toℚᵘ p <ᵘ toℚᵘ q → p < q
-toℚᵘ-cancel-< (*<* p<q) = *<* p<q
+toℚᵘ-cancel-< {p@record{}} {q@record{}} (*<* p<q) = *<* p<q
 
 toℚᵘ-isOrderHomomorphism-< : IsOrderHomomorphism _≡_ _≃ᵘ_ _<_ _<ᵘ_ toℚᵘ
 toℚᵘ-isOrderHomomorphism-< = record
@@ -763,10 +774,10 @@ private
   +-nf p q = gcd (↥+ᵘ p q) (↧+ᵘ p q)
 
 ↥-+ : ∀ p q → ↥ (p + q) ℤ.* +-nf p q ≡ ↥+ᵘ p q
-↥-+ p q = ↥-/ (↥+ᵘ p q) (↧ₙ p ℕ.* ↧ₙ q)
+↥-+ p@record{} q@record{} = ↥-/ (↥+ᵘ p q) (↧ₙ p ℕ.* ↧ₙ q)
 
 ↧-+ : ∀ p q → ↧ (p + q) ℤ.* +-nf p q ≡ ↧+ᵘ p q
-↧-+ p q = ↧-/ (↥+ᵘ p q) (↧ₙ p ℕ.* ↧ₙ q)
+↧-+ p@record{} q@record{} = ↧-/ (↥+ᵘ p q) (↧ₙ p ℕ.* ↧ₙ q)
 
 ------------------------------------------------------------------------
 -- Raw bundles
@@ -825,12 +836,14 @@ private
 open Definitions ℚ ℚᵘ ℚᵘ._≃_
 
 toℚᵘ-homo-+ : Homomorphic₂ toℚᵘ _+_ ℚᵘ._+_
-toℚᵘ-homo-+ p q with +-nf p q ℤ.≟ 0ℤ
-... | yes nf[p,q]≡0 = *≡* (begin
-  ↥ (p + q) ℤ.* ↧+ᵘ p q   ≡⟨ cong (ℤ._* ↧+ᵘ p q) eq ⟩
-  0ℤ        ℤ.* ↧+ᵘ p q   ≡⟨⟩
-  0ℤ        ℤ.* ↧ (p + q) ≡⟨ cong (ℤ._* ↧ (p + q)) (sym eq2) ⟩
-  ↥+ᵘ p q   ℤ.* ↧ (p + q) ∎)
+toℚᵘ-homo-+ p@record{} q@record{} with +-nf p q ℤ.≟ 0ℤ
+... | yes nf[p,q]≡0 = *≡* $ begin
+  ↥ᵘ (toℚᵘ (p + q)) ℤ.* ↧+ᵘ p q   ≡⟨ cong (ℤ._* ↧+ᵘ p q) (↥ᵘ-toℚᵘ (p + q)) ⟩
+  ↥ (p + q) ℤ.* ↧+ᵘ p q           ≡⟨ cong (ℤ._* ↧+ᵘ p q) eq ⟩
+  0ℤ        ℤ.* ↧+ᵘ p q           ≡⟨⟩
+  0ℤ        ℤ.* ↧ (p + q)         ≡⟨ cong (ℤ._* ↧ (p + q)) (sym eq2) ⟩
+  ↥+ᵘ p q   ℤ.* ↧ (p + q)         ≡⟨ cong (↥+ᵘ p q ℤ.*_) (sym (↧ᵘ-toℚᵘ (p + q))) ⟩
+  ↥+ᵘ p q   ℤ.* ↧ᵘ (toℚᵘ (p + q)) ∎
   where
   open ≡-Reasoning
   eq2 : ↥+ᵘ p q ≡ 0ℤ
@@ -839,12 +852,14 @@ toℚᵘ-homo-+ p q with +-nf p q ℤ.≟ 0ℤ
   eq : ↥ (p + q) ≡ 0ℤ
   eq rewrite eq2 = cong ↥_ (0/n≡0 (↧ₙ p ℕ.* ↧ₙ q))
 
-... | no  nf[p,q]≢0 = *≡* (ℤ.*-cancelʳ-≡ _ _ (+-nf p q) {{ℤ.≢-nonZero nf[p,q]≢0}} (begin
-  ↥ (p + q) ℤ.* ↧+ᵘ p q    ℤ.* +-nf p q   ≡⟨ xy∙z≈xz∙y (↥ (p + q)) _ _ ⟩
-  ↥ (p + q) ℤ.* +-nf p q   ℤ.* ↧+ᵘ p q    ≡⟨ cong (ℤ._* ↧+ᵘ p q) (↥-+ p q) ⟩
-  ↥+ᵘ p q   ℤ.* ↧+ᵘ p q                   ≡⟨ cong (↥+ᵘ p q ℤ.*_) (sym (↧-+ p q)) ⟩
-  ↥+ᵘ p q   ℤ.* (↧ (p + q) ℤ.* +-nf p q)  ≡⟨ x∙yz≈xy∙z (↥+ᵘ p q) _ _ ⟩
-  ↥+ᵘ p q   ℤ.* ↧ (p + q)  ℤ.* +-nf p q   ∎))
+... | no  nf[p,q]≢0 = *≡* $ ℤ.*-cancelʳ-≡ _ _ (+-nf p q) {{ℤ.≢-nonZero nf[p,q]≢0}} $ begin
+    (↥ᵘ (toℚᵘ (p + q))) ℤ.* ↧+ᵘ p q  ℤ.* +-nf p q ≡⟨ cong (λ v → v ℤ.* ↧+ᵘ p q ℤ.* +-nf p q) (↥ᵘ-toℚᵘ (p + q)) ⟩
+    ↥ (p + q) ℤ.* ↧+ᵘ p q ℤ.* +-nf p q            ≡⟨ xy∙z≈xz∙y (↥ (p + q)) _ _ ⟩
+    ↥ (p + q) ℤ.* +-nf p q ℤ.* ↧+ᵘ p q            ≡⟨ cong (ℤ._* ↧+ᵘ p q) (↥-+ p q) ⟩
+    ↥+ᵘ p q ℤ.* ↧+ᵘ p q                           ≡⟨ cong (↥+ᵘ p q ℤ.*_) (sym (↧-+ p q)) ⟩
+    ↥+ᵘ p q ℤ.* (↧ (p + q) ℤ.* +-nf p q)          ≡⟨ x∙yz≈xy∙z (↥+ᵘ p q) _ _ ⟩
+    ↥+ᵘ p q ℤ.* ↧ (p + q)  ℤ.* +-nf p q           ≡˘⟨ cong (λ v → ↥+ᵘ p q ℤ.* v ℤ.* +-nf p q) (↧ᵘ-toℚᵘ (p + q)) ⟩
+    ↥+ᵘ p q ℤ.* ↧ᵘ (toℚᵘ (p + q)) ℤ.* +-nf p q    ∎
   where open ≡-Reasoning; open CommSemigroupProperties ℤ.*-commutativeSemigroup
 
 toℚᵘ-isMagmaHomomorphism-+ : IsMagmaHomomorphism +-rawMagma ℚᵘ.+-rawMagma toℚᵘ
@@ -1024,10 +1039,10 @@ private
   *-nf p q = gcd (↥ p ℤ.* ↥ q) (↧ p ℤ.* ↧ q)
 
 ↥-* : ∀ p q → ↥ (p * q) ℤ.* *-nf p q ≡ ↥ p ℤ.* ↥ q
-↥-* p q = ↥-/ (↥ p ℤ.* ↥ q) (↧ₙ p ℕ.* ↧ₙ q)
+↥-* p@record{} q@record{} = ↥-/ (↥ p ℤ.* ↥ q) (↧ₙ p ℕ.* ↧ₙ q)
 
 ↧-* : ∀ p q → ↧ (p * q) ℤ.* *-nf p q ≡ ↧ p ℤ.* ↧ q
-↧-* p q = ↧-/ (↥ p ℤ.* ↥ q) (↧ₙ p ℕ.* ↧ₙ q)
+↧-* p@record{} q@record{} = ↧-/ (↥ p ℤ.* ↥ q) (↧ₙ p ℕ.* ↧ₙ q)
 
 ------------------------------------------------------------------------
 -- Raw bundles
@@ -1049,25 +1064,29 @@ private
 -- Monomorphic to unnormalised _*_
 
 toℚᵘ-homo-* : Homomorphic₂ toℚᵘ _*_ ℚᵘ._*_
-toℚᵘ-homo-* p q with *-nf p q ℤ.≟ 0ℤ
-... | yes nf[p,q]≡0 = *≡* (begin
-  ↥ (p * q)     ℤ.* (↧ p ℤ.* ↧ q) ≡⟨ cong (ℤ._* (↧ p ℤ.* ↧ q)) eq ⟩
-  0ℤ            ℤ.* (↧ p ℤ.* ↧ q) ≡⟨⟩
-  0ℤ            ℤ.* ↧ (p * q)     ≡⟨ cong (ℤ._* ↧ (p * q)) (sym eq2) ⟩
-  (↥ p ℤ.* ↥ q) ℤ.* ↧ (p * q)     ∎)
+toℚᵘ-homo-* p@record{} q@record{} with *-nf p q ℤ.≟ 0ℤ
+... | yes nf[p,q]≡0 = *≡* $ begin
+  ↥ᵘ (toℚᵘ (p * q)) ℤ.* (↧ p ℤ.* ↧ q)     ≡⟨ cong (ℤ._* (↧ p ℤ.* ↧ q)) (↥ᵘ-toℚᵘ (p * q)) ⟩
+  ↥ (p * q)         ℤ.* (↧ p ℤ.* ↧ q)     ≡⟨ cong (ℤ._* (↧ p ℤ.* ↧ q)) eq ⟩
+  0ℤ                ℤ.* (↧ p ℤ.* ↧ q)     ≡⟨⟩
+  0ℤ                ℤ.* ↧ (p * q)         ≡⟨ cong (ℤ._* ↧ (p * q)) (sym eq2) ⟩
+  (↥ p ℤ.* ↥ q)     ℤ.* ↧ (p * q)         ≡⟨ cong ((↥ p ℤ.* ↥ q) ℤ.*_) (sym (↧ᵘ-toℚᵘ (p * q))) ⟩
+  (↥ p ℤ.* ↥ q)     ℤ.* ↧ᵘ (toℚᵘ (p * q)) ∎
   where
   open ≡-Reasoning
   eq2 : ↥ p ℤ.* ↥ q ≡ 0ℤ
   eq2 = gcd[i,j]≡0⇒i≡0 (↥ p ℤ.* ↥ q) (↧ p ℤ.* ↧ q) nf[p,q]≡0
 
   eq : ↥ (p * q) ≡ 0ℤ
   eq rewrite eq2 = cong ↥_ (0/n≡0 (↧ₙ p ℕ.* ↧ₙ q))
-... | no  nf[p,q]≢0 = *≡* (ℤ.*-cancelʳ-≡ _ _ (*-nf p q) {{ℤ.≢-nonZero nf[p,q]≢0}} (begin
-  ↥ (p * q)     ℤ.* (↧ p ℤ.* ↧ q) ℤ.* *-nf p q ≡⟨ xy∙z≈xz∙y (↥ (p * q)) _ _ ⟩
-  ↥ (p * q)     ℤ.* *-nf p q ℤ.* (↧ p ℤ.* ↧ q) ≡⟨ cong (ℤ._* (↧ p ℤ.* ↧ q)) (↥-* p q) ⟩
-  (↥ p ℤ.* ↥ q) ℤ.* (↧ p ℤ.* ↧ q)              ≡⟨ cong ((↥ p ℤ.* ↥ q) ℤ.*_) (sym (↧-* p q)) ⟩
-  (↥ p ℤ.* ↥ q) ℤ.* (↧ (p * q) ℤ.* *-nf p q)   ≡⟨ x∙yz≈xy∙z (↥ p ℤ.* ↥ q) _ _ ⟩
-  (↥ p ℤ.* ↥ q) ℤ.* ↧ (p * q)  ℤ.* *-nf p q    ∎))
+... | no nf[p,q]≢0 = *≡* $ ℤ.*-cancelʳ-≡ _ _ (*-nf p q) {{ℤ.≢-nonZero nf[p,q]≢0}} $ begin
+  ↥ᵘ (toℚᵘ (p * q)) ℤ.* (↧ p ℤ.* ↧ q) ℤ.* *-nf p q     ≡⟨ cong (λ v → v ℤ.* (↧ p ℤ.* ↧ q) ℤ.* *-nf p q) (↥ᵘ-toℚᵘ (p * q)) ⟩
+  ↥ (p * q)         ℤ.* (↧ p ℤ.* ↧ q) ℤ.* *-nf p q     ≡⟨ xy∙z≈xz∙y (↥ (p * q)) _ _ ⟩
+  ↥ (p * q)         ℤ.* *-nf p q ℤ.* (↧ p ℤ.* ↧ q)     ≡⟨ cong (ℤ._* (↧ p ℤ.* ↧ q)) (↥-* p q) ⟩
+  (↥ p ℤ.* ↥ q)     ℤ.* (↧ p ℤ.* ↧ q)                  ≡⟨ cong ((↥ p ℤ.* ↥ q) ℤ.*_) (sym (↧-* p q)) ⟩
+  (↥ p ℤ.* ↥ q)     ℤ.* (↧ (p * q) ℤ.* *-nf p q)       ≡⟨ x∙yz≈xy∙z (↥ p ℤ.* ↥ q) _ _ ⟩
+  (↥ p ℤ.* ↥ q)     ℤ.* ↧ (p * q)  ℤ.* *-nf p q        ≡˘⟨ cong (λ v → (↥ p ℤ.* ↥ q) ℤ.* v ℤ.* *-nf p q) (↧ᵘ-toℚᵘ (p * q)) ⟩
+  (↥ p ℤ.* ↥ q)     ℤ.* ↧ᵘ (toℚᵘ (p * q)) ℤ.* *-nf p q ∎
   where open ≡-Reasoning; open CommSemigroupProperties ℤ.*-commutativeSemigroup
 
 toℚᵘ-homo-1/ : ∀ p .{{_ : NonZero p}} → toℚᵘ (1/ p) ℚᵘ.≃ (ℚᵘ.1/ toℚᵘ p)
@@ -1337,22 +1356,22 @@ neg-distribʳ-* = +-*-Monomorphism.neg-distribʳ-* ℚᵘ.+-0-isGroup ℚᵘ.*-i
 ------------------------------------------------------------------------
 
 p≤q⇒p⊔q≡q : p ≤ q → p ⊔ q ≡ q
-p≤q⇒p⊔q≡q {p} {q} p≤q with p ≤ᵇ q | inspect (p ≤ᵇ_) q
+p≤q⇒p⊔q≡q {p@record{}} {q@record{}} p≤q with p ≤ᵇ q | inspect (p ≤ᵇ_) q
 ... | true  | _       = refl
 ... | false | [ p≰q ] = contradiction (≤⇒≤ᵇ p≤q) (subst (¬_ ∘ T) (sym p≰q) λ())
 
 p≥q⇒p⊔q≡p : p ≥ q → p ⊔ q ≡ p
-p≥q⇒p⊔q≡p {p} {q} p≥q with p ≤ᵇ q | inspect (p ≤ᵇ_) q
+p≥q⇒p⊔q≡p {p@record{}} {q@record{}} p≥q with p ≤ᵇ q | inspect (p ≤ᵇ_) q
 ... | true  | [ p≤q ] = ≤-antisym p≥q (≤ᵇ⇒≤ (subst T (sym p≤q) _))
 ... | false | [ p≤q ] = refl
 
 p≤q⇒p⊓q≡p : p ≤ q → p ⊓ q ≡ p
-p≤q⇒p⊓q≡p {p} {q} p≤q with p ≤ᵇ q | inspect (p ≤ᵇ_) q
+p≤q⇒p⊓q≡p {p@record{}} {q@record{}} p≤q with p ≤ᵇ q | inspect (p ≤ᵇ_) q
 ... | true  | _       = refl
 ... | false | [ p≰q ] = contradiction (≤⇒≤ᵇ p≤q) (subst (¬_ ∘ T) (sym p≰q) λ())
 
 p≥q⇒p⊓q≡q : p ≥ q → p ⊓ q ≡ q
-p≥q⇒p⊓q≡q {p} {q} p≥q with p ≤ᵇ q | inspect (p ≤ᵇ_) q
+p≥q⇒p⊓q≡q {p@record{}} {q@record{}} p≥q with p ≤ᵇ q | inspect (p ≤ᵇ_) q
 ... | true  | [ p≤q ] = ≤-antisym (≤ᵇ⇒≤ (subst T (sym p≤q) _)) p≥q
 ... | false | [ p≤q ] = refl
 
@@ -1603,15 +1622,15 @@ toℚᵘ-homo-∣-∣ (mkℚ -[1+ _ ] _ _) = *≡* refl
 ∣p∣≡0⇒p≡0 (mkℚ +0 zero _) ∣p∣≡0 = refl
 
 0≤∣p∣ : ∀ p → 0ℚ ≤ ∣ p ∣
-0≤∣p∣ p = *≤* (begin
+0≤∣p∣ p@record{} = *≤* (begin
   (↥ 0ℚ) ℤ.* (↧ ∣ p ∣)  ≡⟨ ℤ.*-zeroˡ (↧ ∣ p ∣) ⟩
   0ℤ                    ≤⟨ ℤ.+≤+ ℕ.z≤n ⟩
   ↥ ∣ p ∣               ≡˘⟨ ℤ.*-identityʳ (↥ ∣ p ∣) ⟩
   ↥ ∣ p ∣ ℤ.* 1ℤ        ∎)
   where open ℤ.≤-Reasoning
 
 0≤p⇒∣p∣≡p : 0ℚ ≤ p → ∣ p ∣ ≡ p
-0≤p⇒∣p∣≡p {p} 0≤p = toℚᵘ-injective (ℚᵘ.0≤p⇒∣p∣≃p (toℚᵘ-mono-≤ 0≤p))
+0≤p⇒∣p∣≡p {p@record{}} 0≤p = toℚᵘ-injective (ℚᵘ.0≤p⇒∣p∣≃p (toℚᵘ-mono-≤ 0≤p))
 
 ∣-p∣≡∣p∣ : ∀ p → ∣ - p ∣ ≡ ∣ p ∣
 ∣-p∣≡∣p∣ (mkℚ +[1+ n ] d-1 _) = refl
@@ -1640,7 +1659,7 @@ toℚᵘ-homo-∣-∣ (mkℚ -[1+ _ ] _ _) = *≡* refl
   where open ℚᵘ.≤-Reasoning
 
 ∣p-q∣≤∣p∣+∣q∣ : ∀ p q → ∣ p - q ∣ ≤ ∣ p ∣ + ∣ q ∣
-∣p-q∣≤∣p∣+∣q∣ p q = begin
+∣p-q∣≤∣p∣+∣q∣ p@record{} q@record{} = begin
   ∣ p   -     q ∣  ≤⟨ ∣p+q∣≤∣p∣+∣q∣ p (- q) ⟩
   ∣ p ∣ + ∣ - q ∣  ≡⟨ cong (λ h → ∣ p ∣ + h) (∣-p∣≡∣p∣ q) ⟩
   ∣ p ∣ + ∣   q ∣  ∎