# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1623604678 -32400
# Node ID 08f4ec41ea93707c999aea2bb7cdf15e8bc59a0c
# Parent  f9473f83f6e7995d493780a9e3dc4c0f22bfe87c
even→gcd

diff -r f9473f83f6e7 -r 08f4ec41ea93 automaton-in-agda/src/gcd.agda
--- a/automaton-in-agda/src/gcd.agda	Mon Jun 14 00:25:04 2021 +0900
+++ b/automaton-in-agda/src/gcd.agda	Mon Jun 14 02:17:58 2021 +0900
@@ -65,7 +65,7 @@
 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 i ) (j0f : Factor k j0)
+gcd-gt : ( i i0 j j0 k : ℕ ) → (if : Factor k i) (i0f : Factor k i0 ) (jf : Factor k j ) (j0f : Factor k j0)
    → remain i0f ≡ 0 → remain j0f ≡  0
    → (remain if + i ) ≡ i0  → (remain jf + j ) ≡ j0
    → Dividable k ( gcd1 i i0 j j0 ) 
@@ -76,17 +76,28 @@
 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 i0f)
+    gcd-gt i0 (suc i0) (suc j) (suc (suc j))  k (decf i0f) {!!} {!!} 
        record { factor = factor jf ; remain = remain jf ; is-factor = {!!} } 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 = {!!}
 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) {!!} (decf jf) j0f j0=0 {!!} {!!} {!!} 
+     gcd-gt (suc i) (suc (suc i)) j0 (suc j0) k (decf if) {!!} (decf {!!}) j0f j0=0 {!!} {!!} {!!} 
 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 {!!} {!!}
 
+gcd-div : ( i j k : ℕ ) → (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 (gf4 i0=0) (gf4 j0=0) where
+    gf4 : {m n : ℕ} → n ≡ 0  →  n + m ≡ m
+    gf4 {m} {n} eq = begin
+        n + m ≡⟨ cong (λ k → k + m) eq  ⟩
+        0 + m ≡⟨  refl  ⟩
+        m ∎  where open ≡-Reasoning
+
+
 -- gcd26 : { n m : ℕ} → n > 1 → m > 1 → n - m > 0 → gcd n m ≡ gcd (n - m) m
 -- gcd27 : { n m : ℕ} → n > 1 → m > 1 → n - m > 0 → gcd n k ≡ k → k ≤ n
 
diff -r f9473f83f6e7 -r 08f4ec41ea93 automaton-in-agda/src/root2.agda
--- a/automaton-in-agda/src/root2.agda	Mon Jun 14 00:25:04 2021 +0900
+++ b/automaton-in-agda/src/root2.agda	Mon Jun 14 02:17:58 2021 +0900
@@ -24,6 +24,17 @@
        gcd (suc (suc n)) 2 ≡⟨ even→gcd=2 {suc (suc n)} en (s≤s z≤n) ⟩
        2 ∎ where open ≡-Reasoning
 
+even→gcd : (n m : ℕ) → even n → even m → even (gcd n m)
+even→gcd zero zero en em = tt
+even→gcd zero (suc (suc m)) en em = em
+even→gcd (suc (suc n)) zero en em = en
+even→gcd (suc (suc n)) (suc (suc m)) en em = ee2 n n (suc (suc m)) (suc (suc m))  refl refl
+       (subst (λ k → even k) (gcdsym {suc (suc m)} {n})  (ee2 m m n n refl refl (subst (λ k → even k) (gcdsym {n} {m}) ee1))) where
+   ee1 : even (gcd n m)
+   ee1 = even→gcd n m en em
+   ee2 : (i i0 j j0 : ℕ) → i ≡ i0 → j ≡ j0 → even (gcd1 i i j0 j0)  → even (gcd1 (suc (suc i)) (suc (suc i)) j0 j0) 
+   ee2 i i0 j j0 i=i0 j=j0 e = {!!}
+
 even^2 : {n : ℕ} → even ( n * n ) → even n
 even^2 {n} en with even? n
 ... | yes y = y
@@ -52,8 +63,12 @@
 
 open Factor
 
+-- gcd-div : ( i j k : ℕ ) → (if : Factor k i) (jf : Factor k j )
+--    → remain if ≡ 0 → remain jf ≡  0
+--    → 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-gt n n m m 2 f2 f2 f2 fm (f3 n rot7) refl f4 f4) where 
+root2-irrational n m n>1 m>1 2nm = rot13 ( gcd-div n m 2 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 | ()
@@ -99,11 +114,6 @@
     f3 : ( n : ℕ) → (e : even n ) →  remain (rot11 {n} e)  ≡ 0
     f3 zero e = refl
     f3 (suc (suc n)) e = f3 n e 
-    f4 : {m : ℕ} → remain f2 + m ≡ m
-    f4 {m} = begin
-        remain f2 + m ≡⟨ cong (λ k → k + m) (f3 n rot7)  ⟩
-        0 + m ≡⟨  refl  ⟩
-        m ∎  where open ≡-Reasoning
     fm : Factor 2 m
     fm = record { factor = Even.j E ; remain = 0 ; is-factor = fm1 } where
        fm1 : Even.j E * 2 + 0 ≡ m