Mercurial > hg > Members > kono > Proof > automaton

changeset 244:08994de7c82f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
gcd-euclid1 done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 28 Jun 2021 17:22:56 +0900
parents ea3d184c4b1f
children 186b66d56ab5
files automaton-in-agda/src/gcd.agda
diffstat 1 files changed, 21 insertions(+), 29 deletions(-) [+]
line wrap: on
line diff
--- a/automaton-in-agda/src/gcd.agda	Mon Jun 28 16:26:44 2021 +0900
+++ b/automaton-in-agda/src/gcd.agda	Mon Jun 28 17:22:56 2021 +0900
@@ -355,28 +355,6 @@
 gcd-next1 {i0} {j} {j0} g = record { i<i0 = refl-≤s ; j<j0 = refl-≤s
   ; div-i = proj1 (di-next1 ⟪ GCD.div-i g , GCD.div-j g ⟫ ) ; div-j = proj2 (di-next1 ⟪ GCD.div-i g , GCD.div-j g ⟫ ) }
 
--- i<i0  : zero ≤ i0
--- j<j0  : 1 ≤ j0
--- div-i : Dividable i0 ((j0 + zero) - 1)  -- fi * i0 ≡ (j0 + zero) - 1
--- div-j : Dividable j0 ((i0 + 1) - zero) --  fj * j0 ≡ (i0 + 1) - zero
-gcd-01 : {i0 j0 : ℕ } → (d : GCD zero i0 1 j0 ) → Dividable.factor (GCD.div-i d) ≡ 1
-gcd-01 {i0} {j0} d with <-cmp (Dividable.factor (GCD.div-i d)) 1
-... | tri< a ¬b ¬c = ⊥-elim ( nat-≡< {!!} (GCD.j<j0 d)) where
-   ge003 : 0 ≡ j0
-   ge003 = sym ( begin
-              j0 ≡⟨ {!!} ⟩
-              (( j0 + 0 ) - 1) + 1 ≡⟨ {!!} ⟩
-              {!!} * i0  ≡⟨ {!!} ⟩
-              0 * i0  ≡⟨ {!!} ⟩
-              0 ∎ ) 
-           where open ≡-Reasoning
-... | tri≈ ¬a b ¬c = b
-... | tri> ¬a ¬b c = {!!}  where --    ((j0 + zero) - 1) * fj ≡ ((i0 + 1) - zero) * fi → fi > 1 → fj ≡ 0
-                                 --
-   ge004 : Dividable.factor (GCD.div-i d) ≡ 0
-   ge004 = {!!}
-   ge005 : Dividable.factor (GCD.div-i d) ≡ 0 →  Dividable.factor (GCD.div-j d) ≡ 0
-   ge005 = {!!}
 
 -- gcd-dividable1 : ( i i0 j j0 : ℕ )
 --      → Dividable i0  (j0 + i - j ) ∨ Dividable j0 (i0 + j - i)
@@ -594,12 +572,17 @@
 -- j<j0  : 1 ≤ j0
 -- div-i : Dividable i0 ((j0 + zero) - 1)  -- fi * i0 ≡ (j0 + zero) - 1
 -- div-j : Dividable j0 ((i0 + 1) - zero) --  fj * j0 ≡ (i0 + 1) - zero
-gcd-euclid1 zero i0 (suc zero) j0 di = record { eqa = 1 ; eqb = 1 ; is-equ< = {!!} ; is-equ> = {!!} } where
-   ge6 :  i0 > j0 → i0 - j0 ≡ gcd1 zero i0 1 j0
-   ge6 i0>j0 =  begin
-       i0 - j0   ≡⟨  {!!}  ⟩
+gcd-euclid1 zero i0 (suc zero) j0 di = record { eqa = 1 ; eqb = Dividable.factor (GCD.div-j di) ; is-equ< = λ lt → ⊥-elim ( ge7 lt) ; is-equ> = λ _ → ge6 } where
+   ge6 :  (Dividable.factor (GCD.div-j di) * j0) - (1 * i0) ≡ gcd1 zero i0 1 j0
+   ge6  =  begin
+        (Dividable.factor (GCD.div-j di) * j0) - (1 * i0)   ≡⟨  cong (λ k → k  - (1 * i0)) (+-comm 0 _)  ⟩
+        (Dividable.factor (GCD.div-j di) * j0 + 0) - (1 * i0)   ≡⟨ cong (λ k → k  - (1 * i0)) (Dividable.is-factor (GCD.div-j di) )  ⟩
+        ((i0 + 1) - zero) - (1 * i0)   ≡⟨ refl  ⟩
+        (i0 + 1) - (i0 + 0)   ≡⟨ minus+yx-yz {_} {i0} {0}  ⟩
        1   ∎ where open ≡-Reasoning
-gcd-euclid1 zero zero (suc (suc j)) j0 di = record { eqa = 0 ; eqb = 1 ; is-equ< = {!!} ; is-equ> = {!!} } 
+   ge7 : ¬ ( 1 * i0 > Dividable.factor (GCD.div-j di) * j0 )
+   ge7 lt = ⊥-elim ( nat-≡< (sym ( minus<=0 (<to≤ lt))) (subst (λ k → 0 < k) (sym ge6) (s≤s z≤n)))
+gcd-euclid1 zero zero (suc (suc j)) j0 di = record { eqa = 0 ; eqb = 1 ; is-equ< = λ () ; is-equ> = λ _ → +-comm _ 0 } 
 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 → subst (λ k → ((ea + eb * f) * suc i0) - (eb * j0) ≡ k ) (Euclid.is-equ< e (ge3 lt (ge1 ))) (ge1 )
@@ -617,8 +600,17 @@
       (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 zero) i0 zero j0 di = record { eqb = 1 ; eqa = Dividable.factor (GCD.div-i di) ; is-equ> = λ lt → ⊥-elim ( ge7' lt) ; is-equ< = λ _ → ge6' } where
+   ge6' :  (Dividable.factor (GCD.div-i di) * i0) - (1 * j0) ≡ gcd1 (suc zero) i0 zero j0 
+   ge6'  =  begin
+        (Dividable.factor (GCD.div-i di) * i0) - (1 * j0)   ≡⟨  cong (λ k → k  - (1 * j0)) (+-comm 0 _)  ⟩
+        (Dividable.factor (GCD.div-i di) * i0 + 0) - (1 * j0)   ≡⟨ cong (λ k → k  - (1 * j0)) (Dividable.is-factor (GCD.div-i di) )  ⟩
+        ((j0 + 1) - zero) - (1 * j0)   ≡⟨ refl  ⟩
+        (j0 + 1) - (j0 + 0)   ≡⟨ minus+yx-yz {_} {j0} {0}  ⟩
+       1   ∎ where open ≡-Reasoning
+   ge7' : ¬ ( 1 * j0 > Dividable.factor (GCD.div-i di) * i0 )
+   ge7' lt = ⊥-elim ( nat-≡< (sym ( minus<=0 (<to≤ lt))) (subst (λ k → 0 < k) (sym ge6') (s≤s z≤n)))
+gcd-euclid1 (suc (suc i)) i0 zero zero di = record { eqb = 0 ; eqa = 1 ; is-equ> = λ () ; is-equ< = λ _ → +-comm _ 0 }
 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