← Back to branch summary

~ubuntu-branches/ubuntu/raring/agda-stdlib/raring

« back to all changes in this revision

Viewing changes to src/Data/Nat/Coprimality.agda

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2013-04-10 10:30:20 UTC
  • mfrom: (2.1.7 experimental)
  • Revision ID: package-import@ubuntu.com-20130410103020-bcspfz3whyy5iafu
Tags: 0.7-1
* [6d52289] Imported Upstream version 0.7
* [54104d0] Update Depends and Build-Depends for this version, compatible
  with Agda 2.3.2
* [b3ddce4] No need for the .install file to be executable (thanks lintian)
* [a9a6cb7] Standards-Version → 3.9.4, no changes required

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/Data/Nat/Coprimality.agda
6
6
 
7
7
module Data.Nat.Coprimality where
8
8
 
 
9
open import Data.Empty
 
10
open import Data.Fin using (toℕ; fromℕ≤)
 
11
open import Data.Fin.Props as FinProp
9
12
open import Data.Nat
 
13
open import Data.Nat.Primality
10
14
import Data.Nat.Properties as NatProp
11
15
open import Data.Nat.Divisibility as Div
12
16
open import Data.Nat.GCD
136
140
 
137
141
gcd′ : ∀ m n → ∃ λ d → GCD′ m n d
138
142
gcd′ m n = Prod.map id gcd-gcd′ (gcd m n)
 
143
 
 
144
-- Primality implies coprimality.
 
145
 
 
146
prime⇒coprime : ∀ m → Prime m →
 
147
                ∀ n → 0 < n → n < m → Coprime m n
 
148
prime⇒coprime 0             () _ _  _     _
 
149
prime⇒coprime 1             () _ _  _     _
 
150
prime⇒coprime (suc (suc m)) _  0 () _     _
 
151
prime⇒coprime (suc (suc m)) _  _ _  _ {1} _                       = refl
 
152
prime⇒coprime (suc (suc m)) p  _ _  _ {0} (divides q 2+m≡q*0 , _) =
 
153
  ⊥-elim $ NatProp.i+1+j≢i 0 (begin
 
154
    2 + m  ≡⟨ 2+m≡q*0 ⟩
 
155
    q * 0  ≡⟨ proj₂ CS.zero q ⟩
 
156
    0      ∎)
 
157
  where open PropEq.≡-Reasoning
 
158
prime⇒coprime (suc (suc m)) p (suc n) _ 1+n<2+m {suc (suc i)}
 
159
              (2+i∣2+m , 2+i∣1+n) =
 
160
  ⊥-elim (p _ 2+i′∣2+m)
 
161
  where
 
162
  i<m : i < m
 
163
  i<m = ≤-pred $ ≤-pred (begin
 
164
    3 + i  ≤⟨ s≤s (∣⇒≤ 2+i∣1+n) ⟩
 
165
    2 + n  ≤⟨ 1+n<2+m ⟩
 
166
    2 + m  ∎)
 
167
    where open ≤-Reasoning
 
168
 
 
169
  2+i′∣2+m : 2 + toℕ (fromℕ≤ i<m) ∣ 2 + m
 
170
  2+i′∣2+m = PropEq.subst
 
171
    (λ j → j ∣ 2 + m)
 
172
    (PropEq.sym (PropEq.cong (_+_ 2) (FinProp.toℕ-fromℕ≤ i<m)))
 
173
    2+i∣2+m