# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1624875068 -32400
# Node ID 186b66d56ab53d736582965eb7f6e508ded1381d
# Parent  08994de7c82f4015cd5151281429623cf28910a8
...

diff -r 08994de7c82f -r 186b66d56ab5 automaton-in-agda/src/gcd.agda
--- a/automaton-in-agda/src/gcd.agda	Mon Jun 28 17:22:56 2021 +0900
+++ b/automaton-in-agda/src/gcd.agda	Mon Jun 28 19:11:08 2021 +0900
@@ -330,6 +330,31 @@
                ((suc i0 + suc j)   - i0) ∎ ) div= ⟫    
            where open ≡-Reasoning
 
+gcd>0 : ( i j : ℕ ) → 0 < i → 0 < j → 0 < gcd i j  
+gcd>0 i j 0<i 0<j = gcd>01 i i j j 0<i 0<j where
+     gcd>01 : ( i i0 j j0 : ℕ ) → 0 < i0 → 0 < j0  → gcd1 i i0 j j0 > 0
+     gcd>01 zero i0 zero j0 0<i 0<j with <-cmp i0 j0
+     ... | tri< a ¬b ¬c = 0<i
+     ... | tri≈ ¬a refl ¬c = 0<i
+     ... | tri> ¬a ¬b c = 0<j
+     gcd>01 zero i0 (suc zero) j0 0<i 0<j = s≤s z≤n
+     gcd>01 zero zero (suc (suc j)) j0 0<i 0<j = 0<j 
+     gcd>01 zero (suc i0) (suc (suc j)) j0 0<i 0<j = gcd>01 i0 (suc i0) (suc j) (suc (suc j)) 0<i (s≤s z≤n) -- 0 < suc (suc j)
+     gcd>01 (suc zero) i0 zero j0 0<i 0<j =  s≤s z≤n
+     gcd>01 (suc (suc i)) i0 zero zero 0<i 0<j = 0<i 
+     gcd>01 (suc (suc i)) i0 zero (suc j0) 0<i 0<j = gcd>01 (suc i) (suc (suc i))  j0 (suc j0) (s≤s z≤n) 0<j 
+     gcd>01 (suc i) i0 (suc j) j0 0<i 0<j = subst (λ k → 0 < k ) (sym (gcd033 i i0 j j0 )) (gcd>01 i i0 j j0 0<i 0<j ) where
+         gcd033 : (i i0 j j0  : ℕ) → gcd1 (suc i) i0 (suc j) j0 ≡  gcd1 i i0 j j0
+         gcd033 zero zero zero zero = refl
+         gcd033 zero zero (suc j) zero = refl
+         gcd033 (suc i) zero j zero = refl
+         gcd033 zero zero zero (suc j0) = refl
+         gcd033 (suc i) zero zero (suc j0) = refl
+         gcd033 zero zero (suc j) (suc j0) = refl
+         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 loop invariant
 --
 record GCD ( i i0 j j0 : ℕ ) : Set where
@@ -339,6 +364,18 @@
      div-i : Dividable i0 ((j0 + i) - j)
      div-j : Dividable j0 ((i0 + j) - i)
 
+div-11 : {i j : ℕ } → Dividable i ((j + i) - j)
+div-11 {i} {j} = record { factor = 1 ; is-factor = begin 
+   1 * i + 0 ≡⟨ +-comm _ 0  ⟩
+   i + 0  ≡⟨  +-comm _ 0 ⟩
+   i  ≡⟨ sym (minus+y-y {i} {j}) ⟩
+   (i + j ) - j  ≡⟨ cong (λ k → k  - j ) (+-comm i j )  ⟩
+   (j + i) - j ∎ } where open ≡-Reasoning
+
+
+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 }
+
 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 }
 
@@ -530,10 +567,6 @@
     is-equ< : (eqa * i) > (eqb * j) → ((eqa * i) - (eqb * j) ≡ gcd  )
     is-equ> : (eqb * j) > (eqa * i) → ((eqb * j) - (eqa * i) ≡ gcd  )
 
-postulate 
-   gcd-euclid : ( p q r : ℕ )  → 1 < p  → ((i : ℕ ) → i < p → 0 < i   → gcd p i ≡ 1)  →  Dividable p (q * r)  → Dividable p q ∨ Dividable p r
---   gcd-euclid1 : ( i i0 j j0 : ℕ )  → Dividable i0  ((j0 + i) - j ) ∧ Dividable j0 ((i0 + j) - i) → Euclid i0 j0 (gcd1 i i0 j j0)
-
 ge3 : {a b c d : ℕ } → b > a → b - a ≡ d - c → d > c
 ge3 {a} {b} {c} {d} b>a eq = minus>0→x<y (subst (λ k → 0 < k ) eq (minus>0 b>a))
 
@@ -634,6 +667,53 @@
      gcd-euclid1 (suc i) i0 j j0 (gcd-next di)
 
 
+gcd-euclid : ( p a b : ℕ )  → 1 < p  → 0 < a → 0 < b → ((i : ℕ ) → i < p → 0 < i   → gcd p i ≡ 1)  →  Dividable p (a * b)  → Dividable p a ∨ Dividable p b
+gcd-euclid p a b 1<p 0<a 0<b prime div-ab with decD {p} {a} 1<p
+... | yes y = case1 y
+... | no np = case2 ge16  where
+    ge12 : (x : ℕ) → 0 < x → ( gcd p x ≡ 1 ) ∨ ( Dividable p x )
+    ge12 x 0<x with decD {p} {x} 1<p
+    ... | yes y = case2 y
+    ... | 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 = {!!}
+    ge10 : gcd p a ≡ 1
+    ge10 with ge12 a {!!}
+    ... | case1 x = x
+    ... | case2 x = {!!}
+    ge11 : Euclid p a (gcd p a)
+    ge11 = gcd-euclid1 p p a a GCDi
+    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 - 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 = {!!}
+    ge16 : Dividable p b
+    ge16 with <-cmp ( Euclid.eqa ge11 * p ) (  Euclid.eqb ge11 * a )
+    ... | tri< a ¬b ¬c = record { factor = b * Euclid.eqa ge11 -  Dividable.factor div-ab * Euclid.eqb ge11 ; is-factor = ge14 {!!} }  
+    ... | tri≈ ¬a eq ¬c = record { factor = b * Euclid.eqa ge11 -  Dividable.factor div-ab * Euclid.eqb ge11 ; is-factor = ge14 {!!} }  
+    ... | tri> ¬a ¬b c = record { factor = Dividable.factor div-ab * Euclid.eqb ge11  - b * Euclid.eqa ge11 ; is-factor = ge15 {!!} }  
+
+
 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
@@ -679,31 +759,6 @@
       gcd (m * n + 1) n ≡⟨ gcdmul+1 m n ⟩
       1 ∎ where open ≡-Reasoning
 
-gcd>0 : ( i j : ℕ ) → 0 < i → 0 < j → 0 < gcd i j  
-gcd>0 i j 0<i 0<j = gcd>01 i i j j 0<i 0<j where
-     gcd>01 : ( i i0 j j0 : ℕ ) → 0 < i0 → 0 < j0  → gcd1 i i0 j j0 > 0
-     gcd>01 zero i0 zero j0 0<i 0<j with <-cmp i0 j0
-     ... | tri< a ¬b ¬c = 0<i
-     ... | tri≈ ¬a refl ¬c = 0<i
-     ... | tri> ¬a ¬b c = 0<j
-     gcd>01 zero i0 (suc zero) j0 0<i 0<j = s≤s z≤n
-     gcd>01 zero zero (suc (suc j)) j0 0<i 0<j = 0<j 
-     gcd>01 zero (suc i0) (suc (suc j)) j0 0<i 0<j = gcd>01 i0 (suc i0) (suc j) (suc (suc j)) 0<i (s≤s z≤n) -- 0 < suc (suc j)
-     gcd>01 (suc zero) i0 zero j0 0<i 0<j =  s≤s z≤n
-     gcd>01 (suc (suc i)) i0 zero zero 0<i 0<j = 0<i 
-     gcd>01 (suc (suc i)) i0 zero (suc j0) 0<i 0<j = gcd>01 (suc i) (suc (suc i))  j0 (suc j0) (s≤s z≤n) 0<j 
-     gcd>01 (suc i) i0 (suc j) j0 0<i 0<j = subst (λ k → 0 < k ) (sym (gcd033 i i0 j j0 )) (gcd>01 i i0 j j0 0<i 0<j ) where
-         gcd033 : (i i0 j j0  : ℕ) → gcd1 (suc i) i0 (suc j) j0 ≡  gcd1 i i0 j j0
-         gcd033 zero zero zero zero = refl
-         gcd033 zero zero (suc j) zero = refl
-         gcd033 (suc i) zero j zero = refl
-         gcd033 zero zero zero (suc j0) = refl
-         gcd033 (suc i) zero zero (suc j0) = refl
-         gcd033 zero zero (suc j) (suc j0) = refl
-         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