Mercurial > hg > Members > kono > Proof > automaton

changeset 205:e97cf4fb67fa

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 Fri, 18 Jun 2021 21:09:50 +0900
parents a366f36b1ce9
children f1370437c68e
files automaton-in-agda/src/gcd.agda automaton-in-agda/src/prime.agda
diffstat 2 files changed, 55 insertions(+), 25 deletions(-) [+]
line wrap: on
line diff
--- a/automaton-in-agda/src/gcd.agda	Fri Jun 18 19:21:06 2021 +0900
+++ b/automaton-in-agda/src/gcd.agda	Fri Jun 18 21:09:50 2021 +0900
@@ -39,12 +39,6 @@
 decf : { n k : ℕ } → ( x : Factor k (suc n) ) → Factor k n
 decf {n} {k} record { factor = f ; remain = r ; is-factor = fa } = 
  decf1 {n} {k} f r fa where
-  dr : ( n k : ℕ ) → (f r : ℕ) → ℕ
-  dr n zero (suc f) zero = 0
-  dr n (suc k) (suc f) zero = k
-  dr n k f (suc r) = r
-  dr n zero zero zero = r
-  dr n (suc k) zero zero = r
   decf1 : { n k : ℕ } → (f r : ℕ) → (f * k + r ≡ suc n)  → Factor k n 
   decf1 {n} {k} f (suc r) fa  =  -- this case must be the first
      record { factor = f ; remain = r ; is-factor = ( begin -- fa : f * k + suc r ≡ suc n
@@ -288,3 +282,28 @@
 div+1 {i} {k} k>1 d d1 = div1 k>1 div+11 where
    div+11 : Dividable k 1
    div+11 = subst (λ g → Dividable k g) (minus+y-y {1} {i} ) ( proj2 (div-div k>1 d d1  ) )
+
+gcd>0 : ( i j : ℕ ) → 0 < i → 0 < j → 0 < gcd i j  
+gcd>0 i j 0<i 0<j = gcd>01 i i j j 0<i 0<j where
+     gcd>01 : ( i i0 j j0 : ℕ ) → 0 < i0 → 0 < j0  → gcd1 i i0 j j0 > 0
+     gcd>01 zero i0 zero j0 0<i 0<j with <-cmp i0 j0
+     ... | tri< a ¬b ¬c = 0<i
+     ... | tri≈ ¬a refl ¬c = 0<i
+     ... | tri> ¬a ¬b c = 0<j
+     gcd>01 zero i0 (suc zero) j0 0<i 0<j = s≤s z≤n
+     gcd>01 zero zero (suc (suc j)) j0 0<i 0<j = 0<j 
+     gcd>01 zero (suc i0) (suc (suc j)) j0 0<i 0<j = gcd>01 i0 (suc i0) (suc j) (suc (suc j)) 0<i (s≤s z≤n) -- 0 < suc (suc j)
+     gcd>01 (suc zero) i0 zero j0 0<i 0<j =  s≤s z≤n
+     gcd>01 (suc (suc i)) i0 zero zero 0<i 0<j = 0<i 
+     gcd>01 (suc (suc i)) i0 zero (suc j0) 0<i 0<j = gcd>01 (suc i) (suc (suc i))  j0 (suc j0) (s≤s z≤n) 0<j 
+     gcd>01 (suc i) i0 (suc j) j0 0<i 0<j = subst (λ k → 0 < k ) (sym (gcd033 i i0 j j0 )) (gcd>01 i i0 j j0 0<i 0<j ) where
+         gcd033 : (i i0 j j0  : ℕ) → gcd1 (suc i) i0 (suc j) j0 ≡  gcd1 i i0 j j0
+         gcd033 zero zero zero zero = refl
+         gcd033 zero zero (suc j) zero = refl
+         gcd033 (suc i) zero j zero = refl
+         gcd033 zero zero zero (suc j0) = refl
+         gcd033 (suc i) zero zero (suc j0) = refl
+         gcd033 zero zero (suc j) (suc j0) = refl
+         gcd033 (suc i) zero (suc j) (suc j0) = refl
+         gcd033 zero (suc i0) j j0 = refl
+         gcd033 (suc i) (suc i0) j j0 = refl
--- a/automaton-in-agda/src/prime.agda	Fri Jun 18 19:21:06 2021 +0900
+++ b/automaton-in-agda/src/prime.agda	Fri Jun 18 21:09:50 2021 +0900
@@ -13,8 +13,8 @@
 
 record Prime (i : ℕ ) : Set where
    field
-      p>0 : i > 1
-      isPrime : ( j : ℕ ) → j < i → gcd i j ≡ 1
+      p>1 : i > 1
+      isPrime : ( j : ℕ ) → j < i → 0 < j → gcd i j ≡ 1
 
 
 record NonPrime ( n : ℕ ) : Set where
@@ -24,28 +24,39 @@
       dividable : Dividable factor n
 
 PrimeP : ( n : ℕ ) → Dec ( Prime n )
-PrimeP 0 = no (λ p → ⊥-elim ( nat-<> (Prime.p>0 p) (s≤s z≤n))) 
-PrimeP 1 = no (λ p → ⊥-elim ( nat-≤> (Prime.p>0 p) (s≤s (≤-refl))))
-PrimeP (suc n) = isPrime1 (suc n) n a<sa (λ i m<i i<n → {!!} ) where
-   isPrime1 : ( n m : ℕ ) → m < n → ( (i : ℕ) → m ≤ i → i < n  →  gcd n i ≡ 1 )  → Dec ( Prime n )
-   isPrime1 n zero m<n lt = yes record { isPrime = λ j j<i → lt j z≤n {!!} ; p>0 = {!!} }
-   isPrime1 n (suc m) m<n lt with <-cmp (gcd n (suc m)) 1
-   ... | tri< a ¬b ¬c = {!!}
-   ... | tri≈ ¬a b ¬c = isPrime1 n m {!!} {!!}
-   ... | tri> ¬a ¬b c = no ( λ p → nat-≡< (sym (Prime.isPrime p (suc m) {!!} )) c )
+PrimeP 0 = no (λ p → ⊥-elim ( nat-<> (Prime.p>1 p) (s≤s z≤n))) 
+PrimeP 1 = no (λ p → ⊥-elim ( nat-≤> (Prime.p>1 p) (s≤s (≤-refl))))
+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 m<i i<n ) where
+   isp0 : (n : ℕ) (i : ℕ) ( n<i : n ≤ i) ( i<n : i < suc n ) →  gcd (suc n) i ≡ 1
+   isp0  n i n<i i<n with <-cmp i n
+   ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> n<i a) 
+   ... | tri≈ ¬a refl ¬c = gcd203 i
+   ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c i<n )
+   isPrime1 : ( n m : ℕ ) → n > 1 → m < n → ( (i : ℕ) → m ≤ i → i < n  →  gcd n i ≡ 1 )  → Dec ( Prime n )
+   isPrime1 n zero n>1 m<n lt = yes record { isPrime = λ j j<i 0<j → lt j z≤n j<i ; p>1 = n>1 } 
+   isPrime1 n (suc m) n>1 m<n lt with <-cmp (gcd n (suc m)) 1
+   ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> ( gcd>0 n (suc m) (<-trans (s≤s z≤n) n>1) (s≤s z≤n)) a )
+   ... | tri≈ ¬a b ¬c = isPrime1 n m n>1 (<-trans a<sa m<n) isp1 where
+    --   (i : ℕ) → suc m ≤ i → suc i ≤ n → gcd1 n n i i ≡ 1
+        isp1 :  (i : ℕ) → m ≤ i → i < n → gcd n i ≡ 1
+        isp1 = {!!}
+   ... | tri> ¬a ¬b c = no ( λ p → nat-≡< (sym (Prime.isPrime p (suc m) m<n (s≤s z≤n) )) c )
 
-nonPrime : { n : ℕ } → ¬ Prime n → NonPrime n
-nonPrime {n} np = np1 n (λ j n≤j j<n → ⊥-elim (nat-≤>  n≤j j<n ) ) where
+nonPrime : { n : ℕ } → 1 < n → ¬ Prime n → NonPrime n
+nonPrime {n} 1<n np = np1 n (λ j n≤j j<n → ⊥-elim (nat-≤>  n≤j j<n ) ) where
     np1 : ( m : ℕ ) → ( (j : ℕ ) → m ≤ j → j < n → gcd n j ≡ 1  ) → NonPrime n
-    np1 zero mg = ⊥-elim ( np record { isPrime = λ j lt → mg j z≤n lt ; p>0 = {!!} } ) -- zero < j , j < n
+    np1 zero mg = ⊥-elim ( np record { isPrime = λ j lt _ → mg j z≤n lt ; p>1 = 1<n } ) -- zero < j , j < n
     np1 (suc m) mg with <-cmp ( gcd n (suc m) ) 1
-    ... | tri< a ¬b ¬c = {!!}
+    ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> ( gcd>0 n (suc m) (<-trans (s≤s z≤n) 1<n) (s≤s z≤n)) a )
     ... | tri≈ ¬a b ¬c = np1 m {!!}
     ... | 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 3 (s≤s z≤n) record { isPrime = λ n lt → {!!} ; p>0 = {!!} }
+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
+  pif3 : (n : ℕ) →  n < 3 →  0 < n → gcd 3 n ≡ 1
+  pif3 .1 (s≤s (s≤s z≤n)) _ = refl
+  pif3 .2 (s≤s (s≤s (s≤s z≤n))) _ = refl
 prime-is-infinite (suc m) pmax = getPrime where 
   factorial : (n : ℕ) → ℕ
   factorial zero = 1
@@ -113,11 +124,11 @@
      factorial (suc (suc m))  ∎  } where open ≡-Reasoning
   ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c n<m) 
   fact : (n : ℕ) → Prime n → Dividable n ( factorial (suc m) )
-  fact n p = fact< m n (<-trans (s≤s z≤n) (Prime.p>0 p)) ( prime<max n p )
+  fact n p = fact< m n (<-trans (s≤s z≤n) (Prime.p>1 p)) ( prime<max n p )
   -- div+1 : { i k : ℕ } → k > 1 →  Dividable k i →  ¬ Dividable k (suc i)
   getPrime : ⊥
   getPrime with PrimeP ( suc (factorial (suc m)) )
   ... | yes p = pmax _ f>m p 
-  ... | no np = div+1 (Prime.p>0 (NonPrime.prime p1)) (fact (NonPrime.factor p1) (NonPrime.prime p1) ) (NonPrime.dividable p1) where
+  ... | no np = div+1 (Prime.p>1 (NonPrime.prime p1)) (fact (NonPrime.factor p1) (NonPrime.prime p1) ) (NonPrime.dividable p1) where
       p1 : NonPrime  ( suc (factorial (suc m)) )
-      p1 = nonPrime  np
+      p1 = nonPrime {!!} np