Mercurial > hg > Members > kono > Proof > automaton
comparison automaton-in-agda/src/gcd.agda @ 183:3fa72793620b
fix
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 13 Jun 2021 20:45:17 +0900 |
| parents | automaton-in-agda/src/agda/gcd.agda@567754463810 |
| children | f9473f83f6e7 |
comparison
equal
deleted
inserted
replaced
| 182:567754463810 | 183:3fa72793620b |
|---|---|
| 1 {-# OPTIONS --allow-unsolved-metas #-} | |
| 2 module gcd where | |
| 3 | |
| 4 open import Data.Nat | |
| 5 open import Data.Nat.Properties | |
| 6 open import Data.Empty | |
| 7 open import Data.Unit using (⊤ ; tt) | |
| 8 open import Relation.Nullary | |
| 9 open import Relation.Binary.PropositionalEquality | |
| 10 open import Relation.Binary.Definitions | |
| 11 open import nat | |
| 12 open import logic | |
| 13 | |
| 14 record Factor (n m : ℕ ) : Set where | |
| 15 field | |
| 16 factor : ℕ | |
| 17 remain : ℕ | |
| 18 is-factor : factor * n + remain ≡ m | |
| 19 | |
| 20 record Dividable (n m : ℕ ) : Set where | |
| 21 field | |
| 22 factor : ℕ | |
| 23 is-factor : factor * n + 0 ≡ m | |
| 24 | |
| 25 open Factor | |
| 26 | |
| 27 open ≡-Reasoning | |
| 28 | |
| 29 decf : { n k : ℕ } → ( x : Factor k (suc n) ) → Factor k n | |
| 30 decf {n} {k} x with remain x | |
| 31 ... | zero = record { factor = factor x ; remain = k ; is-factor = {!!} } | |
| 32 ... | suc r = record { factor = factor x ; remain = r ; is-factor = {!!} } | |
| 33 | |
| 34 ifk0 : ( i0 k : ℕ ) → (i0f : Factor k i0 ) → ( i0=0 : remain i0f ≡ 0 ) → factor i0f * k + 0 ≡ i0 | |
| 35 ifk0 i0 k i0f i0=0 = begin | |
| 36 factor i0f * k + 0 ≡⟨ cong (λ m → factor i0f * k + m) (sym i0=0) ⟩ | |
| 37 factor i0f * k + remain i0f ≡⟨ is-factor i0f ⟩ | |
| 38 i0 ∎ | |
| 39 | |
| 40 ifzero : {k : ℕ } → (jf : Factor k zero ) → remain jf ≡ 0 | |
| 41 ifzero = {!!} | |
| 42 | |
| 43 gcd1 : ( i i0 j j0 : ℕ ) → ℕ | |
| 44 gcd1 zero i0 zero j0 with <-cmp i0 j0 | |
| 45 ... | tri< a ¬b ¬c = i0 | |
| 46 ... | tri≈ ¬a refl ¬c = i0 | |
| 47 ... | tri> ¬a ¬b c = j0 | |
| 48 gcd1 zero i0 (suc zero) j0 = 1 | |
| 49 gcd1 zero zero (suc (suc j)) j0 = j0 | |
| 50 gcd1 zero (suc i0) (suc (suc j)) j0 = gcd1 i0 (suc i0) (suc j) (suc (suc j)) | |
| 51 gcd1 (suc zero) i0 zero j0 = 1 | |
| 52 gcd1 (suc (suc i)) i0 zero zero = i0 | |
| 53 gcd1 (suc (suc i)) i0 zero (suc j0) = gcd1 (suc i) (suc (suc i)) j0 (suc j0) | |
| 54 gcd1 (suc i) i0 (suc j) j0 = gcd1 i i0 j j0 | |
| 55 | |
| 56 gcd : ( i j : ℕ ) → ℕ | |
| 57 gcd i j = gcd1 i i j j | |
| 58 | |
| 59 gcd-gt : ( i i0 j j0 k : ℕ ) → (if : Factor k i) (i0f : Factor k i0 ) (jf : Factor k i ) (j0f : Factor k j0) | |
| 60 → remain i0f ≡ 0 → remain j0f ≡ 0 | |
| 61 → (remain if + i ) ≡ i0 → (remain jf + j ) ≡ j0 | |
| 62 → Dividable k ( gcd1 i i0 j j0 ) | |
| 63 gcd-gt zero i0 zero j0 k if i0f jf j0f i0=0 j0=0 ir=i0 jr=j0 with <-cmp i0 j0 | |
| 64 ... | tri< a ¬b ¬c = record { factor = factor i0f ; is-factor = ifk0 i0 k i0f i0=0 } | |
| 65 ... | tri≈ ¬a refl ¬c = record { factor = factor i0f ; is-factor = ifk0 i0 k i0f i0=0 } | |
| 66 ... | tri> ¬a ¬b c = record { factor = factor j0f ; is-factor = ifk0 j0 k j0f j0=0 } | |
| 67 gcd-gt zero i0 (suc zero) j0 k if i0f jf j0f i0=0 j0=0 ir=i0 jr=j0 = {!!} -- can't happen | |
| 68 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 ; is-factor = ifk0 j0 k j0f j0=0 } | |
| 69 gcd-gt zero (suc i0) (suc (suc j)) j0 k if i0f jf j0f i0=0 j0=0 ir=i0 jr=j0 = | |
| 70 gcd-gt i0 (suc i0) (suc j) (suc (suc j)) k (decf i0f) i0f (decf i0f) | |
| 71 record { factor = factor jf ; remain = remain jf ; is-factor = {!!} } i0=0 {!!} {!!} {!!} | |
| 72 gcd-gt (suc zero) i0 zero j0 k if i0f jf j0f i0=0 j0=0 ir=i0 jr=j0 = {!!} -- can't happen | |
| 73 gcd-gt (suc (suc i)) i0 zero zero k if i0f jf j0f i0=0 j0=0 ir=i0 jr=j0 = {!!} | |
| 74 gcd-gt (suc (suc i)) i0 zero (suc j0) k if i0f jf j0f i0=0 j0=0 ir=i0 jr=j0 = | |
| 75 gcd-gt (suc i) (suc (suc i)) j0 (suc j0) k (decf if) {!!} (decf jf) j0f j0=0 {!!} {!!} {!!} | |
| 76 gcd-gt (suc zero) i0 (suc j) j0 k if i0f jf j0f i0=0 j0=0 ir=i0 jr=j0 = | |
| 77 gcd-gt zero i0 j j0 k (decf if) i0f (decf jf) j0f i0=0 j0=0 {!!} {!!} | |
| 78 gcd-gt (suc (suc i)) i0 (suc j) j0 k if i0f jf j0f i0=0 j0=0 ir=i0 jr=j0 = | |
| 79 gcd-gt (suc i) i0 j j0 k (decf if) i0f (decf jf) j0f i0=0 j0=0 {!!} {!!} | |
| 80 | |
| 81 -- gcd26 : { n m : ℕ} → n > 1 → m > 1 → n - m > 0 → gcd n m ≡ gcd (n - m) m | |
| 82 -- gcd27 : { n m : ℕ} → n > 1 → m > 1 → n - m > 0 → gcd n k ≡ k → k ≤ n | |
| 83 | |
| 84 gcd22 : ( i i0 o o0 : ℕ ) → gcd1 (suc i) i0 (suc o) o0 ≡ gcd1 i i0 o o0 | |
| 85 gcd22 zero i0 zero o0 = refl | |
| 86 gcd22 zero i0 (suc o) o0 = refl | |
| 87 gcd22 (suc i) i0 zero o0 = refl | |
| 88 gcd22 (suc i) i0 (suc o) o0 = refl | |
| 89 | |
| 90 gcd20 : (i : ℕ) → gcd i 0 ≡ i | |
| 91 gcd20 zero = refl | |
| 92 gcd20 (suc i) = gcd201 (suc i) where | |
| 93 gcd201 : (i : ℕ ) → gcd1 i i zero zero ≡ i | |
| 94 gcd201 zero = refl | |
| 95 gcd201 (suc zero) = refl | |
| 96 gcd201 (suc (suc i)) = refl | |
| 97 | |
| 98 gcdmm : (n m : ℕ) → gcd1 n m n m ≡ m | |
| 99 gcdmm zero m with <-cmp m m | |
| 100 ... | tri< a ¬b ¬c = refl | |
| 101 ... | tri≈ ¬a refl ¬c = refl | |
| 102 ... | tri> ¬a ¬b c = refl | |
| 103 gcdmm (suc n) m = subst (λ k → k ≡ m) (sym (gcd22 n m n m )) (gcdmm n m ) | |
| 104 | |
| 105 gcdsym2 : (i j : ℕ) → gcd1 zero i zero j ≡ gcd1 zero j zero i | |
| 106 gcdsym2 i j with <-cmp i j | <-cmp j i | |
| 107 ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = ⊥-elim (nat-<> a a₁) | |
| 108 ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = ⊥-elim (nat-≡< (sym b) a) | |
| 109 ... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c = refl | |
| 110 ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ = ⊥-elim (nat-≡< (sym b) a) | |
| 111 ... | tri≈ ¬a refl ¬c | tri≈ ¬a₁ refl ¬c₁ = refl | |
| 112 ... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c = ⊥-elim (nat-≡< b c) | |
| 113 ... | tri> ¬a ¬b c | tri< a ¬b₁ ¬c = refl | |
| 114 ... | tri> ¬a ¬b c | tri≈ ¬a₁ b ¬c = ⊥-elim (nat-≡< b c) | |
| 115 ... | tri> ¬a ¬b c | tri> ¬a₁ ¬b₁ c₁ = ⊥-elim (nat-<> c c₁) | |
| 116 gcdsym1 : ( i i0 j j0 : ℕ ) → gcd1 i i0 j j0 ≡ gcd1 j j0 i i0 | |
| 117 gcdsym1 zero zero zero zero = refl | |
| 118 gcdsym1 zero zero zero (suc j0) = refl | |
| 119 gcdsym1 zero (suc i0) zero zero = refl | |
| 120 gcdsym1 zero (suc i0) zero (suc j0) = gcdsym2 (suc i0) (suc j0) | |
| 121 gcdsym1 zero zero (suc zero) j0 = refl | |
| 122 gcdsym1 zero zero (suc (suc j)) j0 = refl | |
| 123 gcdsym1 zero (suc i0) (suc zero) j0 = refl | |
| 124 gcdsym1 zero (suc i0) (suc (suc j)) j0 = gcdsym1 i0 (suc i0) (suc j) (suc (suc j)) | |
| 125 gcdsym1 (suc zero) i0 zero j0 = refl | |
| 126 gcdsym1 (suc (suc i)) i0 zero zero = refl | |
| 127 gcdsym1 (suc (suc i)) i0 zero (suc j0) = gcdsym1 (suc i) (suc (suc i))j0 (suc j0) | |
| 128 gcdsym1 (suc i) i0 (suc j) j0 = subst₂ (λ j k → j ≡ k ) (sym (gcd22 i _ _ _)) (sym (gcd22 j _ _ _)) (gcdsym1 i i0 j j0 ) | |
| 129 | |
| 130 gcdsym : { n m : ℕ} → gcd n m ≡ gcd m n | |
| 131 gcdsym {n} {m} = gcdsym1 n n m m | |
| 132 | |
| 133 gcd11 : ( i : ℕ ) → gcd i i ≡ i | |
| 134 gcd11 i = gcdmm i i | |
| 135 | |
| 136 gcd203 : (i : ℕ) → gcd1 (suc i) (suc i) i i ≡ 1 | |
| 137 gcd203 zero = refl | |
| 138 gcd203 (suc i) = gcd205 (suc i) where | |
| 139 gcd205 : (j : ℕ) → gcd1 (suc j) (suc (suc i)) j (suc i) ≡ 1 | |
| 140 gcd205 zero = refl | |
| 141 gcd205 (suc j) = subst (λ k → k ≡ 1) (gcd22 (suc j) (suc (suc i)) j (suc i)) (gcd205 j) | |
| 142 gcd204 : (i : ℕ) → gcd1 1 1 i i ≡ 1 | |
| 143 gcd204 zero = refl | |
| 144 gcd204 (suc zero) = refl | |
| 145 gcd204 (suc (suc zero)) = refl | |
| 146 gcd204 (suc (suc (suc i))) = gcd204 (suc (suc i)) | |
| 147 | |
| 148 gcd2 : ( i j : ℕ ) → gcd (i + j) j ≡ gcd i j | |
| 149 gcd2 i j = gcd200 i i j j refl refl where | |
| 150 gcd202 : (i j1 : ℕ) → (i + suc j1) ≡ suc (i + j1) | |
| 151 gcd202 zero j1 = refl | |
| 152 gcd202 (suc i) j1 = cong suc (gcd202 i j1) | |
| 153 gcd201 : (i i0 j j0 j1 : ℕ) → gcd1 (i + j1) (i0 + suc j) j1 j0 ≡ gcd1 i (i0 + suc j) zero j0 | |
| 154 gcd201 i i0 j j0 zero = subst (λ k → gcd1 k (i0 + suc j) zero j0 ≡ gcd1 i (i0 + suc j) zero j0 ) (+-comm zero i) refl | |
| 155 gcd201 i i0 j j0 (suc j1) = begin | |
| 156 gcd1 (i + suc j1) (i0 + suc j) (suc j1) j0 ≡⟨ cong (λ k → gcd1 k (i0 + suc j) (suc j1) j0 ) (gcd202 i j1) ⟩ | |
| 157 gcd1 (suc (i + j1)) (i0 + suc j) (suc j1) j0 ≡⟨ gcd22 (i + j1) (i0 + suc j) j1 j0 ⟩ | |
| 158 gcd1 (i + j1) (i0 + suc j) j1 j0 ≡⟨ gcd201 i i0 j j0 j1 ⟩ | |
| 159 gcd1 i (i0 + suc j) zero j0 ∎ where open ≡-Reasoning | |
| 160 gcd200 : (i i0 j j0 : ℕ) → i ≡ i0 → j ≡ j0 → gcd1 (i + j) (i0 + j) j j0 ≡ gcd1 i i j0 j0 | |
| 161 gcd200 i .i zero .0 refl refl = subst (λ k → gcd1 k k zero zero ≡ gcd1 i i zero zero ) (+-comm zero i) refl | |
| 162 gcd200 (suc (suc i)) i0 (suc j) (suc j0) i=i0 j=j0 = gcd201 (suc (suc i)) i0 j (suc j0) (suc j) | |
| 163 gcd200 zero zero (suc zero) .1 i=i0 refl = refl | |
| 164 gcd200 zero zero (suc (suc j)) .(suc (suc j)) i=i0 refl = begin | |
| 165 gcd1 (zero + suc (suc j)) (zero + suc (suc j)) (suc (suc j)) (suc (suc j)) ≡⟨ gcdmm (suc (suc j)) (suc (suc j)) ⟩ | |
| 166 suc (suc j) ≡⟨ sym (gcd20 (suc (suc j))) ⟩ | |
| 167 gcd1 zero zero (suc (suc j)) (suc (suc j)) ∎ where open ≡-Reasoning | |
| 168 gcd200 zero (suc i0) (suc j) .(suc j) () refl | |
| 169 gcd200 (suc zero) .1 (suc j) .(suc j) refl refl = begin | |
| 170 gcd1 (1 + suc j) (1 + suc j) (suc j) (suc j) ≡⟨ gcd203 (suc j) ⟩ | |
| 171 1 ≡⟨ sym ( gcd204 (suc j)) ⟩ | |
| 172 gcd1 1 1 (suc j) (suc j) ∎ where open ≡-Reasoning | |
| 173 gcd200 (suc (suc i)) i0 (suc j) zero i=i0 () | |
| 174 | |
| 175 gcd52 : {i : ℕ } → 1 < suc (suc i) | |
| 176 gcd52 {zero} = a<sa | |
| 177 gcd52 {suc i} = <-trans (gcd52 {i}) a<sa | |
| 178 | |
| 179 gcd50 : (i i0 j j0 : ℕ) → 1 < i0 → i ≤ i0 → j ≤ j0 → gcd1 i i0 j j0 ≤ i0 | |
| 180 gcd50 zero i0 zero j0 0<i i<i0 j<j0 with <-cmp i0 j0 | |
| 181 ... | tri< a ¬b ¬c = ≤-refl | |
| 182 ... | tri≈ ¬a refl ¬c = ≤-refl | |
| 183 ... | tri> ¬a ¬b c = ≤-trans refl-≤s c | |
| 184 gcd50 zero (suc i0) (suc zero) j0 0<i i<i0 j<j0 = gcd51 0<i where | |
| 185 gcd51 : 1 < suc i0 → gcd1 zero (suc i0) 1 j0 ≤ suc i0 | |
| 186 gcd51 1<i = ≤to< 1<i | |
| 187 gcd50 zero (suc i0) (suc (suc j)) j0 0<i i<i0 j<j0 = gcd50 i0 (suc i0) (suc j) (suc (suc j)) 0<i refl-≤s refl-≤s | |
| 188 gcd50 (suc zero) i0 zero j0 0<i i<i0 j<j0 = ≤to< 0<i | |
| 189 gcd50 (suc (suc i)) i0 zero zero 0<i i<i0 j<j0 = ≤-refl | |
| 190 gcd50 (suc (suc i)) i0 zero (suc j0) 0<i i<i0 j<j0 = ≤-trans (gcd50 (suc i) (suc (suc i)) j0 (suc j0) gcd52 refl-≤s refl-≤s) i<i0 | |
| 191 gcd50 (suc i) i0 (suc j) j0 0<i i<i0 j<j0 = subst (λ k → k ≤ i0 ) (sym (gcd22 i i0 j j0)) | |
| 192 (gcd50 i i0 j j0 0<i (≤-trans refl-≤s i<i0) (≤-trans refl-≤s j<j0)) | |
| 193 | |
| 194 gcd5 : ( n k : ℕ ) → 1 < n → gcd n k ≤ n | |
| 195 gcd5 n k 0<n = gcd50 n n k k 0<n ≤-refl ≤-refl | |
| 196 | |
| 197 gcd6 : ( n k : ℕ ) → 1 < n → gcd k n ≤ n | |
| 198 gcd6 n k 1<n = subst (λ m → m ≤ n) (gcdsym {n} {k}) (gcd5 n k 1<n) | |
| 199 | |
| 200 gcd4 : ( n k : ℕ ) → 1 < n → gcd n k ≡ k → k ≤ n | |
| 201 gcd4 n k 1<n eq = subst (λ m → m ≤ n ) eq (gcd5 n k 1<n) | |
| 202 | |
| 203 gcdmul+1 : ( m n : ℕ ) → gcd (m * n + 1) n ≡ 1 | |
| 204 gcdmul+1 zero n = gcd204 n | |
| 205 gcdmul+1 (suc m) n = begin | |
| 206 gcd (suc m * n + 1) n ≡⟨⟩ | |
| 207 gcd (n + m * n + 1) n ≡⟨ cong (λ k → gcd k n ) (begin | |
| 208 n + m * n + 1 ≡⟨ cong (λ k → k + 1) (+-comm n _) ⟩ | |
| 209 m * n + n + 1 ≡⟨ +-assoc (m * n) _ _ ⟩ | |
| 210 m * n + (n + 1) ≡⟨ cong (λ k → m * n + k) (+-comm n _) ⟩ | |
| 211 m * n + (1 + n) ≡⟨ sym ( +-assoc (m * n) _ _ ) ⟩ | |
| 212 m * n + 1 + n ∎ | |
| 213 ) ⟩ | |
| 214 gcd (m * n + 1 + n) n ≡⟨ gcd2 (m * n + 1) n ⟩ | |
| 215 gcd (m * n + 1) n ≡⟨ gcdmul+1 m n ⟩ | |
| 216 1 ∎ where open ≡-Reasoning | |
| 217 |