Mercurial > hg > Members > kono > Proof > galois
comparison nat.agda @ 112:43731a549950
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 02 Sep 2020 11:29:04 +0900 |
| parents | 482ef04890f8 |
| children | 2eb62a2a34f2 |
comparison
equal
deleted
inserted
replaced
| 111:d3da6e2c0d90 | 112:43731a549950 |
|---|---|
| 309 suc ( suc (suc n) * suc m) | 309 suc ( suc (suc n) * suc m) |
| 310 ≤⟨ ≤-plus-0 {_} {_} {1} (*≤ lt ) ⟩ | 310 ≤⟨ ≤-plus-0 {_} {_} {1} (*≤ lt ) ⟩ |
| 311 suc (suc k * suc m) | 311 suc (suc k * suc m) |
| 312 ∎ where open ≤-Reasoning | 312 ∎ where open ≤-Reasoning |
| 313 open ≡-Reasoning | 313 open ≡-Reasoning |
| 314 | |
| 315 open import Data.List | |
| 316 | |
| 317 ℕL-inject : {h h1 : ℕ } {x y : List ℕ } → h ∷ x ≡ h1 ∷ y → h ≡ h1 | |
| 318 ℕL-inject refl = refl | |
| 319 | |
| 320 ℕL-inject-t : {h h1 : ℕ } {x y : List ℕ } → h ∷ x ≡ h1 ∷ y → x ≡ y | |
| 321 ℕL-inject-t refl = refl | |
| 322 | |
| 323 ℕL-eq? : (x y : List ℕ ) → Dec (x ≡ y ) | |
| 324 ℕL-eq? [] [] = yes refl | |
| 325 ℕL-eq? [] (x ∷ y) = no (λ ()) | |
| 326 ℕL-eq? (x ∷ x₁) [] = no (λ ()) | |
| 327 ℕL-eq? (h ∷ x) (h1 ∷ y) with h ≟ h1 | ℕL-eq? x y | |
| 328 ... | yes y1 | yes y2 = yes ( cong₂ (λ j k → j ∷ k ) y1 y2 ) | |
| 329 ... | yes y1 | no n = no (λ e → n (ℕL-inject-t e)) | |
| 330 ... | no n | t = no (λ e → n (ℕL-inject e)) | |
| 331 |