# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1624236052 -32400
# Node ID 906b43b94228779fdbd80179471cd92de9b8a824
# Parent  9aec75fa796cf23b0a48a5d41bf6aebd917e1266
gcd-dividable  done

diff -r 9aec75fa796c -r 906b43b94228 automaton-in-agda/src/gcd.agda
--- a/automaton-in-agda/src/gcd.agda	Mon Jun 21 08:08:08 2021 +0900
+++ b/automaton-in-agda/src/gcd.agda	Mon Jun 21 09:40:52 2021 +0900
@@ -281,11 +281,13 @@
         ... | tri> ¬a ¬b c | tri< a ¬b₁ ¬c = refl
         ... | tri> ¬a ¬b c | tri≈ ¬a₁ b ¬c = ⊥-elim (¬b (sym b))
         ... | tri> ¬a ¬b c | tri> ¬a₁ ¬b₁ c₁ = ⊥-elim (nat-<> c c₁)
+
         record Fdec ( i j : ℕ ) : Set where
            field
                ni : ℕ 
                nj : ℕ 
                fdec :  0 < F ⟪ i , j ⟫  → F ⟪ ni , nj ⟫  < F ⟪ i , j ⟫
+
         fd1 : ( i j k : ℕ ) → i < j  → k ≡ j - i →  F ⟪ suc i , k ⟫ < F ⟪ suc i , suc j ⟫
         fd1 i j 0 i<j eq = ⊥-elim ( nat-≡< eq (minus>0 {i} {j} i<j )) 
         fd1 i j (suc k) i<j eq = fd2 i j k i<j eq where
@@ -304,6 +306,7 @@
                     fd4 = s≤s a
                ... | tri> ¬a ¬b c | tri≈ ¬a₁ b ¬c =  ⊥-elim (¬a₁ i<j)
                ... | tri> ¬a ¬b c | tri> ¬a₁ ¬b₁ c₁ =  ⊥-elim (¬a₁ i<j)
+
         fedc0 : (i j : ℕ ) → Fdec i j
         fedc0 0 0 = record { ni =  0 ; nj = 0 ; fdec = λ ()  } 
         fedc0 (suc i) 0 = record { ni =  suc i ; nj = 0 ; fdec = λ ()  } 
@@ -318,6 +321,37 @@
               ... | tri> ¬a ¬b c =  ⊥-elim ( ¬b refl )
         ... | tri> ¬a ¬b c = record { ni =  i - j ; nj = suc j ; fdec = λ lt →
             subst₂ (λ s t → s < t) (Fsym {suc j} {i - j}) (Fsym {suc j} {suc i}) (fd1 j i (i - j) c refl ) } 
+
+        ind3 : {i j : ℕ } → i < j 
+               → Dividable (gcd (suc i) (j - i)) (suc i) 
+               → Dividable (gcd (suc i) (suc j)) (suc i) 
+        ind3 {i} {j} a prev = 
+               subst (λ k → Dividable k (suc i)) ( begin
+                 gcd (suc i) (j - i)  ≡⟨ gcdsym {suc i} {j - i} ⟩
+                 gcd (j - i ) (suc i)   ≡⟨ sym (gcd+j (j - i) (suc i)) ⟩
+                 gcd ((j - i) + suc i) (suc i)  ≡⟨ cong (λ k → gcd k (suc i)) ( begin
+                  (suc j - suc i) + suc i ≡⟨ minus+n {suc j} {suc i} (<-trans ( s≤s a) a<sa ) ⟩ -- i ≤ n →  suc (suc i) ≤ suc (suc (suc n)) 
+                  suc j ∎ ) ⟩
+                 gcd (suc j) (suc i)  ≡⟨ gcdsym {suc j} {suc i} ⟩
+                 gcd (suc i) (suc j)  ∎ ) prev where open ≡-Reasoning 
+        ind7 : {i j : ℕ } → (i < j ) → (j - i) + suc i ≡ suc j
+        ind7 {i} {j} a = begin (suc j - suc i) + suc i ≡⟨ minus+n {suc j} {suc i} (<-trans (s≤s a) a<sa)  ⟩
+                        suc j ∎  where open ≡-Reasoning 
+        ind6 : {i j k : ℕ } → i < j
+               → Dividable k (j - i)
+               → Dividable k (suc i) 
+               → Dividable k (suc j)
+        ind6 {i} {j} {k} i<j dj di = subst (λ g → Dividable k g ) (ind7 i<j) (proj1 (div+div dj di)) 
+        ind4 : {i j : ℕ } → i < j
+               → Dividable (gcd (suc i) (j - i)) (j - i)
+               → Dividable (gcd (suc i) (suc j)) (j - i)
+        ind4 {i} {j} i<j prev = subst (λ k → k) ( begin
+                 Dividable (gcd (suc i) (j - i)) (j - i)  ≡⟨ cong  (λ k → Dividable k (j - i)) (gcdsym {suc i}  ) ⟩
+                 Dividable (gcd (j - i ) (suc i) ) (j - i)  ≡⟨ cong  (λ k → Dividable k (j - i)) ( sym (gcd+j  (j - i) (suc i))) ⟩
+                 Dividable (gcd ((j - i) + suc i) (suc i)) (j - i)  ≡⟨ cong  (λ k → Dividable (gcd k (suc i)) (j - i)) (ind7 i<j ) ⟩
+                 Dividable (gcd (suc j) (suc i)) (j - i)    ≡⟨ cong  (λ k → Dividable k (j - i)) (gcdsym {suc j} ) ⟩
+                 Dividable (gcd (suc i) (suc j)) (j - i)   ∎ ) prev where open ≡-Reasoning 
+
         ind :   ( i j : ℕ ) →
               Dividable (gcd (Fdec.ni (fedc0 i j)) (Fdec.nj (fedc0 i j))) (Fdec.ni (fedc0 i j))
             ∧ Dividable (gcd (Fdec.ni (fedc0 i j)) (Fdec.nj (fedc0 i j))) (Fdec.nj (fedc0 i j))
@@ -332,35 +366,28 @@
            ind2 : Dividable (gcd (suc i) zero) (suc i) ∧ Dividable (gcd (suc i) zero) zero
            ind2 = ⟪  subst (λ k → Dividable k (suc i)) (sym (trans refl (gcd20 (suc i)))) div= , div0 ⟫
         ind (suc i) (suc j) prev with <-cmp i j
-        ... | tri< a ¬b ¬c = ⟪ ind3 (proj1 prev)   , ind6 (ind4 (proj2 prev)) (ind3 (proj1 prev)) ⟫ where
-            ind3 :  Dividable (gcd (suc i) (j - i)) (suc i)
-                  → Dividable (gcd (suc i) (suc j)) (suc i) 
-            ind3 prev = 
-               subst (λ k → Dividable k (suc i)) ( begin
-                 gcd (suc i) (j - i)  ≡⟨ gcdsym {suc i} {j - i} ⟩
-                 gcd (j - i ) (suc i)   ≡⟨ sym (gcd+j (j - i) (suc i)) ⟩
-                 gcd ((j - i) + suc i) (suc i)  ≡⟨ cong (λ k → gcd k (suc i)) ( begin
-                  (suc j - suc i) + suc i ≡⟨ minus+n {suc j} {suc i} (<-trans ( s≤s a) a<sa ) ⟩ -- i ≤ n →  suc (suc i) ≤ suc (suc (suc n)) 
-                  suc j ∎ ) ⟩
-                 gcd (suc j) (suc i)  ≡⟨ gcdsym {suc j} {suc i} ⟩
-                 gcd (suc i) (suc j)  ∎ ) prev where open ≡-Reasoning 
-            ind7 : (j - i) + suc i ≡ suc j
-            ind7 = begin (suc j - suc i) + suc i ≡⟨ minus+n {suc j} {suc i} (<-trans (s≤s a) a<sa)  ⟩
-                        suc j ∎  where open ≡-Reasoning 
-            ind6 : {k : ℕ } → Dividable k (j - i) → Dividable k (suc i) → Dividable k (suc j)
-            ind6 {k} dj di = subst (λ g → Dividable k g ) ind7 (proj1 (div+div dj di)) 
-            ind4 : Dividable (gcd (suc i) (j - i)) (j - i)
-                 → Dividable (gcd (suc i) (suc j)) (j - i)
-            ind4 prev = subst (λ k → k) ( begin
-                 Dividable (gcd (suc i) (j - i)) (j - i)  ≡⟨ cong  (λ k → Dividable k (j - i)) (gcdsym {suc i}  ) ⟩
-                 Dividable (gcd (j - i ) (suc i) ) (j - i)  ≡⟨ cong  (λ k → Dividable k (j - i)) ( sym (gcd+j  (j - i) (suc i))) ⟩
-                 Dividable (gcd ((j - i) + suc i) (suc i)) (j - i)  ≡⟨ cong  (λ k → Dividable (gcd k (suc i)) (j - i)) ind7 ⟩
-                 Dividable (gcd (suc j) (suc i)) (j - i)    ≡⟨ cong  (λ k → Dividable k (j - i)) (gcdsym {suc j} ) ⟩
-                 Dividable (gcd (suc i) (suc j)) (j - i)   ∎ ) prev where open ≡-Reasoning 
+        ... | tri< a ¬b ¬c = ⟪ ind3 a (proj1 prev)  , ind6 a (ind4 a (proj2 prev)) (ind3 a (proj1 prev) ) ⟫ where
         ... | tri≈ ¬a refl ¬c = ⟪ ind5 , ind5 ⟫ where
            ind5 : Dividable (gcd (suc i) (suc i)) (suc i) 
            ind5 = subst (λ k → Dividable k (suc j)) (sym (gcdmm (suc i) (suc i))) div=  
-        ... | tri> ¬a ¬b c = {!!}
+        ... | tri> ¬a ¬b c = ⟪ ind8 c (proj1 prev) (proj2 prev) , ind10 c  (proj2 prev) ⟫ where
+           ind9 : {i j : ℕ} → i < j → gcd (j - i) (suc i) ≡ gcd (suc j) (suc i)
+           ind9 {i} {j} i<j = begin
+                 gcd (j - i ) (suc i)    ≡⟨ sym (gcd+j (j - i ) (suc i)  ) ⟩
+                 gcd (j - i + suc i) (suc i)    ≡⟨ cong (λ k → gcd k (suc i)) (ind7 i<j ) ⟩
+                 gcd (suc j) (suc i)   ∎  where open ≡-Reasoning 
+           ind8 :  { i j : ℕ } → i < j
+               → Dividable (gcd (j - i) (suc i)) (j - i) 
+               → Dividable (gcd (j - i) (suc i)) (suc i)
+               → Dividable (gcd (suc j) (suc i)) (suc j)
+           ind8 {i} {j} i<j dji di = ind6 i<j (subst (λ k → Dividable k (j - i)) (ind9 i<j) dji)  (subst (λ k → Dividable k (suc i)) (ind9 i<j) di) 
+           ind10 :  { i j : ℕ } → j < i
+               → Dividable (gcd (i - j) (suc j)) (suc j)
+               → Dividable (gcd (suc i) (suc j)) (suc j)
+           ind10 {i} {j} j<i dji = subst (λ g → Dividable g (suc j) ) (begin
+             gcd (i - j) (suc j)  ≡⟨ sym (gcd+j (i - j) (suc j)) ⟩
+             gcd (i - j + suc j) (suc j)  ≡⟨ cong (λ k → gcd k (suc j)) (ind7 j<i ) ⟩
+             gcd (suc i) (suc j) ∎ ) dji where open ≡-Reasoning 
 
         I : Finduction (ℕ ∧ ℕ) _ F
         I = record {