Mercurial > hg > Members > kono > Proof > automaton

changeset 228:b21027d1d4a9

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 Wed, 23 Jun 2021 22:35:04 +0900
parents a61f121c34a4
children fb080920c104
files automaton-in-agda/src/prime.agda
diffstat 1 files changed, 31 insertions(+), 15 deletions(-) [+]
line wrap: on
line diff
--- a/automaton-in-agda/src/prime.agda	Wed Jun 23 18:10:18 2021 +0900
+++ b/automaton-in-agda/src/prime.agda	Wed Jun 23 22:35:04 2021 +0900
@@ -56,8 +56,8 @@
 open Pair≤
 
 nonPrime1 : { n : ℕ } → 1 < n → ¬ Prime n → NonPrime n
-nonPrime1 {n} 1<n np = f-induction {_} {_} {Pair≤} {λ op → G (ox op) (oy op) → NonPrime n } (λ op → oy op - ox op ) I
-         record { ox = n ; oy = n ; ox<oy = ≤-refl } {!!} where
+nonPrime1 {n} 1<n np = n-induction {_} {_} {Pair≤} {λ op → G (ox op) (oy op) → NonPrime n } (λ op → oy op ) I
+         record { ox = n ; oy = n ; ox<oy = ≤-refl } record { 1<p = 1<n ; div = div=  ; npr = λ _ → np ; is-g = is-g= refl } where
     record G (p g : ℕ) : Set where
       field
         1<p : 1 < p 
@@ -67,7 +67,13 @@
     is-g= : {g p : ℕ} → g ≡ p →  (j : ℕ) → g ≤ j → j < p → gcd p j ≡ 1
     is-g= eq _ g≤j j<p = ⊥-elim ( nat-≡< eq (≤-trans (s≤s g≤j ) j<p))
     next : Pair≤ → Pair≤
-    next record { ox = ox ; oy = oy ; ox<oy = ox<oy } = record { ox = ox ; oy = gcd oy ox ; ox<oy = {!!} } 
+    next record { ox = ox ; oy = oy ; ox<oy = ox≤oy } with <-cmp ox oy
+    ... | tri≈ ¬a b ¬c = record { ox = 0 ; oy = 0 ; ox<oy = ≤-refl  }
+    ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> ox≤oy c )
+    ... | tri< a ¬b ¬c with <-cmp ox (gcd ox oy)
+    ... | tri< ox<g ¬b' ¬c' = record { ox = ox ; oy = gcd ox oy  ; ox<oy = <to≤ ox<g }
+    ... | tri≈ ¬a b ¬c' = record { ox = ox ; oy = ox ; ox<oy = ≤-refl  }
+    ... | tri> ¬a ¬b' c = record { ox = gcd ox oy ; oy = ox ; ox<oy = <to≤ c }
     ind : {p : Pair≤ } → (G (ox (next p)) (oy (next p)) → NonPrime n) → G (ox p) (oy p) → NonPrime n
     ind {p} prev g = {!!} where
       next1  : ( m : ℕ ) →  ℕ  → {!!} → {!!} -- G.g g ≡ m  → G 
@@ -77,11 +83,17 @@
       next1  (suc m) (suc (suc f)) _ with PrimeP (suc (suc f))
       ... | yes p = {!!} -- record { p = suc (suc f) ; g = 0 ; 1<p = Prime.p>1 p ; div = {!!} ; npr = λ () ; is-g = {!!} }
       ... | no np = {!!} -- record { p = suc (suc f) ; g = suc (suc f)  ; 1<p = s≤s (s≤s z≤n) ; div = {!!} ; npr = λ lt → np ; is-g = is-g= refl }
-    pzero : (p : Pair≤ ) →  (oy p - ox p) ≡ zero → G (ox p) (oy p) → NonPrime n
+    pzero : (p : Pair≤ ) →  oy (next p)  ≡ zero → G (ox p) (oy p) → NonPrime n
     pzero p eq g = record { factor = {!!} ; prime = record { p>1 = G.1<p g ; isPrime = {!!} } ;  dividable = G.div g }
-    decline : (p : Pair≤ ) → 0 < (oy p - ox p) → (oy (next p) - ox (next p)) < (oy p - ox p)
-    decline = {!!}
-    I : Finduction Pair≤  _  (λ op → oy op - ox op )
+    decline : (p : Pair≤ ) → 0 < oy p → oy (next p)  < oy p
+    decline record { ox = ox ; oy = oy ; ox<oy = ox≤oy } 0<y with <-cmp ox oy
+    ... | tri≈ ¬a refl ¬c = 0<y
+    ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> ox≤oy c )
+    ... | tri< a ¬b ¬c with <-cmp ox (gcd ox oy)
+    ... | tri< ox<g ¬b' ¬c' = gcd-< ox oy {!!} a -- 0< ox , ox < oy
+    ... | tri≈ ¬a b' ¬c' = {!!} --  ¬ ox=oy ( → gcd ox oy ≡ 0 > ox )
+    ... | tri> ¬a ¬b' c = {!!} -- ¬ ox=oy ( → gcd ox oy ≡ 0 > ox )
+    I : Ninduction Pair≤  _  (λ op → oy op  )
     I = record {
               pnext = next
             ; fzero = λ {p} → pzero p
@@ -92,18 +104,22 @@
 
 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
-    mg1 :  (m : ℕ )→ ( (j : ℕ ) → suc m ≤ j → j < n → gcd n j ≡ 1  ) →  gcd n (suc m) ≡ 1 → (j : ℕ) → m ≤ j → j < n → gcd n j ≡ 1
-    mg1 m mg gcd j m<j j<n with <-cmp j (suc m)
-    ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> (≤-trans {!!} m<j) a)
+    mg1 :  (m : ℕ )→ ( (j : ℕ ) → m < j → j < n → gcd n j ≡ 1  ) →  gcd n m ≡ 1 → (j : ℕ) → m ≤ j → j < n → gcd n j ≡ 1
+    mg1 m mg gcd j m<j j<n with <-cmp m j
+    ... | tri< a ¬b ¬c = mg j a j<n  
     ... | tri≈ ¬a refl ¬c = gcd
-    ... | tri> ¬a ¬b c = mg j {!!} j<n
+    ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> m<j c)
     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>1 = 1<n } ) -- zero < j , j < n
-    np1 (suc m) mg with <-cmp ( gcd n (suc m) ) 1
-    ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> ( gcd>0 n (suc m) (<-trans (s≤s z≤n) 1<n) (s≤s z≤n)) a )
+    np1 (suc m) mg with <-cmp ( gcd n m ) 1
+    ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> ( gcd>0 n m (<-trans (s≤s z≤n) 1<n) 0<m ) a ) where
+         0<m : 0 < m
+         0<m with <-cmp 0 m
+         ... | tri< a ¬b ¬c = a
+         ... | tri≈ ¬a refl ¬c = ⊥-elim ( nat-<> a (subst (λ k → 1 < k) (sym (gcd20 n)) 1<n ))
     ... | tri≈ ¬a b ¬c = np1 m (mg1 m mg b )
-    ... | tri> ¬a ¬b c with PrimeP ( gcd n (suc m) )
-    ... | yes y = record { factor = gcd n (suc m) ; prime = y ;  dividable = proj1 (gcd-divable n (suc m) ) }
+    ... | tri> ¬a ¬b c with PrimeP ( gcd n m )
+    ... | yes y = record { factor = gcd n m ; prime = y ;  dividable = proj1 (gcd-dividable n m ) }
     ... | no ngcd = np1 m (mg1 m mg {!!} )