|
52
|
1 module practice-nat where
|
|
|
2
|
|
|
3 open import Data.Nat
|
|
|
4 open import Data.Empty
|
|
|
5 open import Relation.Nullary
|
|
141
|
6 open import Relation.Binary.PropositionalEquality hiding (_⇔_)
|
|
59
|
7 open import logic
|
|
52
|
8
|
|
59
|
9 -- hint : it has two inputs, use recursion
|
|
52
|
10 nat-<> : { x y : ℕ } → x < y → y < x → ⊥
|
|
141
|
11 nat-<> = {!!}
|
|
52
|
12
|
|
59
|
13 -- hint : use recursion
|
|
52
|
14 nat-<≡ : { x : ℕ } → x < x → ⊥
|
|
59
|
15 nat-<≡ = {!!}
|
|
52
|
16
|
|
59
|
17 -- hint : use refl and recursion
|
|
52
|
18 nat-≡< : { x y : ℕ } → x ≡ y → x < y → ⊥
|
|
|
19 nat-≡< = {!!}
|
|
|
20
|
|
|
21 ¬a≤a : {la : ℕ} → suc la ≤ la → ⊥
|
|
59
|
22 ¬a≤a = {!!}
|
|
52
|
23
|
|
59
|
24 -- hint : make case with la first
|
|
52
|
25 a<sa : {la : ℕ} → la < suc la
|
|
|
26 a<sa = {!!}
|
|
|
27
|
|
59
|
28 -- hint : ¬ has an input, use recursion
|
|
52
|
29 =→¬< : {x : ℕ } → ¬ ( x < x )
|
|
|
30 =→¬< = {!!}
|
|
|
31
|
|
59
|
32 -- hint : two inputs, try nat-<>
|
|
52
|
33 >→¬< : {x y : ℕ } → (x < y ) → ¬ ( y < x )
|
|
|
34 >→¬< = {!!}
|
|
|
35
|
|
59
|
36 -- hint : make cases on all arguments. return case1 or case2
|
|
|
37 -- hint : use with on suc case
|
|
52
|
38 <-∨ : { x y : ℕ } → x < suc y → ( (x ≡ y ) ∨ (x < y) )
|
|
|
39 <-∨ = {!!}
|
|
|
40
|
|
|
41 max : (x y : ℕ) → ℕ
|
|
|
42 max = {!!}
|
|
|
43
|
|
|
44 sum : (x y : ℕ) → ℕ
|
|
141
|
45 sum zero y = y
|
|
|
46 sum (suc x) y = suc ( sum x y )
|
|
|
47
|
|
|
48 sum' : (x y : ℕ) → ℕ
|
|
|
49 sum' x zero = x
|
|
|
50 sum' x (suc y) = suc (sum' x y)
|
|
|
51
|
|
|
52 sum-sym0 : {x y : ℕ} → sum x y ≡ sum' y x
|
|
|
53 sum-sym0 {zero} {zero} = refl
|
|
|
54 sum-sym0 {suc x} {y} = cong (λ k → suc k ) (sum-sym0 {x} {y})
|
|
|
55 sum-sym0 {zero} {y} = refl
|
|
52
|
56
|
|
|
57 sum-6 : sum 3 4 ≡ 7
|
|
141
|
58 sum-6 = refl
|
|
52
|
59
|
|
|
60 sum1 : (x y : ℕ) → sum x (suc y) ≡ suc (sum x y )
|
|
|
61 sum1 x y = let open ≡-Reasoning in
|
|
|
62 begin
|
|
|
63 sum x (suc y)
|
|
|
64 ≡⟨ {!!} ⟩
|
|
|
65 suc (sum x y )
|
|
|
66 ∎
|
|
|
67
|
|
141
|
68 sum0 : (x : ℕ) → sum 0 x ≡ x
|
|
|
69 sum0 zero = refl
|
|
|
70 sum0 (suc x) = refl
|
|
52
|
71
|
|
|
72 sum-sym : (x y : ℕ) → sum x y ≡ sum y x
|
|
|
73 sum-sym = {!!}
|
|
|
74
|
|
|
75 sum-assoc : (x y z : ℕ) → sum x (sum y z ) ≡ sum (sum x y) z
|
|
|
76 sum-assoc = {!!}
|
|
|
77
|
|
|
78 mul : (x y : ℕ) → ℕ
|
|
141
|
79 mul x zero = zero
|
|
|
80 mul x (suc y) = sum x ( mul x y )
|
|
|
81
|
|
|
82 mulr : (x y : ℕ) → ℕ
|
|
|
83 mulr zero y = zero
|
|
|
84 mulr (suc x) y = sum y ( mulr x y )
|
|
|
85
|
|
|
86 mul-sym1 : {x y : ℕ } → mul x y ≡ mulr y x
|
|
|
87 mul-sym1 {zero} {zero} = refl
|
|
|
88 mul-sym1 {zero} {suc y} = begin
|
|
|
89 mul zero (suc y)
|
|
|
90 ≡⟨⟩
|
|
|
91 sum 0 (mul 0 y)
|
|
|
92 ≡⟨ cong (λ k → sum 0 k ) {!!} ⟩
|
|
|
93 sum 0 (mulr y 0)
|
|
|
94 ≡⟨⟩
|
|
|
95 mulr (suc y) zero
|
|
|
96 ∎ where open ≡-Reasoning
|
|
|
97 mul-sym1 {suc x} {y} = {!!}
|
|
52
|
98
|
|
|
99 mul-9 : mul 3 4 ≡ 12
|
|
|
100 mul-9 = {!!}
|
|
|
101
|
|
|
102 mul-distr1 : (x y : ℕ) → mul x (suc y) ≡ sum x ( mul x y )
|
|
|
103 mul-distr1 = {!!}
|
|
|
104
|
|
|
105 mul-sym0 : (x : ℕ) → mul zero x ≡ mul x zero
|
|
|
106 mul-sym0 = {!!}
|
|
|
107
|
|
|
108 mul-sym : (x y : ℕ) → mul x y ≡ mul y x
|
|
|
109 mul-sym = {!!}
|
|
|
110
|
|
|
111 mul-distr : (y z w : ℕ) → sum (mul y z) ( mul w z ) ≡ mul (sum y w) z
|
|
|
112 mul-distr = {!!}
|
|
|
113
|
|
|
114 mul-assoc : (x y z : ℕ) → mul x (mul y z ) ≡ mul (mul x y) z
|
|
|
115 mul-assoc = {!!}
|
|
|
116
|
|
141
|
117 evenp : (x : ℕ) → Bool
|
|
|
118 evenp = {!!}
|
