|
431
|
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
|
|
446
|
13 nat-≤> : { x y : Nat } → x ≤ y → y < x → ⊥
|
|
|
14 nat-≤> (s≤s x<y) (s≤s y<x) = nat-≤> x<y y<x
|
|
|
15
|
|
431
|
16 nat-<≡ : { x : Nat } → x < x → ⊥
|
|
|
17 nat-<≡ (s≤s lt) = nat-<≡ lt
|
|
|
18
|
|
|
19 nat-≡< : { x y : Nat } → x ≡ y → x < y → ⊥
|
|
|
20 nat-≡< refl lt = nat-<≡ lt
|
|
|
21
|
|
|
22 ¬a≤a : {la : Nat} → Suc la ≤ la → ⊥
|
|
|
23 ¬a≤a (s≤s lt) = ¬a≤a lt
|
|
|
24
|
|
|
25 a<sa : {la : Nat} → la < Suc la
|
|
|
26 a<sa {Zero} = s≤s z≤n
|
|
|
27 a<sa {Suc la} = s≤s a<sa
|
|
|
28
|
|
448
|
29 <to≤ : {x y : Nat } → x < y → x ≤ y
|
|
|
30 <to≤ {Zero} {Suc y} (s≤s z≤n) = z≤n
|
|
|
31 <to≤ {Suc x} {Suc y} (s≤s lt) = s≤s (<to≤ {x} {y} lt)
|
|
|
32
|
|
431
|
33 =→¬< : {x : Nat } → ¬ ( x < x )
|
|
|
34 =→¬< {Zero} ()
|
|
|
35 =→¬< {Suc x} (s≤s lt) = =→¬< lt
|
|
|
36
|
|
|
37 >→¬< : {x y : Nat } → (x < y ) → ¬ ( y < x )
|
|
|
38 >→¬< (s≤s x<y) (s≤s y<x) = >→¬< x<y y<x
|
|
|
39
|
|
|
40 <-∨ : { x y : Nat } → x < Suc y → ( (x ≡ y ) ∨ (x < y) )
|
|
|
41 <-∨ {Zero} {Zero} (s≤s z≤n) = case1 refl
|
|
|
42 <-∨ {Zero} {Suc y} (s≤s lt) = case2 (s≤s z≤n)
|
|
|
43 <-∨ {Suc x} {Zero} (s≤s ())
|
|
|
44 <-∨ {Suc x} {Suc y} (s≤s lt) with <-∨ {x} {y} lt
|
|
|
45 <-∨ {Suc x} {Suc y} (s≤s lt) | case1 eq = case1 (cong (λ k → Suc k ) eq)
|
|
|
46 <-∨ {Suc x} {Suc y} (s≤s lt) | case2 lt1 = case2 (s≤s lt1)
|
|
|
47
|
|
|
48 max : (x y : Nat) → Nat
|
|
|
49 max Zero Zero = Zero
|
|
|
50 max Zero (Suc x) = (Suc x)
|
|
|
51 max (Suc x) Zero = (Suc x)
|
|
|
52 max (Suc x) (Suc y) = Suc ( max x y )
|
|
|
53
|
