# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1624462666 -32400
# Node ID fb080920c104e3e9b748e3e8bf2c455dbf52c5a5
# Parent  b21027d1d4a9e07da5ba83fd17655e3102c15060
...

diff -r b21027d1d4a9 -r fb080920c104 automaton-in-agda/src/prime.agda
--- a/automaton-in-agda/src/prime.agda	Wed Jun 23 22:35:04 2021 +0900
+++ b/automaton-in-agda/src/prime.agda	Thu Jun 24 00:37:46 2021 +0900
@@ -48,79 +48,38 @@
 open import logic
 open _∧_
 
-record Pair≤ : Set where
-  field 
-    ox oy : ℕ
-    ox<oy : ox ≤ oy 
-
-open Pair≤
-
-nonPrime1 : { n : ℕ } → 1 < n → ¬ Prime n → NonPrime n
-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 
-        div : Dividable p n
-        npr : g > 0 → ¬ Prime p
-        is-g : (j : ℕ) → g ≤ j → j < p → gcd p j ≡ 1
-    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 } 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 
-      next1  0 _ _ = g
-      next1  _ 0  _ = g
-      next1  (suc m) 1 sm=g = {!!} --record g { g = m ;  npr = λ lt → G.npr g {!!} ; is-g = {!!} }
-      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 (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 → 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
-            ; decline = λ {p} → decline p
-            ; ind = λ {p} → ind {p}
-          }
-
+data Factoring (m : ℕ ) : (n : ℕ) → Set where
+     findFactor : (n : ℕ) → ( (j : ℕ ) → m ≤ j → j < n → gcd n j ≡ 1  ) → Factoring m n
+     skipFactor : (n : ℕ) → n < m →  Factoring m n
 
 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 : ℕ ) → 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
+nonPrime {n} 1<n np = np1 n n np 1<n (findFactor n (λ j n≤j j<n → ⊥-elim (nat-≤>  n≤j j<n ) )) where
+    mg1 :  (n m : ℕ )→ ( (j : ℕ ) → m < j → j < n → gcd n j ≡ 1  ) →  gcd n m ≡ 1 → (j : ℕ) → m ≤ j → j < n → gcd n j ≡ 1
+    mg1 n 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 = ⊥-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 m ) 1
+    np1 : ( n m : ℕ ) → ¬ Prime n → 1 < n → Factoring m n → NonPrime n
+    np1 n zero np 1<n (findFactor n  mg ) = ⊥-elim ( np record { isPrime = λ j lt _ → mg j z≤n lt ; p>1 = 1<n } ) -- zero < j , j < n
+    np1 n (suc m) np 1<n (findFactor n  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 = np1 n m np 1<n (findFactor n (mg1 n m mg b ) )
     ... | 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 {!!} )
+    ... | no ngcd with np1 (gcd n m) m ngcd c (skipFactor (gcd n m) {!!}) 
+    ... | cc = record { factor = NonPrime.factor cc ; prime = NonPrime.prime cc ; dividable =
+                          record { factor = (Dividable.factor (proj1 (gcd-dividable n m))) * (Dividable.factor (NonPrime.dividable cc))
+                              ; is-factor = {!!} } } -- cc : NonPrime (gcd n m )
+    np1 n zero np 1<n (skipFactor n ())
+    np1 n (suc m) np 1<n  (skipFactor n n<m) with <-cmp m n
+    ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> a n<m) 
+    ... | tri> ¬a ¬b c = np1 n m np 1<n  (skipFactor n c) 
+    ... | tri≈ ¬a refl ¬c with np1 n m np 1<n (findFactor m (λ j n≤j j<n → ⊥-elim (nat-≤>  n≤j j<n) ))
+    ... | np2 = np1 n m np 1<n (findFactor m (λ j n≤j j<n → ⊥-elim (nat-≤>  n≤j j<n)))
 
 
 prime-is-infinite : (max-prime : ℕ ) → ¬ ( (j : ℕ) → max-prime < j → ¬ Prime j )