# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1624850944 -32400
# Node ID 41fd713c07ad0cdb9d38b3f784acbeee1ef8eafd
# Parent  ec404f567e5138db6f4b3bcbabc55b4c42284d8f
...

diff -r ec404f567e51 -r 41fd713c07ad automaton-in-agda/src/gcd.agda
--- a/automaton-in-agda/src/gcd.agda	Mon Jun 28 10:32:51 2021 +0900
+++ b/automaton-in-agda/src/gcd.agda	Mon Jun 28 12:29:04 2021 +0900
@@ -522,7 +522,7 @@
             ; ind = λ {p} prev → ind (proj1 p ) ( proj2 p ) prev
           } 
 
-record Equlid (i j gcd : ℕ ) : Set where
+record Euclid (i j gcd : ℕ ) : Set where
   field
     eqa : ℕ
     eqb : ℕ
@@ -530,60 +530,79 @@
     is-equ> : (eqb * j) > (eqa * i) → ((eqb * j) - (eqa * i) ≡ gcd  )
 
 postulate 
-   gcd-equlid : ( p q r : ℕ )  → 1 < p  → ((i : ℕ ) → i < p → 0 < i   → gcd p i ≡ 1)  →  Dividable p (q * r)  → Dividable p q ∨ Dividable p r
---   gcd-equlid1 : ( i i0 j j0 : ℕ )  → Dividable i0  ((j0 + i) - j ) ∧ Dividable j0 ((i0 + j) - i) → Equlid i0 j0 (gcd1 i i0 j j0)
+   gcd-euclid : ( p q r : ℕ )  → 1 < p  → ((i : ℕ ) → i < p → 0 < i   → gcd p i ≡ 1)  →  Dividable p (q * r)  → Dividable p q ∨ Dividable p r
+--   gcd-euclid1 : ( i i0 j j0 : ℕ )  → Dividable i0  ((j0 + i) - j ) ∧ Dividable j0 ((i0 + j) - i) → Euclid i0 j0 (gcd1 i i0 j j0)
 
 ge3 : {a b c d : ℕ } → b > a → b - a ≡ d - c → d > c
 ge3 {a} {b} {c} {d} b>a eq = minus>0→x<y (subst (λ k → 0 < k ) eq (minus>0 b>a))
 
-ge00 : ( i0 j j0 ea eb : ℕ )  
+ge01 : ( i0 j j0 ea eb : ℕ )  
    → ( di : GCD 0 (suc i0) (suc (suc j)) j0 )
-  → (ea + eb * (Dividable.factor (GCD.div-i di))) * suc i0 > eb * j0
-  → Equlid (suc i0)  (suc (suc j)) (gcd1 i0 (suc i0) (suc j) (suc (suc j)))
-  → (((ea + eb * (Dividable.factor (GCD.div-i di))) * suc i0) - (eb * j0)) ≡  gcd1 i0 (suc i0) (suc j) (suc (suc j))
-ge00 i0 j j0 ea eb di lt e = ge2 lt where
+  →  (((ea + eb * (Dividable.factor (GCD.div-i di))) * suc i0)  ≡ (ea * suc i0) + (eb * (Dividable.factor (GCD.div-i di)) ) * suc i0 )
+        ∧ (  (eb * j0) ≡ (eb * suc (suc j) +  (eb * (Dividable.factor (GCD.div-i di)) ) * suc i0) )
+ge01 i0 j j0 ea eb di  = ⟪ ge011 , ge012 ⟫ where
    f = Dividable.factor (GCD.div-i di)
    ge4 :  suc (j0 + 0) > suc (suc j)
    ge4 = subst (λ k → k > suc (suc j)) (+-comm 0 _ ) ( s≤s (GCD.j<j0  di ))
-   ge1 : ((ea + eb * f) * suc i0) - (eb * j0)  ≡ (ea * suc i0) - (eb * suc (suc j))       
-   ge1  = begin
-      ((ea + eb * f ) * suc i0) - (eb * j0)  ≡⟨ cong (λ k →  ((ea + eb * f ) * suc i0) - (eb * k)) (+-comm 0 _) ⟩ 
-      ((ea + eb * f ) * suc i0) - (eb * (j0 + 0) )  ≡⟨ cong (λ k →  ((ea + eb * f ) * suc i0) - (eb * k)) (sym (minus+n {j0 + 0} {suc (suc j)} ge4 )) ⟩ 
-      ((ea + eb * f ) * suc i0) - (eb * (((j0 + 0) -  suc (suc j)) + suc (suc j)  )) ≡⟨ cong (λ k →  ((ea + eb * f ) * suc i0) - (eb * k)) (+-comm _ (suc (suc j)) ) ⟩
-      ((ea + eb * f ) * suc i0) - (eb * (suc (suc j) + ((j0 + 0) -  suc (suc j))))
-              ≡⟨ cong (λ k → ((ea + eb * f ) * suc i0) - (eb * (suc (suc j) + k) )) (sym (Dividable.is-factor (GCD.div-i di))) ⟩ 
-      ((ea + eb * f ) * suc i0) - (eb * (suc (suc j) + (f * suc i0 + 0) )) ≡⟨ cong (λ k →  ((ea + eb * f ) * suc i0) - (eb * (suc (suc j) + k))) (+-comm _ 0) ⟩ 
-      ((ea + eb * f ) * suc i0) - (eb * (suc (suc j) + (f * suc i0 ) )) ≡⟨ cong (λ k →  ((ea + eb * f ) * suc i0) - k) (*-distribˡ-+  eb (suc (suc j)) (f * suc i0)) ⟩ 
-      ((ea + eb * f ) * suc i0) - (eb * suc (suc j) + eb * (f * suc i0)) ≡⟨ cong (λ k → k - (eb * suc (suc j) + eb * (f * suc i0))) (*-distribʳ-+ (suc i0)  ea  _) ⟩ 
-      (ea * suc i0 + (eb * f ) * suc i0 ) - ( eb * suc (suc j) + (eb * (f * (suc i0))) )
-           ≡⟨ cong (λ k →  (ea * suc i0 + (eb * f ) * suc i0 ) - ( eb * suc (suc j) + k )) (sym (*-assoc eb _ _ )) ⟩ 
-      (ea * suc i0 + (eb * f ) * suc i0 ) - ( eb * suc (suc j) + ((eb * f) * (suc i0)) )   ≡⟨ minus+xy-zy {ea * suc i0} {(eb * f ) * suc i0} {eb * suc (suc j)}  ⟩ 
-      (ea * suc i0) - (eb * suc (suc j)) ∎ where open ≡-Reasoning
-   ge2 : {!!} → ((ea + eb * f) * suc i0) - (eb * j0)  ≡ gcd1 i0 (suc i0) (suc j) (suc (suc j))
-   ge2 lt =  subst (λ k → ((ea + eb * f) * suc i0) - (eb * j0) ≡ k ) (Equlid.is-equ< e (ge3 lt {!!})) {!!} 
+   ge011 :   (ea + eb * f) * suc i0 ≡ ea * suc i0 + eb * f * suc i0
+   ge011 = begin
+      (ea + eb * f) * suc i0 ≡⟨ *-distribʳ-+ (suc i0)  ea  _ ⟩ 
+      ea * suc i0 + eb * f * suc i0 ∎ where open ≡-Reasoning
+   ge012 :  eb * j0 ≡ eb * suc (suc j) + eb * f * suc i0
+   ge012 = begin
+      eb * j0  ≡⟨ cong (λ k → eb * k) ( begin
+        j0 ≡⟨ +-comm 0 _ ⟩ 
+        j0 + 0 ≡⟨ sym (minus+n {j0 + 0} {suc (suc j)} ge4)  ⟩ 
+        ((j0 + 0) - (suc (suc j))) + suc (suc j) ≡⟨  +-comm _ (suc (suc j)) ⟩ 
+        suc (suc j) + ((j0 + 0) -  suc (suc j)) ≡⟨ cong (λ k → suc (suc j) + k ) (sym (Dividable.is-factor (GCD.div-i di))) ⟩ 
+        suc (suc j) + (f * suc i0 + 0) ≡⟨  cong (λ k → suc (suc j) + k )  ( +-comm _ 0  ) ⟩ 
+        suc (suc j) + (f * suc i0 )  ∎  ) ⟩ 
+      eb * (suc (suc j) + (f * suc i0 ) ) ≡⟨ *-distribˡ-+  eb (suc (suc j)) (f * suc i0) ⟩ 
+      eb * suc (suc j) + eb * (f * suc i0) ≡⟨ cong (λ k → eb * suc (suc j) + k ) ((sym (*-assoc eb _ _ )) ) ⟩ 
+      eb * suc (suc j) + eb * f * suc i0 ∎ where open ≡-Reasoning
 
-gcd-equlid1 : ( i i0 j j0 : ℕ )  → GCD i i0 j j0  → Equlid i0 j0 (gcd1 i i0 j j0)
-gcd-equlid1 zero i0 zero j0 di with <-cmp i0 j0
+
+gcd-euclid1 : ( i i0 j j0 : ℕ )  → GCD i i0 j j0  → Euclid i0 j0 (gcd1 i i0 j j0)
+gcd-euclid1 zero i0 zero j0 di with <-cmp i0 j0
 ... | tri< a' ¬b ¬c = record { eqa = 1 ; eqb = 0 ; is-equ< = {!!} ; is-equ> = {!!}  }
 ... | tri≈ ¬a refl ¬c = record { eqa = 1 ; eqb = 0 ; is-equ< = {!!} ; is-equ> = {!!} } 
 ... | tri> ¬a ¬b c = record { eqa = 0 ; eqb = 1 ;  is-equ< = {!!} ; is-equ> = {!!} }
-gcd-equlid1 zero i0 (suc zero) j0 di = record { eqa = 1 ; eqb = 1 ; is-equ< = {!!} ; is-equ> = {!!} } 
-gcd-equlid1 zero zero (suc (suc j)) j0 di = record { eqa = 0 ; eqb = 1 ; is-equ< = {!!} ; is-equ> = {!!} } 
-gcd-equlid1 zero (suc i0) (suc (suc j)) j0 di with gcd-equlid1 i0 (suc i0) (suc j) (suc (suc j)) ( gcd-next1 di )
+gcd-euclid1 zero i0 (suc zero) j0 di = record { eqa = 1 ; eqb = 1 ; is-equ< = {!!} ; is-equ> = {!!} } 
+gcd-euclid1 zero zero (suc (suc j)) j0 di = record { eqa = 0 ; eqb = 1 ; is-equ< = {!!} ; is-equ> = {!!} } 
+gcd-euclid1 zero (suc i0) (suc (suc j)) j0 di with gcd-euclid1 i0 (suc i0) (suc j) (suc (suc j)) ( gcd-next1 di )
 ... | e = record { eqa = ea + eb * f ; eqb =  eb
-      ;  is-equ< = λ lt → ge00 i0 j j0 ea eb di lt e ; is-equ> = {!!} } where
-   ea = Equlid.eqa e 
-   eb = Equlid.eqb e
+      ;  is-equ< =  λ lt → subst (λ k → ((ea + eb * f) * suc i0) - (eb * j0) ≡ k ) (Euclid.is-equ< e (ge3 lt (ge1 ))) (ge1 )
+      ;  is-equ> =  λ lt → subst (λ k → (eb * j0) - ((ea + eb * f) * suc i0) ≡ k ) (Euclid.is-equ> e (ge3 lt (ge2 ))) (ge2 ) } where
+   ea = Euclid.eqa e 
+   eb = Euclid.eqb e
    f = Dividable.factor (GCD.div-i di)
-
-gcd-equlid1 (suc zero) i0 zero j0 di = {!!} 
-gcd-equlid1 (suc (suc i)) i0 zero zero di = {!!}
-gcd-equlid1 (suc (suc i)) i0 zero (suc j0) di with gcd-equlid1 (suc i) (suc (suc i)) j0 (suc j0) (GCD-sym (gcd-next1 (GCD-sym di)))
-... | e = {!!}
-gcd-equlid1 (suc zero) i0 (suc j) j0 di =
-     gcd-equlid1 zero i0 j j0  (gcd-next di)
-gcd-equlid1 (suc (suc i)) i0 (suc j) j0  di = 
-     gcd-equlid1 (suc i) i0 j j0 (gcd-next di)
+   ge1 : ((ea + eb * f) * suc i0) - (eb * j0)  ≡ (ea * suc i0) - (eb * suc (suc j))       
+   ge1 = begin
+      ((ea + eb * f) * suc i0) - (eb * j0) ≡⟨ cong₂ (λ j k → j - k ) (proj1 (ge01  i0 j j0 ea eb di)) (proj2 (ge01  i0 j j0 ea eb di))  ⟩
+      (ea * suc i0 + (eb * f ) * suc i0 ) - ( eb * suc (suc j) + ((eb * f) * (suc i0)) )  ≡⟨ minus+xy-zy {ea * suc i0} {(eb * f ) * suc i0} {eb * suc (suc j)}  ⟩
+      (ea * suc i0) - (eb * suc (suc j)) ∎ where open ≡-Reasoning
+   ge2 : (eb * j0) - ((ea + eb * f) * suc i0)  ≡  (eb * suc (suc j)) - (ea * suc i0)
+   ge2 = begin
+      (eb * j0) - ((ea + eb * f) * suc i0)  ≡⟨ cong₂ (λ j k → j - k ) (proj2 (ge01  i0 j j0 ea eb di)) (proj1 (ge01  i0 j j0 ea eb di))  ⟩
+      ( eb * suc (suc j) + ((eb * f) * (suc i0)) ) - (ea * suc i0 + (eb * f ) * suc i0 )   ≡⟨  minus+xy-zy {eb * suc (suc j)}{(eb * f ) * suc i0} {ea * suc i0}  ⟩
+      (eb * suc (suc j)) - (ea * suc i0)   ∎ where open ≡-Reasoning
+gcd-euclid1 (suc zero) i0 zero j0 di = {!!} 
+gcd-euclid1 (suc (suc i)) i0 zero zero di = {!!}
+gcd-euclid1 (suc (suc i)) i0 zero (suc j0) di with gcd-euclid1 (suc i) (suc (suc i)) j0 (suc j0) (GCD-sym (gcd-next1 (GCD-sym di)))
+... | e =  record { eqa = ea ; eqb =  eb + ea * f 
+      ;  is-equ< =  λ lt → subst (λ k → ((ea * i0) - ((eb + ea * f) * suc j0))  ≡ k ) (Euclid.is-equ< e (ge3 lt ge4)) ge4 
+      ;  is-equ> =  λ lt → subst (λ k →  (((eb + ea * f) * suc j0) - (ea * i0)) ≡ k ) (Euclid.is-equ> e (ge3 lt ge5)) ge5 } where
+   ea = Euclid.eqa e 
+   eb = Euclid.eqb e
+   f = Dividable.factor (GCD.div-i di)
+   ge5 : (((eb + ea * f) * suc j0) - (ea * i0)) ≡ ((eb * suc j0) - (ea * suc (suc i)))
+   ge5 = {!!}
+   ge4 : ((ea * i0) - ((eb + ea * f) * suc j0)) ≡ ((ea * suc (suc i)) - (eb * suc j0))
+   ge4 = {!!}
+gcd-euclid1 (suc zero) i0 (suc j) j0 di =
+     gcd-euclid1 zero i0 j j0  (gcd-next di)
+gcd-euclid1 (suc (suc i)) i0 (suc j) j0  di = 
+     gcd-euclid1 (suc i) i0 j j0 (gcd-next di)
 
 
 div→gcd : {n k : ℕ } → k > 1 → Dividable k n → gcd n k ≡ k