From 908363de513ce2cec5268c587f50d0c93c82a9dc Mon Sep 17 00:00:00 2001 From: robert Date: Wed, 17 Jun 2026 18:07:41 +0200 Subject: [PATCH 1/2] Normalised Q plus related --- Cubical/Data/Int/Base.agda | 7 + Cubical/Data/Int/GCD.agda | 18 + Cubical/Data/Int/Properties.agda | 70 ++ Cubical/Data/Nat/Coprime.agda | 7 + Cubical/Data/Nat/GCD.agda | 7 + Cubical/Data/Nat/Properties.agda | 9 +- Cubical/Data/NatPlusOne/Properties.agda | 20 +- .../Data/NatPlusOne/PropertiesWithInt.agda | 24 + .../MoreRationals/NormalisedQ/Base.agda | 660 ++++++++++++++++++ 9 files changed, 820 insertions(+), 2 deletions(-) create mode 100644 Cubical/Data/NatPlusOne/PropertiesWithInt.agda create mode 100644 Cubical/Data/Rationals/MoreRationals/NormalisedQ/Base.agda diff --git a/Cubical/Data/Int/Base.agda b/Cubical/Data/Int/Base.agda index 69fa38f587..76bcc03eca 100644 --- a/Cubical/Data/Int/Base.agda +++ b/Cubical/Data/Int/Base.agda @@ -4,6 +4,7 @@ module Cubical.Data.Int.Base where open import Cubical.Foundations.Prelude +open import Cubical.Data.Empty as ⊥ using (⊥) open import Cubical.Data.Bool open import Cubical.Data.Nat hiding (_+_ ; _·_) renaming (isEven to isEvenℕ ; isOdd to isOddℕ) open import Cubical.Data.Fin.Base @@ -78,6 +79,12 @@ pos (suc n) · m = m + pos n · m negsuc zero · m = - m negsuc (suc n) · m = - m + negsuc n · m +NonZeroℤ : ∀ (z : ℤ) → Type +NonZeroℤ (pos zero) = ⊥ +NonZeroℤ (pos (suc n)) = Unit +NonZeroℤ (negsuc n) = Unit + + -- Natural number and negative integer literals for ℤ open import Cubical.Data.Nat.Literals public diff --git a/Cubical/Data/Int/GCD.agda b/Cubical/Data/Int/GCD.agda index b1053bf3fe..3df50e300f 100644 --- a/Cubical/Data/Int/GCD.agda +++ b/Cubical/Data/Int/GCD.agda @@ -1,8 +1,13 @@ module Cubical.Data.Int.GCD where +open import Cubical.Relation.Nullary using (¬_) open import Cubical.Data.Empty as ⊥ import Cubical.Data.Nat.GCD as ℕ +open import Cubical.Data.Nat using (suc; predℕ; ¬x≡0→NonZero; snotz) open import Cubical.Data.Nat.Divisibility renaming (_∣_ to _∣ℕ_) +open import Cubical.Data.NatPlusOne using (1+_) +open import Cubical.Data.NatPlusOne.PropertiesWithInt + using (ℕ₊₁→ℤ; ℕ₊₁→ℤ-1+pred-def) open import Cubical.Foundations.Prelude open import Cubical.Data.Int.Divisibility open import Cubical.Data.Int @@ -58,3 +63,16 @@ gcd[i,j]≡0⇒i≡0 {i} {j} eqn = abs≡0 i (ℕ.gcd[m,n]≡0⇒m≡0 {abs i}{a gcd[i,j]≡0⇒j≡0 : ∀ {i j} → gcd i j ≡ 0 → j ≡ 0 gcd[i,j]≡0⇒j≡0 {i}{j} eqn = gcd[i,j]≡0⇒i≡0 {j}{i} (gcdSym j i ∙ eqn) + +ℕ₊₁→ℤ-gcd-def : ∀ x d-1 → + ℕ₊₁→ℤ (1+ predℕ (ℕ.gcd x (suc d-1))) ≡ gcd (pos x) (pos (suc d-1)) +ℕ₊₁→ℤ-gcd-def x d-1 = + ℕ₊₁→ℤ-1+pred-def (ℕ.gcd x (suc d-1)) {{¬x≡0→NonZero (ℕ.¬gcdSuc≡0 x d-1)}} + +gcdSucNot0 : ∀ x d → ¬ gcd x (pos (suc d)) ≡ 0 +gcdSucNot0 x d u = snotz (injPos (gcd[i,j]≡0⇒j≡0 {x}{pos (suc d)} u)) + +gcd-ℕ₊₁→ℤ-lemma : ∀ numerator d-1 → + ℕ₊₁→ℤ (1+ (predℕ (ℕ.gcd (abs numerator) (suc d-1)))) ≡ + gcd numerator (pos (suc d-1)) +gcd-ℕ₊₁→ℤ-lemma numerator d-1 = ℕ₊₁→ℤ-gcd-def (abs numerator) d-1 diff --git a/Cubical/Data/Int/Properties.agda b/Cubical/Data/Int/Properties.agda index 8f44b4e7b1..23d88222f4 100644 --- a/Cubical/Data/Int/Properties.agda +++ b/Cubical/Data/Int/Properties.agda @@ -18,6 +18,11 @@ open import Cubical.Data.Sum open import Cubical.Data.Fin.Base open import Cubical.Data.Fin.Properties +private + contraposition : {ℓ : Level} {a b c : Type ℓ} → + (a → (b → c)) → ¬ c → (b → ¬ a) + contraposition = λ z z₁ z₂ z₃ → z₁ (z z₃ z₂) + open import Cubical.Data.Int.Base @@ -1544,3 +1549,68 @@ sumFinℤHom {n = n} = sumFinGenHom _+_ 0 (λ _ → refl) +Comm +Assoc n clamp : ℤ → ℕ clamp (pos n) = n clamp (negsuc n) = zero + + +-- useful lemmas for _·_ + +¬x≡0¬y≡0→¬x·y≡0 : ∀ x y → ¬ x ≡ 0 → ¬ y ≡ 0 → ¬ x · y ≡ 0 +¬x≡0¬y≡0→¬x·y≡0 x y nx0 ny0 = contraposition (isIntegralℤ x y) ny0 nx0 + +ab'c≡ac'b : ∀ a b c → (a · b) · c ≡ (a · c) · b +ab'c≡ac'b a b c = + sym (·Assoc a b c) ∙ cong (λ u → a · u) (·Comm b c) ∙ ·Assoc a c b + +ab'c≡ba'c : ∀ a b c → (a · b) · c ≡ (b · a) · c +ab'c≡ba'c a b c = cong (λ u → u · c) (·Comm a b) + +ab'c≡b'ca : ∀ a b c → (a · b) · c ≡ (b · c) · a +ab'c≡b'ca a b c = ab'c≡ba'c a b c ∙ ab'c≡ac'b b a c + +a'bc≡a'cb : ∀ a b c -> a · (b · c) ≡ a · (c · b) +a'bc≡a'cb a b c = cong (λ u → a · u) (·Comm b c) + +a'bc≡b'ac : ∀ a b c → a · (b · c) ≡ b · (a · c) +a'bc≡b'ac a b c = + (·Assoc a b c) ∙ cong (λ u → u · c) (·Comm a b) ∙ sym (·Assoc b a c) + +abcd≡ab'cd : ∀ a b c d → ((a · b) · c) · d ≡ (a · b) · (c · d) +abcd≡ab'cd a b c d = sym (·Assoc (a · b) c d) + +-- reverses a b c d +ab'cd≡dc'ba : ∀ a b c d → (a · b) · (c · d) ≡ (d · c) · (b · a) +ab'cd≡dc'ba a b c d = + cong₂ (λ u v → u · v) (·Comm a b) (·Comm c d) ∙ + ·Comm (b · a) (d · c) + +-- reverses a b c d +abcd≡dcba : ∀ a b c d → ((a · b) · c) · d ≡ ((d · c) · b) · a +abcd≡dcba a b c d = + abcd≡ab'cd a b c d ∙ ab'cd≡dc'ba a b c d ∙ sym (abcd≡ab'cd d c b a) + +-- flips 2nd and 3rd +ab'cd≡ac'bd : ∀ a b c d -> (a · b) · (c · d) ≡ (a · c) · (b · d) +ab'cd≡ac'bd a b c d = + sym (·Assoc a b (c · d)) ∙ + cong (λ u → a · u) ((·Assoc b c d) ∙ + (cong (λ u → u · d) (·Comm b c)) ∙ + sym (·Assoc c b d)) ∙ ·Assoc a c (b · d) + +-- flips 2nd and 4th +ab'cd≡ad'cb : ∀ a b c d -> (a · b) · (c · d) ≡ (a · d) · (c · b) +ab'cd≡ad'cb a b c d = + a'bc≡a'cb (a · b) c d ∙ ab'cd≡ac'bd a b d c ∙ a'bc≡a'cb (a · d) b c + +ab'cd≡ca'db : ∀ a b c d -> (a · b) · (c · d) ≡ (c · a) · (d · b) +ab'cd≡ca'db a b c d = + ab'cd≡ac'bd a b c d ∙ cong₂ (λ u v → u · v) (·Comm a c) (·Comm b d) + +abcd≡ac'bd : ∀ a b c d → ((a · b) · c) · d ≡ (a · c) · (b · d) +abcd≡ac'bd a b c d = + (cong (λ u → u · d)) (ab'c≡ac'b a b c) ∙ sym (·Assoc (a · c) b d) + +ab'cd≡cb'da : ∀ a b c d -> (a · b) · (c · d) ≡ (c · b) · (d · a) +ab'cd≡cb'da a b c d = ab'cd≡ca'db a b c d ∙ ab'cd≡ad'cb c a d b + +a'bc'd≡ab'cd : ∀ a b c d -> (a · (b · c)) · d ≡ (a · b) · (c · d) +a'bc'd≡ab'cd a b c d = + cong (λ u → u · d) (·Assoc a b c) ∙ sym (·Assoc (a · b) c d) diff --git a/Cubical/Data/Nat/Coprime.agda b/Cubical/Data/Nat/Coprime.agda index c8c28ec5b5..c2e0a8c5ea 100644 --- a/Cubical/Data/Nat/Coprime.agda +++ b/Cubical/Data/Nat/Coprime.agda @@ -3,6 +3,8 @@ module Cubical.Data.Nat.Coprime where open import Cubical.Foundations.Prelude open import Cubical.Foundations.Function +open import Cubical.Relation.Nullary using (¬_) + open import Cubical.Data.Sigma open import Cubical.Data.NatPlusOne open import Cubical.Data.Empty as ⊥ using (⊥) @@ -103,6 +105,11 @@ toCoprime-cancelʳ (m , n) (1+ k) i = r₂ : ℕ₊₁→ℕ c₂' · suc d-1 ≡ ℕ₊₁→ℕ c₂ · suc d-1 r₂ = subst (λ z → ℕ₊₁→ℕ c₂' · z ≡ ℕ₊₁→ℕ c₂ · z) q (inj-·sm q₂ ∙ sym p₂) +coprime≢0 : ∀ m n → ¬ ToCoprime.c₁ (suc m , n) ≡ 0 +coprime≢0 m n = + ¬k·l≡0→¬k≡0 (ToCoprime.c₁ (suc m , n)) (gcd (suc m) (ℕ₊₁→ℕ n)) + λ x → snotz {m} + (sym (∣-untrunc (gcdIsGCD (suc m) (ℕ₊₁→ℕ n) .fst .fst) .snd) ∙ x) private lem₀ : ∀ i j m n → i · m ≡ j · m + n → (i ∸ j) · m ≡ n diff --git a/Cubical/Data/Nat/GCD.agda b/Cubical/Data/Nat/GCD.agda index b56c3bac02..cd4e515d36 100644 --- a/Cubical/Data/Nat/GCD.agda +++ b/Cubical/Data/Nat/GCD.agda @@ -204,6 +204,7 @@ uniqueGCD isgd isgd' = sym (isGCD→gcd≡ isgd) ∙ isGCD→gcd≡ isgd' gcdSym : (m n : ℕ) → (gcd m n) ≡ (gcd n m) gcdSym m n = uniqueGCD (gcdIsGCD m n) (symGCD (gcdIsGCD n m)) + -- multiplicative properties of the gcd isCD-cancelʳ : ∀ k → isCD (m · suc k) (n · suc k) (d · suc k) @@ -270,6 +271,12 @@ gcd[m,n]≡0⇒m≡0 {suc m} {n} gmn = gcd[m,n]≡0⇒n≡0 : ∀ {m n} → gcd m n ≡ 0 → n ≡ 0 gcd[m,n]≡0⇒n≡0 {m}{n} gmn = gcd[m,n]≡0⇒m≡0 {n} {m} (gcdSym n m ∙ gmn) +¬gcdSuc≡0 : ∀ n d-1 → ¬ gcd n (suc d-1) ≡ 0 +¬gcdSuc≡0 n d-1 x = snotz (gcd[m,n]≡0⇒n≡0 {n} {suc d-1} x) + +nonZeroGcd-lemma : ∀ n d-1 → NonZero (gcd n (suc d-1)) +nonZeroGcd-lemma n d-1 = ¬x≡0→NonZero {(gcd n (suc d-1))} (¬gcdSuc≡0 n d-1) + decGCD : ∀ {m}{n}{d} → Dec (isGCD m n d) decGCD {m}{n}{d} with (discreteℕ (gcd m n) d) ... | yes p = yes (gcd≡→isGCD p) diff --git a/Cubical/Data/Nat/Properties.agda b/Cubical/Data/Nat/Properties.agda index eca1bb0cc7..8a2d9075e7 100644 --- a/Cubical/Data/Nat/Properties.agda +++ b/Cubical/Data/Nat/Properties.agda @@ -264,18 +264,25 @@ inj-·sm {suc l} {m} {suc n} p = cong suc (inj-·sm (inj-m+ {m = suc m} p)) inj-sm· : suc m · l ≡ suc m · n → l ≡ n inj-sm· {m} {l} {n} p = inj-·sm (·-comm l (suc m) ∙ p ∙ ·-comm (suc m) n) +¬x≡0→NonZero : ∀ {x : ℕ} → ¬ x ≡ 0 → NonZero x +¬x≡0→NonZero {zero} nx0 = nx0 refl +¬x≡0→NonZero {suc x} nx0 = tt + integral-domain-· : {k l : ℕ} → (k ≡ 0 → ⊥) → (l ≡ 0 → ⊥) → (k · l ≡ 0 → ⊥) integral-domain-· {zero} {l} ¬p ¬q r = ¬p refl integral-domain-· {suc k} {zero} ¬p ¬q r = ¬q refl integral-domain-· {suc k} {suc l} ¬p ¬q r = snotz r +¬k·l≡0→¬k≡0 : ∀ k l → (k · l ≡ 0 → ⊥) → (k ≡ 0 → ⊥) +¬k·l≡0→¬k≡0 zero l ¬0 = ¬0 +¬k·l≡0→¬k≡0 (suc k) l ¬0 = snotz + -- Arithmetic facts about ∸ zero∸ : ∀ n → zero ∸ n ≡ zero zero∸ zero = refl zero∸ (suc _) = refl - n∸n : (n : ℕ) → n ∸ n ≡ 0 n∸n zero = refl n∸n (suc n) = n∸n n diff --git a/Cubical/Data/NatPlusOne/Properties.agda b/Cubical/Data/NatPlusOne/Properties.agda index 8de3a6bf2e..c0a4b128f2 100644 --- a/Cubical/Data/NatPlusOne/Properties.agda +++ b/Cubical/Data/NatPlusOne/Properties.agda @@ -3,7 +3,9 @@ module Cubical.Data.NatPlusOne.Properties where open import Cubical.Foundations.Prelude open import Cubical.Foundations.Univalence -open import Cubical.Data.Nat +open import Cubical.Data.Nat renaming (NonZero to NonZeroℕ) +open import Cubical.Data.Int using (ℤ; pos; injPos; pos·pos; sucℤ; pos+) + renaming (_·_ to _ℤ·_; _+_ to _ℤ+_) open import Cubical.Data.NatPlusOne.Base open import Cubical.Reflection.StrictEquiv @@ -40,3 +42,19 @@ private ·₊₁-identityʳ : ∀ n → n ·₊₁ 1 ≡ n ·₊₁-identityʳ (1+ n) = cong 1+_ (injSuc (·-identityʳ (suc n))) + +-- Useful lemmas +a'bc≡a'cb : ∀ a b c -> a ·₊₁ (b ·₊₁ c) ≡ a ·₊₁ (c ·₊₁ b) +a'bc≡a'cb a b c = cong (λ u → a ·₊₁ u) (·₊₁-comm b c) + +a'bc'd≡ab'cd : ∀ a b c d -> + (a ·₊₁ (b ·₊₁ c)) ·₊₁ d ≡ (a ·₊₁ b) ·₊₁ (c ·₊₁ d) +a'bc'd≡ab'cd a b c d = + cong (λ u → u ·₊₁ d) (·₊₁-assoc a b c) ∙ sym (·₊₁-assoc (a ·₊₁ b) c d) + +ab'cd≡ac'bd : ∀ a b c d -> + (a ·₊₁ b) ·₊₁ (c ·₊₁ d) ≡ (a ·₊₁ c) ·₊₁ (b ·₊₁ d) +ab'cd≡ac'bd a b c d = + sym (·₊₁-assoc a b (c ·₊₁ d)) ∙ cong (λ u → a ·₊₁ u) ((·₊₁-assoc b c d) ∙ + (cong (λ u → u ·₊₁ d) (·₊₁-comm b c)) ∙ + sym (·₊₁-assoc c b d)) ∙ ·₊₁-assoc a c (b ·₊₁ d) diff --git a/Cubical/Data/NatPlusOne/PropertiesWithInt.agda b/Cubical/Data/NatPlusOne/PropertiesWithInt.agda new file mode 100644 index 0000000000..4c927440b3 --- /dev/null +++ b/Cubical/Data/NatPlusOne/PropertiesWithInt.agda @@ -0,0 +1,24 @@ +module Cubical.Data.NatPlusOne.PropertiesWithInt where + +open import Cubical.Foundations.Prelude +open import Cubical.Data.Nat renaming (NonZero to NonZeroℕ) +open import Cubical.Data.Int using (ℤ; pos; injPos; pos·pos; sucℤ; pos+) + renaming (_·_ to _ℤ·_; _+_ to _ℤ+_) +open import Cubical.Data.NatPlusOne.Base +open import Cubical.Data.NatPlusOne.Properties + +ℕ₊₁→ℤ : ℕ₊₁ → ℤ +ℕ₊₁→ℤ n = pos (ℕ₊₁→ℕ n) + +ℕ₊₁→ℤ-inj : ∀{n}{n'} → ℕ₊₁→ℤ n ≡ ℕ₊₁→ℤ n' → n ≡ n' +ℕ₊₁→ℤ-inj {1+ n} {1+ n'} zz' = ℕ₊₁→ℕ-inj (injPos zz') + +ℕ₊₁→ℤ-1+pred-def : ∀ (x : ℕ) → {{px : NonZeroℕ x}} → + ℕ₊₁→ℤ (1+ predℕ x) ≡ pos x +ℕ₊₁→ℤ-1+pred-def (suc x) {{px}} = refl + +·ℕ₊₁→ℤ-distr : ∀ n m → ℕ₊₁→ℤ (n ·₊₁ m) ≡ (ℕ₊₁→ℤ n) ℤ· (ℕ₊₁→ℤ m) +·ℕ₊₁→ℤ-distr n@(1+ n') m@(1+ m') = pos·pos (suc n') (suc m') + ++ℕ₊₁→ℤ-distr : ∀ n m → ℕ₊₁→ℤ (n +₁ m) ≡ (ℕ₊₁→ℤ n) ℤ+ (ℕ₊₁→ℤ m) ++ℕ₊₁→ℤ-distr n@(1+ n') m@(1+ m') = cong sucℤ (pos+ (suc n') m') diff --git a/Cubical/Data/Rationals/MoreRationals/NormalisedQ/Base.agda b/Cubical/Data/Rationals/MoreRationals/NormalisedQ/Base.agda new file mode 100644 index 0000000000..03d7a5a198 --- /dev/null +++ b/Cubical/Data/Rationals/MoreRationals/NormalisedQ/Base.agda @@ -0,0 +1,660 @@ +module Cubical.Data.Rationals.MoreRationals.NormalisedQ.Base where + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Isomorphism using (isoToPath ; iso) +open import Cubical.Foundations.HLevels using (isSetΣ ; isSet×) +open import Cubical.Foundations.Transport +open import Cubical.Relation.Nullary +open import Cubical.Relation.Binary +open BinaryRelation +open isEquivRel +open import Cubical.Data.Empty as ⊥ using (⊥) +open import Cubical.Data.Sigma using (_×_; Σ≡Prop) +open import Cubical.Data.Nat as ℕ + using (ℕ; discreteℕ; znots; snotz; m+n≡0→m≡0×n≡0; +-suc; + ·-suc; _∸_; suc; zero ; predℕ; suc-predℕ; isSetℕ; injSuc; + ¬x≡0→NonZero; ¬k·l≡0→¬k≡0) +open import Cubical.Data.Nat.GCD as ℕ +open import Cubical.Data.Nat.Coprime as ℕ +open import Cubical.Data.Nat.Divisibility as ℕ using (∣-untrunc) +open import Cubical.Data.NatPlusOne using (1+_; ℕ₊₁; -1+_; ℕ₊₁→ℕ; _·₊₁_) +open import Cubical.Data.NatPlusOne.PropertiesWithInt +open import Cubical.Data.Int as ℤ + renaming (_+_ to _ℤ+_; _-_ to _ℤ-_; -_ to -ℤ_; _·_ to _ℤ·_; abs to absℤ) +open import Cubical.Data.Int.GCD as ℤ using (gcd-def; ℕ₊₁→ℤ-gcd-def; gcdSucNot0) +open import Cubical.Data.Int.Order as ℤ using () + + +------------------------------------------------ +-- Core definitions + +-- ℚ as the set of coprime pairs in ℤ × ℕ (where the ℕ is d-1) +-- Essentially reproduces reduced Rationals ℚ as in regular Agda, +-- but the Coprime is handled cubically and ℤ is Cubical.Data.Int. + +ℚ : Type +ℚ = Σ (ℤ × ℕ) λ q → areCoprime ((absℤ (fst q)) , suc (snd q)) + +isSetℚ : isSet ℚ +isSetℚ = isSetΣ (isSet× isSetℤ isSetℕ) (λ _ → isProp→isSet isPropIsGCD) + +-- numerator ℤ +↥_ : ℚ → ℤ +↥ ((z , n) , copr) = z + +-- denominator as ℤ (always greater than 0) +↧_ : ℚ → ℤ +↧ ((z , n) , copr) = pos (suc n) + +sign↧ : ∀ (q : ℚ) → sign (↧ q) ≡ pos 1 +sign↧ q@((z , n) , c) = refl + +sign↥p·↧q≡sign↥p : ∀ p q → sign ((↥ p) ℤ.· (↧ q)) ≡ sign (↥ p) +sign↥p·↧q≡sign↥p p@((z , n) , c) q@((z' , n') , c') = + signx·y≡signx·signy (↥ p) (↧ q) ∙ ·IdR (sign (↥ p)) + +-- denominator-1 as ℕ +↧₋₁_ : ℚ → ℕ +↧₋₁ ((z , n) , copr) = n + +-- denominator as ℕ₊₁ +↧₊₁_ : ℚ → ℕ₊₁ +↧₊₁ ((z , n) , copr) = 1+ n + +↧≡↧→↧₋₁≡↧₋₁ : ∀ {x y : ℚ} → ↧ x ≡ ↧ y → ↧₋₁ x ≡ ↧₋₁ y +↧≡↧→↧₋₁≡↧₋₁ d = ℕ.injSuc (ℤ.injPos d) + +x≡y→↥x≡↥y : ∀ {x y : ℚ} → x ≡ y → ↥ x ≡ ↥ y +x≡y→↥x≡↥y {x}{y} xy = cong (λ u → ↥ u) xy + +x≡y→↧x≡↧y : ∀ {x y : ℚ} → x ≡ y → ↧ x ≡ ↧ y +x≡y→↧x≡↧y {x}{y} xy = cong (λ u → ↧ u) xy + +x≡y→↧₊₁x≡↧₊₁y : ∀ {x y : ℚ} → x ≡ y → ↧₊₁ x ≡ ↧₊₁ y +x≡y→↧₊₁x≡↧₊₁y {x}{y} xy = cong (λ u → ↧₊₁ u) xy + +x≡y→↧₋₁x≡↧₋₁y : ∀ {x y : ℚ} → x ≡ y → ↧₋₁ x ≡ ↧₋₁ y +x≡y→↧₋₁x≡↧₋₁y {x}{y} xy = cong (λ u → ↧₋₁ u) xy + +↥↧₋₁ : ℚ → (ℤ × ℕ) +↥↧₋₁ q = ↥ q , ↧₋₁ q + +↥↧₊₁ : ℚ → (ℤ × ℕ₊₁) +↥↧₊₁ q = ↥ q , ↧₊₁ q + +↥↧ : ℚ → (ℤ × ℤ) +↥↧ q = ↥ q , ↧ q + +-- Uniqueness of the reduced numerator/denominator pair +ℚ-unique₋₁ : ∀ {x y : ℚ} → ↥ x ≡ ↥ y → ↧₋₁ x ≡ ↧₋₁ y → x ≡ y +ℚ-unique₋₁ {x} {y} n d-1 = Σ≡Prop (λ u → isPropIsGCD) λ i → (n i) , (d-1 i) + +ℚ-unique₊₁ : ∀ {x y : ℚ} → ↥ x ≡ ↥ y → ↧₊₁ x ≡ ↧₊₁ y → x ≡ y +ℚ-unique₊₁ {x} {y} n d = ℚ-unique₋₁ n (cong -1+_ d) + +-- Numerator and denominator determine equality +ℚ-unique : ∀ {x y : ℚ} → ↥ x ≡ ↥ y → ↧ x ≡ ↧ y → x ≡ y +ℚ-unique {x}{y} n d-1 = ℚ-unique₋₁ n (↧≡↧→↧₋₁≡↧₋₁ {x}{y} d-1) + +----------------------------------------------- +-- Negation +infix 8 -_ +-_ : ℚ → ℚ +- a@((pos zero , d-1) , c) = a +- ((pos (suc n) , d-1) , c) = ((negsuc n) , d-1) , c +- ((negsuc n , d-1) , c) = (pos (suc n) , d-1) , c + +-- Properties of -_ + +↥-neg : ∀ a → ↥ (- a) ≡ -ℤ (↥ a) +↥-neg ((pos zero , d-1) , c) = refl +↥-neg ((pos (suc n) , d-1) , c) = refl +↥-neg ((negsuc n , d-1) , c) = refl + +↧-neg : ∀ a → ↧ (- a) ≡ ↧ a +↧-neg ((pos zero , d-1) , c) = refl +↧-neg ((pos (suc n) , d-1) , c) = refl +↧-neg ((negsuc n , d-1) , c) = refl + +↧₋₁-neg : ∀ (a : ℚ) → ↧₋₁ (- a) ≡ ↧₋₁ a +↧₋₁-neg a = ↧≡↧→↧₋₁≡↧₋₁ {(- a)} {a} (↧-neg a) + +↧₊₁-neg : ∀ (a : ℚ) → ↧₊₁ (- a) ≡ ↧₊₁ a +↧₊₁-neg a = cong 1+_ (↧₋₁-neg a) + +neg-distr↥ : ∀ {x} {y} → ↥ (- x) ≡ (↥ y) → ↧₋₁ x ≡ ↧₋₁ y → - x ≡ y +neg-distr↥ {x}{y} numerators denominators = + ℚ-unique₋₁ numerators ((↧₋₁-neg x) ∙ denominators ) + +neg-distr↥↧₋₁ : ∀ x → ↥↧₋₁ (- x) ≡ (-ℤ (↥ x) , ↧₋₁ x) +neg-distr↥↧₋₁ x = cong₂ (λ a b → (a , b)) (↥-neg x) (↧₋₁-neg x) + +↥x+↥-x≡0 : ∀ x → (↥ x) ℤ.+ ↥ (- x) ≡ 0 +↥x+↥-x≡0 x = cong ((↥ x) ℤ.+_) (↥-neg x) ∙ -Cancel (↥ x) + +neg-involutive : ∀{a} → - (- a) ≡ a +neg-involutive {(pos zero , d-1) , c} = refl +neg-involutive {(pos (suc n) , d-1) , c} = refl +neg-involutive {(negsuc zero , d-1) , c} = refl +neg-involutive {(negsuc (suc n) , d-1) , c} = refl + +neg-injective : ∀{a}{b} → - a ≡ - b → a ≡ b +neg-injective {a}{b} -a-b = + sym (neg-involutive {a}) ∙ (cong (-_) -a-b) ∙ neg-involutive {b} + +--------------------------------------------------- +-- Signs + +NonZero : (p : ℚ) → Type +NonZero ((pos zero , d-1) , c) = ⊥ +NonZero ((pos (suc n) , d-1) , c) = Unit +NonZero ((negsuc n , d-1) , c) = Unit + +IsZero : (p : ℚ) → Type +IsZero ((pos zero , n) , c) = Unit +IsZero ((pos (suc m) , n) , c) = ⊥ +IsZero ((negsuc m , n) , c) = ⊥ + +¬IsZero→NonZero : ∀ p → ¬ (IsZero p) → NonZero p +¬IsZero→NonZero ((pos zero , n) , c) ¬p0 = ¬p0 tt +¬IsZero→NonZero ((pos (suc m) , n) , c) ¬p0 = tt +¬IsZero→NonZero ((negsuc m , n) , c) ¬p0 = tt + +Positive : (p : ℚ) → Type +Positive ((pos zero , d-1) , c) = ⊥ +Positive ((pos (suc n) , d-1) , c) = Unit +Positive ((negsuc n , d-1) , c) = ⊥ + +Negative : (p : ℚ) → Type +Negative ((pos n , d-1) , c) = ⊥ +Negative ((negsuc n , d-1) , c) = Unit + +NonNegative : (p : ℚ) → Type +NonNegative ((pos m , n) , copr) = Unit +NonNegative ((negsuc m , n) , copr) = ⊥ + +IsZero→NonNegative : {p : ℚ} → IsZero p → NonNegative p +IsZero→NonNegative {(pos m , n) , c} posp = tt + +Positive→NonNegative : ∀ {p : ℚ} → Positive p → NonNegative p +Positive→NonNegative {(pos m , n) , c} pp = tt +Positive→NonNegative {(negsuc m , n) , c} pp = pp + +IsInteger : (p : ℚ) → Type +IsInteger ((z , zero) , c) = Unit +IsInteger ((z , suc n) , c) = ⊥ + +decIsZero : ∀ (p : ℚ) → Dec (IsZero p) +decIsZero p@((pos zero , n) , c) = yes tt +decIsZero ((pos (suc m) , n) , c) = no (λ ()) +decIsZero ((negsuc m , n) , c) = no (λ ()) + +decNonZero : ∀ (p : ℚ) → Dec (NonZero p) +decNonZero ((pos ℕ.zero , n) , copr) = no (λ ()) +decNonZero ((pos (ℕ.suc m) , n) , copr) = yes tt +decNonZero ((negsuc m , n) , copr) = yes tt + +decPositive : ∀ (p : ℚ) → Dec (Positive p) +decPositive ((pos zero , n) , copr) = no λ () +decPositive ((pos (suc m) , n) , copr) = yes tt +decPositive ((negsuc m , n) , copr) = no (λ ()) + +decNegative : ∀ (p : ℚ) → Dec (Negative p) +decNegative ((pos m , n) , copr) = no (λ ()) +decNegative ((negsuc m , n) , copr) = yes tt + +decNonNegative : ∀ (p : ℚ) → Dec (NonNegative p) +decNonNegative ((pos m , n) , c) = yes tt +decNonNegative ((negsuc m , n) , c) = no (λ ()) + +decIsInteger : ∀ (p : ℚ) → Dec (IsInteger p) +decIsInteger ((z , zero) , c) = yes tt +decIsInteger ((z , suc n) , c) = no (λ ()) + +--------------------------------------------- +-- Abs +abs : ℚ → ℚ +abs z@((pos m , n) , copr) = z +abs z@((negsuc m , n) , copr) = ((pos (suc m) , n) , copr) + +absDef : ∀ x → abs (- x) ≡ abs x +absDef ((pos zero , n) , copr) = refl +absDef ((pos (suc m) , n) , copr) = refl +absDef ((negsuc m , n) , copr) = refl + +absNegative : ∀ x → Negative x → abs x ≡ - x +absNegative ((negsuc m , n) , c) negx = refl + +absNonNegative : ∀ x → NonNegative x → abs x ≡ x +absNonNegative ((pos zero , n) , c) nnegx = refl +absNonNegative ((pos (suc m) , n) , c) nnegx = refl +absNonNegative ((negsuc m , n) , c) nnegx = ⊥.elim nnegx + +absIsNonNegative : ∀ x → NonNegative (abs x) +absIsNonNegative ((pos zero , n) , c) = tt +absIsNonNegative ((pos (suc m) , n) , c) = tt +absIsNonNegative ((negsuc m , n) , c) = tt + +------------------------------------------------- +-- Constructing rationals + +normalise : ℕ → ℕ₊₁ → ℚ +normalise m n = let numden = toCoprime (m , n) in + ((pos (fst numden)) , -1+ (snd numden)) , toCoprimeAreCoprime (m , n) + +normalise-id : (m : ℕ) → (n : ℕ₊₁) → let numden = toCoprime (m , n) in + normalise m n ≡ + (((pos (fst numden)) , -1+ (snd numden)) , toCoprimeAreCoprime (m , n)) +normalise-id m n = refl + +-- Constructors for ℚ that take two numbers, say -6 and 21, +-- and returns them in normalized form, e.g, -2 and 7. +[_] : (ℤ × ℕ₊₁) → ℚ +[ pos m , n ] = normalise m n +[ negsuc m , n ] = - normalise (suc m) n + +-- Some constants +0ℚ : ℚ +0ℚ = [ 0 , 1 ] + +1ℚ : ℚ +1ℚ = [ 1 , 1 ] + +-1ℚ : ℚ +-1ℚ = [ -1 , 1 ] + +½ : ℚ +½ = [ 1 , 2 ] + +-½ : ℚ +-½ = - ½ + +ℤ→ℚ : ℤ → ℚ +ℤ→ℚ z = [ z , 1 ] + +---------------------------------------------------- + +-- About 0ℚ + +↥a≡0→a≡0ℚ : {a : ℚ} → ↥ a ≡ 0 → a ≡ 0ℚ +↥a≡0→a≡0ℚ {a@((z , d-1) , c)} a0 = ℚ-unique₋₁ a0 (ℕ.injSuc (zeroCoprime' copr)) + where + copr = transport (cong (λ u → areCoprime (u , suc d-1)) (cong absℤ a0)) c + +↥0→↧₋₁0 : {a : ℚ} → ↥ a ≡ 0 → ↧₋₁ a ≡ 0 +↥0→↧₋₁0 {a@((n , d-1) , c)} a0 = ℕ.injSuc (zeroCoprime' copr) + where + copr = transport (cong (λ u → areCoprime (u , suc d-1)) (cong absℤ a0)) c + +↥0→↧1 : {a : ℚ} → ↥ a ≡ 0 → ↧ a ≡ 1 +↥0→↧1 {a} a0 = cong (λ u → pos (suc u)) (↥0→↧₋₁0 {a} a0) + +0-id : ∀ {n}{c} → ((pos zero , n) , c) ≡ 0ℚ +0-id {n}{c} = ↥a≡0→a≡0ℚ refl + +a≡0→↥a≡0 :{a : ℚ} → a ≡ 0ℚ → ↥ a ≡ 0 +a≡0→↥a≡0 {((n , d-1) , c)} a0 = cong ↥_ a0 + +↥a≡↥b≡0⇒a≡b : ∀ {a} {b} → ↥ a ≡ 0 → ↥ b ≡ 0 → a ≡ b +↥a≡↥b≡0⇒a≡b {a@((n , d-1) , c)} {b@((n' , d-1') , c')} a0 b0 = + (↥a≡0→a≡0ℚ a0) ∙ sym (↥a≡0→a≡0ℚ b0) + +-- equality depends on numerator and denominator +↥↧₊₁a≡↥↧₊₁b→a≡b : ∀ {a}{b} → ↥↧₊₁ a ≡ ↥↧₊₁ b → a ≡ b +↥↧₊₁a≡↥↧₊₁b→a≡b {a}{b} ab = ℚ-unique₊₁ (cong fst ab) (cong snd ab) + +↥↧₋₁a≡↥↧₋₁b→a≡b : ∀ {a}{b} → ↥↧₋₁ a ≡ ↥↧₋₁ b → a ≡ b +↥↧₋₁a≡↥↧₋₁b→a≡b {a}{b} ab = ℚ-unique₋₁ (cong fst ab) (cong snd ab) + +↥↧a≡↥↧b→a≡b : ∀ {a}{b} → ↥↧ a ≡ ↥↧ b → a ≡ b +↥↧a≡↥↧b→a≡b {a}{b} ab = ℚ-unique (cong fst ab) (cong snd ab) + +---------------------------------------------------- +-- Properties of normalise and [ _ ] + +toCoprime→Normalise≡ : ∀ {x y u v} → toCoprime (x , y) ≡ toCoprime (u , v) → + ↥↧₋₁ (normalise x y) ≡ ↥↧₋₁ (normalise u v) +toCoprime→Normalise≡ cc = cong (λ ab → forNormalise ab) cc + where + forNormalise : ∀ (ab : ℕ × ℕ₊₁) → ℤ × ℕ + forNormalise (a , b) = (pos a , -1+ b) + +↥↧₊₁-normalise : (m : ℕ) → (n : ℕ₊₁) → areCoprime (m , (ℕ₊₁→ℕ n)) → + (↥↧₊₁ (normalise m n)) ≡ (pos m , n) +↥↧₊₁-normalise m (1+ n') copr = cong step1 step2 + where + step1 : (ℕ × ℕ₊₁) → Σ ℤ (λ v → ℕ₊₁) + step1 = (λ a → (pos (fst a) , (snd a))) + step2 : (ToCoprime.c₁ (m , (1+ n')) , ToCoprime.c₂ (m , (1+ n'))) ≡ + (m , (1+ n')) + step2 = toCoprime-idem (m , (1+ n')) copr + +normalise-coprime : {m : ℕ} → {n : ℕ₊₁} → + (copr : areCoprime (m , (ℕ₊₁→ℕ n))) → + normalise m n ≡ ((pos m , -1+ n) , copr) +normalise-coprime {m}{n} copr = ↥↧₊₁a≡↥↧₊₁b→a≡b (↥↧₊₁-normalise m n copr) + +normalise-coprime' : {m : ℕ} → {n : ℕ} → + (copr : areCoprime (m , suc n)) → + normalise m (1+ n) ≡ ((pos m , n) , copr) +normalise-coprime' {m}{n} copr = normalise-coprime copr + +normaliseZero : ∀ n → normalise 0 n ≡ 0ℚ +normaliseZero n = ℚ-unique₋₁ refl (zeroCoprime (snd (normalise 0 n))) + +normaliseNonZero : ∀ m n → ¬ (normalise (suc m) n ≡ 0ℚ) +normaliseNonZero m n x = coprime≢0 m n + (ℤ.injPos ((cong (↥_) (normalise-id (suc m) n)) ∙ (cong ↥_ x))) + +numerator[]≢0 : ∀ z {n+} → ¬ ([ z , n+ ] ≡ 0ℚ) → ¬ (z ≡ 0) +numerator[]≢0 (pos zero) {n+} ¬0 x = + ⊥.elim {A = λ u → ⊥} (¬0 (normaliseZero n+)) +numerator[]≢0 (pos (suc n)) {n+} ¬0 x = + ⊥.elim {A = λ u → ⊥} (snotz (injPos x)) +numerator[]≢0 (negsuc n) {n+} ¬0 x = + ⊥.elim {A = λ u → ⊥} (negsucNotpos n zero x) + +[0,n]≡0 : ∀ n → [ 0 , n ] ≡ 0ℚ +[0,n]≡0 n = normaliseZero n + +[z,n]≡0→z≡0 : ∀ {z}{n} → [ z , n ] ≡ 0ℚ → z ≡ 0 +[z,n]≡0→z≡0 {pos zero} {n} zn0 = refl +[z,n]≡0→z≡0 {pos (suc m)} {n} zn0 = + ⊥.elim {A = λ x → pos (suc m) ≡ pos 0} (normaliseNonZero m n zn0) +[z,n]≡0→z≡0 {negsuc m} {n} zn0 = + ⊥.elim {A = λ x → negsuc m ≡ pos 0} + (normaliseNonZero m n ((sym neg-involutive) ∙ (cong -_ zn0) )) + +[negsuc]≡[-pos] : ∀ n d → [ negsuc n , d ] ≡ - [ pos (suc n) , d ] +[negsuc]≡[-pos] n d = refl + +[_]Def : ∀ {z}{n} copr → [ z , (1+ n) ] ≡ ((z , n) , copr) +[_]Def {pos m} {n} copr = normalise-coprime copr +[_]Def {negsuc m} {n} copr = cong -_ (normalise-coprime copr) + +≡↥↧₊₁ : ∀ x → x ≡ [ ↥ x , ↧₊₁ x ] +≡↥↧₊₁ x@((z , n) , copr) = sym [ copr ]Def + +gcd≡1→↥↧₊₁[x]≡x : ∀{z : ℤ}{n} → + ℕ.gcd (absℤ z) (suc n) ≡ 1 → ↥↧₊₁ [ z , (1+ n) ] ≡ (z , 1+ n) +gcd≡1→↥↧₊₁[x]≡x {z}{n} zn1 = cong ↥↧₊₁ [ gcd≡→isGCD zn1 ]Def + +·CancelR-normalise : ∀ ((m , n) : ℕ × ℕ₊₁) (k : ℕ₊₁) → + normalise (m ℕ.· ℕ₊₁→ℕ k) (n ·₊₁ k) ≡ normalise m n +·CancelR-normalise (m , n) k = + ↥↧₋₁a≡↥↧₋₁b→a≡b (toCoprime→Normalise≡ {m ℕ.· ℕ₊₁→ℕ k}{n ·₊₁ k}{m}{n} + (toCoprime-cancelʳ (m , n) k)) + +----------------------------------------------- +-- Equality of rational numbers + +infix 4 _≃_ + +data _≃_ : Rel ℚ ℚ ℓ-zero where + *≡* : ∀ {p q} → (↥ p ℤ· ↧ q) ≡ (↥ q ℤ· ↧ p) → p ≃ q + +_≄_ : Rel ℚ ℚ ℓ-zero +p ≄ q = ¬ (p ≃ q) + +*≡*⁻¹ : ∀ {p : ℚ} {q : ℚ} → p ≃ q → ↥ p ℤ· ↧ q ≡ ↥ q ℤ· ↧ p +*≡*⁻¹ {p} {q} (*≡* x) = x + +isProp≃ : ∀ {p q} → isProp (p ≃ q) +isProp≃ {(n , d-1) , c} {(n' , d-1') , c'} (*≡* x) (*≡* y) = cong *≡* + (isSetℤ (n ℤ· (↧ ((n' , d-1') , c'))) (n' ℤ· (↧ ((n , d-1) , c))) x y) + +dec≃ : ∀ {p q} → Dec (p ≃ q) +dec≃ {p}{q} with discreteℤ (↥ p ℤ· ↧ q) (↥ q ℤ· ↧ p) +... | yes pq = yes (*≡* pq) +... | no ¬pq = no λ x → ¬pq (*≡*⁻¹ x) + +≃-def : ∀ (p : ℚ) (q : ℚ) → (↥ p ℤ· ↧ q ≡ ↥ q ℤ· ↧ p) ≡ (p ≃ q) +≃-def p q = isoToPath + (iso (*≡* {p}{q}) (*≡*⁻¹ {p}{q}) (λ b → isProp≃ (*≡* (*≡*⁻¹ b)) b) + (λ a → isSetℤ ((↥ p) ℤ· (↧ q)) ((↥ q) ℤ· (↧ p)) + (*≡*⁻¹ {p}{q} (*≡* {p}{q} a)) a)) + +↥↧→≃ : ∀ {x}{y} → ↥ x ≡ ↥ y → ↧ x ≡ ↧ y → x ≃ y +↥↧→≃ nums dens = *≡* (cong₂ (ℤ._·_) nums (sym dens)) + +≡→≃ : ∀ {x} {y} → x ≡ y → x ≃ y +≡→≃ {x}{y} xy = ↥↧→≃ (cong (λ u → ↥ u) xy) (cong (λ u → ↧ u) xy) + +≄→¬≡ : ∀ {x} {y} → x ≄ y → ¬ (x ≡ y) +≄→¬≡ {x} {y} nxy = λ u → nxy (≡→≃ u) + +p≃q→-p≃-q : ∀ {p}{q} → ↥ p ℤ.· ↧ q ≡ ↥ q ℤ.· ↧ p → + ↥ (- p) ℤ.· ↧ (- q) ≡ ↥ (- q) ℤ.· ↧ (- p) +p≃q→-p≃-q {p}{q} pq = cong₂ (λ a b → a ℤ.· b) (↥-neg p) (↧-neg q) ∙ + sym (-DistL· (↥ p) (↧ q)) ∙ cong -ℤ_ pq ∙ -DistL· (↥ q) (↧ p) ∙ + sym (cong₂ (λ a b → a ℤ.· b) (↥-neg q) (↧-neg p)) + +↥p·↧q≡↥q·↧p'→↥↧p≡↥↧qPos : ∀ {m}{n}{m'}{n'}{c}{c'} → + ↥ ((pos m , n) , c) ℤ· ↧ ((pos m' , n') , c') ≡ + ↥ ((pos m' , n') , c') ℤ· ↧ ((pos m , n) , c) → + ↥↧ ((pos m , n) , c) ≡ ↥↧ ((pos m' , n') , c') +↥p·↧q≡↥q·↧p'→↥↧p≡↥↧qPos {zero} {n} {zero} {n'} {c} {c'} pq = + cong ↥↧ (0-id {n}{c}) ∙ sym (cong ↥↧ (0-id {n'}{c'})) +↥p·↧q≡↥q·↧p'→↥↧p≡↥↧qPos {zero} {n} {suc m'} {n'} {c} {c'} pq = + ⊥.elim {ℓ-zero}{λ x → ↥↧ ((pos zero , n) , c) ≡ + ↥↧ ((pos (suc m') , n') , c')} + (snotz (injPos (sym (signx·y≡signx·signy + (↥ ((pos (suc m') , n') , c')) (↧ ((pos zero , n) , c))) ∙ + sym (cong sign pq) ∙ + signx·y≡signx·signy (pos (zero)) (pos (suc n'))))) +↥p·↧q≡↥q·↧p'→↥↧p≡↥↧qPos {suc m}{n}{zero}{n'}{c}{c'} pq = + ⊥.elim {A = λ x → ↥↧ ((pos (suc m) , n) , c) ≡ + ↥↧ ((pos zero , n') , c')} (znots (ℤ.injPos ((sym (cong sign pq)) ∙ + (signx·y≡signx·signy (pos (suc m)) (pos (suc n')))))) +↥p·↧q≡↥q·↧p'→↥↧p≡↥↧qPos m@{suc p}{n} m'@{suc q}{n'}{c}{c'} pq i = + (cong pos m≡m' i) , (cong (λ a → pos (suc a)) (sym n≡n') i) + where + ℕHlp : suc p ℕ.· suc n' ≡ suc q ℕ.· suc n + ℕHlp = injPos + ((pos·pos m (suc n') ∙ pq ∙ sym (pos·pos m' (suc n)))) + m≡m' = natDivisibility c c' ℕHlp + n≡n' = injSuc (ℕ.inj-sm· {q} + ((sym (cong (λ v → v ℕ.· suc n') m≡m')) ∙ ℕHlp)) + +≃→≡ : ∀ {p}{q} → p ≃ q → p ≡ q +≃→≡ {p@((pos m , n) , c)} {q@((pos m' , n') , c')} (*≡* pq) = + ↥↧a≡↥↧b→a≡b (↥p·↧q≡↥q·↧p'→↥↧p≡↥↧qPos {c = c}{c' = c'} pq) +≃→≡ {p@((pos zero , n) , c)} {q@((negsuc m' , n') , c')} (*≡* pq) = + ⊥.elim {A = λ x → p ≡ q} ((posNotnegsuc 0 0) + (sym (sign↥p·↧q≡sign↥p p q) ∙ (cong sign pq) ∙ (sign↥p·↧q≡sign↥p q p))) +≃→≡ {p@((pos (suc m) , n) , c)} {q@((negsuc m' , n') , c')} (*≡* pq) = + ⊥.elim {A = λ x → p ≡ q} ((posNotnegsuc 1 0) + (sym (sign↥p·↧q≡sign↥p p q) ∙ (cong sign pq) ∙ (sign↥p·↧q≡sign↥p q p))) +≃→≡ {p@((negsuc m , n) , c)} {q@((pos zero , n') , c')} (*≡* pq) = + ⊥.elim {A = λ x → p ≡ q} ((negsucNotpos 0 0) + (sym (sign↥p·↧q≡sign↥p p q) ∙ (cong sign pq) ∙ (sign↥p·↧q≡sign↥p q p))) +≃→≡ {p@((negsuc m , n) , c)} {q@((pos (suc m') , n') , c')} (*≡* pq) = + ⊥.elim {A = λ x → p ≡ q} ((negsucNotpos 0 1) + (sym (sign↥p·↧q≡sign↥p p q) ∙ (cong sign pq) ∙ (sign↥p·↧q≡sign↥p q p))) +≃→≡ {p@((negsuc m , n) , c)} {q@((negsuc m' , n') , c')} (*≡* pq) = + let npq = (↥p·↧q≡↥q·↧p'→↥↧p≡↥↧qPos {c = c}{c' = c'} (p≃q→-p≃-q {p}{q} pq)) + in ℚ-unique (cong negsuc (injSuc (injPos (cong (λ a → (a .fst)) npq)))) + (cong (λ a → (a .snd)) npq) + +-- Equality relation and equality +≃≡≡ : ∀ (p q : ℚ) → (p ≃ q) ≡ (p ≡ q) +≃≡≡ p q = isoToPath (iso ≃→≡ ≡→≃ (λ b → isSetℚ p q (≃→≡ (≡→≃ b)) b) + (λ a → isProp≃ (≡→≃ (≃→≡ a)) a)) + +discreteℚ : Discrete ℚ +discreteℚ m n = subst Dec (≃≡≡ m n) dec≃ + +refl≃ : ∀ p → p ≃ p +refl≃ p = transport⁻ (≃≡≡ p p) refl + +sym≃-≡ : ∀ p q → (p ≃ q) ≡ (q ≃ p) +sym≃-≡ p q = isoToPath + (iso (λ x → *≡* (sym (*≡*⁻¹ x))) (λ x → *≡* (sym (*≡*⁻¹ x))) + (λ b → isProp≃ + (*≡* (λ i → *≡*⁻¹ {p}{q} (*≡* (λ i₁ → *≡*⁻¹ b (~ i₁))) (~ i))) b) + (λ a → isProp≃ + (*≡* (λ i → *≡*⁻¹ {q}{p} (*≡* (λ i₁ → *≡*⁻¹ a (~ i₁))) (~ i))) a)) + +isEquiv≃ : isEquivRel _≃_ +isEquiv≃ = equivRel (λ a → refl≃ a) (λ a b x → transport (sym≃-≡ a b) x) + λ a b c x y → ≡→≃ ((≃→≡ x) ∙ (≃→≡ y)) + +sym≃ : ∀{p}{q} → p ≃ q → q ≃ p +sym≃ {p}{q} = isEquiv≃ .symmetric p q + +trans≃ : ∀ {p}{q}{r} → p ≃ q → q ≃ r → p ≃ r +trans≃ {p}{q}{r} = isEquiv≃ .transitive p q r + +---------------------------------------------------------- +-- Unnormalised equivalence + +module gcd-helpers where + ↥·gcd-pos : ∀ n d1 → + pos n ≡ (↥ normalise n (1+ d1)) ℤ· ℤ.gcd (pos n) (pos (suc d1)) + ↥·gcd-pos n d1 = sym (let open ToCoprime (n , (1+ d1)) in cong pos p₁) ∙ + (pos·pos (fst (ToCoprime.toCoprime (n , (1+ d1)))) (gcd n (suc d1))) + + ↥·gcd-negsuc : ∀ n d1 → negsuc n ≡ + ↥ (- normalise (suc n) (1+ d1)) ℤ· ℤ.gcd (negsuc n) (pos (suc d1)) + ↥·gcd-negsuc n d1 = + (cong -ℤ_ (↥·gcd-pos (suc n) d1) ∙ + (-DistL· (↥ normalise (suc n) (1+ d1)) + (ℤ.gcd (pos (suc n)) (pos (suc d1))))) ∙ + (cong₂ (λ a b → a ℤ· b) (sym (↥-neg (normalise (suc n) (1+ d1)))) + (gcd-def (negsuc n) (pos (suc d1)) ∙ + sym (gcd-def (negsuc n) (pos (suc d1))))) + + ↧·gcd-pos : ∀ n d1 → pos (suc d1) ≡ + ↧ normalise n (1+ d1) ℤ· ℤ.gcd (pos n) (pos (suc d1)) + ↧·gcd-pos n d1 = sym (let open ToCoprime (n , (1+ d1)) in cong pos p₂) ∙ + pos·pos (ℕ₊₁→ℕ (ToCoprime.c₂ (n , (1+ d1)))) (gcd n (ℕ₊₁→ℕ (1+ d1))) ∙ + (cong (λ a → a ℤ· ℤ.gcd (pos n) (pos (suc d1))) step) + where + step : pos (ℕ₊₁→ℕ (ToCoprime.c₂ (n , (1+ d1)))) ≡ ↧ normalise n (1+ d1) + step = refl + + ↧·gcd-negsuc : ∀ n d1 → + pos (suc d1) ≡ ↧ (- normalise (suc n) (1+ d1)) ℤ· + ℤ.gcd (negsuc n) (pos (suc d1)) + ↧·gcd-negsuc n d1 = + let open ToCoprime ((suc n) , (1+ d1)) in sym (cong pos p₂) ∙ + pos·pos (ℕ₊₁→ℕ (ToCoprime.c₂ ((suc n) , (1+ d1)))) + (gcd (suc n) (ℕ₊₁→ℕ (1+ d1))) ∙ + cong (λ a → a ℤ· ℤ.gcd (pos (suc n)) (pos (suc d1))) step ∙ + cong (λ a → a ℤ· ℤ.gcd (negsuc n) (pos (suc d1))) + (sym (↧-neg (normalise (suc n) (1+ d1)))) + where + step : pos (ℕ₊₁→ℕ (ToCoprime.c₂ ((suc n) , (1+ d1)))) ≡ + ↧ normalise (suc n) (1+ d1) + step = refl + + ↧₊₁·gcd-pos : ∀ n d-1 → + 1+ d-1 ≡ ↧₊₁ (normalise n (1+ d-1)) ·₊₁ 1+ (predℕ (gcd n (suc d-1))) + ↧₊₁·gcd-pos n d-1 = ℕ₊₁→ℤ-inj (step1 ∙ step2) + where + step1 = ↧·gcd-pos n d-1 ∙ cong (λ u → ↧ normalise n (1+ d-1) ℤ· u) + (sym (ℕ₊₁→ℤ-gcd-def n d-1)) + step2 = sym (·ℕ₊₁→ℤ-distr (↧₊₁ normalise n (1+ d-1)) + (1+ predℕ (gcd n (suc d-1)))) + + ↧₊₁·gcd-negsuc : ∀ n d-1 → + 1+ d-1 ≡ ↧₊₁ (- normalise (suc n) (1+ d-1)) ·₊₁ 1+ + (predℕ (gcd (suc n) (suc d-1))) + ↧₊₁·gcd-negsuc n d-1 = ℕ₊₁→ℤ-inj (step1 ∙ step2) + where + step1 = ↧·gcd-negsuc n d-1 ∙ cong + (λ u → ℕ₊₁→ℤ (↧₊₁ (- normalise (suc n) (1+ d-1))) ℤ· u) + (sym (ℕ₊₁→ℤ-gcd-def (suc n) d-1)) + step2 = sym (·ℕ₊₁→ℤ-distr (↧₊₁ (- normalise (suc n) (1+ d-1))) + (1+ predℕ (gcd (suc n) (suc d-1)))) + +open gcd-helpers + +↥·gcd-lemma : ∀ numerator d-1 -> numerator ≡ + (↥ [ numerator , 1+ d-1 ]) ℤ· (ℤ.gcd numerator (pos (suc d-1))) +↥·gcd-lemma (pos n) d-1 = ↥·gcd-pos n d-1 +↥·gcd-lemma (negsuc n) d-1 = ↥·gcd-negsuc n d-1 + +↧·gcd-lemma : ∀ numerator d-1 -> pos (suc d-1) ≡ + (↧ [ numerator , 1+ d-1 ]) ℤ· (ℤ.gcd numerator (pos (suc d-1))) +↧·gcd-lemma (pos n) d-1 = ↧·gcd-pos n d-1 +↧·gcd-lemma (negsuc n) d-1 = ↧·gcd-negsuc n d-1 + +↧₊₁·gcd-lemma : ∀ numerator d-1 → + 1+ d-1 ≡ (↧₊₁ [ numerator , 1+ d-1 ]) ·₊₁ + (1+ (predℕ (gcd (absℤ numerator) (suc d-1)))) +↧₊₁·gcd-lemma (pos n) d-1 = ↧₊₁·gcd-pos n d-1 +↧₊₁·gcd-lemma (negsuc n) d-1 = ↧₊₁·gcd-negsuc n d-1 + +*≃*ᵘ : ∀{x}{y}{d-1}{d-1'} → + x ℤ· pos (suc d-1') ≡ y ℤ· pos (suc d-1) → [ x , 1+ d-1 ] ≃ [ y , 1+ d-1' ] +*≃*ᵘ {x}{y}{d-1}{d-1'} xy = *≡* res + where + lhs = cong₂ (λ x' d-1'' → x' ℤ· d-1'') + (↥·gcd-lemma x d-1) (↧·gcd-lemma y d-1') + rhs = cong₂ (λ x' d-1'' → x' ℤ· d-1'') + (↥·gcd-lemma y d-1') (↧·gcd-lemma x d-1) + step : ∀ {a}{b}{c}{d}{x}{y} → ¬ (x ≡ 0) → ¬ (y ≡ 0) → + (a ℤ· x) ℤ· (b ℤ· y) ≡ (c ℤ· y) ℤ· (d ℤ· x) → (a ℤ· b) ≡ (c ℤ· d) + step {a}{b}{c}{d}{x}{y} nx0 ny0 abcd = + ·rCancel (x ℤ· y) (a ℤ· b) (c ℤ· d) + (sym (ab'cd≡ac'bd a x b y) ∙ abcd ∙ (ab'cd≡ac'bd c y d x) ∙ + (cong (λ u → (c ℤ· d) ℤ· u) (·Comm y x))) (¬x≡0¬y≡0→¬x·y≡0 x y nx0 ny0) + res : (↥ [ x , (1+ d-1) ]) ℤ· (↧ [ y , (1+ d-1') ]) ≡ + (↥ [ y , (1+ d-1') ]) ℤ· (↧ [ x , (1+ d-1) ]) + res = step + {↥ [ x , (1+ d-1) ]}{↧ [ y , (1+ d-1') ]} + {↥ [ y , (1+ d-1') ]}{↧ [ x , (1+ d-1) ]} + {ℤ.gcd x (pos (suc d-1))}{ℤ.gcd y (pos (suc d-1'))} + (gcdSucNot0 x d-1) (gcdSucNot0 y d-1') ((sym lhs) ∙ xy ∙ rhs) + +*≃*ᵘ⁻¹ : ∀{x}{y}{d-1}{d-1'} → [ x , 1+ d-1 ] ≃ [ y , 1+ d-1' ] → + x ℤ· pos (suc d-1') ≡ y ℤ· pos (suc d-1) +*≃*ᵘ⁻¹ {x} {y} {d-1} {d-1'} (*≡* xy) = step1 ∙ step2 ∙ step3 ∙ step4 + where + step1 = sym (abcd≡ac'bd (↥ [ x , (1+ d-1) ]) (↧ [ y , (1+ d-1') ]) + (ℤ.gcd x (pos (suc d-1))) (ℤ.gcd y (pos (suc d-1'))) ∙ + cong₂ (λ a b → a ℤ· b) (sym (↥·gcd-lemma x d-1)) (sym (↧·gcd-lemma y d-1'))) + step2 = cong (λ a → a ℤ· ℤ.gcd x (pos (suc d-1)) ℤ· + ℤ.gcd y (pos (suc d-1'))) xy + step3 = (ab'c≡ac'b ((↥ [ y , (1+ d-1') ]) ℤ· + ((↧ [ x , (1+ d-1) ]))) (ℤ.gcd x (pos (suc d-1))) (ℤ.gcd y (pos (suc d-1')))) + step4 = abcd≡ac'bd (↥ [ y , (1+ d-1') ]) (↧ [ x , (1+ d-1) ]) + (ℤ.gcd y (pos (suc d-1'))) (ℤ.gcd x (pos (suc d-1))) ∙ + cong₂ (λ a b → a ℤ· b) (sym (↥·gcd-lemma y d-1')) (sym (↧·gcd-lemma x d-1)) + +*≡*ᵘ : ∀{x}{y}{d-1}{d-1'} → + x ℤ· pos (suc d-1') ≡ y ℤ· pos (suc d-1) → [ x , 1+ d-1 ] ≡ [ y , 1+ d-1' ] +*≡*ᵘ {x}{y}{d-1}{d-1'} xy = ≃→≡ (*≃*ᵘ {x}{y}{d-1}{d-1'} xy) + +*≡*ᵘ⁻¹ : ∀{x}{y}{d-1}{d-1'} → [ x , 1+ d-1 ] ≡ [ y , 1+ d-1' ] → + x ℤ· pos (suc d-1') ≡ y ℤ· pos (suc d-1) +*≡*ᵘ⁻¹ {x}{y}{d-1}{d-1'} xy = *≃*ᵘ⁻¹ {x}{y}{d-1}{d-1'} (≡→≃ xy) + +---------------------------------------------------------- +-- Type ordering + +infix 4 _≤_ +_≤_ : ℚ → ℚ → Type +p ≤ q = (↥ p ℤ.· ↧ q) ℤ.≤ (↥ q ℤ.· ↧ p) + +≤Dec : ∀ p q → Dec (p ≤ q) +≤Dec p q = ℤ.≤Dec (↥ p ℤ.· ↧ q) (↥ q ℤ.· ↧ p) + +----------------------------------------------------------- +-- Natural number and negative integer literals for ℚ + +open import Cubical.Data.Nat.Literals public + +instance + fromNatℚ : HasFromNat ℚ + fromNatℚ = record { Constraint = λ _ → Unit ; + fromNat = λ n → [ pos n , 1 ]} +negDisplay : ℕ → ℚ +negDisplay zero = [ pos 0 , 1 ] +negDisplay (suc n) = [ negsuc n , 1 ] + +instance + fromNegℚ : HasFromNeg ℚ + fromNegℚ = record { Constraint = λ _ → Unit ; + fromNeg = λ n → negDisplay n } From 95a5e8534b1cad40887050eb65ae83eaf21680dd Mon Sep 17 00:00:00 2001 From: robert Date: Mon, 29 Jun 2026 10:46:36 +0200 Subject: [PATCH 2/2] some minor additions --- Cubical/Data/Int/Properties.agda | 4 +- Cubical/Data/Nat/Coprime.agda | 13 ++ .../MoreRationals/NormalisedQ/Base.agda | 177 ++++++++++-------- 3 files changed, 116 insertions(+), 78 deletions(-) diff --git a/Cubical/Data/Int/Properties.agda b/Cubical/Data/Int/Properties.agda index 23d88222f4..9e4fc91574 100644 --- a/Cubical/Data/Int/Properties.agda +++ b/Cubical/Data/Int/Properties.agda @@ -1553,8 +1553,8 @@ clamp (negsuc n) = zero -- useful lemmas for _·_ -¬x≡0¬y≡0→¬x·y≡0 : ∀ x y → ¬ x ≡ 0 → ¬ y ≡ 0 → ¬ x · y ≡ 0 -¬x≡0¬y≡0→¬x·y≡0 x y nx0 ny0 = contraposition (isIntegralℤ x y) ny0 nx0 +¬x≡0¬y≡0→¬x·y≡0 : ∀ {x}{y} → ¬ x ≡ 0 → ¬ y ≡ 0 → ¬ x · y ≡ 0 +¬x≡0¬y≡0→¬x·y≡0 {x}{y} nx0 ny0 = contraposition (isIntegralℤ x y) ny0 nx0 ab'c≡ac'b : ∀ a b c → (a · b) · c ≡ (a · c) · b ab'c≡ac'b a b c = diff --git a/Cubical/Data/Nat/Coprime.agda b/Cubical/Data/Nat/Coprime.agda index c2e0a8c5ea..7450191c5c 100644 --- a/Cubical/Data/Nat/Coprime.agda +++ b/Cubical/Data/Nat/Coprime.agda @@ -7,6 +7,7 @@ open import Cubical.Relation.Nullary using (¬_) open import Cubical.Data.Sigma open import Cubical.Data.NatPlusOne +open import Cubical.Data.Sum open import Cubical.Data.Empty as ⊥ using (⊥) open import Cubical.HITs.PropositionalTruncation as PropTrunc @@ -209,3 +210,15 @@ natDivisibility' {suc m} {n} {zero} {n'} c c' mn = natDivisibility' m@{suc p} {n} m'@{suc q} {n'} c c' mn = injSuc (inj-sm· {p}{suc n} (cong (λ x → x · suc n) (natDivisibility c c' mn) ∙ sym mn)) + +symCoprime : ∀ m n → fst (toCoprime (suc m , (1+ n))) ≡ + ℕ₊₁→ℕ (snd (toCoprime (suc n , (1+ m)))) +symCoprime m n = inj-·sm ((sym (cong (λ u → c₁ · u) sucd1)) ∙ p₁ ∙ (sym p₂') ∙ + cong (λ u → ℕ₊₁→ℕ c₂' · u) (sym (gcdSym (suc m) (suc n))) ∙ + cong (λ u → (ℕ₊₁→ℕ c₂') · u) sucd1) + where + open ToCoprime (suc m , 1+ n) + open ToCoprime (suc n , 1+ m) using () + renaming (c₁ to c₁'; p₁ to p₁'; c₂ to c₂'; p₂ to p₂'; d to d') + d-1' = predℕ d + sucd1 = suc-predℕ d (gcd[m,n]≢0 (suc m) (suc n) (inl snotz)) diff --git a/Cubical/Data/Rationals/MoreRationals/NormalisedQ/Base.agda b/Cubical/Data/Rationals/MoreRationals/NormalisedQ/Base.agda index 03d7a5a198..2e3a7f068e 100644 --- a/Cubical/Data/Rationals/MoreRationals/NormalisedQ/Base.agda +++ b/Cubical/Data/Rationals/MoreRationals/NormalisedQ/Base.agda @@ -24,6 +24,9 @@ open import Cubical.Data.Int as ℤ open import Cubical.Data.Int.GCD as ℤ using (gcd-def; ℕ₊₁→ℤ-gcd-def; gcdSucNot0) open import Cubical.Data.Int.Order as ℤ using () +converse : {ℓ : Level} {a b : Type ℓ} → + (a → b) → ¬ b → ¬ a +converse = λ z z₁ z₂ → z₁ (z z₂) ------------------------------------------------ -- Core definitions @@ -142,6 +145,81 @@ neg-injective : ∀{a}{b} → - a ≡ - b → a ≡ b neg-injective {a}{b} -a-b = sym (neg-involutive {a}) ∙ (cong (-_) -a-b) ∙ neg-involutive {b} +------------------------------------------------- +-- Constructing rationals + +normalise : ℕ → ℕ₊₁ → ℚ +normalise m n = let numden = toCoprime (m , n) in + ((pos (fst numden)) , -1+ (snd numden)) , toCoprimeAreCoprime (m , n) + +normalise-id : (m : ℕ) → (n : ℕ₊₁) → let numden = toCoprime (m , n) in + normalise m n ≡ + (((pos (fst numden)) , -1+ (snd numden)) , toCoprimeAreCoprime (m , n)) +normalise-id m n = refl + +-- Constructors for ℚ that take two numbers, say -6 and 21, +-- and returns them in normalized form, e.g, -2 and 7. +[_] : (ℤ × ℕ₊₁) → ℚ +[ pos m , n ] = normalise m n +[ negsuc m , n ] = - normalise (suc m) n + +-- Some constants +0ℚ : ℚ +0ℚ = [ 0 , 1 ] + +1ℚ : ℚ +1ℚ = [ 1 , 1 ] + +-1ℚ : ℚ +-1ℚ = [ -1 , 1 ] + +½ : ℚ +½ = [ 1 , 2 ] + +-½ : ℚ +-½ = - ½ + +ℤ→ℚ : ℤ → ℚ +ℤ→ℚ z = [ z , 1 ] + +---------------------------------------------------- + +-- About 0ℚ + +↥a≡0→a≡0ℚ : {a : ℚ} → ↥ a ≡ 0 → a ≡ 0ℚ +↥a≡0→a≡0ℚ {a@((z , d-1) , c)} a0 = ℚ-unique₋₁ a0 (ℕ.injSuc (zeroCoprime' copr)) + where + copr = transport (cong (λ u → areCoprime (u , suc d-1)) (cong absℤ a0)) c + +↥0→↧₋₁0 : {a : ℚ} → ↥ a ≡ 0 → ↧₋₁ a ≡ 0 +↥0→↧₋₁0 {a@((n , d-1) , c)} a0 = ℕ.injSuc (zeroCoprime' copr) + where + copr = transport (cong (λ u → areCoprime (u , suc d-1)) (cong absℤ a0)) c + +↥0→↧1 : {a : ℚ} → ↥ a ≡ 0 → ↧ a ≡ 1 +↥0→↧1 {a} a0 = cong (λ u → pos (suc u)) (↥0→↧₋₁0 {a} a0) + +0-id : ∀ {n}{c} → ((pos zero , n) , c) ≡ 0ℚ +0-id {n}{c} = ↥a≡0→a≡0ℚ refl + +a≡0→↥a≡0 :{a : ℚ} → a ≡ 0ℚ → ↥ a ≡ 0 +a≡0→↥a≡0 {((n , d-1) , c)} a0 = cong ↥_ a0 + +↥a≡↥b≡0⇒a≡b : ∀ {a} {b} → ↥ a ≡ 0 → ↥ b ≡ 0 → a ≡ b +↥a≡↥b≡0⇒a≡b {a@((n , d-1) , c)} {b@((n' , d-1') , c')} a0 b0 = + (↥a≡0→a≡0ℚ a0) ∙ sym (↥a≡0→a≡0ℚ b0) + +-- equality depends on numerator and denominator +↥↧₊₁a≡↥↧₊₁b→a≡b : ∀ {a}{b} → ↥↧₊₁ a ≡ ↥↧₊₁ b → a ≡ b +↥↧₊₁a≡↥↧₊₁b→a≡b {a}{b} ab = ℚ-unique₊₁ (cong fst ab) (cong snd ab) + +↥↧₋₁a≡↥↧₋₁b→a≡b : ∀ {a}{b} → ↥↧₋₁ a ≡ ↥↧₋₁ b → a ≡ b +↥↧₋₁a≡↥↧₋₁b→a≡b {a}{b} ab = ℚ-unique₋₁ (cong fst ab) (cong snd ab) + +↥↧a≡↥↧b→a≡b : ∀ {a}{b} → ↥↧ a ≡ ↥↧ b → a ≡ b +↥↧a≡↥↧b→a≡b {a}{b} ab = ℚ-unique (cong fst ab) (cong snd ab) + + --------------------------------------------------- -- Signs @@ -211,6 +289,17 @@ decIsInteger : ∀ (p : ℚ) → Dec (IsInteger p) decIsInteger ((z , zero) , c) = yes tt decIsInteger ((z , suc n) , c) = no (λ ()) +NonZero→¬≡0 : ∀ {p : ℚ} → NonZero p → ¬ p ≡ 0ℚ +NonZero→¬≡0 p@{(pos (suc m) , n) , c} tt = + converse a≡0→↥a≡0 (λ x → snotz (injPos x)) +NonZero→¬≡0 p@{(negsuc m , n) , c} tt = + converse a≡0→↥a≡0 (λ x → ℤ.negsucNotpos m 0 x) + +¬≡0→NonZero : ∀ {p : ℚ} → ¬ p ≡ 0ℚ → NonZero p +¬≡0→NonZero {(pos zero , n) , c} ¬p0 = ¬p0 (↥a≡0→a≡0ℚ refl) +¬≡0→NonZero {(pos (suc m) , n) , c} ¬p0 = tt +¬≡0→NonZero {(negsuc m , n) , c} ¬p0 = tt + --------------------------------------------- -- Abs abs : ℚ → ℚ @@ -235,80 +324,6 @@ absIsNonNegative ((pos zero , n) , c) = tt absIsNonNegative ((pos (suc m) , n) , c) = tt absIsNonNegative ((negsuc m , n) , c) = tt -------------------------------------------------- --- Constructing rationals - -normalise : ℕ → ℕ₊₁ → ℚ -normalise m n = let numden = toCoprime (m , n) in - ((pos (fst numden)) , -1+ (snd numden)) , toCoprimeAreCoprime (m , n) - -normalise-id : (m : ℕ) → (n : ℕ₊₁) → let numden = toCoprime (m , n) in - normalise m n ≡ - (((pos (fst numden)) , -1+ (snd numden)) , toCoprimeAreCoprime (m , n)) -normalise-id m n = refl - --- Constructors for ℚ that take two numbers, say -6 and 21, --- and returns them in normalized form, e.g, -2 and 7. -[_] : (ℤ × ℕ₊₁) → ℚ -[ pos m , n ] = normalise m n -[ negsuc m , n ] = - normalise (suc m) n - --- Some constants -0ℚ : ℚ -0ℚ = [ 0 , 1 ] - -1ℚ : ℚ -1ℚ = [ 1 , 1 ] - --1ℚ : ℚ --1ℚ = [ -1 , 1 ] - -½ : ℚ -½ = [ 1 , 2 ] - --½ : ℚ --½ = - ½ - -ℤ→ℚ : ℤ → ℚ -ℤ→ℚ z = [ z , 1 ] - ----------------------------------------------------- - --- About 0ℚ - -↥a≡0→a≡0ℚ : {a : ℚ} → ↥ a ≡ 0 → a ≡ 0ℚ -↥a≡0→a≡0ℚ {a@((z , d-1) , c)} a0 = ℚ-unique₋₁ a0 (ℕ.injSuc (zeroCoprime' copr)) - where - copr = transport (cong (λ u → areCoprime (u , suc d-1)) (cong absℤ a0)) c - -↥0→↧₋₁0 : {a : ℚ} → ↥ a ≡ 0 → ↧₋₁ a ≡ 0 -↥0→↧₋₁0 {a@((n , d-1) , c)} a0 = ℕ.injSuc (zeroCoprime' copr) - where - copr = transport (cong (λ u → areCoprime (u , suc d-1)) (cong absℤ a0)) c - -↥0→↧1 : {a : ℚ} → ↥ a ≡ 0 → ↧ a ≡ 1 -↥0→↧1 {a} a0 = cong (λ u → pos (suc u)) (↥0→↧₋₁0 {a} a0) - -0-id : ∀ {n}{c} → ((pos zero , n) , c) ≡ 0ℚ -0-id {n}{c} = ↥a≡0→a≡0ℚ refl - -a≡0→↥a≡0 :{a : ℚ} → a ≡ 0ℚ → ↥ a ≡ 0 -a≡0→↥a≡0 {((n , d-1) , c)} a0 = cong ↥_ a0 - -↥a≡↥b≡0⇒a≡b : ∀ {a} {b} → ↥ a ≡ 0 → ↥ b ≡ 0 → a ≡ b -↥a≡↥b≡0⇒a≡b {a@((n , d-1) , c)} {b@((n' , d-1') , c')} a0 b0 = - (↥a≡0→a≡0ℚ a0) ∙ sym (↥a≡0→a≡0ℚ b0) - --- equality depends on numerator and denominator -↥↧₊₁a≡↥↧₊₁b→a≡b : ∀ {a}{b} → ↥↧₊₁ a ≡ ↥↧₊₁ b → a ≡ b -↥↧₊₁a≡↥↧₊₁b→a≡b {a}{b} ab = ℚ-unique₊₁ (cong fst ab) (cong snd ab) - -↥↧₋₁a≡↥↧₋₁b→a≡b : ∀ {a}{b} → ↥↧₋₁ a ≡ ↥↧₋₁ b → a ≡ b -↥↧₋₁a≡↥↧₋₁b→a≡b {a}{b} ab = ℚ-unique₋₁ (cong fst ab) (cong snd ab) - -↥↧a≡↥↧b→a≡b : ∀ {a}{b} → ↥↧ a ≡ ↥↧ b → a ≡ b -↥↧a≡↥↧b→a≡b {a}{b} ab = ℚ-unique (cong fst ab) (cong snd ab) - ---------------------------------------------------- -- Properties of normalise and [ _ ] @@ -476,7 +491,8 @@ p≃q→-p≃-q {p}{q} pq = cong₂ (λ a b → a ℤ.· b) (↥-neg p) (↧-neg in ℚ-unique (cong negsuc (injSuc (injPos (cong (λ a → (a .fst)) npq)))) (cong (λ a → (a .snd)) npq) --- Equality relation and equality + +-- Equality relation (normalised) and equality ≃≡≡ : ∀ (p q : ℚ) → (p ≃ q) ≡ (p ≡ q) ≃≡≡ p q = isoToPath (iso ≃→≡ ≡→≃ (λ b → isSetℚ p q (≃→≡ (≡→≃ b)) b) (λ a → isProp≃ (≡→≃ (≃→≡ a)) a)) @@ -599,7 +615,7 @@ open gcd-helpers step {a}{b}{c}{d}{x}{y} nx0 ny0 abcd = ·rCancel (x ℤ· y) (a ℤ· b) (c ℤ· d) (sym (ab'cd≡ac'bd a x b y) ∙ abcd ∙ (ab'cd≡ac'bd c y d x) ∙ - (cong (λ u → (c ℤ· d) ℤ· u) (·Comm y x))) (¬x≡0¬y≡0→¬x·y≡0 x y nx0 ny0) + (cong (λ u → (c ℤ· d) ℤ· u) (·Comm y x))) (¬x≡0¬y≡0→¬x·y≡0 nx0 ny0) res : (↥ [ x , (1+ d-1) ]) ℤ· (↧ [ y , (1+ d-1') ]) ≡ (↥ [ y , (1+ d-1') ]) ℤ· (↧ [ x , (1+ d-1) ]) res = step @@ -631,6 +647,15 @@ open gcd-helpers x ℤ· pos (suc d-1') ≡ y ℤ· pos (suc d-1) *≡*ᵘ⁻¹ {x}{y}{d-1}{d-1'} xy = *≃*ᵘ⁻¹ {x}{y}{d-1}{d-1'} (≡→≃ xy) +-- Equality relation (unnormalised) and equality +≃ᵘ≡≡ : ∀ {x}{y}{d-1}{d-1'} → + (x ℤ.· pos (suc d-1') ≡ y ℤ.· pos (suc d-1)) ≡ ([ x , 1+ d-1 ] ≡ [ y , 1+ d-1' ]) +≃ᵘ≡≡ {x}{y}{d-1}{d-1'} = isoToPath (iso (*≡*ᵘ {x}{y}{d-1}{d-1'}) (*≡*ᵘ⁻¹ {x}{y}{d-1}{d-1'}) + (λ b → (isSetℚ [ x , (1+ d-1) ] [ y , (1+ d-1') ]) + (*≡*ᵘ {x}{y}{d-1}{d-1'} (*≡*ᵘ⁻¹ {x}{y}{d-1}{d-1'} b)) b) + (λ a → (ℤ.isSetℤ (x ℤ.· pos (suc d-1')) (y ℤ.· pos (suc d-1))) + (*≡*ᵘ⁻¹ {x}{y}{d-1}{d-1'} (*≡*ᵘ {x}{y}{d-1}{d-1'} a)) a)) + ---------------------------------------------------------- -- Type ordering