# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1624282499 -32400
# Node ID 4f9cc768640f67ee22258678b58330f0b3be7ffc
# Parent  689be82c08fabc6a73fe6ba5f53cfbfd928c86e4
...

diff -r 689be82c08fa -r 4f9cc768640f automaton-in-agda/src/gcd.agda
--- a/automaton-in-agda/src/gcd.agda	Mon Jun 21 19:22:06 2021 +0900
+++ b/automaton-in-agda/src/gcd.agda	Mon Jun 21 22:34:59 2021 +0900
@@ -242,21 +242,29 @@
         F0 0 eq =   no (λ d → ⊥-elim ( nat-≡< refl (proj2 d)))
         F0 (suc m) eq with <-cmp k (suc m)
         ... | tri< a ¬b ¬c = yes ⟪ record { factor = 1 ; is-factor =
-            subst (λ g → 1 * k + 0 ≡ g ) (sym (i-j=0→i=j (<to≤ a) eq )) div1*k+0=k }  , {!!} ⟫ where -- (suc m - k) ≡ 0 → k ≡ suc m, k ≤ suc m
-        ... | tri≈ ¬a refl ¬c =  yes  ⟪ record { factor = 1 ; is-factor = div1*k+0=k } , {!!} ⟫
+            subst (λ g → 1 * k + 0 ≡ g ) (sym (i-j=0→i=j (<to≤ a) eq )) div1*k+0=k }  , s≤s z≤n  ⟫ where -- (suc m - k) ≡ 0 → k ≡ suc m, k ≤ suc m
+        ... | tri≈ ¬a refl ¬c =  yes  ⟪ record { factor = 1 ; is-factor = div1*k+0=k } ,  s≤s z≤n ⟫
         ... | tri> ¬a ¬b c = no ( λ d →  ⊥-elim (div<k k>1 (s≤s z≤n ) c (proj1 d)) )
         decl : {m  : ℕ } → 0 < m → m - k < m
         decl {m} 0<m = y-x<y (<-trans a<sa k>1 ) 0<m 
         ind : (p : ℕ ) → Dec (Dividable k (p - k) ∧ ( 0 < p - k)) → Dec (Dividable k p ∧ ( 0 < p))
-        ind p (yes y) = yes ⟪ (subst (λ g → Dividable k g) (minus+n k≤p ) (proj1 ( div+div (proj1 y) div= ))) , {!!} ⟫ where
-           k≤p :  k < suc p -- k * factor y + 0 ≡ p - k 
-           k≤p  = {!!}
-        ind p (no n) = no (λ d → n {!!} )
+        ind p (yes y) = yes ⟪ (subst (λ g → Dividable k g) (minus+n (<-trans k<p a<sa)) (proj1 ( div+div (proj1 y) div= ))) , <-trans (<-trans a<sa k>1) k<p ⟫ where
+           k<p :  k < p -- k * factor y + 0 ≡ p - k , 0 < p - k
+           k<p with <-cmp k p
+           ... | tri< a ¬b ¬c = a 
+           ... | tri≈ ¬a refl ¬c = ⊥-elim ( nat-≡< (sym ( minus<=0 {k} ≤-refl )) (proj2 y)) 
+           ... | tri> ¬a ¬b c = ⊥-elim ( nat-≡< (sym ( minus<=0 {p} {k} (≤-trans refl-≤s c ))) (proj2 y)) 
+        ind p (no n) = no (λ d → n ⟪ proj1 (div-div k>1 (proj1 d) div=) , 0<pk (Dividable.factor (proj1 d)) (proj2 d) (Dividable.is-factor (proj1 d)  ) ⟫ ) where
+           -- Dividable k p ∧ (0 < p) → Dividable k (p - k) ∧ (0 < (p - k))
+           0<pk : (f : ℕ) →  0 < p → f * k + 0 ≡ p  → 0 < p - k  
+           0<pk f 0<p eq with <-cmp 0 (p - k)
+           ... | tri< a ¬b ¬c = a
+           ... | tri≈ ¬a b ¬c = {!!}  -- f * k + 0 ≡ p → p ≡ 0 ∨ k ≤ p
         I : Ninduction ℕ  _  F
         I = record {
               pnext = λ p → p - k
             ; fzero = λ {m} eq → F0 m eq
-            ; decline = λ {m} lt → decl lt -- Dec (Dividable k (p - k)) → Dec (Dividable k p)
+            ; decline = λ {m} lt → decl lt 
             ; ind = λ {p} prev → ind p prev
           } 
 
@@ -286,85 +294,46 @@
 
 gcd-divable : ( i j  : ℕ )
       → Dividable ( gcd i j ) i ∧ Dividable ( gcd i j ) j
-gcd-divable i j  = f-induction {_} {_} {ℕ ∧ ℕ}
+gcd-divable i j  = n-induction {_} {_} {ℕ ∧ ℕ}
    {λ p  → Dividable ( gcd (proj1 p) (proj2 p) ) (proj1 p) ∧ Dividable ( gcd (proj1 p)  (proj2 p) ) (proj2 p)} F I ⟪ i , j ⟫ where
         F : ℕ ∧ ℕ → ℕ
-        F ⟪ 0 , 0 ⟫ = 0
-        F ⟪ 0 , suc j ⟫ = 0
-        F ⟪ suc i , 0 ⟫ = 0
-        F ⟪ suc i , suc j ⟫ with <-cmp i j
-        ... | tri< a ¬b ¬c = suc j
+        F ⟪ i , j ⟫ with <-cmp i j
+        ... | tri< a ¬b ¬c = j
         ... | tri≈ ¬a b ¬c = 0
-        ... | tri> ¬a ¬b c = suc i
+        ... | tri> ¬a ¬b c = i
+        next :  ℕ ∧ ℕ → ℕ ∧ ℕ
+        next ⟪ i , j ⟫ with <-cmp i j
+        ... | tri< a ¬b ¬c = ⟪ i , j - i ⟫
+        ... | tri≈ ¬a b ¬c = ⟪ 0 , 0 ⟫
+        ... | tri> ¬a ¬b c = ⟪ i - j , j  ⟫
         F0 : { i j : ℕ } → F ⟪ i , j ⟫ ≡ 0 → (i ≡ j) ∨ (i ≡ 0 ) ∨ (j ≡ 0)
         F0 {zero} {zero} p = case1 refl
         F0 {zero} {suc j} p =  case2 (case1 refl)
         F0 {suc i} {zero} p =  case2 (case2 refl)
         F0 {suc i} {suc j} p with <-cmp i j
-        ... | tri< a ¬b ¬c = ⊥-elim ( nat-≡< (sym p) (s≤s z≤n ))
-        ... | tri≈ ¬a refl ¬c =  case1 refl
-        ... | tri> ¬a ¬b c = ⊥-elim ( nat-≡< (sym p) (s≤s z≤n ))
-        F00 :  {p : ℕ ∧ ℕ} → F p ≡ zero → Dividable (gcd (proj1 p) (proj2 p)) (proj1 p) ∧ Dividable (gcd (proj1 p) (proj2 p)) (proj2 p)
-        F00 {⟪ i , j ⟫} eq with F0 {i} {j} eq
+        ... | tri< a ¬b ¬c = {!!} -- ⊥-elim ( nat-≡< (sym p) (s≤s z≤n ))
+        ... | tri≈ ¬a refl ¬c = case1 refl
+        ... | tri> ¬a ¬b c = {!!} --⊥-elim ( nat-≡< (sym p) (s≤s z≤n ))
+        F00 :  {p : ℕ ∧ ℕ} → F (next p) ≡ zero → Dividable (gcd (proj1 p) (proj2 p)) (proj1 p) ∧ Dividable (gcd (proj1 p) (proj2 p)) (proj2 p)
+        F00 {⟪ i , j ⟫} eq with F0 {i} {j} {!!}
         ... | case1 refl = ⟪  subst (λ k → Dividable k i) (sym (gcdmm i i)) div= , subst (λ k → Dividable k i) (sym (gcdmm i i)) div= ⟫
         ... | case2 (case1 refl) = ⟪  subst (λ k → Dividable k i) (sym (trans (gcdsym {0} {j} ) (gcd20 j)))div0
                                     , subst (λ k → Dividable k j) (sym (trans (gcdsym {0} {j}) (gcd20 j))) div= ⟫
         ... | case2 (case2 refl) = ⟪  subst (λ k → Dividable k i) (sym (gcd20 i)) div=
                                     , subst (λ k → Dividable k j) (sym (gcd20 i)) div0 ⟫
-        Fsym :  {i j : ℕ } → F ⟪ i , j ⟫ ≡ F ⟪ j , i ⟫
-        Fsym {0} {0} = refl
-        Fsym {0} {suc j} = refl
-        Fsym {suc i} {0} = refl
-        Fsym {suc i} {suc j} with <-cmp i j | <-cmp j i
-        ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = ⊥-elim (nat-<> a a₁)
-        ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = ⊥-elim (¬b (sym b))
-        ... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c = refl
-        ... | tri≈ ¬a refl ¬c | tri< a ¬b ¬c₁ = ⊥-elim (¬b refl)
-        ... | tri≈ ¬a refl ¬c | tri≈ ¬a₁ refl ¬c₁ = refl
-        ... | tri≈ ¬a refl ¬c | tri> ¬a₁ ¬b c = ⊥-elim (¬b refl)
-        ... | 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
-               fd2 : ( i j k : ℕ ) → i < j → suc k ≡ j - i  →  F ⟪ suc i , suc k ⟫ < F ⟪ suc i , suc j ⟫
-               fd2 i j k i<j eq with <-cmp i k | <-cmp i j
-               ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = fd3 where
-                    fd3 : suc k < suc j  -- suc j - suc i < suc j
-                    fd3 = subst (λ g → g < suc j) (sym eq) (y-x<y {suc i} {suc j} (s≤s z≤n) (s≤s z≤n))
-               ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = ⊥-elim (⊥-elim (¬a i<j))
-               ... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c = ⊥-elim (⊥-elim (¬a i<j))
-               ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ = s≤s z≤n
-               ... | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ = ⊥-elim (¬a₁ i<j)
-               ... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c =  s≤s z≤n -- i > j
-               ... | tri> ¬a ¬b c | tri< a ¬b₁ ¬c = fd4 where
-                    fd4 : suc i < suc j
-                    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 = λ ()  } 
-        fedc0 0 (suc j)  = record { ni =  0 ; nj = suc j ; fdec = λ ()  } 
-        fedc0 (suc i) (suc j) with <-cmp i j
-        ... | tri< i<j ¬b ¬c = record { ni =  suc i ; nj = j - i ; fdec = λ lt → fd1 i j (j - i) i<j refl  } 
-        ... | tri≈ ¬a refl ¬c = record { ni =  suc i ; nj = suc j     ; fdec = λ lt → ⊥-elim (nat-≡< fd0 lt) } where
-              fd0 : {i : ℕ } → 0 ≡ F ⟪ suc i , suc i ⟫
-              fd0 {i} with <-cmp i i
-              ... | tri< a ¬b ¬c = ⊥-elim ( ¬b refl )
-              ... | tri≈ ¬a b ¬c = refl
-              ... | 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 ) } 
+        Fdecl :  ( p : ℕ ∧ ℕ ) → 0 < F p  →  F (next p) < F p
+        Fdecl ⟪ i , j ⟫ 0<F with <-cmp i j 
+        ... | tri< a ¬b ¬c = fd1  where
+             fd1 : F ⟪ i , j - i ⟫ < j
+             fd1 with <-cmp i ( j - i )
+             ... | tri< a ¬b ¬c = {!!}  -- j - i < j
+             ... | tri≈ ¬a b ¬c = {!!} -- 0 < j
+             ... | tri> ¬a ¬b c = a -- i < j
+        ... | tri≈ ¬a refl ¬c  = ⊥-elim ( nat-≡< refl 0<F )
+        ... | tri> ¬a ¬b c = fd2 where
+             fd2 : F ⟪ i  - j , j  ⟫ < i
+             fd2 = {!!}
 
         ind3 : {i j : ℕ } → i < j 
                → Dividable (gcd (suc i) (j - i)) (suc i) 
@@ -396,25 +365,25 @@
                  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))
-            → Dividable (gcd i j) i ∧ Dividable (gcd i j) j
-        ind zero zero prev = ind0 where
+        ind :  (p : ℕ ∧  ℕ ) → (
+                 Dividable (gcd (proj1 (next p)) (proj2 (next p))) (proj1 (next p))
+                       ∧ Dividable (gcd (proj1 (next p)) (proj2 (next p))) (proj2 (next p)) )
+            → Dividable (gcd (proj1 p) (proj2 p)) (proj1 p) ∧ Dividable (gcd (proj1 p) (proj2 p)) (proj2 p)
+        ind ⟪ zero , zero ⟫ prev = ind0 where
            ind0 : Dividable (gcd zero zero) zero ∧ Dividable (gcd zero zero) zero
            ind0 = ⟪ div0 , div0 ⟫
-        ind zero (suc j) prev = ind1 where
+        ind ⟪ zero , (suc j) ⟫ prev = ind1 where
            ind1 : Dividable (gcd zero (suc j)) zero ∧ Dividable (gcd zero (suc j)) (suc j)
            ind1 = ⟪ div0 , subst (λ k → Dividable k (suc j)) (sym (trans (gcdsym {zero} {suc j}) (gcd20 (suc j)))) div=  ⟫
-        ind (suc i) zero prev = ind2 where
+        ind ⟪ (suc i) , zero ⟫ prev = ind2 where
            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 a (proj1 prev)  , ind6 a (ind4 a (proj2 prev)) (ind3 a (proj1 prev) ) ⟫ where
+        ind ⟪ (suc i) , (suc j) ⟫ prev with <-cmp i j
+        ... | tri< a ¬b ¬c = ⟪ ind3 a {!!}  , ind6 a (ind4 a {!!}) (ind3 a {!!} ) ⟫ 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 = ⟪ ind8 c (proj1 prev) (proj2 prev) , ind10 c  (proj2 prev) ⟫ where
+        ... | tri> ¬a ¬b c = ⟪ ind8 c {!!} {!!} , ind10 c  {!!} ⟫ 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)  ) ⟩
@@ -433,12 +402,12 @@
              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 : Ninduction (ℕ ∧ ℕ) _ F
         I = record {
-              fzero = F00 
-            ; pnext = λ p → ⟪ Fdec.ni (fedc0 (proj1 p) (proj2 p)) ,  Fdec.nj (fedc0 (proj1 p) (proj2 p)) ⟫ 
-            ; decline = λ {p} lt → Fdec.fdec (fedc0 (proj1 p) (proj2 p))  lt
-            ; ind = λ {p} prev → ind (proj1 p ) ( proj2 p ) prev
+              pnext = λ p → next p
+            ; fzero = F00 
+            ; decline = λ {p} lt → {!!}
+            ; ind = λ {p} prev → ind p prev
           }