Mercurial > hg > Members > kono > Proof > automaton

changeset 171:70beed7c4e30

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 13 Mar 2021 17:33:26 +0900
parents 6cd9d874cc55
children 684f53fb9b2c
files agda/prime.agda
diffstat 1 files changed, 17 insertions(+), 11 deletions(-) [+]
line wrap: on
line diff
--- a/agda/prime.agda	Sat Mar 13 15:20:54 2021 +0900
+++ b/agda/prime.agda	Sat Mar 13 17:33:26 2021 +0900
@@ -20,6 +20,7 @@
 record NonPrime ( n : ℕ ) : Set where
    field
       factor : ℕ
+      prime : Prime factor
       dividable : Dividable factor n
 
 nonPrime : ( n : ℕ ) → ¬ Prime n → NonPrime n
@@ -29,7 +30,7 @@
     np1 (suc m) mg with <-cmp ( gcd n (suc m) ) 1
     ... | tri< a ¬b ¬c = {!!}
     ... | tri≈ ¬a b ¬c = np1 m {!!}
-    ... | tri> ¬a ¬b c = record { factor = gcd n (suc m) ; dividable = record { factor = {!!} ; is-factor = {!!} } }
+    ... | tri> ¬a ¬b c = record { factor = gcd n (suc m) ; prime = {!!} ; dividable = record { factor = {!!} ; is-factor = {!!} } }
 
 prime-is-infinite : (max-prime : ℕ ) → ¬ ( (j : ℕ) → max-prime < j → ¬ Prime j ) 
 prime-is-infinite zero pmax = pmax 1 {!!} record { isPrime = λ n lt → {!!} }
@@ -42,13 +43,18 @@
   factm : (n m : ℕ ) → n < (suc m) →  Dividable n (factorial m )
   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 {!!}) ⟩
-     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 :  NonPrime (factorial (suc m ))
-       d with <-cmp n (suc m)
-       ... | 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 {!!} {!!} 
+  fact n lt = fact12  (nonPrime (factorial (suc m )) ( pmax (factorial (suc m )) ? )) where
+       fact10 : Dividable n (factorial (suc m)) → gcd (suc (factorial (suc m))) n ≡ 1
+       fact10 d = begin
+            gcd (suc (factorial (suc m))) n ≡⟨ cong (λ k → gcd (suc k) n) (sym (Dividable.is-factor d )) ⟩
+            gcd (suc (Dividable.factor d * n + 0))   n   ≡⟨ cong (λ k → gcd ( k + 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 ∎  
+       fact12 : NonPrime (factorial (suc m)) → gcd (suc (factorial (suc m))) n ≡ 1
+       fact12 np = {!!}
+       fact11 : gcd (suc (factorial (suc m))) n ≡ 1
+       fact11 with <-cmp n (suc m)
+       ... | tri< a ¬b ¬c = fact10 ( factm n (suc m) {!!} ) 
+       ... | tri≈ ¬a b ¬c = fact10 ( factm n (suc m) {!!} ) 
+       ... | tri> ¬a ¬b c = fact12 (nonPrime (factorial (suc m )) ( pmax (factorial (suc m )) {!!} ))