# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1624888887 -32400
# Node ID 61d9fdb22f2dcaff7e1f17b21090396cbfac030c
# Parent  6cd80d8432ead8ee0d76dd240dc91737dfb1386d
...

diff -r 6cd80d8432ea -r 61d9fdb22f2d automaton-in-agda/src/gcd.agda
--- a/automaton-in-agda/src/gcd.agda	Mon Jun 28 19:28:52 2021 +0900
+++ b/automaton-in-agda/src/gcd.agda	Mon Jun 28 23:01:27 2021 +0900
@@ -372,9 +372,38 @@
    (i + j ) - j  ≡⟨ cong (λ k → k  - j ) (+-comm i j )  ⟩
    (j + i) - j ∎ } where open ≡-Reasoning
 
+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
+          } 
 
 GCDi : {i j : ℕ } → GCD i i j j
-GCDi {i} {j} = record { i<i0 = refl-≤ ; j<j0 = refl-≤ ; div-i = div-11 ; div-j = div-11 }
+GCDi {i} {j} = record { i<i0 = refl-≤ ; j<j0 = refl-≤ ; div-i = div-11 {i} {j} ; div-j = div-11 {j} {i} }
 
 GCD-sym : {i i0 j j0 : ℕ} → GCD i i0 j j0 → GCD j j0 i i0
 GCD-sym g = record { i<i0 = GCD.j<j0 g ; j<j0 = GCD.i<i0 g ; div-i = GCD.div-j g ; div-j = GCD.div-i g }
@@ -560,6 +589,33 @@
             ; ind = λ {p} prev → ind (proj1 p ) ( proj2 p ) prev
           } 
 
+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 : ( i j  : ℕ ) → 0 < i → i ≤ j → gcd i j ≤ i
+gcd-≤i zero _ () z≤n 
+gcd-≤i (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 (proj1 (gcd-dividable (suc i) (suc j))) * gcd (suc i) (suc j) + 0 ≡⟨ Dividable.is-factor (proj1 (gcd-dividable (suc i) (suc j)))  ⟩
+      suc i  ∎ where
+          d = proj1 (gcd-dividable (suc i) (suc j))
+          f = Dividable.factor (proj1 (gcd-dividable (suc i) (suc j)))
+          open ≤-Reasoning
+
+gcd-≤ : { i j  : ℕ } → 0 < i → 0 < j  →  gcd i j ≤ i
+gcd-≤ {i} {j} 0<i 0<j with <-cmp i j
+... | tri< a ¬b ¬c = gcd-≤i i j 0<i (<to≤ a)
+... | tri≈ ¬a refl ¬c = gcd-≤i i j 0<i refl-≤
+... | tri> ¬a ¬b c = ≤-trans (subst (λ k → k ≤ j) (gcdsym {j} {i}) (gcd-≤i j i 0<j (<to≤ c))) (<to≤ c)
+
 record Euclid (i j gcd : ℕ ) : Set where
   field
     eqa : ℕ
@@ -677,36 +733,57 @@
     ... | no nx with <-cmp (gcd p x ) 1
     ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> a (s≤s (gcd>0 p x (<-trans a<sa 1<p)  0<x) ) )
     ... | tri≈ ¬a b ¬c = case1 b
-    ... | tri> ¬a ¬b c = ⊥-elim ( nat-≡< (sym (prime (gcd p x)  {!!} (gcd>0 p x (<-trans a<sa 1<p)  0<x))) {!!} ) where
-        ge13 : gcd p (gcd p x) ≡ gcd p x
-        ge13 = {!!}
+    ... | tri> ¬a ¬b c = ⊥-elim ( nat-≡< (sym (prime (gcd p x) ge13 (<to≤ c) )) ge18 ) where
+        --  1 < gcd p x 
+        ge13 :  gcd p x < p -- gcd p x ≡ p → ¬ nx
+        ge13 with <-cmp (gcd p x ) p
+        ... | tri< a ¬b ¬c = a
+        ... | tri≈ ¬a b ¬c = ⊥-elim ( nx (subst (λ k → Dividable k x) b (proj2 (gcd-dividable p x ))))
+        ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> (gcd-≤ (<-trans a<sa 1<p) 0<x) c )
+        ge19 : Dividable (gcd p x) p
+        ge19 = proj1 (gcd-dividable p x )
+        ge18 :   1 < gcd p  (gcd p x) --  Dividable p  (gcd p x) → gcd p  (gcd p x) ≡  (gcd p x) > 1
+        ge18 = subst (λ k → 1 < k ) (sym (div→gcd {p} {gcd p x} c ge19 )) c
     ge10 : gcd p a ≡ 1
     ge10 with ge12 a 0<a
     ... | case1 x = x
     ... | case2 x = ⊥-elim ( np x )
     ge11 : Euclid p a (gcd p a)
     ge11 = gcd-euclid1 p p a a GCDi
+    ge18 : (Dividable.factor div-ab * Euclid.eqb ge11) * p ≡  b * (a * Euclid.eqb ge11 )
+    ge18 = begin
+         (Dividable.factor div-ab * Euclid.eqb ge11) * p  ≡⟨ {!!}   ⟩
+         (Euclid.eqb ge11 * p)  ≡⟨ {!!}   ⟩
+         (p * Euclid.eqb ge11 )  ≡⟨ {!!}   ⟩
+         (Dividable.factor div-ab * p ) * Euclid.eqb ge11   ≡⟨ {!!}   ⟩
+         (Dividable.factor div-ab * p + 0) * Euclid.eqb ge11   ≡⟨ {!!}   ⟩
+         (a * b) * Euclid.eqb ge11   ≡⟨ {!!}   ⟩
+         (b * a) * Euclid.eqb ge11   ≡⟨ {!!}   ⟩
+         b * (a * Euclid.eqb ge11 ) ∎ where open ≡-Reasoning
     ge14 : ( Euclid.eqa ge11 * p ) ≤ (  Euclid.eqb ge11 * a ) → (b * Euclid.eqa ge11 - Dividable.factor div-ab * Euclid.eqb ge11) * p + 0 ≡ b
     ge14 lt = begin
          (b * Euclid.eqa ge11 - Dividable.factor div-ab * Euclid.eqb ge11) * p + 0 ≡⟨ {!!}   ⟩
          (b * Euclid.eqa ge11 - Dividable.factor div-ab * Euclid.eqb ge11) * p  ≡⟨ {!!}   ⟩
-         (b * Euclid.eqa ge11) * p - (Dividable.factor div-ab * Euclid.eqb ge11) * p  ≡⟨ {!!}   ⟩
-         (b * Euclid.eqa ge11) * p - (Dividable.factor div-ab * Euclid.eqb ge11) * p  ≡⟨ {!!}   ⟩
-         (b * Euclid.eqa ge11) * p - Dividable.factor div-ab * (Euclid.eqb ge11 * p)  ≡⟨ {!!}   ⟩
-         (b * Euclid.eqa ge11) * p - Dividable.factor div-ab * (p * Euclid.eqb ge11 )  ≡⟨ {!!}   ⟩
-         (b * Euclid.eqa ge11) * p - (Dividable.factor div-ab * p ) * Euclid.eqb ge11   ≡⟨ {!!}   ⟩
-         (b * Euclid.eqa ge11) * p - (Dividable.factor div-ab * p + 0) * Euclid.eqb ge11   ≡⟨ {!!}   ⟩
-         (b * Euclid.eqa ge11) * p - (a * b) * Euclid.eqb ge11   ≡⟨ {!!}   ⟩
-         (b * Euclid.eqa ge11) * p - (b * a) * Euclid.eqb ge11   ≡⟨ {!!}   ⟩
-         (b * Euclid.eqa ge11) * p - b * (a * Euclid.eqb ge11 )  ≡⟨ {!!}   ⟩
-         b * (Euclid.eqa ge11 * p) - b * (a * Euclid.eqb ge11 )  ≡⟨ {!!}   ⟩
+         (b * Euclid.eqa ge11) * p - ((Dividable.factor div-ab * Euclid.eqb ge11) * p)  ≡⟨ cong (λ k → (b * Euclid.eqa ge11) * p  - k  ) ge18 ⟩
+         (b * Euclid.eqa ge11) * p - (b * (a * Euclid.eqb ge11 ))  ≡⟨ {!!}   ⟩
+         b * (Euclid.eqa ge11 * p) - (b * (a * Euclid.eqb ge11 ))  ≡⟨ {!!}   ⟩
          b * ( Euclid.eqa ge11 * p - a * Euclid.eqb ge11 )  ≡⟨ {!!}   ⟩
          b * ( Euclid.eqa ge11 * p -  Euclid.eqb ge11 * a )  ≡⟨ cong (b *_) {!!} ⟩
          b * gcd p a  ≡⟨ cong (b *_) ge10 ⟩
          b * 1  ≡⟨ m*1=m ⟩
          b ∎ where open ≡-Reasoning
     ge15 : ( Euclid.eqa ge11 * p ) > (  Euclid.eqb ge11 * a ) →  (Dividable.factor div-ab * Euclid.eqb ge11 - b * Euclid.eqa ge11  ) * p + 0 ≡ b
-    ge15 = {!!}
+    ge15 lt = begin
+         (Dividable.factor div-ab * Euclid.eqb ge11 - b * Euclid.eqa ge11  ) * p + 0  ≡⟨ {!!}   ⟩
+         (Dividable.factor div-ab * Euclid.eqb ge11 - b * Euclid.eqa ge11  ) * p   ≡⟨ {!!}   ⟩
+         ((Dividable.factor div-ab * Euclid.eqb ge11) * p) - ((b * Euclid.eqa ge11) * p)    ≡⟨ cong (λ k → k - ((b * Euclid.eqa ge11) * p)   ) ge18 ⟩
+         (b * (a * Euclid.eqb ge11 )) - ((b * Euclid.eqa ge11) * p )   ≡⟨ {!!}   ⟩
+         (b * (a * Euclid.eqb ge11 )) - (b * (Euclid.eqa ge11 * p) )   ≡⟨ {!!}   ⟩
+         b * ( a * Euclid.eqb ge11 - (Euclid.eqa ge11 * p) )  ≡⟨ {!!}   ⟩
+         b * ( Euclid.eqb ge11 * a - Euclid.eqa ge11 * p  )  ≡⟨ cong (b *_) {!!} ⟩
+         b * gcd p a  ≡⟨ cong (b *_) ge10 ⟩
+         b * 1  ≡⟨ m*1=m ⟩
+         b ∎ where open ≡-Reasoning
     ge17 : (x  y : ℕ ) → x ≡ y → x ≤ y
     ge17 x x refl = refl-≤
     ge16 : Dividable p b
@@ -716,35 +793,6 @@
     ... | tri> ¬a ¬b c = record { factor = Dividable.factor div-ab * Euclid.eqb ge11  - b * Euclid.eqa ge11 ; is-factor = ge15 c }  
 
 
-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
-          } 
 
 gcdmul+1 : ( m n : ℕ ) → gcd (m * n + 1) n ≡ 1
 gcdmul+1 zero n = gcd204 n
@@ -764,29 +812,6 @@
 --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
-
 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 ≤ i
-gcd-≤ zero _ () z≤n 
-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 (proj1 (gcd-dividable (suc i) (suc j))) * gcd (suc i) (suc j) + 0 ≡⟨ Dividable.is-factor (proj1 (gcd-dividable (suc i) (suc j)))  ⟩
-      suc i  ∎ where
-          d = proj1 (gcd-dividable (suc i) (suc j))
-          f = Dividable.factor (proj1 (gcd-dividable (suc i) (suc j)))
-          open ≤-Reasoning
-
-gcd-≥ : ( i j  : ℕ ) → 0 < i → i ≤ j → gcd j i ≤ i
-gcd-≥ i j 0<i i≤j = subst (λ k → k ≤ i) (gcdsym {i} {j}) ( gcd-≤ i j 0<i i≤j )