# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1623763813 -32400
# Node ID 8007206a5a19ddec83719ed9262c01790b401d97
# Parent  a3a72db6aed32705e879780ad18fb53f5d073228
...

diff -r a3a72db6aed3 -r 8007206a5a19 automaton-in-agda/src/gcd.agda
--- a/automaton-in-agda/src/gcd.agda	Tue Jun 15 15:39:17 2021 +0900
+++ b/automaton-in-agda/src/gcd.agda	Tue Jun 15 22:30:13 2021 +0900
@@ -63,8 +63,10 @@
    decf-step1 : {i k i0 : ℕ } →  (f r : ℕ) → (fa : f * k + r ≡ suc i) →  (i0f : Factor k i0)
         → Dividable k (suc i - r)  → Dividable k (i - remain (decf record {factor = f ; remain = r ; is-factor = fa}))
    decf-step1 {i} {k} {i0}  f (suc r) fa i0f div = 
-      record { factor = f ;  is-factor = (
-        begin f * k + 0 ≡⟨ {!!} ⟩
+      record { factor = f ;  is-factor = ( --  f * k + suc r ≡ suc i → f * k + suc r ≡ suc i
+        begin f * k + 0 ≡⟨ +-comm _ 0 ⟩
+        f * k ≡⟨ sym ( x=y+z→x-z=y {suc i} {_} {suc r} (sym fa) ) ⟩
+        suc i - suc r ≡⟨ refl ⟩
         i - r ≡⟨ refl ⟩
          (i - remain (decf (record { factor = f ; remain = suc r ; is-factor = fa }))) ∎ ) }  where
             open ≡-Reasoning
@@ -74,8 +76,14 @@
         suc zero ≤⟨ s≤s z≤n ⟩
         suc i ∎ )) where open ≤-Reasoning  -- suc (0 + i) ≡ i0
    decf-step1 {i} {suc k} {i0} (suc f)  zero fa i0f div = 
-      record { factor = f ;  is-factor = (
-        begin f * suc k + 0 ≡⟨ {!!} ⟩
+      record { factor = f ;  is-factor = ( --  suc (k + f * suc k + zero) ≡ suc i →  f * suc k + 0 ≡ i - k 
+        begin f * suc k + 0 ≡⟨ sym ( x=y+z→x-z=y {i} {_} {k} (begin
+          i ≡⟨ sym (cong pred fa) ⟩
+          pred (suc f * suc k + zero) ≡⟨ refl ⟩
+          pred ((suc k + f * suc k) + zero) ≡⟨ cong pred ( +-assoc (suc k) _ zero) ⟩
+          pred (suc k + (f * suc k + zero))  ≡⟨ refl ⟩
+          k + (f * suc k + 0) ≡⟨ +-comm k _ ⟩
+          f * suc k + 0 + k ∎ ))  ⟩ 
         i - k ∎ ) }  where open ≡-Reasoning
 
 ifk0 : (  i0 k : ℕ ) → (i0f : Factor k i0 )  → ( i0=0 : remain i0f ≡ 0 )  → factor i0f * k + 0 ≡ i0
@@ -109,31 +117,34 @@
 gcd : ( i j : ℕ ) → ℕ
 gcd i j = gcd1 i i j j 
 
-gcd-gt : ( i i0 j j0 k : ℕ ) → (if : Factor k i) (i0f : Factor k i0 ) (jf : Factor k j ) (j0f : Factor k j0)
+nfk : (k : ℕ ) → k > 1 → ¬ (Dividable k 1)
+nfk k k>1 fk1 = ⊥-elim ( nat-≡< (sym (Dividable.is-factor fk1))  {!!} )
+
+gcd-gt : ( i i0 j j0 k : ℕ ) → k > 1 → (if : Factor k i) (i0f : Factor k i0 ) (jf : Factor k j ) (j0f : Factor k j0)
    → remain i0f ≡ 0 → remain j0f ≡  0
    → Dividable k (i - remain if) → Dividable k (j - remain jf) 
    → Dividable k ( gcd1 i i0 j j0 ) 
-gcd-gt zero i0 zero j0 k if i0f jf j0f i0=0 j0=0 ir=i0 jr=j0 with <-cmp i0 j0
+gcd-gt zero i0 zero j0 k k>1 if i0f jf j0f i0=0 j0=0 ir=i0 jr=j0 with <-cmp i0 j0
 ... | tri< a ¬b ¬c = record { factor = factor i0f ; is-factor = ifk0 i0 k i0f i0=0 } 
 ... | tri≈ ¬a refl ¬c = record { factor = factor i0f ;  is-factor = ifk0 i0 k i0f i0=0 } 
 ... | tri> ¬a ¬b c = record { factor = factor j0f ;  is-factor = ifk0 j0 k j0f j0=0 } 
-gcd-gt zero i0 (suc zero) j0 k if i0f jf j0f i0=0 j0=0 ir=i0 jr=j0 = {!!} -- can't happen
-gcd-gt zero zero (suc (suc j)) j0 k if i0f jf j0f i0=0 j0=0 ir=i0 jr=j0 = record { factor = factor j0f ; is-factor = ifk0 j0 k j0f j0=0 } 
-gcd-gt zero (suc i0) (suc (suc j)) j0 k if i0f jf j0f i0=0 j0=0 ir=i0 jr=j0 =  
-    gcd-gt i0 (suc i0) (suc j) (suc (suc j))  k (decf i0f) i0f (decf jf) jf i0=0 {!!} {!!} {!!}  
-gcd-gt (suc zero) i0 zero j0 k if i0f jf j0f i0=0 j0=0 ir=i0 jr=j0 = {!!} -- can't happen
-gcd-gt (suc (suc i)) i0 zero zero k if i0f jf j0f i0=0 j0=0 ir=i0 jr=j0 = record { factor = factor i0f ; is-factor = ifk0 i0 k i0f i0=0 } 
-gcd-gt (suc (suc i)) i0 zero (suc j0) k if i0f jf j0f i0=0 j0=0 ir=i0 jr=j0 =
-     gcd-gt (suc i) (suc (suc i)) j0 (suc j0) k (decf if) if (decf j0f) j0f {!!} {!!} {!!} {!!} 
-gcd-gt (suc zero) i0 (suc j) j0 k if i0f jf j0f i0=0 j0=0 ir=i0 jr=j0 = 
-     gcd-gt zero i0 j j0 k (decf if) i0f (decf jf) j0f i0=0 j0=0 {!!} {!!}
-gcd-gt (suc (suc i)) i0 (suc j) j0 k if i0f jf j0f i0=0 j0=0 ir=i0 jr=j0 = 
-     gcd-gt (suc i) i0 j j0 k (decf if) i0f (decf jf) j0f i0=0 j0=0 (decf-step if i0f ir=i0 ) (decf-step jf j0f jr=j0 )
+gcd-gt zero i0 (suc zero) j0 k k>1 if i0f jf j0f i0=0 j0=0 ir=i0 jr=j0 = {!!} -- can't happen
+gcd-gt zero zero (suc (suc j)) j0 k k>1 if i0f jf j0f i0=0 j0=0 ir=i0 jr=j0 = record { factor = factor j0f ; is-factor = ifk0 j0 k j0f j0=0 } 
+gcd-gt zero (suc i0) (suc (suc j)) j0 k k>1 if i0f jf j0f i0=0 j0=0 ir=i0 jr=j0 =  
+    gcd-gt i0 (suc i0) (suc j) (suc (suc j))  k k>1 (decf i0f) i0f (decf jf) jf i0=0 {!!} ? (decf-step jf j0f jr=j0 )
+gcd-gt (suc zero) i0 zero j0 k k>1 if i0f jf j0f i0=0 j0=0 ir=i0 jr=j0 = {!!} -- can't happen
+gcd-gt (suc (suc i)) i0 zero zero k k>1 if i0f jf j0f i0=0 j0=0 ir=i0 jr=j0 = record { factor = factor i0f ; is-factor = ifk0 i0 k i0f i0=0 } 
+gcd-gt (suc (suc i)) i0 zero (suc j0) k k>1 if i0f jf j0f i0=0 j0=0 ir=i0 jr=j0 =
+     gcd-gt (suc i) (suc (suc i)) j0 (suc j0) k k>1 (decf if) if (decf j0f) j0f {!!}  j0=0 (decf-step if i0f ir=i0 ) {!!}
+gcd-gt (suc zero) i0 (suc j) j0 k k>1 if i0f jf j0f i0=0 j0=0 ir=i0 jr=j0 =  
+     gcd-gt zero i0 j j0 k k>1 (decf if) i0f (decf jf) j0f i0=0 j0=0 (decf-step if i0f ir=i0 ) (decf-step jf j0f jr=j0 )
+gcd-gt (suc (suc i)) i0 (suc j) j0 k k>1 if i0f jf j0f i0=0 j0=0 ir=i0 jr=j0 = 
+     gcd-gt (suc i) i0 j j0 k k>1 (decf if) i0f (decf jf) j0f i0=0 j0=0 (decf-step if i0f ir=i0 ) (decf-step jf j0f jr=j0 )
 
-gcd-div : ( i j k : ℕ ) → (if : Factor k i) (jf : Factor k j ) 
+gcd-div : ( i j k : ℕ ) → k > 1 → (if : Factor k i) (jf : Factor k j ) 
    → remain if ≡ 0 → remain jf ≡  0
    → Dividable k ( gcd i  j ) 
-gcd-div i j k if jf i0=0 j0=0 = gcd-gt i i j j k if if jf jf i0=0 j0=0 {!!} {!!} where
+gcd-div i j k k>1 if jf i0=0 j0=0 = gcd-gt i i j j k k>1 if if jf jf i0=0 j0=0 {!!} {!!} where
     gf4 : {m n : ℕ} → n ≡ 0  →  n + m ≡ m
     gf4 {m} {n} eq = begin
         n + m ≡⟨ cong (λ k → k + m) eq  ⟩
diff -r a3a72db6aed3 -r 8007206a5a19 automaton-in-agda/src/nat.agda
--- a/automaton-in-agda/src/nat.agda	Tue Jun 15 15:39:17 2021 +0900
+++ b/automaton-in-agda/src/nat.agda	Tue Jun 15 22:30:13 2021 +0900
@@ -187,6 +187,10 @@
 refl-≤s {zero} = z≤n
 refl-≤s {suc x} = s≤s (refl-≤s {x})
 
+refl-≤ : {x : ℕ } → x ≤ x
+refl-≤ {zero} = z≤n
+refl-≤ {suc x} = s≤s (refl-≤ {x})
+
 x<y→≤ : {x y : ℕ } → x < y →  x ≤ suc y
 x<y→≤ {zero} {.(suc _)} (s≤s z≤n) = z≤n
 x<y→≤ {suc x} {suc y} (s≤s lt) = s≤s (x<y→≤ {x} {y} lt)
@@ -312,6 +316,19 @@
                       ∎   where open ≤-Reasoning
              open ≡-Reasoning
 
+x=y+z→x-z=y : {x y z : ℕ } → x ≡ y + z → x - z ≡ y
+x=y+z→x-z=y {x} {zero} {.x} refl = minus<=0 {x} {x} refl-≤ -- x ≡ suc (y + z) → (x ≡ y + z → x - z ≡ y)   → (x - z) ≡ suc y
+x=y+z→x-z=y {suc x} {suc y} {zero} eq = begin -- suc x ≡ suc (y + zero) → (suc x - zero) ≡ suc y
+       suc x - zero ≡⟨ refl ⟩
+       suc x  ≡⟨ eq ⟩
+       suc y + zero ≡⟨ +-comm _ zero ⟩
+       suc y ∎  where open ≡-Reasoning
+x=y+z→x-z=y {suc x} {suc y} {suc z} eq = x=y+z→x-z=y {x} {suc y} {z} ( begin
+       x ≡⟨ cong pred eq ⟩
+       pred (suc y + suc z) ≡⟨ +-comm _ (suc z)  ⟩
+       suc z + y ≡⟨ cong suc ( +-comm _ y ) ⟩
+       suc y + z ∎  ) where open ≡-Reasoning
+
 record Finduction {n m : Level} (P : Set n ) (Q : P → Set m ) (f : P → ℕ) : Set  (n Level.⊔ m) where
   field
     fzero   : {p : P} → f p ≡ zero → Q p
diff -r a3a72db6aed3 -r 8007206a5a19 automaton-in-agda/src/root2.agda
--- a/automaton-in-agda/src/root2.agda	Tue Jun 15 15:39:17 2021 +0900
+++ b/automaton-in-agda/src/root2.agda	Tue Jun 15 22:30:13 2021 +0900
@@ -58,7 +58,7 @@
 --    → Dividable k ( gcd i  j )
 
 root2-irrational : ( n m : ℕ ) → n > 1 → m > 1  →  2 * n * n ≡ m * m  → ¬ (gcd n m ≡ 1)
-root2-irrational n m n>1 m>1 2nm = rot13 ( gcd-div n m 2 f2 fm (f3 n rot7) refl ) where 
+root2-irrational n m n>1 m>1 2nm = rot13 ( gcd-div n m 2 (s≤s (s≤s z≤n)) f2 fm (f3 n rot7) refl ) where 
     rot13 : {m : ℕ } → Dividable 2 m →  m ≡ 1 → ⊥
     rot13 d refl with Dividable.factor d | Dividable.is-factor d
     ... | zero | ()