Merge tag 'upstream/0.17'

Upstream version 0.17

# gpg: Signature made Fri 23 Nov 2018 05:29:18 PM MST
# gpg:                using RSA key 9B917007AE030E36E4FC248B695B7AE4BF066240
# gpg:                issuer "spwhitton@spwhitton.name"
# gpg: Good signature from "Sean Whitton <spwhitton@spwhitton.name>" [ultimate]
# Primary key fingerprint: 8DC2 487E 51AB DD90 B5C4  753F 0F56 D055 3B6D 411B
#      Subkey fingerprint: 9B91 7007 AE03 0E36 E4FC  248B 695B 7AE4 BF06 6240

1 files changed, 24 insertions, 29 deletions

diff --git a/src/Data/Nat/Coprimality.agda b/src/Data/Nat/Coprimality.agda
index 85ed06c..19fdbf5 100644
--- a/src/Data/Nat/Coprimality.agda
+++ b/src/Data/Nat/Coprimality.agda
@@ -8,27 +8,25 @@ module Data.Nat.Coprimality where
 
 open import Data.Empty
 open import Data.Fin using (toℕ; fromℕ≤)
-open import Data.Fin.Properties as FinProp
+open import Data.Fin.Properties using (toℕ-fromℕ≤)
 open import Data.Nat
-open import Data.Nat.Primality
-import Data.Nat.Properties as NatProp
-open import Data.Nat.Divisibility as Div
+open import Data.Nat.Divisibility
 open import Data.Nat.GCD
 open import Data.Nat.GCD.Lemmas
+open import Data.Nat.Primality
+open import Data.Nat.Properties
 open import Data.Product as Prod
 open import Function
-open import Relation.Binary.PropositionalEquality as PropEq
-  using (_≡_; _≢_; refl)
+open import Level using (0ℓ)
+open import Relation.Binary.PropositionalEquality as P
+  using (_≡_; _≢_; refl; cong; subst; module ≡-Reasoning)
 open import Relation.Nullary
 open import Relation.Binary
-open import Algebra
-private
-  module P  = Poset Div.poset
 
 -- Coprime m n is inhabited iff m and n are coprime (relatively
 -- prime), i.e. if their only common divisor is 1.
 
-Coprime : (m n : ℕ) → Set
+Coprime : Rel ℕ 0ℓ
 Coprime m n = ∀ {i} → i ∣ m × i ∣ n → i ≡ 1
 
 -- Coprime numbers have 1 as their gcd.
@@ -37,15 +35,14 @@ coprime-gcd : ∀ {m n} → Coprime m n → GCD m n 1
 coprime-gcd {m} {n} c = GCD.is (1∣ m , 1∣ n) greatest
   where
   greatest : ∀ {d} → d ∣ m × d ∣ n → d ∣ 1
-  greatest      cd with c cd
-  greatest .{1} cd | refl = 1∣ 1
+  greatest cd with c cd
+  ... | refl = 1∣ 1
 
 -- If two numbers have 1 as their gcd, then they are coprime.
 
 gcd-coprime : ∀ {m n} → GCD m n 1 → Coprime m n
 gcd-coprime g cd with GCD.greatest g cd
-gcd-coprime g cd | divides q eq =
-  NatProp.i*j≡1⇒j≡1 q _ (PropEq.sym eq)
+... | divides q eq = i*j≡1⇒j≡1 q _ (P.sym eq)
 
 -- Coprime is decidable.
 
@@ -59,12 +56,12 @@ private
 coprime? : Decidable Coprime
 coprime? i j with gcd i j
 ... | (0           , g) = no  (0≢1  ∘ GCD.unique g ∘ coprime-gcd)
-... | (1           , g) = yes (λ {i} → gcd-coprime g {i})
+... | (1           , g) = yes (gcd-coprime g)
 ... | (suc (suc d) , g) = no  (2+≢1 ∘ GCD.unique g ∘ coprime-gcd)
 
 -- The coprimality relation is symmetric.
 
-sym : ∀ {m n} → Coprime m n → Coprime n m
+sym : Symmetric Coprime
 sym c = c ∘ swap
 
 -- Everything is coprime to 1.
@@ -75,12 +72,12 @@ sym c = c ∘ swap
 -- Nothing except for 1 is coprime to 0.
 
 0-coprimeTo-1 : ∀ {m} → Coprime 0 m → m ≡ 1
-0-coprimeTo-1 {m} c = c (m ∣0 , P.refl)
+0-coprimeTo-1 {m} c = c (m ∣0 , ∣-refl)
 
 -- If m and n are coprime, then n + m and n are also coprime.
 
 coprime-+ : ∀ {m n} → Coprime m n → Coprime (n + m) n
-coprime-+ c (d₁ , d₂) = c (∣-∸ d₁ d₂ , d₂)
+coprime-+ c (d₁ , d₂) = c (∣m+n∣m⇒∣n d₁ d₂ , d₂)
 
 -- If the "gcd" in Bézout's identity is non-zero, then the "other"
 -- divisors are coprime.
@@ -125,14 +122,13 @@ data GCD′ : ℕ → ℕ → ℕ → Set where
 gcd-gcd′ : ∀ {d m n} → GCD m n d → GCD′ m n d
 gcd-gcd′         g with GCD.commonDivisor g
 gcd-gcd′ {zero}  g | (divides q₁ refl , divides q₂ refl)
-                     with q₁ * 0 | NatProp.*-comm 0 q₁
-                        | q₂ * 0 | NatProp.*-comm 0 q₂
-...                  | .0 | refl | .0 | refl = gcd-* 1 1 (1-coprimeTo 1)
+  with q₁ * 0 | *-comm 0 q₁ | q₂ * 0 | *-comm 0 q₂
+... | .0 | refl | .0 | refl = gcd-* 1 1 (1-coprimeTo 1)
 gcd-gcd′ {suc d} g | (divides q₁ refl , divides q₂ refl) =
   gcd-* q₁ q₂ (Bézout-coprime (Bézout.identity g))
 
 gcd′-gcd : ∀ {m n d} → GCD′ m n d → GCD m n d
-gcd′-gcd (gcd-* q₁ q₂ c) = GCD.is (∣-* q₁ , ∣-* q₂) (coprime-factors c)
+gcd′-gcd (gcd-* q₁ q₂ c) = GCD.is (n∣m*n q₁ , n∣m*n q₂) (coprime-factors c)
 
 -- Calculates (the alternative representation of) the gcd of the
 -- arguments.
@@ -149,11 +145,11 @@ prime⇒coprime 1             () _ _  _     _
 prime⇒coprime (suc (suc m)) _  0 () _     _
 prime⇒coprime (suc (suc m)) _  _ _  _ {1} _                       = refl
 prime⇒coprime (suc (suc m)) p  _ _  _ {0} (divides q 2+m≡q*0 , _) =
-  ⊥-elim $ NatProp.i+1+j≢i 0 (begin
+  ⊥-elim $ i+1+j≢i 0 (begin
     2 + m  ≡⟨ 2+m≡q*0 ⟩
-    q * 0  ≡⟨ proj₂ NatProp.*-zero q ⟩
+    q * 0  ≡⟨ *-zeroʳ q ⟩
     0      ∎)
-  where open PropEq.≡-Reasoning
+  where open ≡-Reasoning
 prime⇒coprime (suc (suc m)) p (suc n) _ 1+n<2+m {suc (suc i)}
               (2+i∣2+m , 2+i∣1+n) =
   ⊥-elim (p _ 2+i′∣2+m)
@@ -163,10 +159,9 @@ prime⇒coprime (suc (suc m)) p (suc n) _ 1+n<2+m {suc (suc i)}
     3 + i  ≤⟨ s≤s (∣⇒≤ 2+i∣1+n) ⟩
     2 + n  ≤⟨ 1+n<2+m ⟩
     2 + m  ∎)
-    where open NatProp.≤-Reasoning
+    where open ≤-Reasoning
 
   2+i′∣2+m : 2 + toℕ (fromℕ≤ i<m) ∣ 2 + m
-  2+i′∣2+m = PropEq.subst
-    (λ j → j ∣ 2 + m)
-    (PropEq.sym (PropEq.cong (_+_ 2) (FinProp.toℕ-fromℕ≤ i<m)))
+  2+i′∣2+m = subst (_∣ 2 + m)
+    (P.sym (cong (2 +_) (toℕ-fromℕ≤ i<m)))
     2+i∣2+m