# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1623913258 -32400
# Node ID daeae196aa50535d550344e3a3793d6586d3594d
# Parent  6764fe96994fd18a2669af572c36720de55a64ae
...

diff -r 6764fe96994f -r daeae196aa50 automaton-in-agda/src/gcd.agda
--- a/automaton-in-agda/src/gcd.agda	Thu Jun 17 11:13:58 2021 +0900
+++ b/automaton-in-agda/src/gcd.agda	Thu Jun 17 16:00:58 2021 +0900
@@ -82,42 +82,6 @@
 div0 :  {k : ℕ} → Dividable k 0
 div0 {k} = record { factor = 0; is-factor = refl }
 
-decf-step : {i j k : ℕ } → k > 1 → (if : Factor k (suc i))  → (jf : Factor k (suc j)) 
-   → Dividable k (i - j) ∧ Dividable k (j - i)
-decf-step {i} {j} {suc k}  k>1 if jf = decf-step0 {i} {j} {suc k}  k>1 if jf where
-   decf-step1 : {i k : ℕ } →  (f r : ℕ) → (fa : f * k + r ≡ suc i) 
-        → Dividable k (suc i - r)  → Dividable k (i - remain (decf record {factor = f ; remain = r ; is-factor = fa}))
-   decf-step1 {i} {k}   f (suc r) fa div = 
-      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
-   decf-step1 {i} {zero}  (suc f) zero fa div = ⊥-elim (nat-≡< fa (
-        begin suc (suc f * zero + zero) ≡⟨ cong suc (+-comm _ zero)  ⟩
-        suc (f * 0) ≡⟨ cong suc (*-comm f zero)  ⟩
-        suc zero ≤⟨ s≤s z≤n ⟩
-        suc i ∎ )) where open ≤-Reasoning  -- suc (0 + i) ≡ i0
-   decf-step1 {i} {suc k}  (suc f)  zero fa div = 
-      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
-   decf-step0 : {i j k : ℕ } → k > 1 → (if : Factor k (suc i))  → (jf : Factor k (suc j)) 
-           → Dividable k (i - j) ∧ Dividable k (j - i)
-   decf-step0 {i} {j} {suc k}  k>1 if jf with <-cmp i j
-   ... | tri< a ¬b ¬c = ⟪ subst (λ g → Dividable (suc k) g) (sym (minus<=0 {i} {j} (<to≤ a))) div0 , {!!}  ⟫ 
-   ... | tri≈ ¬a refl ¬c = ⟪ subst (λ g → Dividable (suc k) g) (sym (minus<=0 {i} {i} refl-≤)) div0 ,
-                             subst (λ g → Dividable (suc k) g) (sym (minus<=0 {i} {i} refl-≤)) div0 ⟫
-   ... | tri> ¬a ¬b c = ⟪ {!!} , subst (λ g → Dividable (suc k) g) (sym (minus<=0 {j} {i} (<to≤ c))) div0  ⟫ 
-
 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)  ⟩
@@ -158,6 +122,41 @@
     suc f * k ≡⟨ +-comm 0 _ ⟩
     suc f * k + 0 ∎  )) where open ≤-Reasoning  
 
+div-div : { i j k : ℕ } → k > 1 →  Dividable k i →  Dividable k j → Dividable k (i - j) ∧ Dividable k (j - i)
+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
+      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
+          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
+             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 ⟫ 
+   ... | tri≈ ¬a refl ¬c = ⟪ subst (λ g → Dividable (suc k) g) (sym (minus<=0 {i} {i} refl-≤)) div0 ,
+                             subst (λ g → Dividable (suc k) g) (sym (minus<=0 {i} {i} refl-≤)) div0 ⟫
+   ... | tri> ¬a ¬b c    = ⟪ div-div1 dj di c , subst (λ g → Dividable (suc k) g) (sym (minus<=0 {j} {i} (<to≤ c))) div0  ⟫ 
+
 open _∧_
 
 gcd-gt : ( i i0 j j0 k : ℕ ) → k > 1 → (if : Factor k i) (i0f : Dividable k i0 ) (jf : Factor k j ) (j0f : Dividable k j0)
@@ -170,16 +169,11 @@
 gcd-gt zero i0 (suc zero) j0 k k>1 if i0f jf j0f i-j = ⊥-elim (div1 k>1 (proj2 i-j)) -- can't happen
 gcd-gt zero zero (suc (suc j)) j0 k k>1 if i0f jf j0f i-j = j0f
 gcd-gt zero (suc i0) (suc (suc j)) j0 k k>1 if i0f jf j0f i-j =   
-    gcd-gt i0 (suc i0) (suc j) (suc (suc j))  k k>1 (decf (DtoF i0f)) i0f (decf jf) (proj2 i-j) {!!}
-     --  if  : Factor k zero
-     -- i0f : Dividable k (suc i0)
-     -- jf  : Factor k (suc (suc j))
-     -- j0f : Dividable k j0
-     --   Dividable k (zero - suc (suc j)) ∧ Dividable k (suc (suc j) - zero) → Dividable k (i0 - suc j) ∧ Dividable k (suc j - i0)
+    gcd-gt i0 (suc i0) (suc j) (suc (suc j))  k k>1 (decf (DtoF i0f)) i0f (decf jf) (proj2 i-j) (div-div k>1 i0f (proj2 i-j))
 gcd-gt (suc zero) i0 zero j0 k k>1 if i0f jf j0f i-j  = ⊥-elim (div1 k>1 (proj1 i-j)) -- can't happen
 gcd-gt (suc (suc i)) i0 zero zero k k>1 if i0f jf j0f i-j  = i0f
 gcd-gt (suc (suc i)) i0 zero (suc j0) k k>1 if i0f jf j0f i-j  = --   
-     gcd-gt (suc i) (suc (suc i)) j0 (suc j0) k k>1 (decf if) (proj1 i-j) (decf (DtoF j0f)) j0f {!!} 
+     gcd-gt (suc i) (suc (suc i)) j0 (suc j0) k k>1 (decf if) (proj1 i-j) (decf (DtoF j0f)) j0f (div-div k>1 (proj1 i-j) j0f )
 gcd-gt (suc zero) i0 (suc j) j0 k k>1 if i0f jf j0f i-j  =  
      gcd-gt zero i0 j j0 k k>1 (decf if) i0f (decf jf) j0f i-j
 gcd-gt (suc (suc i)) i0 (suc j) j0 k k>1 if i0f jf j0f i-j  = 
@@ -187,11 +181,7 @@
 
 gcd-div : ( i j k : ℕ ) → k > 1 → (if : Dividable k i) (jf : Dividable k j ) 
    → Dividable k ( gcd i  j ) 
-gcd-div i j k k>1 if jf = gcd-gt i i j j k k>1 (DtoF if) if (DtoF jf) jf {!!} 
-
-
--- 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
+gcd-div i j k k>1 if jf = gcd-gt i i j j k k>1 (DtoF if) if (DtoF jf) jf (div-div k>1 if jf)
 
 gcd22 : ( i i0 o o0 : ℕ ) → gcd1 (suc i) i0 (suc o) o0 ≡ gcd1 i i0 o o0
 gcd22 zero i0 zero o0 = refl
diff -r 6764fe96994f -r daeae196aa50 automaton-in-agda/src/nat.agda
--- a/automaton-in-agda/src/nat.agda	Thu Jun 17 11:13:58 2021 +0900
+++ b/automaton-in-agda/src/nat.agda	Thu Jun 17 16:00:58 2021 +0900
@@ -197,6 +197,18 @@
 
 open import Data.Product
 
+minus+1 : {x y  : ℕ } → y ≤ x  → suc (minus x y)  ≡ minus (suc x) y 
+minus+1 {zero} {zero} y≤x = refl
+minus+1 {suc x} {zero} y≤x = refl
+minus+1 {suc x} {suc y} (s≤s y≤x) = minus+1 {x} {y} y≤x 
+
+minus+yz : {x y z : ℕ } → z ≤ y  → x + minus y z  ≡ minus (x + y) z
+minus+yz {zero} {y} {z} _ = refl
+minus+yz {suc x} {y} {z} z≤y = begin
+         suc x + minus y z ≡⟨ cong suc ( minus+yz z≤y ) ⟩
+         suc (minus (x + y) z) ≡⟨ minus+1 {x + y} {z} (≤-trans z≤y (subst (λ g → y ≤ g) (+-comm y x) x≤x+y) ) ⟩
+         minus (suc x + y) z ∎  where open ≡-Reasoning
+
 minus<=0 : {x y : ℕ } → x ≤ y → minus x y ≡ 0
 minus<=0 {0} {zero} z≤n = refl
 minus<=0 {0} {suc y} z≤n = refl