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