[Agda] primes decidable
Andreas Abel
andreas.abel at ifi.lmu.de
Sun Jan 10 10:50:11 CET 2010
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:
-------------- next part --------------
A non-text attachment was scrubbed...
Name: TerminationTwoConstructors.agda
Type: application/octet-stream
Size: 234 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20100110/dc3ead39/TerminationTwoConstructors-0001.obj
-------------- next part --------------
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
More information about the Agda
mailing list