|
53
|
1 module chap0 where
|
|
|
2
|
|
|
3 open import Data.List
|
|
|
4 open import Data.Nat hiding (_⊔_)
|
|
56
|
5 -- open import Data.Integer hiding (_⊔_ ; _≟_ ; _+_ )
|
|
53
|
6 open import Data.Product
|
|
|
7
|
|
|
8 A : List ℕ
|
|
|
9 A = 1 ∷ 2 ∷ []
|
|
|
10
|
|
|
11 data Literal : Set where
|
|
|
12 x : Literal
|
|
|
13 y : Literal
|
|
|
14 z : Literal
|
|
|
15
|
|
|
16 B : List Literal
|
|
|
17 B = x ∷ y ∷ z ∷ []
|
|
|
18
|
|
|
19
|
|
|
20 ListProduct : {A B : Set } → List A → List B → List ( A × B )
|
|
59
|
21 ListProduct = {!!}
|
|
53
|
22
|
|
|
23 ex05 : List ( ℕ × Literal )
|
|
|
24 ex05 = ListProduct A B -- (1 , x) ∷ (1 , y) ∷ (1 , z) ∷ (2 , x) ∷ (2 , y) ∷ (2 , z) ∷ []
|
|
|
25
|
|
|
26 ex06 : List ( ℕ × Literal × ℕ )
|
|
|
27 ex06 = ListProduct A (ListProduct B A)
|
|
|
28
|
|
|
29 ex07 : Set
|
|
|
30 ex07 = ℕ × ℕ
|
|
|
31
|
|
|
32 data ex08-f : ℕ → ℕ → Set where
|
|
|
33 ex08f0 : ex08-f 0 1
|
|
|
34 ex08f1 : ex08-f 1 2
|
|
|
35 ex08f2 : ex08-f 2 3
|
|
|
36 ex08f3 : ex08-f 3 4
|
|
|
37 ex08f4 : ex08-f 4 0
|
|
|
38
|
|
|
39 data ex09-g : ℕ → ℕ → ℕ → ℕ → Set where
|
|
|
40 ex09g0 : ex09-g 0 1 2 3
|
|
|
41 ex09g1 : ex09-g 1 2 3 0
|
|
|
42 ex09g2 : ex09-g 2 3 0 1
|
|
|
43 ex09g3 : ex09-g 3 0 1 2
|
|
|
44
|
|
|
45 open import Data.Nat.DivMod
|
|
|
46 open import Relation.Binary.PropositionalEquality
|
|
56
|
47 open import Relation.Binary.Core
|
|
|
48 open import Data.Nat.Properties
|
|
|
49
|
|
|
50 -- _%_ : ℕ → ℕ → ℕ
|
|
|
51 -- _%_ a b with <-cmp a b
|
|
|
52 -- _%_ a b | tri< a₁ ¬b ¬c = a
|
|
|
53 -- _%_ a b | tri≈ ¬a b₁ ¬c = 0
|
|
|
54 -- _%_ a b | tri> ¬a ¬b c = _%_ (a - b) b
|
|
53
|
55
|
|
|
56 _≡7_ : ℕ → ℕ → Set
|
|
|
57 n ≡7 m = (n % 7) ≡ (m % 7 )
|
|
|
58
|
|
|
59 refl7 : { n : ℕ} → n ≡7 n
|
|
|
60 refl7 = {!!}
|
|
|
61
|
|
|
62 sym7 : { n m : ℕ} → n ≡7 m → m ≡7 n
|
|
|
63 sym7 = {!!}
|
|
|
64
|
|
|
65 trans7 : { n m o : ℕ} → n ≡7 m → m ≡7 o → n ≡7 o
|
|
|
66 trans7 = {!!}
|
|
|
67
|
|
|
68 open import Level renaming ( zero to Zero ; suc to Suc )
|
|
|
69
|
|
|
70 record Graph { v v' : Level } : Set (Suc v ⊔ Suc v' ) where
|
|
|
71 field
|
|
|
72 vertex : Set v
|
|
|
73 edge : vertex → vertex → Set v'
|
|
|
74
|
|
55
|
75 open Graph
|
|
|
76
|
|
|
77 -- open import Data.Fin hiding ( _≟_ )
|
|
|
78 open import Data.Empty
|
|
|
79 open import Relation.Nullary
|
|
|
80 open import Data.Unit hiding ( _≟_ )
|
|
|
81
|
|
|
82
|
|
|
83 -- data Dec (P : Set) : Set where
|
|
|
84 -- yes : P → Dec P
|
|
|
85 -- no : ¬ P → Dec P
|
|
|
86 --
|
|
|
87 -- _≟_ : (s t : ℕ ) → Dec ( s ≡ t )
|
|
|
88
|
|
163
|
89 -- ¬ A = A → ⊥
|
|
|
90
|
|
|
91 _n≟_ : (s t : ℕ ) → Dec ( s ≡ t )
|
|
|
92 zero n≟ zero = yes refl
|
|
|
93 zero n≟ suc t = no (λ ())
|
|
|
94 suc s n≟ zero = no (λ ())
|
|
|
95 suc s n≟ suc t with s n≟ t
|
|
|
96 ... | yes refl = yes refl
|
|
|
97 ... | no n = no (λ k → n (tt1 k) ) where
|
|
|
98 tt1 : suc s ≡ suc t → s ≡ t
|
|
|
99 tt1 refl = refl
|
|
|
100
|
|
55
|
101 open import Data.Bool hiding ( _≟_ )
|
|
|
102
|
|
|
103 conn : List ( ℕ × ℕ ) → ℕ → ℕ → Bool
|
|
|
104 conn [] _ _ = false
|
|
|
105 conn ((n1 , m1 ) ∷ t ) n m with n ≟ n1 | m ≟ m1
|
|
|
106 conn ((n1 , m1) ∷ t) n m | yes refl | yes refl = true
|
|
|
107 conn ((n1 , m1) ∷ t) n m | _ | _ = conn t n m
|
|
|
108
|
|
|
109 list012a : List ( ℕ × ℕ )
|
|
|
110 list012a = (1 , 2) ∷ (2 , 3) ∷ (3 , 4) ∷ (4 , 5) ∷ (5 , 1) ∷ []
|
|
53
|
111
|
|
54
|
112 graph012a : Graph {Zero} {Zero}
|
|
59
|
113 graph012a = record { vertex = ℕ ; edge = λ s t → (conn list012a s t) ≡ true }
|
|
53
|
114
|
|
|
115 data edge012b : ℕ → ℕ → Set where
|
|
|
116 e012b-1 : edge012b 1 2
|
|
|
117 e012b-2 : edge012b 1 3
|
|
|
118 e012b-3 : edge012b 1 4
|
|
|
119 e012b-4 : edge012b 2 3
|
|
|
120 e012b-5 : edge012b 2 4
|
|
|
121 e012b-6 : edge012b 3 4
|
|
|
122
|
|
55
|
123 edge? : (E : ℕ → ℕ → Set) → ( a b : ℕ ) → Set
|
|
|
124 edge? E a b = Dec ( E a b )
|
|
|
125
|
|
|
126 lemma3 : ( a b : ℕ ) → edge? edge012b a b
|
|
|
127 lemma3 1 2 = yes e012b-1
|
|
|
128 lemma3 1 3 = yes e012b-2
|
|
|
129 lemma3 1 4 = yes e012b-3
|
|
|
130 lemma3 2 3 = yes e012b-4
|
|
|
131 lemma3 2 4 = yes e012b-5
|
|
|
132 lemma3 3 4 = yes e012b-6
|
|
|
133 lemma3 1 1 = no ( λ () )
|
|
|
134 lemma3 2 1 = no ( λ () )
|
|
|
135 lemma3 2 2 = no ( λ () )
|
|
|
136 lemma3 3 1 = no ( λ () )
|
|
|
137 lemma3 3 2 = no ( λ () )
|
|
|
138 lemma3 3 3 = no ( λ () )
|
|
|
139 lemma3 0 _ = no ( λ () )
|
|
|
140 lemma3 _ 0 = no ( λ () )
|
|
|
141 lemma3 _ (suc (suc (suc (suc (suc _))))) = no ( λ () )
|
|
|
142 lemma3 (suc (suc (suc (suc _)))) _ = no ( λ () )
|
|
|
143
|
|
53
|
144 graph012b : Graph {Zero} {Zero}
|
|
|
145 graph012b = record { vertex = ℕ ; edge = edge012b }
|
|
|
146
|
|
|
147 data connected { V : Set } ( E : V -> V -> Set ) ( x y : V ) : Set where
|
|
59
|
148 direct : E x y → connected E x y
|
|
|
149 indirect : ( z : V ) -> E x z → connected {V} E z y → connected E x y
|
|
55
|
150
|
|
|
151 lemma1 : connected ( edge graph012a ) 1 2
|
|
59
|
152 lemma1 = direct refl where
|
|
53
|
153
|
|
55
|
154 lemma1-2 : connected ( edge graph012a ) 1 3
|
|
59
|
155 lemma1-2 = indirect 2 refl (direct refl )
|
|
53
|
156
|
|
55
|
157 lemma2 : connected ( edge graph012b ) 1 2
|
|
|
158 lemma2 = direct e012b-1
|
|
53
|
159
|
|
|
160 reachable : { V : Set } ( E : V -> V -> Set ) ( x y : V ) -> Set
|
|
|
161 reachable {V} E X Y = Dec ( connected {V} E X Y )
|
|
|
162
|
|
|
163 dag : { V : Set } ( E : V -> V -> Set ) -> Set
|
|
|
164 dag {V} E = ∀ (n : V) → ¬ ( connected E n n )
|
|
|
165
|
|
56
|
166 open import Function
|
|
|
167
|
|
|
168 lemma4 : ¬ ( dag ( edge graph012a) )
|
|
|
169 lemma4 neg = neg 1 $ indirect 2 refl $ indirect 3 refl $ indirect 4 refl $ indirect 5 refl $ direct refl
|
|
|
170
|
|
55
|
171 dgree : List ( ℕ × ℕ ) → ℕ → ℕ
|
|
|
172 dgree [] _ = 0
|
|
56
|
173 dgree ((e , e1) ∷ t) e0 with e0 ≟ e | e0 ≟ e1
|
|
55
|
174 dgree ((e , e1) ∷ t) e0 | yes _ | _ = 1 + (dgree t e0)
|
|
|
175 dgree ((e , e1) ∷ t) e0 | _ | yes p = 1 + (dgree t e0)
|
|
|
176 dgree ((e , e1) ∷ t) e0 | no _ | no _ = dgree t e0
|
|
53
|
177
|
|
56
|
178 dgree-c : {t : Set} → List ( ℕ × ℕ ) → ℕ → (ℕ → t) → t
|
|
|
179 dgree-c {t} [] e0 next = next 0
|
|
|
180 dgree-c {t} ((e , e1) ∷ tail ) e0 next with e0 ≟ e | e0 ≟ e1
|
|
|
181 ... | yes _ | _ = dgree-c tail e0 ( λ n → next (n + 1 ))
|
|
|
182 ... | _ | yes _ = dgree-c tail e0 ( λ n → next (n + 1 ))
|
|
|
183 ... | no _ | no _ = dgree-c tail e0 next
|
|
|
184
|
|
55
|
185 lemma6 = dgree list012a 2
|
|
56
|
186 lemma7 = dgree-c list012a 2 ( λ n → n )
|
|
|
187
|
|
|
188 even2 : (n : ℕ ) → n % 2 ≡ 0 → (n + 2) % 2 ≡ 0
|
|
|
189 even2 0 refl = refl
|
|
|
190 even2 1 ()
|
|
|
191 even2 (suc (suc n)) eq = trans ([a+n]%n≡a%n n _) eq -- [a+n]%n≡a%n : ∀ a n → (a + suc n) % suc n ≡ a % suc n
|
|
|
192
|
|
|
193 sum-of-dgree : ( g : List ( ℕ × ℕ )) → ℕ
|
|
|
194 sum-of-dgree [] = 0
|
|
|
195 sum-of-dgree ((e , e1) ∷ t) = 2 + sum-of-dgree t
|
|
|
196
|
|
|
197 dgree-even : ( g : List ( ℕ × ℕ )) → sum-of-dgree g % 2 ≡ 0
|
|
|
198 dgree-even [] = refl
|
|
57
|
199 dgree-even ((e , e1) ∷ t) = begin
|
|
59
|
200 sum-of-dgree ((e , e1) ∷ t) % 2
|
|
|
201 ≡⟨⟩
|
|
|
202 (2 + sum-of-dgree t ) % 2
|
|
|
203 ≡⟨ cong ( λ k → k % 2 ) ( +-comm 2 (sum-of-dgree t) ) ⟩
|
|
|
204 (sum-of-dgree t + 2) % 2
|
|
|
205 ≡⟨ [a+n]%n≡a%n (sum-of-dgree t) _ ⟩
|
|
|
206 sum-of-dgree t % 2
|
|
|
207 ≡⟨ dgree-even t ⟩
|
|
|
208 0
|
|
|
209 ∎ where open ≡-Reasoning
|
|
56
|
210
|
