Prime (and composite) numbers #1228
Conversation
|
Hi @qlbrpl , thanks for contributing! |
| decToN (yes _) = 1 | ||
| decToN (no _) = 0 | ||
|
|
||
| data All {A : Type ℓ} (P : A → Type ℓ') : List A → Type (ℓ-max ℓ ℓ') where |
There was a problem hiding this comment.
I don't think this should be a private definition here because it's useful in other places, you should move it to Data.List
| 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 |
There was a problem hiding this comment.
This is cong₂ _+_ (cong₂ is defined in the prelude)
| <≠ {m = m} m<n m=n = <-asym m<n (0 , sym m=n) | ||
|
|
||
|
|
||
| DecProd-aux : {A : Type ℓ} (P : A → Type ℓ') (Q : A → Type ℓ'') → ∀ {a} → |
There was a problem hiding this comment.
This could be in Cubical.Relation.Nullary.DecidablePropositions
| 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') |
There was a problem hiding this comment.
Feels like this could also be useful elsewhere, you might want to extract this out (or make it a named where block so the definitions are accessible outside)
|
|
||
| step→ : {A : Type ℓ} (B : Type ℓ') → (A → B) → A → B | ||
| step→ _ f = f | ||
| step⇒ : {A : Type ℓ} (B : Type ℓ') → (A → B) → A → B |
There was a problem hiding this comment.
This isn't related to primes, and it could be useful in other places so this could be moved to Foundations.Function
| -- All and mapAll | ||
| -- All | ||
|
|
||
| data All {A : Type ℓ} (P : A → Type ℓ') : List A → Type (ℓ-max ℓ ℓ') where |
There was a problem hiding this comment.
This is duplicated in Data.Nat.Count
|
@felixwellen Are there any more changes you're looking for on this, or is it ready to be merged? |
3 participants
Defined and formalized a bunch of properties of prime and composite numbers, all working up to the ultimate result of proving that ℕ is isomorphic to Σ ℕ isPrime. This is my first pull request, and I only started learning Agda about a month ago; constructive criticism of any sort is very much appreciated!