Skip to content
{{ message }}

Instantly share code, notes, and snippets.

# copumpkin/Prime.agda

Last active May 17, 2020
There are infinite primes
 module Prime where open import Coinduction open import Data.Empty open import Data.Nat open import Data.Nat.Properties open import Data.Nat.Divisibility open import Data.Fin hiding (pred; _+_; _<_; _≤_; compare) open import Data.Fin.Props hiding (_≟_) open import Data.Sum open import Data.Product open import Data.Stream open import Function open import Relation.Nullary open import Relation.Binary open import Relation.Binary.PropositionalEquality open import Induction.WellFounded as WF import Induction.Nat as NI open import Algebra open DecTotalOrder decTotalOrder using () renaming (refl to ≤-refl; trans to ≤-trans) open CommutativeSemiring commutativeSemiring using (*-assoc; *-comm; *-identity; +-assoc; +-comm; +-identity) -- We can negate a decision on a type A not : {A : Set} → Dec A → Dec (¬ A) not (yes p) = no (λ z → z p) not (no ¬p) = yes ¬p -- Decisions exactly the law of excluded middle for a specific type, which gives us double negation elimination on that type DNE : {A : Set} → Dec A → ¬ ¬ A → A DNE (yes p) f = p DNE (no ¬p) f = ⊥-elim (f ¬p) -- A decision procedure for an arbitrary predicate P Decide : {A : Set} (P : A → Set) → Set Decide P = ∀ i → Dec (P i) module Finite where -- Either the decidable predicate is true over its entire (finite) domain, or there exists an input for which it is false. -- Thanks to Ulf Norell for this! LPO : ∀ {n} {P : Fin n → Set} (p? : Decide P) → (∀ i → P i) ⊎ ∃ (¬_ ∘ P) LPO {zero} p? = inj₁ (λ ()) LPO {suc n} p? with LPO (p? ∘ suc) LPO {suc n} p? | inj₁ ok with p? zero LPO {suc n} p? | inj₁ ok | yes p = inj₁ (λ { zero → p ; (suc i) → ok i }) LPO {suc n} p? | inj₁ ok | no ¬p = inj₂ (zero , ¬p) LPO {suc n} p? | inj₂ (i , ¬pi) = inj₂ (suc i , ¬pi) -- A simple negation of the above, using DNE defined earlier, because this is the one we're usually interested in ¬LPO : ∀ {n} {P : Fin n → Set} (p? : Decide P) → ∃ P ⊎ (∀ i → ¬ P i) ¬LPO p? with LPO (not ∘ p?) ¬LPO p? | inj₁ x = inj₂ x ¬LPO p? | inj₂ (n , pf) = inj₁ (n , DNE (p? n) pf) -- We actually care about the LPO on naturals < k, instead of finite sets, so let's convert the above definition to work with them LPO : ∀ n {P : ℕ → Set} (p? : ∀ i → i < n → Dec (P i)) → (∀ i → i < n → P i) ⊎ ∃ (λ i → i < n × ¬ P i) LPO _ p? with Finite.LPO (λ i → p? _ (bounded i)) LPO _ {P} p? | inj₁ x = inj₁ (λ i i1 : p > 1 -- If you have something that divides our p, it's either 1 or p pf : ∀ {d} → d ∣ p → d ≡ 1 ⊎ d ≡ p -- A composite number has a prime divisor smaller than it record Composite (c : ℕ) : Set where constructor composite field {d} : ℕ P[d] : Prime d d1 pf₁) (composite d>1 d1 pf₁) (composite (prime (s≤s ()) _) d1 pf₁) (composite d>1 d 1 → Prime p ⊎ Composite p primality 0 () primality 1 (s≤s ()) primality (suc (suc p)) p>1 = <-rec _ helper p where module ∣-Poset = Poset poset helper : ∀ p → (∀ i → i < p → Prime (2 + i) ⊎ Composite (2 + i)) → Prime (2 + p) ⊎ Composite (2 + p) helper p f with ¬LPO p (λ i i

### akazakov commented Jun 7, 2016

 I don't understand the language, but this is almost like reading a math book LPO : ∀ n {P : ℕ → Set} (p? : ∀ i → i < n → Dec (P i)) → (∀ i → i < n → P i) ⊎ ∃ (λ i → i < n × ¬ P i) very cool
to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.