Mercurial > hg > Members > kono > Proof > automaton
comparison agda/gcd.agda @ 164:bee86ee07fff
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 12 Mar 2021 21:45:53 +0900 |
| parents | 690a8352c1ad |
| children | 6cb442050825 |
comparison
equal
deleted
inserted
replaced
| 163:26407ce19d66 | 164:bee86ee07fff |
|---|---|
| 24 gcd1 (suc (suc i)) i0 zero (suc j0) = gcd1 (suc i) (suc (suc i)) j0 (suc j0) | 24 gcd1 (suc (suc i)) i0 zero (suc j0) = gcd1 (suc i) (suc (suc i)) j0 (suc j0) |
| 25 gcd1 (suc i) i0 (suc j) j0 = gcd1 i i0 j j0 | 25 gcd1 (suc i) i0 (suc j) j0 = gcd1 i i0 j j0 |
| 26 | 26 |
| 27 gcd : ( i j : ℕ ) → ℕ | 27 gcd : ( i j : ℕ ) → ℕ |
| 28 gcd i j = gcd1 i i j j | 28 gcd i j = gcd1 i i j j |
| 29 | |
| 30 record Factor (n m : ℕ ) : Set where | |
| 31 field | |
| 32 -- n<m : n ≤ m | |
| 33 factor : ℕ | |
| 34 remain : ℕ | |
| 35 is-factor : factor * n + remain ≡ m | |
| 36 | |
| 37 open Factor | |
| 38 | |
| 39 open ≡-Reasoning | |
| 40 | |
| 41 decf : { n k : ℕ } → ( x : Factor k (suc n) ) → Factor k n | |
| 42 decf {n} {k} x with remain x | |
| 43 ... | zero = record { factor = factor x ; remain = k ; is-factor = {!!} } | |
| 44 ... | suc r = record { factor = factor x ; remain = r ; is-factor = {!!} } | |
| 45 | |
| 46 ifk0 : ( i0 k : ℕ ) → (i0f : Factor k i0 ) → ( i0=0 : remain i0f ≡ 0 ) → factor i0f * k + 0 ≡ i0 | |
| 47 ifk0 i0 k i0f i0=0 = begin | |
| 48 factor i0f * k + 0 ≡⟨ cong (λ m → factor i0f * k + m) (sym i0=0) ⟩ | |
| 49 factor i0f * k + remain i0f ≡⟨ is-factor i0f ⟩ | |
| 50 i0 ∎ | |
| 51 | |
| 52 ifzero : {k : ℕ } → (jf : Factor k zero ) → remain jf ≡ 0 | |
| 53 ifzero = {!!} | |
| 54 | |
| 55 gcd-gt : ( i i0 j j0 k : ℕ ) → (if : Factor k i) (i0f : Factor k i0 ) (jf : Factor k i ) (j0f : Factor k j0) | |
| 56 → remain i0f ≡ 0 → remain j0f ≡ 0 | |
| 57 → (remain if + i ) ≡ i0 → (remain jf + j ) ≡ j0 | |
| 58 → Factor k ( gcd1 i i0 j j0 ) | |
| 59 gcd-gt zero i0 zero j0 k if i0f jf j0f i0=0 j0=0 ir=i0 jr=j0 with <-cmp i0 j0 | |
| 60 ... | tri< a ¬b ¬c = record { factor = factor i0f ; remain = 0 ; is-factor = ifk0 i0 k i0f i0=0 } | |
| 61 ... | tri≈ ¬a refl ¬c = record { factor = factor i0f ; remain = 0 ; is-factor = ifk0 i0 k i0f i0=0 } | |
| 62 ... | tri> ¬a ¬b c = record { factor = factor j0f ; remain = 0 ; is-factor = ifk0 j0 k j0f j0=0 } | |
| 63 gcd-gt zero i0 (suc zero) j0 k if i0f jf j0f i0=0 j0=0 ir=i0 jr=j0 = {!!} -- can't happen | |
| 64 gcd-gt zero zero (suc (suc j)) j0 k if i0f jf j0f i0=0 j0=0 ir=i0 jr=j0 = record { factor = factor j0f ; remain = 0 ; is-factor = ifk0 j0 k j0f j0=0 } | |
| 65 gcd-gt zero (suc i0) (suc (suc j)) j0 k if i0f jf j0f i0=0 j0=0 ir=i0 jr=j0 = | |
| 66 gcd-gt i0 (suc i0) (suc j) (suc (suc j)) k (decf i0f) i0f (decf i0f) | |
| 67 record { factor = factor jf ; remain = remain jf ; is-factor = {!!} } i0=0 {!!} {!!} {!!} | |
| 68 gcd-gt (suc zero) i0 zero j0 k if i0f jf j0f i0=0 j0=0 ir=i0 jr=j0 = {!!} -- can't happen | |
| 69 gcd-gt (suc (suc i)) i0 zero zero k if i0f jf j0f i0=0 j0=0 ir=i0 jr=j0 = {!!} | |
| 70 gcd-gt (suc (suc i)) i0 zero (suc j0) k if i0f jf j0f i0=0 j0=0 ir=i0 jr=j0 = {!!} | |
| 71 gcd-gt (suc i) i0 (suc j) j0 k if i0f jf j0f i0=0 j0=0 ir=i0 jr=j0 = {!!} -- gcd-gt i i0 j j0 k (decf if) i0f (decf jf) j0f ? ? ? ? | |
| 29 | 72 |
| 30 -- gcd26 : { n m : ℕ} → n > 1 → m > 1 → n - m > 0 → gcd n m ≡ gcd (n - m) m | 73 -- gcd26 : { n m : ℕ} → n > 1 → m > 1 → n - m > 0 → gcd n m ≡ gcd (n - m) m |
| 31 -- gcd27 : { n m : ℕ} → n > 1 → m > 1 → n - m > 0 → gcd n k ≡ k → k ≤ n | 74 -- gcd27 : { n m : ℕ} → n > 1 → m > 1 → n - m > 0 → gcd n k ≡ k → k ≤ n |
| 32 | 75 |
| 33 gcd22 : ( i i0 o o0 : ℕ ) → gcd1 (suc i) i0 (suc o) o0 ≡ gcd1 i i0 o o0 | 76 gcd22 : ( i i0 o o0 : ℕ ) → gcd1 (suc i) i0 (suc o) o0 ≡ gcd1 i i0 o o0 |