[Agda] primes decidable

Ruben Henner Zilibowitz rzilibowitz at yahoo.com.au
Sun Jan 10 21:42:27 CET 2010 

Hi Andreas,

I have rewritten my code now taking into account this issue and I'm glad to say it now compiles without any issues.

What I can't quite tell is whether this is a bug or a feature of the language. Perhaps it is just that a new feature is needed as you seem to be saying below. Certainly this sort of workaround seems quite cumbersome.

Regards,
Ruben

On 10/01/2010, at 8:56 PM, Andreas Abel wrote:

> 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