Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison src/nat.agda @ 431:a5f8084b8368
reorganiztion for apkg
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Mon, 21 Dec 2020 10:23:37 +0900 |
parents | |
children | eb4049abad70 |
comparison
equal
deleted
inserted
replaced
430:28c7be8f252c | 431:a5f8084b8368 |
---|---|
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 | |
41 max : (x y : Nat) → Nat | |
42 max Zero Zero = Zero | |
43 max Zero (Suc x) = (Suc x) | |
44 max (Suc x) Zero = (Suc x) | |
45 max (Suc x) (Suc y) = Suc ( max x y ) | |
46 |