|
0
|
1 module day where
|
|
|
2
|
|
1
|
3 open import Relation.Binary.PropositionalEquality
|
|
|
4
|
|
0
|
5 data day : Set where
|
|
|
6 monday : day
|
|
|
7 tuesday : day
|
|
|
8 wednesday : day
|
|
|
9 thursday : day
|
|
|
10 friday : day
|
|
|
11 saturday : day
|
|
|
12 sunday : day
|
|
|
13
|
|
|
14 -- ↑はただのデータ
|
|
|
15
|
|
|
16 nextWeekday : day → day
|
|
|
17 nextWeekday monday = tuesday
|
|
|
18 nextWeekday tuesday = wednesday
|
|
|
19 nextWeekday wednesday = thursday
|
|
|
20 nextWeekday thursday = friday
|
|
|
21 nextWeekday friday = monday
|
|
|
22 nextWeekday saturday = monday
|
|
|
23 nextWeekday sunday = monday
|
|
|
24
|
|
|
25 hoge : day → day
|
|
|
26 hoge x = nextWeekday x
|
|
|
27
|
|
|
28 data bool : Set where
|
|
|
29 true : bool
|
|
|
30 false : bool
|
|
|
31
|
|
|
32 negb : bool → bool
|
|
|
33 negb true = false
|
|
|
34 negb false = true
|
|
|
35
|
|
|
36 andb : bool → bool → bool
|
|
|
37 -- andb true true = true
|
|
|
38 -- andb true false = false
|
|
|
39 -- andb false true = false
|
|
|
40 -- andb false false = false
|
|
|
41 andb true b = b
|
|
|
42 andb false _ = false
|
|
|
43
|
|
|
44 orb : (x y : bool) → bool
|
|
|
45 orb true _ = true
|
|
|
46 orb false y = y
|
|
|
47
|
|
1
|
48 -- data _≡_ {a} { A : Set a} ( x : A ) : A → Set a where
|
|
|
49 -- refl : x ≡ x
|
|
0
|
50
|
|
|
51 testOrb1 : (orb true false) ≡ true
|
|
|
52 testOrb1 = refl
|
|
|
53
|
|
|
54 data nat : Set where
|
|
|
55 O : nat
|
|
|
56 Succ : nat → nat
|
|
|
57
|
|
|
58 pred : nat → nat
|
|
|
59 pred O = O
|
|
|
60 pred (Succ x) = x
|
|
|
61
|
|
|
62 minustwo : nat → nat
|
|
|
63 minustwo x = pred (pred x)
|
|
|
64
|
|
|
65 evenb : nat → bool
|
|
|
66 evenb O = true
|
|
|
67 evenb (Succ O) = false
|
|
|
68 evenb (Succ (Succ x)) = evenb x
|
|
|
69
|
|
|
70 open import Data.Nat.Base
|
|
|
71
|
|
|
72 factorial : ℕ → ℕ
|
|
|
73 factorial zero = 1
|
|
|
74 factorial (suc x) = x * (factorial (x))
|
|
|
75
|
|
|
76 beqNat : ℕ → ℕ → bool
|
|
|
77 beqNat zero zero = true
|
|
|
78 beqNat zero (suc y) = false
|
|
|
79 beqNat (suc x) zero = false
|
|
|
80 beqNat (suc x) (suc y) = beqNat x y
|
|
|
81
|
|
|
82 -- beqNat x y with x | y
|
|
|
83 -- beqNat x y | zero | zero = true
|
|
|
84 -- beqNat x y | zero | suc a = false
|
|
|
85 -- beqNat x y | suc z | zero = false
|
|
|
86 -- beqNat x y | suc z | suc a = beqNat z a
|
|
|
87
|
|
|
88 open import Data.Nat.Properties
|
|
|
89 open import Data.Empty
|
|
|
90
|
|
|
91 n+0 : ( n : ℕ ) → ( n + 0 ) ≡ n
|
|
|
92 n+0 zero = refl
|
|
|
93 n+0 (suc x) rewrite ( +-comm (suc x) 0 ) = refl
|
|
|
94
|
|
|
95 andbTrueElim2 : ( b c : bool ) → (andb b c ) ≡ true → c ≡ true
|
|
|
96 -- andbTrueElim2 true c d with d
|
|
|
97 -- andbTrueElim2 true .true d | refl = refl
|
|
|
98 andbTrueElim2 _ true d = refl
|
|
|
99 andbTrueElim2 false false ()
|
|
|
100 andbTrueElim2 true false ()
|
|
|
101
|
|
1
|
102 mult0r : ( n : ℕ ) → ( n * zero) ≡ zero
|
|
|
103 mult0r zero = refl
|
|
|
104 -- mult0r (suc n) = mult0r n
|
|
|
105 mult0r (suc n) rewrite ( *-comm (suc n) 0 ) = refl
|
|
|
106
|
|
|
107 double : (n : ℕ ) → ℕ
|
|
|
108 double zero = zero
|
|
|
109 double (suc x) = suc ( suc ( double x))
|
|
|
110
|
|
|
111 sucEqPlus1 : ( n : ℕ ) → (n + 1) ≡(suc n)
|
|
|
112 sucEqPlus1 x rewrite (+-comm x 1 ) = refl
|
|
|
113
|
|
|
114
|
|
|
115 plusNSm : (n m : ℕ ) → (suc ( n + m)) ≡ (n + suc (m))
|
|
|
116 plusNSm zero zero = refl
|
|
|
117 plusNSm zero (suc y) = refl
|
|
|
118 plusNSm (suc x) zero rewrite sucEqPlus1 x | n+0 x = refl
|
|
|
119 plusNSm (suc x) (suc y) = cong (suc) (plusNSm x (suc y))
|
|
|
120
|
|
|
121 doublePlus : (n : ℕ ) → (double n) ≡ (n + n)
|
|
|
122 doublePlus zero = refl
|
|
|
123 doublePlus (suc n) rewrite (doublePlus n) | plusNSm n n = refl
|
|
|
124
|
|
|
125 plusSwap : ( n m p : ℕ ) → ( n + (m + p)) ≡ ( m + (n + p))
|
|
|
126 plusSwap zero y z = refl
|
|
|
127 plusSwap (suc x) y z rewrite sym (plusNSm (y) (x + z)) | plusSwap x y z = refl
|
