Normalised Q plus related

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

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

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)

Cubical/Data/Nat/Coprime.agda

@@ -3,8 +3,11 @@ 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.Sum
 open import Cubical.Data.Empty as ⊥ using (⊥)
 
 open import Cubical.HITs.PropositionalTruncation as PropTrunc
@@ -103,6 +106,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
@@ -202,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))

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)

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

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)

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')