Mercurial > hg > Members > kono > Proof > automaton
changeset 170:6cd9d874cc55
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 13 Mar 2021 15:20:54 +0900 |
| parents | 1c43d0713dfc |
| children | 70beed7c4e30 |
| files | agda/prime.agda |
| diffstat | 1 files changed, 7 insertions(+), 8 deletions(-) [+] |
line wrap: on
line diff
--- a/agda/prime.agda Sat Mar 13 15:12:18 2021 +0900 +++ b/agda/prime.agda Sat Mar 13 15:20:54 2021 +0900 @@ -43,13 +43,12 @@ factm = {!!} 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 ≡⟨ 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 ⟩ + gcd (suc (factorial (suc m))) n ≡⟨ cong (λ k → gcd k n) (Dividable.is-factor {!!}) ⟩ + gcd ( (NonPrime.factor d * n + 0) + 1) n ≡⟨ cong (λ k → gcd ( k + 1 ) n ) (+-comm (NonPrime.factor d * n) 0) ⟩ + gcd ( NonPrime.factor d * n + 1) n ≡⟨ gcdmul+1 (NonPrime.factor d) n ⟩ 1 ∎ where - d : Dividable n (factorial (suc m )) + d : NonPrime (factorial (suc m )) d with <-cmp n (suc m) - ... | tri< a ¬b ¬c = factm n (suc m) {!!} - ... | tri≈ ¬a b ¬c = factm n (suc m) {!!} - ... | tri> ¬a ¬b c = NonPrime.dividable (nonPrime ? ? ) + ... | tri< a ¬b ¬c = record { factor = {!!} ; dividable = factm n (suc m) {!!} } + ... | tri≈ ¬a b ¬c = record { factor = {!!} ; dividable = factm n (suc m) {!!} } + ... | tri> ¬a ¬b c = nonPrime {!!} {!!}