Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison nat.agda @ 213:22d435172d1a
separate logic and nat
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Fri, 02 Aug 2019 12:17:10 +0900 |
parents | |
children | 95a26d1698f4 |
comparison
equal
deleted
inserted
replaced
212:0a1804cc9d0a | 213:22d435172d1a |
---|---|
1 module nat where | |
2 | |
3 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ ) | |
4 open import Data.Empty | |
5 open import Relation.Nullary | |
6 open import Relation.Binary.PropositionalEquality | |
7 open import logic | |
8 | |
9 | |
10 nat-<> : { x y : Nat } → x < y → y < x → ⊥ | |
11 nat-<> (s≤s x<y) (s≤s y<x) = nat-<> x<y y<x | |
12 | |
13 nat-<≡ : { x : Nat } → x < x → ⊥ | |
14 nat-<≡ (s≤s lt) = nat-<≡ lt | |
15 | |
16 nat-≡< : { x y : Nat } → x ≡ y → x < y → ⊥ | |
17 nat-≡< refl lt = nat-<≡ lt | |
18 | |
19 ¬a≤a : {la : Nat} → Suc la ≤ la → ⊥ | |
20 ¬a≤a (s≤s lt) = ¬a≤a lt | |
21 | |
22 a<sa : {la : Nat} → la < Suc la | |
23 a<sa {Zero} = s≤s z≤n | |
24 a<sa {Suc la} = s≤s a<sa | |
25 | |
26 =→¬< : {x : Nat } → ¬ ( x < x ) | |
27 =→¬< {Zero} () | |
28 =→¬< {Suc x} (s≤s lt) = =→¬< lt | |
29 | |
30 >→¬< : {x y : Nat } → (x < y ) → ¬ ( y < x ) | |
31 >→¬< (s≤s x<y) (s≤s y<x) = >→¬< x<y y<x | |
32 | |
33 <-∨ : { x y : Nat } → x < Suc y → ( (x ≡ y ) ∨ (x < y) ) | |
34 <-∨ {Zero} {Zero} (s≤s z≤n) = case1 refl | |
35 <-∨ {Zero} {Suc y} (s≤s lt) = case2 (s≤s z≤n) | |
36 <-∨ {Suc x} {Zero} (s≤s ()) | |
37 <-∨ {Suc x} {Suc y} (s≤s lt) with <-∨ {x} {y} lt | |
38 <-∨ {Suc x} {Suc y} (s≤s lt) | case1 eq = case1 (cong (λ k → Suc k ) eq) | |
39 <-∨ {Suc x} {Suc y} (s≤s lt) | case2 lt1 = case2 (s≤s lt1) | |
40 |