# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1624578552 -32400
# Node ID 54977cc189e648713c2a9f3bcb88d28856eebf9b
# Parent  a72bcc6eadad32b4fafd40001080169d628a86b1
...

diff -r a72bcc6eadad -r 54977cc189e6 automaton-in-agda/src/gcd.agda
--- a/automaton-in-agda/src/gcd.agda	Thu Jun 24 11:02:58 2021 +0900
+++ b/automaton-in-agda/src/gcd.agda	Fri Jun 25 08:49:12 2021 +0900
@@ -299,6 +299,16 @@
    → 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-dividable1 : ( i i0 j j0 : ℕ )
+--      → Dividable i0  (j0 + i - j ) ∨ Dividable j0 (i0 + j - i)
+--      → Dividable ( gcd1 i i0 j j0  ) i0 ∧ Dividable ( gcd1 i i0 j j0  ) j0
+-- gcd-dividable1  zero i0 zero j0 with <-cmp i0 j0
+-- ... | tri< a ¬b ¬c = ⟪ div= , {!!} ⟫ -- Dividable i0  (j0 + i - j ) ∧ Dividable j0 (i0 + j - i)
+-- ... | tri≈ ¬a refl ¬c = {!!}
+-- ... | tri> ¬a ¬b c = {!!}
+-- gcd-dividable1 zero i0 (suc zero) j0 = {!!}
+-- gcd-dividable1 i i0 j j0 = {!!}
+
 gcd-dividable : ( i j  : ℕ )
       → Dividable ( gcd i j ) i ∧ Dividable ( gcd i j ) j
 gcd-dividable i j  = f-induction {_} {_} {ℕ ∧ ℕ}
@@ -456,6 +466,26 @@
             ; ind = λ {p} prev → ind (proj1 p ) ( proj2 p ) prev
           } 
 
+-- gcd-equlid : ( i i0 j j0 b0  : ℕ ) 
+--           Dividable i0  (j0 + i - j ) ∨ Dividable j0 (i0 + j - i)
+--           (x0 < j0 → gcd x0 j0 ≡ 1) → gcd (i0 * b0) j0  ≡ j0 → gcd1 i i0 j j0  ≡ 1 → gcd b0 j0  ≡ j0
+-- gcd-equlid zero i0 zero j0  a a0 b b0 ab ab0 x0 x0<j0 gxj=1 a*b gabj ga1 with <-cmp i0 j0
+-- ... | tri< a' ¬b ¬c = {!!}
+-- ... | tri≈ ¬a refl ¬c = {!!}
+-- ... | tri> ¬a ¬b c = {!!}
+-- gcd-equlid zero i0 (suc zero) j0 a a0 b b0 ab ab0 x0 x0<j0 gxj=1 a*b gabj ga1 = {!!}
+-- gcd-equlid zero zero (suc (suc j)) j0 a a0 b b0 ab ab0 x0 x0<j0 gxj=1 a*b gabj ga1 = {!!}
+-- gcd-equlid zero (suc i0) (suc (suc j)) j0 a a0 b b0 ab ab0 x0 x0<j0 gxj=1 a*b gabj ga1 =    {!!}
+--     gcd-equlid i0 (suc i0) (suc j) (suc (suc j)) {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!}
+-- gcd-equlid (suc zero) i0 zero j0 = {!!}
+-- gcd-equlid (suc (suc i)) i0 zero zero a a0 b b0 ab ab0 x0 x0<j0 gxj=1 a*b gabj ga1 = {!!}
+-- gcd-equlid (suc (suc i)) i0 zero (suc j0) a a0 b b0 ab ab0 x0 x0<j0 gxj=1 a*b gabj ga1 = 
+--      gcd-equlid (suc i) (suc (suc i)) j0 (suc j0) {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!}
+-- gcd-equlid (suc zero) i0 (suc j) j0 a a0 b b0 ab ab0 x0 x0<j0 gxj=1 a*b gabj ga1 =  
+--      gcd-equlid zero i0 j j0 {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!}
+-- gcd-equlid (suc (suc i)) i0 (suc j) j0 a a0 b b0 ab ab0 x0 x0<j0 gxj=1 a*b gabj ga1 = 
+--      gcd-equlid (suc i) i0 j j0 {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!}
+
 
 gcdmul+1 : ( m n : ℕ ) → gcd (m * n + 1) n ≡ 1
 gcdmul+1 zero n = gcd204 n
diff -r a72bcc6eadad -r 54977cc189e6 automaton-in-agda/src/prime.agda
--- a/automaton-in-agda/src/prime.agda	Thu Jun 24 11:02:58 2021 +0900
+++ b/automaton-in-agda/src/prime.agda	Fri Jun 25 08:49:12 2021 +0900
@@ -107,7 +107,7 @@
   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 
+prime-is-infinite (suc m) pmax = newPrime where 
   factorial : (n : ℕ) → ℕ
   factorial zero = 1
   factorial (suc n) = (suc n) * (factorial n)
@@ -176,10 +176,12 @@
   fact : (n : ℕ) → Prime n → Dividable n ( factorial (suc m) )
   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 
+  newPrime : ⊥
+  newPrime with PrimeP ( suc (factorial (suc m)) )
+  ... | yes p = pmax _ f>m p   -- yes, we found a prime not in list
   ... | no np = div+1 (Prime.p>1 (NonPrime.prime p1)) (fact (NonPrime.factor p1) (NonPrime.prime p1) ) (NonPrime.dividable p1) where
+      -- n!+1 cannot be dividable, because n! is dividable
+      -- the factor need not be a prime, but anyway we prove that there is a prime factor in NonPrime
       p1 : NonPrime  ( suc (factorial (suc m)) )
       p1 = nonPrime (begin
        2 ≤⟨ s≤s ( s≤s z≤n) ⟩
diff -r a72bcc6eadad -r 54977cc189e6 automaton-in-agda/src/root2.agda
--- a/automaton-in-agda/src/root2.agda	Thu Jun 24 11:02:58 2021 +0900
+++ b/automaton-in-agda/src/root2.agda	Fri Jun 25 08:49:12 2021 +0900
@@ -11,19 +11,61 @@
 open import gcd
 open import even
 open import nat
+open import logic
 
 record Rational : Set where
   field
     i j : ℕ
     coprime : gcd i j ≡ 1
 
-even→gcd=2 : {n : ℕ} → even n → gcd n 2 ≡ 2
-even→gcd=2 {zero} en  = refl
-even→gcd=2 {suc (suc zero)} en  = refl
-even→gcd=2 {suc (suc (suc (suc n)))} en  = begin
-       gcd (suc (suc (suc (suc n)))) 2 ≡⟨⟩
-       gcd (suc (suc n)) 2 ≡⟨ even→gcd=2 {suc (suc n)} en  ⟩
-       2 ∎ where open ≡-Reasoning
+open _∧_
+
+div→gcd : {n k : ℕ } → k > 1 → Dividable k n → gcd n k ≡ k
+div→gcd {n} {k} k>1 = n-induction {_} {_} {ℕ} {λ m → Dividable k m → gcd m k ≡ k } (λ x → x) I n where
+        decl : {m  : ℕ } → 0 < m → m - k < m
+        decl {m} 0<m = y-x<y (<-trans a<sa k>1 ) 0<m 
+        ind : (m : ℕ ) → (Dividable k (m - k) → gcd (m - k) k ≡ k) → Dividable k m → gcd m k ≡ k
+        ind m prev d with <-cmp (suc m) k
+        ... | tri≈ ¬a refl ¬c = ⊥-elim ( div+1 k>1 d div= )
+        ... | tri>  ¬a ¬b c = subst (λ g → g ≡ k) ind1 ( prev (proj2 (div-div k>1 div= d))) where
+           ind1 : gcd (m - k) k ≡ gcd m k
+           ind1 = begin
+               gcd (m - k) k  ≡⟨ sym (gcd+j (m - k)  _) ⟩
+               gcd (m - k + k) k ≡⟨ cong (λ g → gcd g k) (minus+n {m} {k} c) ⟩
+               gcd m k ∎ where open ≡-Reasoning
+        ... | tri< a ¬b ¬c with <-cmp 0 m 
+        ... | tri< a₁ ¬b₁ ¬c₁ = ⊥-elim ( div<k k>1 a₁ (<-trans a<sa a) d )
+        ... | tri≈ ¬a refl ¬c₁ = subst (λ g → g ≡ k ) (gcdsym {k} {0} ) (gcd20 k)
+        fzero : (m : ℕ) → (m - k) ≡ zero → Dividable k m → gcd m k ≡ k 
+        fzero 0 eq d = trans  (gcdsym {0} {k} ) (gcd20 k) 
+        fzero (suc m) eq d with <-cmp (suc m) k
+        ... | tri< a ¬b ¬c = ⊥-elim ( div<k k>1 (s≤s z≤n) a d )
+        ... | tri≈ ¬a refl ¬c = gcdmm k k
+        ... | tri> ¬a ¬b c = ⊥-elim ( nat-≡< (sym eq) (minus>0 c) )
+        I : Ninduction ℕ  _  (λ x → x)
+        I = record {
+              pnext = λ p → p - k
+            ; fzero = λ {m} eq → fzero m eq
+            ; decline = λ {m} lt → decl lt 
+            ; ind = λ {p} prev → ind p prev
+          } 
+
+--  n ≡ i * k + r
+--  n^2 = (i * k)^2 + i * r * k  + r^2
+--  r^2 | k   yes → jj
+
+open import prime
+
+-- equlid : ( n m k : ℕ ) → 1 < k → 1 < n → Prime k → Dividable k ( n * m ) → Dividable k n ∨ Dividable k m
+-- equlid = {!!}
+
+-- divdable^2 : ( n k : ℕ ) → 1 < k → 1 < n → Prime k → Dividable k ( n * n ) → Dividable k n
+-- divdable^2 zero zero 1<k 1<n pk dn2 = {!!}
+-- divdable^2 (suc n) (suc k) 1<k 1<n pk dn2 with decD {suc k} {suc n} 1<k
+-- ... | yes y = y
+-- ... | no non with equlid (suc n) (suc n) (suc k) 1<k {!!} pk dn2
+-- ... | case1 dn = dn
+-- ... | case2 dm = dm
 
 even^2 : {n : ℕ} → even ( n * n ) → even n
 even^2 {n} en with even? n