Mercurial > hg > Members > kono > Proof > automaton
annotate automaton-in-agda/src/prime.agda @ 294:248711134141
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 29 Dec 2021 19:08:28 +0900 |
| parents | 4e4e148eb7e5 |
| children | a3fb231feeb9 |
| 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 |
| 255 | 51 -- find prime factor |
| 52 | |
| 229 | 53 data Factoring (m : ℕ ) : (n : ℕ) → Set where |
| 230 | 54 findFactor : (n : ℕ) → m ≤ n → ( (j : ℕ ) → m ≤ j → j < n → gcd n j ≡ 1 ) → Factoring m n |
| 229 | 55 skipFactor : (n : ℕ) → n < m → Factoring m n |
| 226 | 56 |
| 205 | 57 nonPrime : { n : ℕ } → 1 < n → ¬ Prime n → NonPrime n |
| 230 | 58 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 | 59 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 |
| 60 mg1 n m mg gcd j m<j j<n with <-cmp m j | |
| 228 | 61 ... | tri< a ¬b ¬c = mg j a j<n |
| 225 | 62 ... | tri≈ ¬a refl ¬c = gcd |
| 228 | 63 ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> m<j c) |
| 229 | 64 np1 : ( n m : ℕ ) → ¬ Prime n → 1 < n → Factoring m n → NonPrime n |
| 230 | 65 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 |
| 66 np1 n (suc m) np 1<n (findFactor n m≤n mg) with <-cmp ( gcd n m ) 1 | |
| 228 | 67 ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> ( gcd>0 n m (<-trans (s≤s z≤n) 1<n) 0<m ) a ) where |
| 68 0<m : 0 < m | |
| 69 0<m with <-cmp 0 m | |
| 70 ... | tri< a ¬b ¬c = a | |
| 71 ... | tri≈ ¬a refl ¬c = ⊥-elim ( nat-<> a (subst (λ k → 1 < k) (sym (gcd20 n)) 1<n )) | |
| 230 | 72 ... | tri≈ ¬a b ¬c = np1 n m np 1<n (findFactor n (≤-trans refl-≤s m≤n) (mg1 n m mg b ) ) |
| 228 | 73 ... | tri> ¬a ¬b c with PrimeP ( gcd n m ) |
| 74 ... | yes y = record { factor = gcd n m ; prime = y ; dividable = proj1 (gcd-dividable n m ) } | |
| 230 | 75 ... | no ngcd = np2 where |
| 76 skip-case : NonPrime (gcd n m) → NonPrime n | |
| 77 skip-case cc = record { factor = NonPrime.factor cc ; prime = NonPrime.prime cc ; dividable = | |
| 229 | 78 record { factor = (Dividable.factor (proj1 (gcd-dividable n m))) * (Dividable.factor (NonPrime.dividable cc)) |
| 230 | 79 ; is-factor = begin |
| 80 Dividable.factor (proj1 (gcd-dividable n m)) * Dividable.factor (NonPrime.dividable cc) * NonPrime.factor cc + 0 ≡⟨ refl ⟩ | |
| 81 g * d * p + 0 ≡⟨ +-comm _ 0 ⟩ | |
| 82 g * d * p ≡⟨ *-assoc g d p ⟩ | |
| 83 g * (d * p) ≡⟨ cong (λ k → g * k ) (+-comm 0 _) ⟩ | |
| 84 g * (d * p + 0) ≡⟨ cong (λ k → g * k ) (Dividable.is-factor (NonPrime.dividable cc) ) ⟩ | |
| 85 g * gcd n m ≡⟨ +-comm 0 _ ⟩ | |
| 86 g * gcd n m + 0 ≡⟨ Dividable.is-factor (proj1 (gcd-dividable n m)) ⟩ | |
| 87 n ∎ }} where | |
| 88 open ≡-Reasoning | |
| 89 g = Dividable.factor (proj1 (gcd-dividable n m)) | |
| 90 d = Dividable.factor (NonPrime.dividable cc) | |
| 91 p = NonPrime.factor cc | |
| 92 np2 : NonPrime n | |
| 93 np2 with <-cmp (gcd n m) m | |
| 94 ... | tri< a ¬b ¬c = skip-case (np1 (gcd n m) m ngcd c (skipFactor (gcd n m) a )) | |
| 95 ... | tri≈ ¬a b ¬c = skip-case (np1 (gcd n m) m ngcd c | |
| 96 (subst (λ k → Factoring m k) (sym b) (findFactor m ≤-refl (λ j n≤j j<n → ⊥-elim (nat-≤> n≤j j<n) )))) | |
| 97 ... | tri> ¬a ¬b' c with <-cmp 0 m | |
| 250 | 98 ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> (subst (λ k → k ≤ m) (gcdsym {m} {n}) (gcd-≤ a (<-trans a m≤n))) c ) |
| 230 | 99 ... | 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 | 100 np1 n zero np 1<n (skipFactor n ()) |
| 101 np1 n (suc m) np 1<n (skipFactor n n<m) with <-cmp m n | |
| 102 ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> a n<m) | |
| 230 | 103 ... | tri> ¬a ¬b c = np1 n m np 1<n (skipFactor n c) |
| 104 ... | 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 | 105 |
| 252 | 106 factorial : (n : ℕ) → ℕ |
| 107 factorial zero = 1 | |
| 108 factorial (suc n) = (suc n) * (factorial n) | |
| 109 factorial-mono : (n : ℕ) → factorial n ≤ factorial (suc n) | |
| 110 factorial-mono n = begin | |
| 200 | 111 factorial n ≤⟨ x≤x+y ⟩ |
| 112 factorial n + n * factorial n ≡⟨ refl ⟩ | |
| 113 (suc n) * factorial n ≡⟨ refl ⟩ | |
| 114 factorial (suc n) ∎ where open ≤-Reasoning | |
| 252 | 115 factorial≥1 : {m : ℕ} → 1 ≤ factorial m |
| 116 factorial≥1 {zero} = ≤-refl | |
| 117 factorial≥1 {suc m} = begin | |
| 200 | 118 1 ≤⟨ s≤s z≤n ⟩ |
| 119 (suc m) * 1 ≤⟨ *-monoʳ-≤ (suc m) (factorial≥1 {m}) ⟩ | |
| 120 (suc m) * factorial m ≡⟨ refl ⟩ | |
| 121 factorial (suc m) ∎ where open ≤-Reasoning | |
| 252 | 122 m<factorial : (m : ℕ) → m ≤ factorial m |
| 123 m<factorial zero = z≤n | |
| 124 m<factorial (suc m) = begin | |
| 200 | 125 suc m ≡⟨ cong suc (+-comm 0 _) ⟩ |
| 126 1 * suc m ≡⟨ *-comm 1 _ ⟩ | |
| 127 (suc m) * 1 ≤⟨ *-monoʳ-≤ (suc m) (factorial≥1 {m}) ⟩ | |
| 128 (suc m) * factorial m ≡⟨ refl ⟩ | |
| 129 factorial (suc m) ∎ where open ≤-Reasoning | |
| 252 | 130 -- *-monoˡ-≤ (suc m) {!!} |
| 131 fact< : (m n : ℕ) → 0 < n → n < suc (suc m) → Dividable n ( factorial (suc m) ) | |
| 132 fact< zero 1 0<n (s≤s (s≤s z≤n)) = record { factor = 1 ; is-factor = refl } | |
| 133 fact< (suc m) (suc zero) 0<n n<m = record { factor = factorial (suc (suc m)) ; is-factor = begin | |
| 204 | 134 factorial (suc (suc m)) * 1 + 0 ≡⟨ +-comm _ 0 ⟩ |
| 135 factorial (suc (suc m)) * 1 ≡⟨ m*1=m ⟩ | |
| 136 (suc (suc m)) * factorial (suc m) ≡⟨ refl ⟩ | |
| 137 factorial (suc (suc m)) ∎ } where open ≡-Reasoning | |
| 252 | 138 fact< (suc m) (suc (suc n)) 0<n n<m with <-cmp (suc (suc n)) (suc (suc m)) |
| 139 ... | 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
|
140 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
|
141 fact1 = fact< m (suc (suc n)) 0<n a |
| 204 | 142 d = (fact< m (suc (suc n)) 0<n a) |
| 143 fact2 : suc (suc m) * Dividable.factor d * suc (suc n) + 0 ≡ factorial (suc (suc m)) | |
| 144 fact2 = begin | |
| 145 suc (suc m) * Dividable.factor d * suc (suc n) + 0 ≡⟨ +-comm _ 0 ⟩ | |
| 146 suc (suc m) * Dividable.factor d * suc (suc n) ≡⟨ *-assoc (suc (suc m)) (Dividable.factor d) ( suc (suc n)) ⟩ | |
| 147 suc (suc m) * (Dividable.factor d * suc (suc n)) ≡⟨ cong (λ k → suc (suc m) * k ) ( +-comm 0 (Dividable.factor d * suc (suc n)) ) ⟩ | |
| 148 suc (suc m) * (Dividable.factor d * suc (suc n) + 0) ≡⟨ cong (λ k → suc (suc m) * k ) (Dividable.is-factor d) ⟩ | |
| 149 suc (suc m) * factorial (suc m) ≡⟨ refl ⟩ | |
| 150 factorial (suc (suc m)) ∎ where open ≡-Reasoning | |
| 252 | 151 ... | tri≈ ¬a b ¬c = record { factor = factorial (suc m) ; is-factor = begin |
| 204 | 152 factorial (suc m) * suc (suc n) + 0 ≡⟨ +-comm _ 0 ⟩ |
| 153 factorial (suc m) * suc (suc n) ≡⟨ *-comm (factorial (suc m)) (suc (suc n)) ⟩ | |
| 154 (suc (suc n)) * factorial (suc m) ≡⟨ cong (λ k → k * factorial (suc m) ) b ⟩ | |
| 155 (suc (suc m)) * factorial (suc m) ≡⟨ refl ⟩ | |
| 156 factorial (suc (suc m)) ∎ } where open ≡-Reasoning | |
| 252 | 157 ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c n<m) |
| 158 | |
| 159 f>m : {m : ℕ} → suc m < suc (factorial (suc m)) | |
| 160 f>m {m} = begin | |
| 161 suc (suc m) ≡⟨ cong (λ k → 1 + suc k ) (+-comm _ m) ⟩ | |
| 162 suc (1 + 1 * m) ≡⟨ cong (λ k → suc (1 + k )) (*-comm 1 m) ⟩ | |
| 163 suc (1 + m * 1) ≤⟨ s≤s (s≤s (*-monoʳ-≤ m (factorial≥1 {m}) )) ⟩ | |
| 164 suc (1 + m * factorial m) ≤⟨ s≤s (+-monoˡ-≤ _ (factorial≥1 {m})) ⟩ | |
| 165 suc (factorial m + m * factorial m) ≡⟨ refl ⟩ | |
| 166 suc (factorial (suc m)) ∎ where open ≤-Reasoning | |
| 167 | |
| 168 prime-is-infinite : (max-prime : ℕ ) → ¬ ( (j : ℕ) → max-prime < j → ¬ Prime j ) | |
| 169 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 | |
| 170 pif3 : (n : ℕ) → n < 3 → 0 < n → gcd 3 n ≡ 1 | |
| 171 pif3 .1 (s≤s (s≤s z≤n)) _ = refl | |
| 172 pif3 .2 (s≤s (s≤s (s≤s z≤n))) _ = refl | |
| 173 prime-is-infinite (suc m) pmax = newPrime where | |
| 174 prime<max : (n : ℕ ) → Prime n → n < suc (suc m) | |
| 175 prime<max n p with <-cmp n (suc m) | |
| 176 ... | tri< a ¬b ¬c = ≤-trans a refl-≤s | |
| 177 ... | tri≈ ¬a refl ¬c = ≤-refl | |
| 178 ... | tri> ¬a ¬b c = ⊥-elim ( pmax n c p ) | |
| 199 | 179 fact : (n : ℕ) → Prime n → Dividable n ( factorial (suc m) ) |
| 205 | 180 fact n p = fact< m n (<-trans (s≤s z≤n) (Prime.p>1 p)) ( prime<max n p ) |
| 199 | 181 -- div+1 : { i k : ℕ } → k > 1 → Dividable k i → ¬ Dividable k (suc i) |
| 231 | 182 newPrime : ⊥ |
| 183 newPrime with PrimeP ( suc (factorial (suc m)) ) | |
| 184 ... | yes p = pmax _ f>m p -- yes, we found a prime not in list | |
| 205 | 185 ... | no np = div+1 (Prime.p>1 (NonPrime.prime p1)) (fact (NonPrime.factor p1) (NonPrime.prime p1) ) (NonPrime.dividable p1) where |
| 231 | 186 -- n!+1 cannot be dividable, because n! is dividable |
| 187 -- the factor need not be a prime, but anyway we prove that there is a prime factor in NonPrime | |
| 199 | 188 p1 : NonPrime ( suc (factorial (suc m)) ) |
| 225 | 189 p1 = nonPrime (begin |
| 190 2 ≤⟨ s≤s ( s≤s z≤n) ⟩ | |
| 191 suc (suc m) ≤⟨ s≤s (m<factorial (suc m)) ⟩ | |
| 192 suc (factorial (suc m)) ∎ ) np where open ≤-Reasoning |