Mercurial > hg > Members > kono > Proof > automaton

comparison automaton-in-agda/src/gcd.agda @ 205:e97cf4fb67fa

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 Fri, 18 Jun 2021 21:09:50 +0900
parents 4a83abf7b822
children f1370437c68e
comparison
equal deleted inserted replaced
204:a366f36b1ce9 205:e97cf4fb67fa
37 --divdable^2 n k dn2 = {!!} 37 --divdable^2 n k dn2 = {!!}
38 38
39 decf : { n k : ℕ } → ( x : Factor k (suc n) ) → Factor k n 39 decf : { n k : ℕ } → ( x : Factor k (suc n) ) → Factor k n
40 decf {n} {k} record { factor = f ; remain = r ; is-factor = fa } = 40 decf {n} {k} record { factor = f ; remain = r ; is-factor = fa } =
41 decf1 {n} {k} f r fa where 41 decf1 {n} {k} f r fa where
42 dr : ( n k : ℕ ) → (f r : ℕ) → ℕ
43 dr n zero (suc f) zero = 0
44 dr n (suc k) (suc f) zero = k
45 dr n k f (suc r) = r
46 dr n zero zero zero = r
47 dr n (suc k) zero zero = r
48 decf1 : { n k : ℕ } → (f r : ℕ) → (f * k + r ≡ suc n) → Factor k n 42 decf1 : { n k : ℕ } → (f r : ℕ) → (f * k + r ≡ suc n) → Factor k n
49 decf1 {n} {k} f (suc r) fa = -- this case must be the first 43 decf1 {n} {k} f (suc r) fa = -- this case must be the first
50 record { factor = f ; remain = r ; is-factor = ( begin -- fa : f * k + suc r ≡ suc n 44 record { factor = f ; remain = r ; is-factor = ( begin -- fa : f * k + suc r ≡ suc n
51 f * k + r ≡⟨ cong pred ( begin 45 f * k + r ≡⟨ cong pred ( begin
52 suc ( f * k + r ) ≡⟨ +-comm _ r ⟩ 46 suc ( f * k + r ) ≡⟨ +-comm _ r ⟩
286 280
287 div+1 : { i k : ℕ } → k > 1 → Dividable k i → ¬ Dividable k (suc i) 281 div+1 : { i k : ℕ } → k > 1 → Dividable k i → ¬ Dividable k (suc i)
288 div+1 {i} {k} k>1 d d1 = div1 k>1 div+11 where 282 div+1 {i} {k} k>1 d d1 = div1 k>1 div+11 where
289 div+11 : Dividable k 1 283 div+11 : Dividable k 1
290 div+11 = subst (λ g → Dividable k g) (minus+y-y {1} {i} ) ( proj2 (div-div k>1 d d1 ) ) 284 div+11 = subst (λ g → Dividable k g) (minus+y-y {1} {i} ) ( proj2 (div-div k>1 d d1 ) )
285
286 gcd>0 : ( i j : ℕ ) → 0 < i → 0 < j → 0 < gcd i j
287 gcd>0 i j 0<i 0<j = gcd>01 i i j j 0<i 0<j where
288 gcd>01 : ( i i0 j j0 : ℕ ) → 0 < i0 → 0 < j0 → gcd1 i i0 j j0 > 0
289 gcd>01 zero i0 zero j0 0<i 0<j with <-cmp i0 j0
290 ... | tri< a ¬b ¬c = 0<i
291 ... | tri≈ ¬a refl ¬c = 0<i
292 ... | tri> ¬a ¬b c = 0<j
293 gcd>01 zero i0 (suc zero) j0 0<i 0<j = s≤s z≤n
294 gcd>01 zero zero (suc (suc j)) j0 0<i 0<j = 0<j
295 gcd>01 zero (suc i0) (suc (suc j)) j0 0<i 0<j = gcd>01 i0 (suc i0) (suc j) (suc (suc j)) 0<i (s≤s z≤n) -- 0 < suc (suc j)
296 gcd>01 (suc zero) i0 zero j0 0<i 0<j = s≤s z≤n
297 gcd>01 (suc (suc i)) i0 zero zero 0<i 0<j = 0<i
298 gcd>01 (suc (suc i)) i0 zero (suc j0) 0<i 0<j = gcd>01 (suc i) (suc (suc i)) j0 (suc j0) (s≤s z≤n) 0<j
299 gcd>01 (suc i) i0 (suc j) j0 0<i 0<j = subst (λ k → 0 < k ) (sym (gcd033 i i0 j j0 )) (gcd>01 i i0 j j0 0<i 0<j ) where
300 gcd033 : (i i0 j j0 : ℕ) → gcd1 (suc i) i0 (suc j) j0 ≡ gcd1 i i0 j j0
301 gcd033 zero zero zero zero = refl
302 gcd033 zero zero (suc j) zero = refl
303 gcd033 (suc i) zero j zero = refl
304 gcd033 zero zero zero (suc j0) = refl
305 gcd033 (suc i) zero zero (suc j0) = refl
306 gcd033 zero zero (suc j) (suc j0) = refl
307 gcd033 (suc i) zero (suc j) (suc j0) = refl
308 gcd033 zero (suc i0) j j0 = refl
309 gcd033 (suc i) (suc i0) j j0 = refl