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