[Agda] primes decidable
Ruben Henner Zilibowitz
rzilibowitz at yahoo.com.au
Sun Jan 10 02:39:48 CET 2010
I've been toying with a decidable primes type. My code is included below. Currently the main problem is that although the code type checks ok, the testComposite function does not pass the termination checker, even although I think it should. If anyone can give some more insight into this for me that would be great. I'm on agda 2.2.4.
Regards,
Ruben
--------
module Primes where
open import Data.Nat
open import Data.Nat.Divisibility
open import Data.Empty
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary.Negation
open import Data.Fin
renaming ( _+_ to _F+_; _-_ to _F-_
; _≤_ to _F≤_; _<_ to _F<_
; suc to fsuc; zero to fzero
; pred to fpred)
open import Relation.Nullary
open import Relation.Binary
-- open import Relation.Binary.PreorderReasoning
open import Relation.Binary.PropositionalEquality as PropEq
open import Data.Product
open import Data.Sum
open import Data.Function
open import Data.Bool renaming ( _≟_ to _B≟_ )
-- Prime m is inhabited iff m is a prime number.
-- In this setup, 0 and 1, contrary to convention are considered primes.
Prime : (m : ℕ) → Set
Prime m = ∀ {i} → i < m → i ∣ m → i ≡ 1
-- Composite m is inhabited iff m is a composite number.
Composite : (m : ℕ) → Set
Composite m = ∃ (λ d → 1 < d × d < m × d ∣ m)
0-prime : Prime 0
0-prime ()
1-prime : Prime 1
1-prime (s≤s z≤n) 0∣1 = contradiction (0∣0 0∣1) (λ())
2-prime : Prime 2
2-prime (s≤s z≤n) 0∣2 = contradiction (0∣0 0∣2) (λ())
2-prime (s≤s (s≤s z≤n)) _ = refl
3-prime : Prime 3
3-prime (s≤s z≤n) 0∣3 = contradiction (0∣0 0∣3) (λ())
3-prime (s≤s (s≤s z≤n)) _ = refl
3-prime (s≤s (s≤s (s≤s z≤n))) 2∣3 = 1∣1 (∣-∸ (divides 2 refl) 2∣3)
5-prime : Prime 5
5-prime (s≤s z≤n) 0∣5 = contradiction (0∣0 0∣5) (λ())
5-prime (s≤s (s≤s z≤n)) _ = refl
5-prime (s≤s (s≤s (s≤s z≤n))) 2∣5 = 1∣1 (∣-∸ (divides 3 refl) 2∣5)
5-prime (s≤s (s≤s (s≤s (s≤s z≤n)))) 3∣5 = 1∣1 (∣-∸ (divides 2 refl) 3∣5)
5-prime (s≤s (s≤s (s≤s (s≤s (s≤s z≤n))))) 4∣5 = 1∣1 (∣-∸ 4∣5 (divides 1 refl))
7-prime : Prime 7
7-prime (s≤s z≤n) 0∣7 = contradiction (0∣0 0∣7) (λ())
7-prime (s≤s (s≤s z≤n)) _ = refl
7-prime (s≤s (s≤s (s≤s z≤n))) 2∣7
= contradiction 2∣7 (nonZeroDivisor-lemma 1 3 (fromℕ 1) (λ()))
7-prime (s≤s (s≤s (s≤s (s≤s z≤n)))) 3∣7
= contradiction 3∣7 (nonZeroDivisor-lemma 2 2 (fromℕ≤ (s≤s (s≤s z≤n))) (λ()))
7-prime (s≤s (s≤s (s≤s (s≤s (s≤s z≤n))))) 4∣7
= contradiction 4∣7 (nonZeroDivisor-lemma 3 1 (fromℕ 3) (λ()))
7-prime (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s z≤n)))))) 5∣7
= contradiction 5∣7 (nonZeroDivisor-lemma 4 1 (fromℕ≤ (s≤s (s≤s (s≤s z≤n)))) (λ()))
7-prime (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s z≤n))))))) 6∣7
= contradiction 6∣7 (nonZeroDivisor-lemma 5 1 (fromℕ≤ (s≤s (s≤s z≤n))) (λ()))
11-prime : Prime 11
11-prime (s≤s z≤n) 0∣11 = contradiction (0∣0 0∣11) (λ())
11-prime (s≤s (s≤s z≤n)) _ = refl
11-prime (s≤s (s≤s (s≤s z≤n))) 2∣11
= contradiction 2∣11 (nonZeroDivisor-lemma 1 5 (fsuc fzero) (λ()))
11-prime (s≤s (s≤s (s≤s (s≤s z≤n)))) 3∣11
= contradiction 3∣11 (nonZeroDivisor-lemma 2 3 (fsuc (fsuc fzero)) (λ()))
11-prime (s≤s (s≤s (s≤s (s≤s (s≤s z≤n))))) 4∣11
= contradiction 4∣11 (nonZeroDivisor-lemma 3 2 (fsuc (fsuc (fsuc fzero))) (λ()))
11-prime (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s z≤n)))))) 5∣11
= contradiction 5∣11 (nonZeroDivisor-lemma 4 2 (fsuc fzero) (λ()))
11-prime (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s z≤n))))))) 6∣11
= contradiction 6∣11 (nonZeroDivisor-lemma 5 1 (fsuc (fsuc (fsuc (fsuc (fsuc fzero))))) (λ()))
11-prime (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s z≤n)))))))) 7∣11
= contradiction 7∣11 (nonZeroDivisor-lemma 6 1 (fsuc (fsuc (fsuc (fsuc fzero)))) (λ()))
11-prime (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s z≤n))))))))) 8∣11
= contradiction 8∣11 (nonZeroDivisor-lemma 7 1 (fsuc (fsuc (fsuc fzero))) (λ()))
11-prime (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s z≤n)))))))))) 9∣11
= contradiction 9∣11 (nonZeroDivisor-lemma 8 1 (fsuc (fsuc fzero)) (λ()))
11-prime (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s z≤n))))))))))) 10∣11
= contradiction 10∣11 (nonZeroDivisor-lemma 9 1 (fsuc fzero) (λ()))
4-composite : Composite 4
4-composite = 2 , (s≤s (s≤s z≤n)) , (s≤s (s≤s (s≤s z≤n))) , divides 2 refl
6-composite : Composite 6
6-composite = 2 , (s≤s (s≤s z≤n)) , (s≤s (s≤s (s≤s z≤n))) , divides 3 refl
∃-primes : ∃ Prime
∃-primes = 2 , λ {_} → 2-prime
∃-composites : ∃ Composite
∃-composites = 4 , 4-composite
a<b⟶a≢b : ∀ {a b} → a < b → a ≢ b
a<b⟶a≢b {zero} {zero} () _
a<b⟶a≢b {suc a} {zero} _ ()
a<b⟶a≢b {zero} {suc b} _ ()
a<b⟶a≢b {suc a} {suc b} (s≤s a<b) sa=sb = a<b⟶a≢b {a} {b} a<b (cong pred sa=sb)
composite⟶¬prime : ∀ {n} → Composite n → ¬ (Prime n)
composite⟶¬prime (d , 1<d , d<n , d∣n) primen = (a<b⟶a≢b 1<d) (sym (primen {d} d<n d∣n))
4-¬prime : ¬ (Prime 4)
4-¬prime = composite⟶¬prime 4-composite
prime⟶¬composite : ∀ {n} → Prime n → ¬ (Composite n)
prime⟶¬composite = flip composite⟶¬prime
5-¬composite : ¬ (Composite 5)
5-¬composite = prime⟶¬composite (λ {_} → 5-prime)
¬composite⟶prime : ∀ {n} → ¬ (Composite n) → Prime n
¬composite⟶prime _ {0} 0<n 0∣n = contradiction (sym (0∣0 0∣n)) (a<b⟶a≢b 0<n)
¬composite⟶prime _ {1} _ _ = refl
¬composite⟶prime ¬composite-n {suc (suc i)} ssi<n ssi∣n = contradiction ((s≤s (s≤s z≤n)) , ssi<n , ssi∣n) (¬∃⟶∀¬ ¬composite-n (suc (suc i)))
-- Compositeness is decidable.
≤-trans : Transitive _≤_
≤-trans = IsPreorder.trans (IsPartialOrder.isPreorder (IsTotalOrder.isPartialOrder (IsDecTotalOrder.isTotalOrder (DecTotalOrder.isDecTotalOrder decTotalOrder))))
∣-trans : Transitive _∣_
∣-trans = IsPreorder.trans (IsPartialOrder.isPreorder (Poset.isPartialOrder Data.Nat.Divisibility.poset))
∣-refl : _≡_ ⇒ _∣_
∣-refl = IsPreorder.reflexive (IsPartialOrder.isPreorder (Poset.isPartialOrder Data.Nat.Divisibility.poset))
≤-refl : _≡_ ⇒ _≤_
≤-refl = IsPreorder.reflexive (IsPartialOrder.isPreorder (IsTotalOrder.isPartialOrder (IsDecTotalOrder.isTotalOrder (DecTotalOrder.isDecTotalOrder decTotalOrder))))
≤-antisym : Antisymmetric _≡_ _≤_
≤-antisym = IsPartialOrder.antisym (IsTotalOrder.isPartialOrder (IsDecTotalOrder.isTotalOrder (DecTotalOrder.isDecTotalOrder decTotalOrder)))
a≢b⟶a≤b⟶a<b : ∀ {a b} → a ≢ b → a ≤ b → a < b
a≢b⟶a≤b⟶a<b {zero} {zero} 0≢0 _ = contradiction refl 0≢0
a≢b⟶a≤b⟶a<b {suc a} {zero} _ ()
a≢b⟶a≤b⟶a<b {zero} {suc b} _ _ = s≤s z≤n
a≢b⟶a≤b⟶a<b {suc a} {suc b} sa≢sb (s≤s a≤b) = s≤s (a≢b⟶a≤b⟶a<b {a} {b} (λ a≡b → sa≢sb (cong suc a≡b)) a≤b)
k≤i⟶k≡i⊎k<i : ∀ {k i} → k ≤ i → ((k ≡ i) ⊎ (k < i))
k≤i⟶k≡i⊎k<i {k} {i} k≤i with k ≟ i
.... | (yes k≡i) = inj₁ k≡i
.... | (no k≢i) = inj₂ (a≢b⟶a≤b⟶a<b k≢i k≤i)
n≤sn : ∀ {n} → n ≤ suc n
n≤sn {zero} = z≤n
n≤sn {suc n} = s≤s (n≤sn {n})
testComposite : (n : ℕ) → (k : ℕ) → k < n → (∀ {i} → k < i → i < n → ¬ (i ∣ n)) → Dec (Composite n)
testComposite 0 _ () _
testComposite n 0 _ n-partial-prime = no (λ x → n-partial-prime {proj₁ x} (≤-trans (s≤s z≤n) (proj₁ (proj₂ x))) (proj₁ (proj₂ (proj₂ x))) (proj₂ (proj₂ (proj₂ x))))
testComposite n 1 _ n-partial-prime = no (λ x → n-partial-prime {proj₁ x} (≤-trans (s≤s (s≤s z≤n)) (proj₁ (proj₂ x))) (proj₁ (proj₂ (proj₂ x))) (proj₂ (proj₂ (proj₂ x))))
testComposite n (suc (suc k)) ssk<n n-partial-prime with (suc (suc k)) ∣? n
.... | (yes ssk∣n) = yes (suc (suc k) , s≤s (s≤s z≤n) , ssk<n , ssk∣n)
.... | (no ¬ssk∣n) = testComposite n (suc k) (≤-trans n≤sn ssk<n) (λ {i} sk<i i<n → [ (λ ssk≡i i∣n → ¬ssk∣n (∣-trans (∣-refl ssk≡i) i∣n)) , (λ ssk<i → n-partial-prime {i} ssk<i i<n) ]′ (k≤i⟶k≡i⊎k<i sk<i))
a<b⟶¬b≤a : ∀ {a b} → a < b → ¬ (b ≤ a)
a<b⟶¬b≤a {a} {b} a<b b≤a = (a<b⟶a≢b a<b) (≤-antisym (≤-trans n≤sn a<b) b≤a)
composite? : (n : ℕ) → Dec (Composite n)
composite? zero = no (prime⟶¬composite 0-prime)
composite? (suc n) = testComposite (suc n) n (≤-refl refl) (λ {i} n<i i<sn → contradiction n<i (a<b⟶¬b≤a i<sn))
prime? : (n : ℕ) → Dec (Prime n)
prime? n with composite? n
.... | (yes n-composite) = no (composite⟶¬prime n-composite)
.... | (no ¬n-composite) = yes (λ {_} → ¬composite⟶prime ¬n-composite)
composite-⊎-prime : ∀ {n} → (Composite n) ⊎ (Prime n)
composite-⊎-prime {n} with composite? n
.... | (yes n-composite) = inj₁ n-composite
.... | (no ¬n-composite) = inj₂ (λ {_} → ¬composite⟶prime ¬n-composite)
¬prime⟶composite : ∀ {n} → ¬ (Prime n) → (Composite n)
¬prime⟶composite {n} ¬primen = [ id , (λ primen → contradiction primen ¬primen) ]′ (composite-⊎-prime {n})
{-
∞-primes : ∀ {n} → ∃ (λ m → m > n × Prime m)
∞-primes = {!!}
-}
More information about the Agda
mailing list