# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1624439418 -32400
# Node ID a61f121c34a4b0c1cf1ca7cc5b6351068e90c590
# Parent  6e8b163ca73717b10ae95a1322867bb11d7487c0
...

diff -r 6e8b163ca737 -r a61f121c34a4 automaton-in-agda/src/gcd.agda
--- a/automaton-in-agda/src/gcd.agda	Wed Jun 23 11:31:00 2021 +0900
+++ b/automaton-in-agda/src/gcd.agda	Wed Jun 23 18:10:18 2021 +0900
@@ -228,6 +228,12 @@
           k + f * k + 0 ≡⟨ eq ⟩
           m ∎  where open ≤-Reasoning  
 
+div→k≤m : { m k : ℕ } → k > 1 → m > 0 →  Dividable k m → m ≥ k
+div→k≤m {m} {k} k>1 m>0 d with <-cmp m k
+... | tri< a ¬b ¬c = ⊥-elim ( div<k k>1 m>0 a d )
+... | tri≈ ¬a refl ¬c = ≤-refl
+... | tri> ¬a ¬b c = <to≤ c
+
 div1*k+0=k : {k : ℕ } → 1 * k + 0 ≡ k
 div1*k+0=k {k} =  begin
    1 * k + 0 ≡⟨ cong (λ g → g + 0) (+-comm _ 0) ⟩
@@ -293,9 +299,9 @@
    → Dividable k ( gcd i  j ) 
 gcd-div i j k k>1 if jf = gcd-gt i i j j k k>1 (DtoF if) if (DtoF jf) jf (div-div k>1 if jf)
 
-gcd-divable : ( i j  : ℕ )
+gcd-dividable : ( i j  : ℕ )
       → Dividable ( gcd i j ) i ∧ Dividable ( gcd i j ) j
-gcd-divable i j  = f-induction {_} {_} {ℕ ∧ ℕ}
+gcd-dividable i j  = f-induction {_} {_} {ℕ ∧ ℕ}
    {λ p  → Dividable ( gcd (proj1 p) (proj2 p) ) (proj1 p) ∧ Dividable ( gcd (proj1 p)  (proj2 p) ) (proj2 p)} F I ⟪ i , j ⟫ where
         F : ℕ ∧ ℕ → ℕ
         F ⟪ 0 , 0 ⟫ = 0
@@ -490,3 +496,51 @@
          gcd033 (suc i) zero (suc j) (suc j0) = refl
          gcd033 zero (suc i0) j j0 = refl
          gcd033 (suc i) (suc i0) j j0 = refl
+
+--gcd-dividable : ( i j  : ℕ )
+--      → Dividable ( gcd i j ) i ∧ Dividable ( gcd i j ) j
+
+f-div>0 :  { k i  : ℕ } → (d : Dividable k i ) → 0 < i → 0 < Dividable.factor d 
+f-div>0 {k} {i} d 0<i with <-cmp 0 (Dividable.factor d)
+... | tri< a ¬b ¬c = a
+... | tri≈ ¬a b ¬c = ⊥-elim ( nat-≡< (begin
+      0 * k + 0  ≡⟨ cong (λ g → g * k + 0) b  ⟩
+      Dividable.factor d * k + 0  ≡⟨ Dividable.is-factor d ⟩
+      i  ∎ ) 0<i ) where open ≡-Reasoning
+
+gcd-≤ : ( i j  : ℕ ) → i ≤ j → gcd i j ≤ j
+gcd-≤ zero zero z≤n = ≤-refl
+gcd-≤ 0 (suc j) z≤n = subst (λ k → k ≤ suc j ) (trans (sym (gcd20 (suc j))) (gcdsym  {suc j} {zero})) ≤-refl
+gcd-≤ (suc i) (suc j) (s≤s i<j) = begin
+      gcd (suc i) (suc j)   ≡⟨ sym m*1=m ⟩
+      gcd (suc i) (suc j) * 1  ≤⟨ *-monoʳ-≤ (gcd (suc i) (suc j)) (f-div>0 d (s≤s z≤n)) ⟩
+      gcd (suc i) (suc j) * f  ≡⟨ +-comm 0 _ ⟩
+      gcd (suc i) (suc j) * f  + 0  ≡⟨ cong (λ k → k + 0) (*-comm (gcd (suc i) (suc j)) _  ) ⟩
+      Dividable.factor (proj2 (gcd-dividable (suc i) (suc j))) * gcd (suc i) (suc j) + 0 ≡⟨ Dividable.is-factor (proj2 (gcd-dividable (suc i) (suc j)))  ⟩
+      suc j  ∎ where
+          d = proj2 (gcd-dividable (suc i) (suc j))
+          f = Dividable.factor (proj2 (gcd-dividable (suc i) (suc j)))
+          open ≤-Reasoning
+
+m*n=m→n : {m n : ℕ } → 0 < m → m * n ≡ m * 1 → n ≡ 1
+m*n=m→n {suc m} {n} (s≤s lt) eq = *-cancelˡ-≡ m eq 
+
+gcd-< : ( i j  : ℕ ) → 0 < i → i < j → gcd i j < j
+gcd-<  i j  0<i  i<j with <-cmp ( gcd i j ) j
+... | tri< a ¬b ¬c = a
+... | tri≈ ¬a b ¬c = ⊥-elim (g111 (Dividable.factor (proj1 (gcd-dividable i j)))
+                 (subst (λ k → (Dividable.factor (proj1 (gcd-dividable i j))) * k + 0 ≡ i ) b (Dividable.is-factor (proj1 (gcd-dividable i j))))) where
+   g111 : (f : ℕ) → f * j + 0 ≡ i → ⊥
+   g111 zero eq = nat-≡<  eq 0<i
+   g111 (suc zero) eq = nat-≡< (sym eq) (begin
+       suc i ≤⟨ i<j ⟩
+       j ≡⟨ trans (+-comm 0 _) (+-comm 0 _) ⟩
+       1 * j + 0 ∎ )  where open ≤-Reasoning
+   g111 (suc (suc f)) eq = nat-≡< (sym eq) ( begin
+       suc i ≤⟨ i<j ⟩
+       j ≡⟨ +-comm  0 _  ⟩
+       j + 0 ≤⟨ +-monoʳ-≤ j z≤n ⟩
+       j + ((j + f * j) + 0) ≡⟨ sym (+-assoc j _ _) ⟩
+       j + (j + f * j) + 0 ≡⟨ refl ⟩
+       suc (suc f) * j + 0 ∎ )  where open ≤-Reasoning
+... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> (gcd-≤ i j (<to≤ i<j)) c )
diff -r 6e8b163ca737 -r a61f121c34a4 automaton-in-agda/src/prime.agda
--- a/automaton-in-agda/src/prime.agda	Wed Jun 23 11:31:00 2021 +0900
+++ b/automaton-in-agda/src/prime.agda	Wed Jun 23 18:10:18 2021 +0900
@@ -48,40 +48,45 @@
 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 {_} {_} {G} {λ m → NonPrime n } (λ g → G.g g) I
-         record { p = n ; 1<p = 1<n ; g = n ; npr = λ lt → np ; div = div= ; is-g = is-g= refl } where
-    record G  : Set where
+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
+    record G (p g : ℕ) : Set where
       field
-        p : ℕ
         1<p : 1 < p 
-        g : ℕ
         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 : G → G 
-    next g = next1 (G.g g) (gcd (G.g g) (G.p g)) where
-      next1  : ℕ →  ℕ  → G 
-      next1  0 _ = g
-      next1  _ 0  = g
-      next1  (suc m) 1 = 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 : G ) → G.g (next p) ≡ zero → NonPrime n
-    pzero g eq = record { factor = G.p g ; prime = record { p>1 = G.1<p g ; isPrime = {!!} } ;  dividable = G.div g }
-    ind :  (p : G ) → NonPrime n → NonPrime n
-    ind = {!!}
-    decline : (p : G ) → 0 < G.g p → G.g (next p) < G.g p
+    next : Pair≤ → Pair≤
+    next record { ox = ox ; oy = oy ; ox<oy = ox<oy } = record { ox = ox ; oy = gcd oy ox ; ox<oy = {!!} } 
+    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 p - ox 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 : Ninduction G  _  (λ g → G.g g)
+    I : Finduction Pair≤  _  (λ op → oy op - ox op )
     I = record {
               pnext = next
             ; fzero = λ {p} → pzero p
             ; decline = λ {p} → decline p
-            ; ind = λ {p} → ind p
+            ; ind = λ {p} → ind {p}
           }