# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1624067691 -32400
# Node ID f1370437c68eb50f2d4db9b3205a33e40a7dbff0
# Parent  e97cf4fb67fafad8d31c57e3cdafcdb82748347d
...

diff -r e97cf4fb67fa -r f1370437c68e automaton-in-agda/src/gcd.agda
--- a/automaton-in-agda/src/gcd.agda	Fri Jun 18 21:09:50 2021 +0900
+++ b/automaton-in-agda/src/gcd.agda	Sat Jun 19 10:54:51 2021 +0900
@@ -170,6 +170,103 @@
    → 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 (div-div k>1 if jf)
 
+-- open import Data.Sum.Base
+-- factor-0 : (i j : ℕ) → j ≤ i → Factor (i - j) 0 → i ≡ j
+-- factor-0 i j lt eq with m*n≡0⇒m≡0∨n≡0 (factor eq) ( m+n≡0⇒m≡0 (factor eq * (i - j)) (is-factor eq ) )
+-- ... | inj₁ x = {!!}
+-- ... | inj₂ y =  i-j=0→i=j lt y
+--     factor eq * (i - j) + remain eq ≡⟨ is-factor eq ⟩ 
+
+gg1 : {i0 : ℕ } → 1 * i0 + 0 ≡ i0
+gg1 {i0} = begin  1 * i0 + 0 ≡⟨ +-comm _ 0 ⟩
+    i0 + 0 ≡⟨ +-comm _ 0 ⟩
+    i0 ∎   where open ≡-Reasoning  
+
+gg3 : {i0 : ℕ } → i0 * 1 + 0 ≡ i0
+gg3 = trans (+-comm _ 0 ) m*1=m
+
+open import Data.Sum.Base
+
+gcd-divable : ( i i0 j j0 : ℕ )
+      → (if : Factor i0 j0) (jf : Factor j0 i0)   -- factor eq * i0 + (j0 - i0) = j0
+      → remain if ≡ j - i  → remain jf ≡ i - j
+      → Dividable ( gcd1 i i0 j j0 ) i0 ∧ Dividable ( gcd1 i i0 j j0 ) j0
+gcd-divable zero i0 zero j0 if jf if=0 jf=0 with <-cmp i0 j0
+... | tri< a ¬b ¬c = ⟪ record { factor = 1 ; is-factor = gg1 } ,  record { factor = factor if ; is-factor = gg2 } ⟫ where
+    gg2 : factor if *  i0 + 0 ≡ j0
+    gg2 = begin
+      factor if * i0 + 0 ≡⟨ cong (λ k → factor if * i0 + k) (sym if=0) ⟩
+      factor if * i0 + remain if ≡⟨ is-factor if ⟩
+      j0 ∎   where open ≡-Reasoning  
+... | tri≈ ¬a refl ¬c = ⟪ record { factor = 1 ; is-factor = gg1 } ,  record { factor = 1 ; is-factor = gg1 } ⟫
+... | tri> ¬a ¬b c = ⟪ record { factor = factor jf ; is-factor = gg2 } ,  record { factor = 1 ; is-factor = gg1 } ⟫ where
+    gg2 : factor jf *  j0 + 0 ≡ i0
+    gg2 = begin
+      factor jf * j0 + 0 ≡⟨ cong (λ k → factor jf * j0 + k) (sym jf=0)  ⟩
+      factor jf * j0 + remain jf ≡⟨ is-factor jf ⟩
+      i0 ∎   where open ≡-Reasoning  
+gcd-divable zero i0 (suc zero) j0 if jf if=0 jf=0 =  ⟪ record { factor = i0 ; is-factor = gg3 } ,  record { factor = j0 ; is-factor = gg3 } ⟫ 
+gcd-divable zero zero (suc (suc j)) j0 if jf if=0 jf=0 = ⟪ record { factor = factor jf ; is-factor = gg4 } ,  record { factor = 1 ; is-factor = gg1 } ⟫
+   where
+    gg4 :  factor jf * j0  + 0 ≡ zero
+    gg4 with  m*n≡0⇒m≡0∨n≡0 (factor jf) (  m+n≡0⇒m≡0 (factor jf * j0) (is-factor jf))
+    ... | inj₁ x = begin
+      factor jf * j0 + 0 ≡⟨ +-comm _ 0 ⟩
+      factor jf * j0  ≡⟨ cong (λ k → k * j0) x  ⟩
+      0 ∎   where open ≡-Reasoning
+    ... | inj₂ y = begin
+      factor jf * j0 + 0 ≡⟨ +-comm _ 0 ⟩
+      factor jf * j0  ≡⟨ cong (λ k → factor jf * k) y  ⟩
+      factor jf * 0  ≡⟨ *-comm (factor jf) 0  ⟩
+      0 ∎   where open ≡-Reasoning
+gcd-divable zero (suc i0) (suc (suc j)) j0 if jf if=0 jf=0
+    with gcd-divable i0 (suc i0) (suc j) (suc (suc j))
+        record { factor = {!!} ; is-factor = {!!} ; remain = suc j - i0 }
+        record { factor = {!!} ; is-factor = {!!} ; remain = i0 - suc j } refl refl 
+... | t = ⟪ record { factor = {!!} ; is-factor = {!!} } , {!!} ⟫ -- Dividable (gcd1 i0 (suc i0) (suc j) (suc (suc j))) (suc i0)
+gcd-divable (suc zero) i0 zero j0 if jf if=0 jf=0 = ⟪ record { factor = i0 ; is-factor = gg3 } ,  record { factor = j0 ; is-factor = gg3 } ⟫
+gcd-divable (suc (suc i)) i0 zero zero if jf if=0 jf=0 = ⟪ record { factor = 1 ; is-factor = gg1 } ,  record { factor = factor if ; is-factor = gg4 } ⟫
+   where
+    gg4 :  factor if * i0  + 0 ≡ zero
+    gg4 with  m*n≡0⇒m≡0∨n≡0 (factor if) (  m+n≡0⇒m≡0 (factor if * i0) (is-factor if))
+    ... | inj₁ x = begin
+      factor if * i0 + 0 ≡⟨ +-comm _ 0 ⟩
+      factor if * i0  ≡⟨ cong (λ k → k * i0) x  ⟩
+      0 ∎   where open ≡-Reasoning
+    ... | inj₂ y = begin
+      factor if * i0 + 0 ≡⟨ +-comm _ 0 ⟩
+      factor if * i0  ≡⟨ cong (λ k → factor if * k) y  ⟩
+      factor if * 0  ≡⟨ *-comm (factor if) 0  ⟩
+      0 ∎   where open ≡-Reasoning
+gcd-divable (suc (suc i)) i0 zero (suc j0) if jf if=0 jf=0 with gcd-divable (suc i) (suc (suc i)) j0 (suc j0) {!!} {!!} refl refl
+... | t = ⟪ {!!} , {!!} ⟫
+gcd-divable (suc zero) i0 (suc j) j0 if jf if=0 jf=0 =  
+     gcd-divable zero i0 j j0 record {  factor = factor if ; is-factor = gg4 ; remain = j - zero }
+                              record {  factor = factor jf ; is-factor = gg5 ; remain = zero - j  } refl refl where
+    gg4 : factor if * i0 + (j - zero) ≡ j0
+    gg4 = begin
+      factor if * i0 + (j - zero)  ≡⟨  cong ( λ k → factor if * i0 + k) (sym if=0) ⟩
+      factor if * i0 + remain if ≡⟨ is-factor if   ⟩
+      j0 ∎   where open ≡-Reasoning  
+    gg5 : factor jf * j0 + (zero - j) ≡ i0
+    gg5 = begin
+      factor jf * j0 + (zero - j)  ≡⟨  cong ( λ k → factor jf * j0 + k) (sym jf=0) ⟩
+      factor jf * j0 + remain jf ≡⟨ is-factor jf   ⟩
+      i0 ∎   where open ≡-Reasoning  
+gcd-divable (suc (suc i)) i0 (suc j) j0 if jf if=0 jf=0 = 
+     gcd-divable (suc i) i0 j j0 record {  factor = factor if ; is-factor = gg4 ; remain = j - suc i }
+                              record {  factor = factor jf ; is-factor = gg5 ; remain = suc i - j } refl refl where
+    gg4 : factor if * i0 + (j - suc i ) ≡ j0
+    gg4 = begin
+      factor if * i0 + ( j - suc i ) ≡⟨ cong ( λ k → factor if * i0 + k ) (sym if=0) ⟩ 
+      factor if * i0 + remain if  ≡⟨ is-factor if   ⟩
+      j0 ∎   where open ≡-Reasoning  
+    gg5 : factor jf * j0 + (suc i - j) ≡ i0
+    gg5 = begin
+      factor jf * j0 + ( suc i - j ) ≡⟨ cong ( λ k → factor jf * j0 + k ) (sym jf=0) ⟩  
+      factor jf * j0 + remain jf  ≡⟨ is-factor jf   ⟩
+      i0 ∎   where open ≡-Reasoning  
+
 gcd22 : ( i i0 o o0 : ℕ ) → gcd1 (suc i) i0 (suc o) o0 ≡ gcd1 i i0 o o0
 gcd22 zero i0 zero o0 = refl
 gcd22 zero i0 (suc o) o0 = refl
diff -r e97cf4fb67fa -r f1370437c68e automaton-in-agda/src/logic.agda
--- a/automaton-in-agda/src/logic.agda	Fri Jun 18 21:09:50 2021 +0900
+++ b/automaton-in-agda/src/logic.agda	Sat Jun 19 10:54:51 2021 +0900
@@ -23,6 +23,13 @@
 _⇔_ : {n m : Level } → ( A : Set n ) ( B : Set m )  → Set (n ⊔ m)
 _⇔_ A B =  ( A → B ) ∧ ( B → A )
 
+∧-exch : {n m : Level} {A  : Set n} { B : Set m } → A ∧ B → B ∧ A
+∧-exch p = ⟪ _∧_.proj2 p , _∧_.proj1 p ⟫
+
+∨-exch : {n m : Level} {A  : Set n} { B : Set m } → A ∨ B → B ∨ A
+∨-exch (case1 x) = case2 x
+∨-exch (case2 x) = case1 x
+
 contra-position : {n m : Level } {A : Set n} {B : Set m} → (A → B) → ¬ B → ¬ A
 contra-position {n} {m} {A} {B}  f ¬b a = ¬b ( f a )
 
diff -r e97cf4fb67fa -r f1370437c68e automaton-in-agda/src/nat.agda
--- a/automaton-in-agda/src/nat.agda	Fri Jun 18 21:09:50 2021 +0900
+++ b/automaton-in-agda/src/nat.agda	Sat Jun 19 10:54:51 2021 +0900
@@ -200,6 +200,12 @@
 
 open import Data.Product
 
+i-j=0→i=j : {i j  : ℕ } → j ≤ i  → i - j ≡ 0 → i ≡ j
+i-j=0→i=j {zero} {zero} _ refl = refl
+i-j=0→i=j {zero} {suc j} () refl
+i-j=0→i=j {suc i} {zero} z≤n ()
+i-j=0→i=j {suc i} {suc j} (s≤s lt) eq = cong suc (i-j=0→i=j {i} {j} lt eq)
+
 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