Prime (and composite) numbers

Cubical/Data/Nat/Primes/Split.agda → Cubical/Data/Nat/Count.agda

@@ -1,20 +1,55 @@
-{-# OPTIONS --safe -W noUnsupportedIndexedMatch #-}
+{-# OPTIONS --safe #-}
 
-module Cubical.Data.Nat.Primes.Split where
+module Cubical.Data.Nat.Count where
 
-open import Cubical.Data.Nat.Primes.Imports
-open import Cubical.Data.Nat.Primes.Lemmas
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Function
+open import Cubical.Data.Nat
+open import Cubical.Data.Nat.Order
+open import Cubical.Data.Sigma
+open import Cubical.Data.Sum hiding (elim ; rec ; map)
+open import Cubical.Data.List hiding (elim ; rec ; map)
+
+open import Cubical.Relation.Nullary
 open import Cubical.Data.Empty as ⊥ hiding (elim)
 
 
 private
     variable
-        ℓ ℓ' : Level
+        ℓ ℓ' ℓ'' : Level
+
+    -- some definitions and lemmas
 
     decToN : {A : Type ℓ} → Dec A → ℕ
     decToN (yes _) = 1
     decToN (no  _) = 0
 
+    data All {A : Type ℓ} (P : A → Type ℓ') : List A → Type (ℓ-max ℓ ℓ') where
+      []  :                             All P []
+      _∷_ : ∀ {x xs} → P x → All P xs → All P (x ∷ xs)
+
+    mapAll : {A : Type ℓ} {P Q : A → Type ℓ'} {xs : List A} → (∀ {a} → P a → Q a) → All P xs → All Q xs
+    mapAll f [] = []
+    mapAll f (Px ∷ Pxs) = f Px ∷ mapAll f Pxs
+
+    add-equations : ∀ {a} {b} {c} {d} → a ≡ b → c ≡ d → a + c ≡ b + d
+    add-equations {b = b} {c = c} a=b c=d = cong (_+ c) a=b ∙ cong (b +_) c=d
+
+    <≠ : forall {m} {n} → m < n → ¬ m ≡ n
+    <≠ {m = m} m<n m=n = <-asym m<n (0 , sym m=n)
+
+
+DecProd-aux : {A : Type ℓ} (P : A → Type ℓ') (Q : A → Type ℓ'') → ∀ {a} →
+              Dec (P a) → Dec (Q a) → Dec (P a × Q a)
+DecProd-aux _ _ (yes Pa) (yes Qa) = yes (Pa , Qa)
+DecProd-aux _ _ (yes Pa) (no ¬Qa) = no (λ pf → ¬Qa (pf .snd))
+DecProd-aux _ _ (no ¬Pa) _        = no (λ pf → ¬Pa (pf .fst))
+
+DecProd : {A : Type ℓ} {P : A → Type ℓ'} {Q : A → Type ℓ''} →
+          (∀ a → Dec (P a)) → (∀ a → Dec (Q a)) → (∀ a → Dec (P a × Q a))
+DecProd {P = P} {Q = Q} Pdec Qdec a = DecProd-aux P Q (Pdec a) (Qdec a)
+
+
 -- splitting naturals below a bound
 -- into those for which a given decidable property holds
 -- and those for which it does not

Cubical/Data/Nat/Primes/Base.agda

@@ -2,17 +2,23 @@
 
 module Cubical.Data.Nat.Primes.Base where
 
-open import Cubical.Data.Nat.Primes.Imports
+open import Cubical.Foundations.Prelude public
+open import Cubical.Data.Nat
+open import Cubical.Data.Nat.Order
+open import Cubical.Data.Nat.Divisibility
+open import Cubical.Data.Sum hiding (elim ; rec ; map)
 open import Cubical.Data.Nat.Primes.Lemmas using (1<·1<=3<)
 
 
 record isPrime (n : ℕ) : Type where
+    no-eta-equality
     constructor prime
     field
         n-proper : 1 < n
         primality : ∀ d → d ∣ n → (d ≡ 1) ⊎ (d ≡ n)
 
 record isComposite (n : ℕ) : Type where
+    no-eta-equality
     constructor composite
     field
         p q : ℕ

Cubical/Data/Nat/Primes/DecProps.agda

@@ -8,6 +8,7 @@ open import Cubical.Data.Nat.Primes.Base
 open import Cubical.Data.Nat.Primes.Factors
 open import Cubical.Data.Empty as ⊥ hiding (elim)
 open import Cubical.Data.Sum.Properties
+open import Cubical.Reflection.RecordEquiv
 
 open isPrime
 open isComposite
@@ -23,50 +24,61 @@ private
     PropIso : ∀ {A : Type ℓ} {B : Type ℓ'} → isProp A → isProp B → (A → B) → (B → A) → Iso A B
     PropIso propA propB fun inv = iso fun inv (λ _ → propB _ _) (λ _ → propA _ _)
 
+
 primeProp : ∀ n → isProp (isPrime n)
-primeProp n (prime 1<n primality) (prime 1<n' primality') =
-    cong₂ prime
-    (isProp≤ 1<n 1<n')
+primeProp n np np' i .n-proper = isProp≤ (np .n-proper) (np' .n-proper) i
+primeProp n np np' i .primality =
     (funcProp  (λ x → funcProp  (λ x∣n →
     isProp⊎ (isSetℕ x 1) (isSetℕ x n)
-    λ x=1 x=n → ¬n<n (subst (λ y → y < n) (sym x=1 ∙ x=n) 1<n)
-    ))
-    primality primality' )
+    λ x=1 x=n → ¬n<n (subst (λ y → y < n) (sym x=1 ∙ x=n) (np .n-proper))))
+    (np .primality) (np' .primality)) i
 
 compProp : ∀ n → isProp (isComposite n)
-compProp n (composite p q pp 1<q pq=n least) (composite p' q' pp' 1<q' pq=n' least') =
-    λ i → composite
-    (p=p' i)
-    (q=q' i)
-    ((isProp→PathP (λ j → primeProp (p=p' j)) pp pp') i)
-    ((isProp→PathP (λ j → isProp≤ {n = q=q' j}) 1<q 1<q') i)
-    ((isProp→PathP (λ j → isSetℕ (p=p' j · q=q' j) n) pq=n pq=n') i)
-    ((isProp→PathP (λ j → leastProp (p=p' j)) least least') i)
-    where
-        1<p : 1 < p
-        1<p = n-proper pp
-        1<p' : 1 < p'
-        1<p' = n-proper pp'
-
-        p∣n : p ∣ n
-        p∣n = ∣ (q , ·-comm q p ∙ pq=n) ∣₁
-        p'∣n : p' ∣ n
-        p'∣n = ∣ (q' , ·-comm q' p' ∙ pq=n') ∣₁
-
-        p=p' : p ≡ p'
-        p=p' = ≤-antisym (least p' 1<p' p'∣n) (least' p 1<p p∣n)
-
-        q=q' : q ≡ q'
-        q=q' = inj-·0< q q' (<-weaken 1<p) (pq=n ∙ sym (subst (λ x → x · q' ≡ n) (sym p=p') pq=n'))
-
-        leastProp : ∀ x → isProp ((p'' : ℕ) → 1 < p'' → p'' ∣ n → x ≤ p'')
-        leastProp x = funcProp (λ a → funcProp (λ 1<a → funcProp (λ a∣n → isProp≤)))
+compProp n nc nc' = answer where
+    p1 = nc .p
+    p2 = nc' .p
+    q1 = nc .q
+    q2 = nc' .q
+    pp1 = nc .p-prime
+    pp2 = nc' .p-prime
+    1<p1 = pp1 .n-proper
+    1<p2 = pp2 .n-proper
+    1<q1 = nc .q-proper
+    1<q2 = nc' .q-proper
+    pq=n = nc .factors
+    pq=n' = nc' .factors
+    least1 = nc .least
+    least2 = nc' .least
+
+    p1∣n = ∣ (q1 , ·-comm q1 p1 ∙ pq=n) ∣₁
+    p2∣n = ∣ (q2 , ·-comm q2 p2 ∙ pq=n') ∣₁
+
+    p1=p2 : p1 ≡ p2
+    p1=p2 = ≤-antisym (least1 p2 1<p2 p2∣n) (least2 p1 1<p1 p1∣n)
+
+    q1=q2 : q1 ≡ q2
+    q1=q2 = inj-·0< q1 q2 (<-weaken 1<p1) (pq=n ∙ sym (subst (λ x → x · q2 ≡ n) (sym p1=p2) pq=n'))
+
+    leastProp : ∀ x → isProp ((p2' : ℕ) → 1 < p2' → p2' ∣ n → x ≤ p2')
+    leastProp x = funcProp (λ a → funcProp (λ 1<a → funcProp (λ a∣n → isProp≤)))
+
+    answer : nc ≡ nc'
+    answer i .p = ≤-antisym (least1 p2 1<p2 p2∣n) (least2 p1 1<p1 p1∣n) i
+    answer i .q = q1=q2 i
+    answer i .p-prime = isProp→PathP (λ j → primeProp (p1=p2 j)) pp1 pp2 i
+    answer i .q-proper = isProp→PathP (λ j → isProp≤ {n = q1=q2 j}) 1<q1 1<q2 i
+    answer i .factors = isProp→PathP (λ j → isSetℕ (p1=p2 j · q1=q2 j) n) pq=n pq=n' i
+    answer i .least = isProp→PathP (λ j → leastProp (p1=p2 j)) least1 least2 i
+
 
 prime→¬comp : ∀ n → isPrime n → ¬ isComposite n
-prime→¬comp n (prime 1<n primality) (composite p q pp 1<q pq=n _)
-    with (primality q ∣ (p , pq=n) ∣₁)
-... | inl q=1 = <≠ 1<q (sym q=1)
-... | inr q=n = <≠ (PropFac< q p n (n-proper pp) (<-weaken 1<n) (·-comm q p ∙ pq=n)) q=n
+prime→¬comp n pn cn with (pn .primality) (cn .q) (∣ (cn .p , cn .factors) ∣₁)
+... | inl q=1 = <≠ (cn .q-proper) (sym q=1)
+... | inr q=n = <≠ (PropFac< qfac pfac n (n-proper pp) (<-weaken (pn .n-proper)) (·-comm qfac pfac ∙ pq=n)) q=n where
+        pfac = cn .p
+        pp = cn .p-prime
+        qfac = cn .q
+        pq=n = cn .factors
 
 ¬comp→prime : ∀ n → 1 < n → ¬ isComposite n → isPrime n
 ¬comp→prime n 1<n ¬nc with primeOrComp n 1<n
@@ -90,8 +102,8 @@ comp≡¬prime n 1<n =
     isoToPath (PropIso (compProp n) (isProp¬ (isPrime n)) (comp→¬prime n) (¬prime→comp n 1<n))
 
 DecPrime : ∀ n → Dec (isPrime n)
-DecPrime 0 = no λ (prime 1<0 _) → ¬-<-zero 1<0
-DecPrime 1 = no λ (prime 1<1 _) → ¬n<n 1<1
+DecPrime 0 = no λ 0p → ¬-<-zero (0p .n-proper)
+DecPrime 1 = no λ 1p → ¬n<n (1p .n-proper)
 DecPrime n@(suc (suc n-2)) with (primeOrComp n (n-2 , +-comm n-2 2))
 ... | inl np = yes np
 ... | inr nc = no (comp→¬prime n nc)

Cubical/Data/Nat/Primes/Factors.agda

@@ -59,15 +59,18 @@ primeOrComp n@(suc n-1) 1<n = answer where
                                                         (sym (·-identityʳ p)) ∙ pq=n)
                                                   p<n))
 
+open isPrime
+open isComposite
+
 newPrime : ∀ n → Σ[ p ∈ ℕ ] (n < p) × (isPrime p)
 newPrime n with primeOrComp (suc (factorial n)) (suc< (0<factorial n))
 ... | inl sfnp = (suc (factorial n)) , suc-≤-suc (n≤! n) , sfnp
-... | inr (composite p q pp 1<q pq=n least) with Dichotomyℕ p n
-... | inr n<p = p , n<p , pp
-... | inl p≤n = ⊥.rec (<≠ 1<p (sym (div1→1 p p∣1))) where
-        1<p = pp .isPrime.n-proper
-        p∣1 : p ∣ 1
-        p∣1 = ∣+-cancel p 1 (n !) (≤n∣n! p n p≤n (1<→¬=0 p 1<p)) (∥_∥₁.∣ q , ·-comm q p ∙ pq=n ∣₁)
+... | inr cn with Dichotomyℕ (cn .p) n
+... | inr n<p = (cn .p) , n<p , (cn .p-prime)
+... | inl p≤n = ⊥.rec (<≠ 1<p (sym (div1→1 (cn .p) p∣1))) where
+        1<p = cn .p-prime .n-proper
+        p∣1 : (cn .p) ∣ 1
+        p∣1 = ∣+-cancel (cn .p) 1 (n !) (≤n∣n! (cn .p) n p≤n (1<→¬=0 (cn .p) 1<p)) (∣ (cn .q) , ·-comm (cn .q) (cn .p) ∙ (cn .factors) ∣₁)
 
 
 record PrimeFactors (n : ℕ) : Type where
@@ -84,16 +87,22 @@ PF-prime n np = pfs (n ∷ []) (·-identityʳ n) (np ∷ [])
 
 PF-comp-work : ∀ n → (∀ m → m < n → isComposite m → PrimeFactors m) → isComposite n →
                PrimeFactors n
-PF-comp-work n rec nComp@(composite p q p-prime 1<q pq=n _) =
-    pfs (p ∷ primes qFacs)
-        (subst (λ x → p · x ≡ n) (sym (factored qFacs)) pq=n)
-        (p-prime ∷ allPrime qFacs)
+PF-comp-work n rec nComp =
+    pfs (pfac ∷ primes qFacs)
+        (subst (λ x → pfac · x ≡ n) (sym (factored qFacs)) pq=n)
+        (pp ∷ allPrime qFacs)
         where
-            qFacs : PrimeFactors q
-            qFacs with (primeOrComp q 1<q)
-            ... | inl qp = PF-prime q qp
-            ... | inr qc = rec q (PropFac< q p n 1<p 0<n (·-comm q p ∙ pq=n)) qc where
-                    1<p = isPrime.n-proper p-prime
+            pfac = nComp .p
+            qfac = nComp .q
+            pp = nComp .p-prime
+            1<q = nComp .q-proper
+            pq=n = nComp .factors
+
+            qFacs : PrimeFactors qfac
+            qFacs with (primeOrComp qfac 1<q)
+            ... | inl qp = PF-prime qfac qp
+            ... | inr qc = rec qfac (PropFac< qfac pfac n 1<p 0<n (·-comm qfac pfac ∙ pq=n)) qc where
+                    1<p = isPrime.n-proper pp
                     0<n = <-trans (2 , refl) (isComposite.3<n nComp)
 
 PF-comp : ∀ n → isComposite n → PrimeFactors n

Cubical/Data/Nat/Primes/Infinitude.agda

@@ -1,14 +1,14 @@
-{-# OPTIONS --safe -W noUnsupportedIndexedMatch #-}
+{-# OPTIONS --safe #-}
 
 module Cubical.Data.Nat.Primes.Infinitude where
 
 open import Cubical.Data.Nat.Primes.Imports
 open import Cubical.Data.Nat.Primes.Lemmas
 open import Cubical.Data.Nat.Primes.Base
-open import Cubical.Data.Nat.Primes.Split
 open import Cubical.Data.Nat.Primes.Concrete
 open import Cubical.Data.Nat.Primes.Factors
 open import Cubical.Data.Nat.Primes.DecProps
+open import Cubical.Data.Nat.Count
 
 
 nextPrime : (n : ℕ) → Σ[ p ∈ ℕ ] ((n < p) × (isPrime p)) × ((z : ℕ) → (n < z) × isPrime z → p ≤ z)
@@ -47,10 +47,10 @@ nthPrime (suc n) = (next-prime .fst , next-prime .snd .fst .snd , snprimes) wher
 
 open Iso
 ℕ≅primeℕ : Iso ℕ (Σ ℕ isPrime)
-fun      ℕ≅primeℕ n = (pn .fst , pn .snd .fst) where pn = nthPrime n
-inv      ℕ≅primeℕ (p , _) = countBelow isPrime DecPrime p
-leftInv  ℕ≅primeℕ n = nthPrime n .snd .snd
-rightInv ℕ≅primeℕ (p , p-prime) =
+ℕ≅primeℕ .fun n = (pn .fst , pn .snd .fst) where pn = nthPrime n
+ℕ≅primeℕ .inv (p , _) = countBelow isPrime DecPrime p
+ℕ≅primeℕ .leftInv n = nthPrime n .snd .snd
+ℕ≅primeℕ .rightInv (p , p-prime) =
     ΣPathP (answer , isProp→PathP (λ i → primeProp (answer i)) pn-prime p-prime) where
         pn = nthPrime (countBelow isPrime DecPrime p)
         pn-prime = pn .snd .fst