Mercurial > hg > Members > kono > Proof > galois
diff 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 |
line wrap: on
line diff
--- a/nat.agda Tue Sep 01 21:58:15 2020 +0900 +++ b/nat.agda Wed Sep 02 11:29:04 2020 +0900 @@ -311,3 +311,21 @@ suc (suc k * suc m) ∎ where open ≤-Reasoning open ≡-Reasoning + +open import Data.List + +ℕL-inject : {h h1 : ℕ } {x y : List ℕ } → h ∷ x ≡ h1 ∷ y → h ≡ h1 +ℕL-inject refl = refl + +ℕL-inject-t : {h h1 : ℕ } {x y : List ℕ } → h ∷ x ≡ h1 ∷ y → x ≡ y +ℕL-inject-t refl = refl + +ℕL-eq? : (x y : List ℕ ) → Dec (x ≡ y ) +ℕL-eq? [] [] = yes refl +ℕL-eq? [] (x ∷ y) = no (λ ()) +ℕL-eq? (x ∷ x₁) [] = no (λ ()) +ℕL-eq? (h ∷ x) (h1 ∷ y) with h ≟ h1 | ℕL-eq? x y +... | yes y1 | yes y2 = yes ( cong₂ (λ j k → j ∷ k ) y1 y2 ) +... | yes y1 | no n = no (λ e → n (ℕL-inject-t e)) +... | no n | t = no (λ e → n (ℕL-inject e)) +