Mercurial > hg > Members > kono > Proof > automaton
annotate automaton-in-agda/src/prime.agda @ 252:9fc9e19f2c37
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Tue, 29 Jun 2021 20:03:32 +0900 |
parents | 89120ac828b7 |
children | 4e4e148eb7e5 |
rev | line source |
---|---|
160 | 1 module prime where |
57 | 2 |
141 | 3 open import Data.Nat |
4 open import Data.Nat.Properties | |
57 | 5 open import Data.Empty |
141 | 6 open import Data.Unit using (⊤ ; tt) |
57 | 7 open import Relation.Nullary |
8 open import Relation.Binary.PropositionalEquality | |
141 | 9 open import Relation.Binary.Definitions |
57 | 10 |
148 | 11 open import gcd |
142 | 12 open import nat |
141 | 13 |
160 | 14 record Prime (i : ℕ ) : Set where |
15 field | |
205 | 16 p>1 : i > 1 |
17 isPrime : ( j : ℕ ) → j < i → 0 < j → gcd i j ≡ 1 | |
159 | 18 |
19 | |
169 | 20 record NonPrime ( n : ℕ ) : Set where |
21 field | |
22 factor : ℕ | |
171 | 23 prime : Prime factor |
169 | 24 dividable : Dividable factor n |
25 | |
199 | 26 PrimeP : ( n : ℕ ) → Dec ( Prime n ) |
205 | 27 PrimeP 0 = no (λ p → ⊥-elim ( nat-<> (Prime.p>1 p) (s≤s z≤n))) |
28 PrimeP 1 = no (λ p → ⊥-elim ( nat-≤> (Prime.p>1 p) (s≤s (≤-refl)))) | |
225 | 29 PrimeP (suc (suc n)) = isPrime1 (suc (suc n)) (suc n) (s≤s (s≤s z≤n)) a<sa (λ i m<i i<n → isp0 (suc n) i (<to≤ m<i) i<n ) where |
205 | 30 isp0 : (n : ℕ) (i : ℕ) ( n<i : n ≤ i) ( i<n : i < suc n ) → gcd (suc n) i ≡ 1 |
31 isp0 n i n<i i<n with <-cmp i n | |
32 ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> n<i a) | |
33 ... | tri≈ ¬a refl ¬c = gcd203 i | |
34 ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c i<n ) | |
225 | 35 isPrime1 : ( n m : ℕ ) → n > 1 → m < n → ( (i : ℕ) → m < i → i < n → gcd n i ≡ 1 ) → Dec ( Prime n ) |
36 isPrime1 n zero n>1 m<n lt = yes record { isPrime = λ j j<i 0<j → lt j 0<j j<i ; p>1 = n>1 } | |
205 | 37 isPrime1 n (suc m) n>1 m<n lt with <-cmp (gcd n (suc m)) 1 |
38 ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> ( gcd>0 n (suc m) (<-trans (s≤s z≤n) n>1) (s≤s z≤n)) a ) | |
39 ... | tri≈ ¬a b ¬c = isPrime1 n m n>1 (<-trans a<sa m<n) isp1 where | |
225 | 40 -- lt : (i : ℕ) → suc m ≤ i → suc i ≤ n → gcd1 n n i i ≡ 1 |
41 isp1 : (i : ℕ) → m < i → i < n → gcd n i ≡ 1 | |
42 isp1 i m<i i<n with <-cmp (suc m) i | |
43 ... | tri< a ¬b ¬c = lt i a i<n | |
44 ... | tri≈ ¬a m=i ¬c = subst (λ k → gcd n k ≡ 1) m=i b -- gcd n (suc m) ≡ 1 → gcd n i ≡ 1 | |
45 ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> m<i c) -- suc i ≤ suc m → i < m | |
205 | 46 ... | tri> ¬a ¬b c = no ( λ p → nat-≡< (sym (Prime.isPrime p (suc m) m<n (s≤s z≤n) )) c ) |
172 | 47 |
225 | 48 open import logic |
49 open _∧_ | |
226 | 50 |
229 | 51 data Factoring (m : ℕ ) : (n : ℕ) → Set where |
230 | 52 findFactor : (n : ℕ) → m ≤ n → ( (j : ℕ ) → m ≤ j → j < n → gcd n j ≡ 1 ) → Factoring m n |
229 | 53 skipFactor : (n : ℕ) → n < m → Factoring m n |
226 | 54 |
205 | 55 nonPrime : { n : ℕ } → 1 < n → ¬ Prime n → NonPrime n |
230 | 56 nonPrime {n} 1<n np = np1 n n np 1<n (findFactor n ≤-refl (λ j n≤j j<n → ⊥-elim (nat-≤> n≤j j<n ) )) where |
229 | 57 mg1 : (n m : ℕ )→ ( (j : ℕ ) → m < j → j < n → gcd n j ≡ 1 ) → gcd n m ≡ 1 → (j : ℕ) → m ≤ j → j < n → gcd n j ≡ 1 |
58 mg1 n m mg gcd j m<j j<n with <-cmp m j | |
228 | 59 ... | tri< a ¬b ¬c = mg j a j<n |
225 | 60 ... | tri≈ ¬a refl ¬c = gcd |
228 | 61 ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> m<j c) |
229 | 62 np1 : ( n m : ℕ ) → ¬ Prime n → 1 < n → Factoring m n → NonPrime n |
230 | 63 np1 n zero np 1<n (findFactor n m≤n mg ) = ⊥-elim ( np record { isPrime = λ j lt _ → mg j z≤n lt ; p>1 = 1<n } ) -- zero < j , j < n |
64 np1 n (suc m) np 1<n (findFactor n m≤n mg) with <-cmp ( gcd n m ) 1 | |
228 | 65 ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> ( gcd>0 n m (<-trans (s≤s z≤n) 1<n) 0<m ) a ) where |
66 0<m : 0 < m | |
67 0<m with <-cmp 0 m | |
68 ... | tri< a ¬b ¬c = a | |
69 ... | tri≈ ¬a refl ¬c = ⊥-elim ( nat-<> a (subst (λ k → 1 < k) (sym (gcd20 n)) 1<n )) | |
230 | 70 ... | tri≈ ¬a b ¬c = np1 n m np 1<n (findFactor n (≤-trans refl-≤s m≤n) (mg1 n m mg b ) ) |
228 | 71 ... | tri> ¬a ¬b c with PrimeP ( gcd n m ) |
72 ... | yes y = record { factor = gcd n m ; prime = y ; dividable = proj1 (gcd-dividable n m ) } | |
230 | 73 ... | no ngcd = np2 where |
74 skip-case : NonPrime (gcd n m) → NonPrime n | |
75 skip-case cc = record { factor = NonPrime.factor cc ; prime = NonPrime.prime cc ; dividable = | |
229 | 76 record { factor = (Dividable.factor (proj1 (gcd-dividable n m))) * (Dividable.factor (NonPrime.dividable cc)) |
230 | 77 ; is-factor = begin |
78 Dividable.factor (proj1 (gcd-dividable n m)) * Dividable.factor (NonPrime.dividable cc) * NonPrime.factor cc + 0 ≡⟨ refl ⟩ | |
79 g * d * p + 0 ≡⟨ +-comm _ 0 ⟩ | |
80 g * d * p ≡⟨ *-assoc g d p ⟩ | |
81 g * (d * p) ≡⟨ cong (λ k → g * k ) (+-comm 0 _) ⟩ | |
82 g * (d * p + 0) ≡⟨ cong (λ k → g * k ) (Dividable.is-factor (NonPrime.dividable cc) ) ⟩ | |
83 g * gcd n m ≡⟨ +-comm 0 _ ⟩ | |
84 g * gcd n m + 0 ≡⟨ Dividable.is-factor (proj1 (gcd-dividable n m)) ⟩ | |
85 n ∎ }} where | |
86 open ≡-Reasoning | |
87 g = Dividable.factor (proj1 (gcd-dividable n m)) | |
88 d = Dividable.factor (NonPrime.dividable cc) | |
89 p = NonPrime.factor cc | |
90 np2 : NonPrime n | |
91 np2 with <-cmp (gcd n m) m | |
92 ... | tri< a ¬b ¬c = skip-case (np1 (gcd n m) m ngcd c (skipFactor (gcd n m) a )) | |
93 ... | tri≈ ¬a b ¬c = skip-case (np1 (gcd n m) m ngcd c | |
94 (subst (λ k → Factoring m k) (sym b) (findFactor m ≤-refl (λ j n≤j j<n → ⊥-elim (nat-≤> n≤j j<n) )))) | |
95 ... | tri> ¬a ¬b' c with <-cmp 0 m | |
250 | 96 ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> (subst (λ k → k ≤ m) (gcdsym {m} {n}) (gcd-≤ a (<-trans a m≤n))) c ) |
230 | 97 ... | tri≈ ¬a' b' ¬c = ⊥-elim ( np record { isPrime = λ j lt 0<j → mg j (subst (λ k → k < j) b' 0<j) lt ; p>1 = 1<n } ) -- suc m ≤ j |
229 | 98 np1 n zero np 1<n (skipFactor n ()) |
99 np1 n (suc m) np 1<n (skipFactor n n<m) with <-cmp m n | |
100 ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> a n<m) | |
230 | 101 ... | tri> ¬a ¬b c = np1 n m np 1<n (skipFactor n c) |
102 ... | tri≈ ¬a refl ¬c = np1 n m np 1<n (findFactor m ≤-refl (λ j n≤j j<n → ⊥-elim (nat-≤> n≤j j<n) )) | |
199 | 103 |
252 | 104 factorial : (n : ℕ) → ℕ |
105 factorial zero = 1 | |
106 factorial (suc n) = (suc n) * (factorial n) | |
107 factorial-mono : (n : ℕ) → factorial n ≤ factorial (suc n) | |
108 factorial-mono n = begin | |
200 | 109 factorial n ≤⟨ x≤x+y ⟩ |
110 factorial n + n * factorial n ≡⟨ refl ⟩ | |
111 (suc n) * factorial n ≡⟨ refl ⟩ | |
112 factorial (suc n) ∎ where open ≤-Reasoning | |
252 | 113 factorial≥1 : {m : ℕ} → 1 ≤ factorial m |
114 factorial≥1 {zero} = ≤-refl | |
115 factorial≥1 {suc m} = begin | |
200 | 116 1 ≤⟨ s≤s z≤n ⟩ |
117 (suc m) * 1 ≤⟨ *-monoʳ-≤ (suc m) (factorial≥1 {m}) ⟩ | |
118 (suc m) * factorial m ≡⟨ refl ⟩ | |
119 factorial (suc m) ∎ where open ≤-Reasoning | |
252 | 120 m<factorial : (m : ℕ) → m ≤ factorial m |
121 m<factorial zero = z≤n | |
122 m<factorial (suc m) = begin | |
200 | 123 suc m ≡⟨ cong suc (+-comm 0 _) ⟩ |
124 1 * suc m ≡⟨ *-comm 1 _ ⟩ | |
125 (suc m) * 1 ≤⟨ *-monoʳ-≤ (suc m) (factorial≥1 {m}) ⟩ | |
126 (suc m) * factorial m ≡⟨ refl ⟩ | |
127 factorial (suc m) ∎ where open ≤-Reasoning | |
252 | 128 -- *-monoˡ-≤ (suc m) {!!} |
129 fact< : (m n : ℕ) → 0 < n → n < suc (suc m) → Dividable n ( factorial (suc m) ) | |
130 fact< zero 1 0<n (s≤s (s≤s z≤n)) = record { factor = 1 ; is-factor = refl } | |
131 fact< (suc m) (suc zero) 0<n n<m = record { factor = factorial (suc (suc m)) ; is-factor = begin | |
204 | 132 factorial (suc (suc m)) * 1 + 0 ≡⟨ +-comm _ 0 ⟩ |
133 factorial (suc (suc m)) * 1 ≡⟨ m*1=m ⟩ | |
134 (suc (suc m)) * factorial (suc m) ≡⟨ refl ⟩ | |
135 factorial (suc (suc m)) ∎ } where open ≡-Reasoning | |
252 | 136 fact< (suc m) (suc (suc n)) 0<n n<m with <-cmp (suc (suc n)) (suc (suc m)) |
137 ... | tri< a ¬b ¬c = record { factor = suc (suc m) * Dividable.factor fact1 ; is-factor = fact2 } where | |
203
f1ee71c7c93a
another method on fact<
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
202
diff
changeset
|
138 fact1 : Dividable (suc (suc n)) (factorial (suc m )) |
f1ee71c7c93a
another method on fact<
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
202
diff
changeset
|
139 fact1 = fact< m (suc (suc n)) 0<n a |
204 | 140 d = (fact< m (suc (suc n)) 0<n a) |
141 fact2 : suc (suc m) * Dividable.factor d * suc (suc n) + 0 ≡ factorial (suc (suc m)) | |
142 fact2 = begin | |
143 suc (suc m) * Dividable.factor d * suc (suc n) + 0 ≡⟨ +-comm _ 0 ⟩ | |
144 suc (suc m) * Dividable.factor d * suc (suc n) ≡⟨ *-assoc (suc (suc m)) (Dividable.factor d) ( suc (suc n)) ⟩ | |
145 suc (suc m) * (Dividable.factor d * suc (suc n)) ≡⟨ cong (λ k → suc (suc m) * k ) ( +-comm 0 (Dividable.factor d * suc (suc n)) ) ⟩ | |
146 suc (suc m) * (Dividable.factor d * suc (suc n) + 0) ≡⟨ cong (λ k → suc (suc m) * k ) (Dividable.is-factor d) ⟩ | |
147 suc (suc m) * factorial (suc m) ≡⟨ refl ⟩ | |
148 factorial (suc (suc m)) ∎ where open ≡-Reasoning | |
252 | 149 ... | tri≈ ¬a b ¬c = record { factor = factorial (suc m) ; is-factor = begin |
204 | 150 factorial (suc m) * suc (suc n) + 0 ≡⟨ +-comm _ 0 ⟩ |
151 factorial (suc m) * suc (suc n) ≡⟨ *-comm (factorial (suc m)) (suc (suc n)) ⟩ | |
152 (suc (suc n)) * factorial (suc m) ≡⟨ cong (λ k → k * factorial (suc m) ) b ⟩ | |
153 (suc (suc m)) * factorial (suc m) ≡⟨ refl ⟩ | |
154 factorial (suc (suc m)) ∎ } where open ≡-Reasoning | |
252 | 155 ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c n<m) |
156 | |
157 f>m : {m : ℕ} → suc m < suc (factorial (suc m)) | |
158 f>m {m} = begin | |
159 suc (suc m) ≡⟨ cong (λ k → 1 + suc k ) (+-comm _ m) ⟩ | |
160 suc (1 + 1 * m) ≡⟨ cong (λ k → suc (1 + k )) (*-comm 1 m) ⟩ | |
161 suc (1 + m * 1) ≤⟨ s≤s (s≤s (*-monoʳ-≤ m (factorial≥1 {m}) )) ⟩ | |
162 suc (1 + m * factorial m) ≤⟨ s≤s (+-monoˡ-≤ _ (factorial≥1 {m})) ⟩ | |
163 suc (factorial m + m * factorial m) ≡⟨ refl ⟩ | |
164 suc (factorial (suc m)) ∎ where open ≤-Reasoning | |
165 | |
166 prime-is-infinite : (max-prime : ℕ ) → ¬ ( (j : ℕ) → max-prime < j → ¬ Prime j ) | |
167 prime-is-infinite zero pmax = pmax 3 (s≤s z≤n) record { isPrime = λ n lt 0<j → pif3 n lt 0<j ; p>1 = s≤s (s≤s z≤n) } where | |
168 pif3 : (n : ℕ) → n < 3 → 0 < n → gcd 3 n ≡ 1 | |
169 pif3 .1 (s≤s (s≤s z≤n)) _ = refl | |
170 pif3 .2 (s≤s (s≤s (s≤s z≤n))) _ = refl | |
171 prime-is-infinite (suc m) pmax = newPrime where | |
172 prime<max : (n : ℕ ) → Prime n → n < suc (suc m) | |
173 prime<max n p with <-cmp n (suc m) | |
174 ... | tri< a ¬b ¬c = ≤-trans a refl-≤s | |
175 ... | tri≈ ¬a refl ¬c = ≤-refl | |
176 ... | tri> ¬a ¬b c = ⊥-elim ( pmax n c p ) | |
199 | 177 fact : (n : ℕ) → Prime n → Dividable n ( factorial (suc m) ) |
205 | 178 fact n p = fact< m n (<-trans (s≤s z≤n) (Prime.p>1 p)) ( prime<max n p ) |
199 | 179 -- div+1 : { i k : ℕ } → k > 1 → Dividable k i → ¬ Dividable k (suc i) |
231 | 180 newPrime : ⊥ |
181 newPrime with PrimeP ( suc (factorial (suc m)) ) | |
182 ... | yes p = pmax _ f>m p -- yes, we found a prime not in list | |
205 | 183 ... | no np = div+1 (Prime.p>1 (NonPrime.prime p1)) (fact (NonPrime.factor p1) (NonPrime.prime p1) ) (NonPrime.dividable p1) where |
231 | 184 -- n!+1 cannot be dividable, because n! is dividable |
185 -- the factor need not be a prime, but anyway we prove that there is a prime factor in NonPrime | |
199 | 186 p1 : NonPrime ( suc (factorial (suc m)) ) |
225 | 187 p1 = nonPrime (begin |
188 2 ≤⟨ s≤s ( s≤s z≤n) ⟩ | |
189 suc (suc m) ≤⟨ s≤s (m<factorial (suc m)) ⟩ | |
190 suc (factorial (suc m)) ∎ ) np where open ≤-Reasoning |