Mercurial > hg > Members > kono > Proof > automaton
changeset 168:c25b7de9cc35
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 13 Mar 2021 09:50:44 +0900 |
| parents | fc770d1661d4 |
| children | 1c43d0713dfc |
| files | agda/prime.agda |
| diffstat | 1 files changed, 2 insertions(+), 2 deletions(-) [+] |
line wrap: on
line diff
--- a/agda/prime.agda Sat Mar 13 09:38:30 2021 +0900 +++ b/agda/prime.agda Sat Mar 13 09:50:44 2021 +0900 @@ -18,7 +18,7 @@ open ≡-Reasoning prime-is-infinite : (max-prime : ℕ ) → ¬ ( (j : ℕ) → max-prime < j → ¬ Prime j ) -prime-is-infinite zero pmax = {!!} +prime-is-infinite zero pmax = pmax 1 {!!} record { isPrime = λ n lt → {!!} } prime-is-infinite (suc m) pmax = pmax (suc (factorial (suc m))) f>m record { isPrime = λ n lt → fact n lt } where factorial : (n : ℕ) → ℕ factorial zero = 1 @@ -30,7 +30,7 @@ fact : (n : ℕ ) → n < (suc (factorial (suc m))) → gcd (suc (factorial (suc m))) n ≡ 1 fact n lt = begin gcd (suc (factorial (suc m))) n ≡⟨ cong (λ k → gcd k n) (Dividable.is-factor d ) ⟩ - gcd ( (Dividable.factor d * n + 0) + 1) n ≡⟨ {!!} ⟩ + gcd ( (Dividable.factor d * n + 0) + 1) n ≡⟨ cong (λ k → gcd ( k + 1 ) n ) (+-comm (Dividable.factor d * n) 0) ⟩ gcd ( Dividable.factor d * n + 1) n ≡⟨ gcdmul+1 (Dividable.factor d) n ⟩ 1 ∎ where d : Dividable n (factorial (suc m ))