[Agda] primes decidable
Andreas Abel
andreas.abel at ifi.lmu.de
Sun Jan 10 10:56:54 CET 2010
Actually, it is a known bug, nr. 59.
http://code.google.com/p/agda/issues/detail?id=59&can=1&q=termination
See there how to rewrite your code.
My personal opinion on this (further) issue with "with" is that in
addition to the "with" which allows refinement of already present
patterns (into dot patterns, for instance), a more simplistic "case"
is called for which does not create an auxiliary function.
Cheers,
Andreas
On Jan 10, 2010, at 10:50 AM, Andreas Abel wrote:
> Hi Ruben,
>
> yes, your function should termination check, since
>
> suc k < suc (suc k)
>
> This information, however, is lost through the use of "with", which
> is translated into an auxiliary function which is mutually recursive
> with "testComposite". You found a bug which can be boiled down to
> the following trivial instance:
>
> <TerminationTwoConstructors.agda>
>
>
> For a quick fix, you can reformulate "testComposite" such that it
> does not use "with".
>
> @Ulf or Conor (the "with" architects): Do you have an idea how to
> salvage termination checking?
>
> Cheers,
> Andreas
>
>
> On Jan 10, 2010, at 2:39 AM, Ruben Henner Zilibowitz wrote:
>
>> 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 = {!!}
>> -}
>>
>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>
> Andreas ABEL
> INRIA, Projet Pi.R2
> 23, avenue d'Italie
> F-75013 Paris
> Tel: +33.1.39.63.59.41
>
>
>
Andreas ABEL
INRIA, Projet Pi.R2
23, avenue d'Italie
F-75013 Paris
Tel: +33.1.39.63.59.41
More information about the Agda
mailing list