|
70
|
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
|
|
|
47 -- _*_ : Nat → Nat → Nat
|
|
|
48 -- _*_ zero _ = zero
|
|
|
49 -- _*_ (suc n) m = m + ( n * m )
|
|
|
50
|
|
|
51 exp : Nat → Nat → Nat
|
|
|
52 exp _ Zero = 1
|
|
|
53 exp n (Suc m) = n * ( exp n m )
|
