Mercurial > hg > Members > kono > Proof > automaton

changeset 240:ec404f567e51

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 28 Jun 2021 10:32:51 +0900
parents d475257ffe30
children 41fd713c07ad
files automaton-in-agda/src/gcd.agda
diffstat 1 files changed, 6 insertions(+), 5 deletions(-) [+]
line wrap: on
line diff
--- a/automaton-in-agda/src/gcd.agda	Mon Jun 28 10:22:46 2021 +0900
+++ b/automaton-in-agda/src/gcd.agda	Mon Jun 28 10:32:51 2021 +0900
@@ -539,8 +539,9 @@
 ge00 : ( 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
-  → (((ea + eb * (Dividable.factor (GCD.div-i di))) * suc i0) - (eb * j0)) ≡ (ea * suc i0) - (eb * suc (suc j))       
-ge00 i0 j j0 ea eb di lt = ge1 where
+  → 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
    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 ))
@@ -558,6 +559,8 @@
            ≡⟨ 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 {!!})) {!!} 
 
 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
@@ -568,12 +571,10 @@
 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 )
 ... | e = record { eqa = ea + eb * f ; eqb =  eb
-      ;  is-equ< =  λ lt → subst (λ k → ((ea + eb * f) * suc i0) - (eb * j0) ≡ k ) (Equlid.is-equ< e (ge3 lt (ge1 lt))) (ge1 lt) ; is-equ> = {!!} } where
+      ;  is-equ< = λ lt → ge00 i0 j j0 ea eb di lt e ; is-equ> = {!!} } where
    ea = Equlid.eqa e 
    eb = Equlid.eqb e
    f = Dividable.factor (GCD.div-i di)
-   ge1 : (ea + eb * Dividable.factor (GCD.div-i di)) * suc i0 > eb * j0 → ((ea + eb * f) * suc i0) - (eb * j0)  ≡ (ea * suc i0) - (eb * suc (suc j))       
-   ge1 lt = ge00  i0 j j0 ea eb di lt
 
 gcd-equlid1 (suc zero) i0 zero j0 di = {!!} 
 gcd-equlid1 (suc (suc i)) i0 zero zero di = {!!}