# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1623917796 -32400
# Node ID 4b452c9d7e7b63f592d2a51b9c9f24eeb9656839
# Parent  daeae196aa50535d550344e3a3793d6586d3594d
gcd done

diff -r daeae196aa50 -r 4b452c9d7e7b automaton-in-agda/src/gcd.agda
--- a/automaton-in-agda/src/gcd.agda	Thu Jun 17 16:00:58 2021 +0900
+++ b/automaton-in-agda/src/gcd.agda	Thu Jun 17 17:16:36 2021 +0900
@@ -62,41 +62,9 @@
         (k + f * suc k) + zero  ≡⟨ cong pred fa ⟩
         n ∎ ) }  where open ≡-Reasoning
 
-decf-eq : {i k : ℕ } → k > 1 → (if : Factor k (suc i)) 
-     → (div : Dividable k (suc i - remain if))  → factor if ≡ Dividable.factor div
-decf-eq {i} {suc k} k>1 if div = if1 where
-   if0 : suc (suc i) > remain if
-   if0 = begin
-        suc (remain if) ≤⟨ s≤s (m≤n+m _ (factor if * suc k)) ⟩
-        suc (factor if * suc k + remain if) ≡⟨ cong suc ( is-factor if) ⟩
-        suc (suc i) ∎  where open ≤-Reasoning
-   if1 : factor if ≡ Dividable.factor div
-   if1 = begin
-        factor if  ≡⟨ *-cancelʳ-≡ _ _ {k} ( +-cancelʳ-≡ _ _ ( begin
-        factor if * suc k + remain if ≡⟨ is-factor if ⟩
-        suc i ≡⟨ sym (minus+n {suc i} {remain if} if0) ⟩
-        (suc i - remain if) + remain if ≡⟨ cong (λ g → g + remain if) (sym (Dividable.is-factor div )) ⟩
-        (Dividable.factor div * suc k + 0) + remain if  ≡⟨ cong (λ g → g + remain if) (+-comm _ 0) ⟩
-        Dividable.factor div * suc k + remain if ∎  )) ⟩ Dividable.factor div ∎   where open ≡-Reasoning
-
 div0 :  {k : ℕ} → Dividable k 0
 div0 {k} = record { factor = 0; is-factor = refl }
 
-ifk0 : (  i0 k : ℕ ) → (i0f : Factor k i0 )  → ( i0=0 : remain i0f ≡ 0 )  → factor i0f * k + 0 ≡ i0
-ifk0 i0 k i0f i0=0 = begin
-   factor i0f * k + 0  ≡⟨ cong (λ m → factor i0f * k + m) (sym i0=0)  ⟩
-   factor i0f * k + remain i0f  ≡⟨ is-factor i0f ⟩
-   i0 ∎ 
-         where open ≡-Reasoning
-
-ifzero : {k : ℕ } → (jf :  Factor k zero ) →  remain jf ≡ 0
-ifzero {k} record { factor = zero ; remain = zero ; is-factor = is-factor } = refl
-ifzero {zero} record { factor = (suc factor₁) ; remain = zero ; is-factor = is-factor } = refl
-ifzero {zero} record { factor = (suc f) ; remain = (suc r) ; is-factor = is-factor } =
-      ⊥-elim (nat-≡< (sym is-factor) (subst (λ k → zero < k ) (+-comm (suc r)  _) if1 )) where
-   if1 : zero < suc r + suc f * zero 
-   if1 = s≤s z≤n
-
 gcd1 : ( i i0 j j0 : ℕ ) → ℕ
 gcd1 zero i0 zero j0 with <-cmp i0 j0
 ... | tri< a ¬b ¬c = i0
@@ -126,30 +94,49 @@
 div-div {i} {j} {suc k} k>1 di dj = div-div0 di dj where
    div-div1 : {i j : ℕ}   →  Dividable (suc k) i →  Dividable (suc k) j → i < j  → Dividable (suc k) (j - i)
    div-div1 {i} {j} record { factor = fi ; is-factor = fai } record { factor = fj ; is-factor = faj } i<j =
-            subst (λ g →  Dividable (suc k) g ) div-div3 ( div-div2 fj fi {!!} ) where
+            subst (λ g →  Dividable (suc k) g ) div-div3 ( div-div2 fj fi fi<fj ) where
+      fi<fj : fi < fj
+      fi<fj with <-cmp fi fj
+      ... | tri< a ¬b ¬c = a
+      ... | tri≈ ¬a b ¬c = ⊥-elim ( nat-≡< (cong (λ g → g * suc k + 0) b) (begin
+             suc (fi * suc k + 0)  ≡⟨ cong suc fai ⟩
+             suc i  ≤⟨ i<j ⟩
+             j  ≡⟨ sym faj ⟩
+             fj * suc k + 0 ∎  )) where open ≤-Reasoning  
+      ... | tri> ¬a ¬b c = ⊥-elim ( nat-<> (*-monoˡ-< k c ) (begin
+             suc (fi * suc k) ≡⟨ +-comm 0 _ ⟩
+             suc (fi * suc k + 0) ≡⟨ cong suc fai ⟩
+             suc i ≤⟨ i<j ⟩
+             j ≡⟨ sym faj ⟩
+             fj * suc k + 0 ≡⟨ +-comm _ 0 ⟩
+             fj * suc k ∎  )) where open ≤-Reasoning  
       div-div3 : (fj * suc k) - (fi * suc k) ≡ j - i
       div-div3 = begin (fj * suc k) - (fi * suc k) ≡⟨  cong₂ (λ g h → g - h) (+-comm 0 (fj * suc k)) (+-comm 0 (fi * suc k)) ⟩
           (fj * suc k + 0) - (fi * suc k + 0) ≡⟨  cong₂ (λ g h → g - h) faj  fai ⟩
           j - i ∎  where open ≡-Reasoning  
-      div-div2 : (fj fi : ℕ) → fi ≤ fj → Dividable (suc k) ((fj * suc k) - (fi * suc k))
-      div-div2 zero fi i≤j = subst (λ g → Dividable (suc k) g) (begin
+      div-div2 : (fj fi : ℕ) → fi < fj → Dividable (suc k) ((fj * suc k) - (fi * suc k))
+      div-div2 zero fi i<j = subst (λ g → Dividable (suc k) g) (begin
           0 ≡⟨ sym (minus<=0 {0} {fi * suc k} z≤n ) ⟩
           0 -  (fi * suc k) ≡⟨ refl ⟩
           (zero * suc k) - (fi * suc k) ∎ ) div0
           where open ≡-Reasoning  
-      div-div2 (suc fj) zero i≤j = {!!}
-      div-div2 (suc fj) (suc fi) i≤j = record { factor = suc (Dividable.factor (div-div2 fj (suc fi) fi<fj )) ; is-factor = ( begin 
-          suc (Dividable.factor (div-div2 fj (suc fi) fi<fj )) * suc k + 0 ≡⟨ +-comm _ 0 ⟩
-          suc (Dividable.factor (div-div2 fj (suc fi) fi<fj )) * suc k  ≡⟨ refl ⟩
-          suc k + ((Dividable.factor (div-div2 fj (suc fi) fi<fj )) * suc k )  ≡⟨ cong (λ g → suc k + g ) (+-comm 0 _) ⟩
-          suc k + ((Dividable.factor (div-div2 fj (suc fi) fi<fj )) * suc k + 0)
-                     ≡⟨ cong (λ g → suc k + g) (Dividable.is-factor (div-div2 fj (suc fi) fi<fj) ) ⟩
-          suc k + ((fj * suc k) - ((suc fi) * suc k)) ≡⟨ minus+yz {suc k} {fj * suc k} {(suc fi) * suc k} {!!}  ⟩
-           ( (suc k + (fj * suc k)) - ((suc fi) * suc k)) ≡⟨ refl ⟩
-          ((suc fj * suc k) - ((suc fi) * suc k)) ∎ ) } where
+      div-div2 (suc fj) fi i<j with <-cmp fi fj
+      ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c i<j  )
+      ... | tri≈ ¬a refl ¬c = record { factor = 1 ; is-factor = (begin
+             1 * suc k + 0 ≡⟨ +-comm _ 0 ⟩
+               1 * suc k ≡⟨ cong suc (+-comm _ 0) ⟩
+             suc k ≡⟨ sym (minus+y-y {suc k} {fj * suc k}) ⟩
+             (suc k + fj * suc k) - (fj * suc k) ≡⟨ refl ⟩
+             (suc (k + fj * suc k)) - (fj * suc k) ∎  )} where open ≡-Reasoning  
+      ... | tri< fi<fj ¬b ¬c = record { factor = suc (Dividable.factor (div-div2 fj fi fi<fj )) ; is-factor = ( begin 
+          suc (Dividable.factor (div-div2 fj fi fi<fj )) * suc k + 0 ≡⟨ +-comm _ 0 ⟩
+          suc (Dividable.factor (div-div2 fj fi fi<fj )) * suc k  ≡⟨ refl ⟩
+          suc k + ((Dividable.factor (div-div2 fj fi fi<fj )) * suc k )  ≡⟨ cong (λ g → suc k + g ) (+-comm 0 _) ⟩
+          suc k + ((Dividable.factor (div-div2 fj fi fi<fj )) * suc k + 0)  ≡⟨ cong (λ g → suc k + g) (Dividable.is-factor (div-div2 fj fi fi<fj) ) ⟩
+          suc k + ((fj * suc k) - (fi * suc k)) ≡⟨ minus+yz {suc k} {fj * suc k} {fi * suc k} (<to≤ (*-monoˡ-< k fi<fj )) ⟩
+           ( (suc k + (fj * suc k)) - (fi * suc k)) ≡⟨ refl ⟩
+          ((suc fj * suc k) - (fi * suc k)) ∎ ) } where
              open ≡-Reasoning  
-             fi<fj : suc fi ≤ fj 
-             fi<fj = {!!}
    div-div0 : { i j : ℕ } →  Dividable (suc k) i →  Dividable (suc k) j → Dividable (suc k) (i - j) ∧ Dividable (suc k) (j - i)
    div-div0 {i} {j} di dj with <-cmp i j
    ... | tri< a ¬b ¬c    = ⟪ subst (λ g → Dividable (suc k) g) (sym (minus<=0 {i} {j} (<to≤ a))) div0 , div-div1 di dj a ⟫ 
@@ -241,6 +228,7 @@
    gcd205 : (j : ℕ) → gcd1 (suc j) (suc (suc i)) j (suc i) ≡ 1
    gcd205 zero = refl
    gcd205 (suc j) = subst (λ k → k ≡ 1) (gcd22 (suc j)  (suc (suc i)) j (suc i)) (gcd205 j)
+
 gcd204 : (i : ℕ) → gcd1 1 1 i i ≡ 1
 gcd204 zero = refl
 gcd204 (suc zero) = refl
@@ -274,33 +262,6 @@
           gcd1 1 1 (suc j) (suc j) ∎ where open ≡-Reasoning
        gcd200 (suc (suc i)) i0 (suc j) zero i=i0 ()
 
-gcd52 : {i : ℕ } → 1 < suc (suc i)
-gcd52 {zero} = a<sa
-gcd52 {suc i} = <-trans (gcd52 {i}) a<sa
-
-gcd50 : (i i0 j j0 : ℕ) → 1 < i0 → i ≤ i0 → j ≤ j0 →  gcd1 i i0 j j0 ≤ i0 
-gcd50 zero i0 zero j0 0<i i<i0 j<j0 with <-cmp i0 j0
-... | tri< a ¬b ¬c = ≤-refl    
-... | tri≈ ¬a refl ¬c =  ≤-refl 
-... | tri> ¬a ¬b c = ≤-trans refl-≤s c  
-gcd50 zero (suc i0) (suc zero) j0 0<i i<i0 j<j0 = gcd51 0<i where 
-   gcd51 : 1 < suc i0 → gcd1 zero (suc i0) 1 j0 ≤ suc i0
-   gcd51 1<i = <to≤ 1<i
-gcd50 zero (suc i0) (suc (suc j)) j0 0<i i<i0 j<j0 = gcd50 i0 (suc i0) (suc j) (suc (suc j)) 0<i refl-≤s refl-≤s
-gcd50 (suc zero) i0 zero j0 0<i i<i0 j<j0 = <to≤ 0<i
-gcd50 (suc (suc i)) i0 zero zero 0<i i<i0 j<j0 = ≤-refl
-gcd50 (suc (suc i)) i0 zero (suc j0) 0<i i<i0 j<j0 = ≤-trans (gcd50 (suc i) (suc (suc i))  j0 (suc j0) gcd52  refl-≤s refl-≤s) i<i0
-gcd50 (suc i) i0 (suc j) j0 0<i i<i0 j<j0 = subst (λ k → k ≤ i0 ) (sym (gcd22 i i0 j j0))
-   (gcd50 i i0 j j0 0<i (≤-trans refl-≤s i<i0) (≤-trans refl-≤s j<j0)) 
-
-gcd5 : ( n k : ℕ ) → 1 < n → gcd n k ≤ n
-gcd5 n k 0<n = gcd50 n n k k 0<n ≤-refl ≤-refl 
-
-gcd6 : ( n k : ℕ ) → 1 < n → gcd k n ≤ n
-gcd6 n k 1<n = subst (λ m → m ≤ n) (gcdsym {n} {k}) (gcd5 n k 1<n)
-
-gcd4 : ( n k : ℕ ) → 1 < n  → gcd n k ≡ k → k ≤ n
-gcd4 n k 1<n eq = subst (λ m → m ≤ n ) eq (gcd5 n k 1<n)
 
 gcdmul+1 : ( m n : ℕ ) → gcd (m * n + 1) n ≡ 1
 gcdmul+1 zero n = gcd204 n
diff -r daeae196aa50 -r 4b452c9d7e7b automaton-in-agda/src/nat.agda
--- a/automaton-in-agda/src/nat.agda	Thu Jun 17 16:00:58 2021 +0900
+++ b/automaton-in-agda/src/nat.agda	Thu Jun 17 17:16:36 2021 +0900
@@ -144,6 +144,9 @@
 x≤x+y {zero} {y} = z≤n
 x≤x+y {suc z} {y} = s≤s  (x≤x+y {z} {y})
 
+x≤y+x : {z y : ℕ } → z ≤ y + z
+x≤y+x {z} {y} = subst (λ k → z ≤ k ) (+-comm _ y ) x≤x+y
+
 <-plus : {x y z : ℕ } → x < y → x + z < y + z 
 <-plus {zero} {suc y} {z} (s≤s z≤n) = s≤s (subst (λ k → z ≤ k ) (+-comm z _ ) x≤x+y  )
 <-plus {suc x} {suc y} {z} (s≤s lt) = s≤s (<-plus {x} {y} {z} lt)
@@ -218,6 +221,13 @@
 minus>0 {zero} {suc _} (s≤s z≤n) = s≤s z≤n
 minus>0 {suc x} {suc y} (s≤s lt) = minus>0 {x} {y} lt
 
+minus+y-y : {x y : ℕ } → (x + y) - y  ≡ x
+minus+y-y {zero} {y} = minus<=0 {zero + y} {y} ≤-refl 
+minus+y-y {suc x} {y} = begin
+         (suc x + y) - y ≡⟨ sym (minus+1 {_} {y} x≤y+x) ⟩
+         suc ((x + y) - y) ≡⟨ cong suc (minus+y-y {x} {y}) ⟩
+         suc x ∎  where open ≡-Reasoning
+
 open import Relation.Binary.Definitions
 
 distr-minus-* : {x y z : ℕ } → (minus x y) * z ≡ minus (x * z) (y * z) 
diff -r daeae196aa50 -r 4b452c9d7e7b automaton-in-agda/src/root2.agda
--- a/automaton-in-agda/src/root2.agda	Thu Jun 17 16:00:58 2021 +0900
+++ b/automaton-in-agda/src/root2.agda	Thu Jun 17 17:16:36 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 (s≤s (s≤s z≤n)) 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)) {!!} {!!} ) where 
     rot13 : {m : ℕ } → Dividable 2 m →  m ≡ 1 → ⊥
     rot13 d refl with Dividable.factor d | Dividable.is-factor d
     ... | zero | ()