|
53
|
1 module chap0 where
|
|
|
2
|
|
|
3 open import Data.List
|
|
|
4 open import Data.Nat hiding (_⊔_)
|
|
|
5 open import Data.Integer hiding (_⊔_)
|
|
|
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 )
|
|
|
21 ListProduct = {!!}
|
|
|
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
|
|
|
47
|
|
|
48 _≡7_ : ℕ → ℕ → Set
|
|
|
49 n ≡7 m = (n % 7) ≡ (m % 7 )
|
|
|
50
|
|
|
51 refl7 : { n : ℕ} → n ≡7 n
|
|
|
52 refl7 = {!!}
|
|
|
53
|
|
|
54 sym7 : { n m : ℕ} → n ≡7 m → m ≡7 n
|
|
|
55 sym7 = {!!}
|
|
|
56
|
|
|
57 trans7 : { n m o : ℕ} → n ≡7 m → m ≡7 o → n ≡7 o
|
|
|
58 trans7 = {!!}
|
|
|
59
|
|
|
60 open import Level renaming ( zero to Zero ; suc to Suc )
|
|
|
61
|
|
|
62 record Graph { v v' : Level } : Set (Suc v ⊔ Suc v' ) where
|
|
|
63 field
|
|
|
64 vertex : Set v
|
|
|
65 edge : vertex → vertex → Set v'
|
|
|
66
|
|
|
67 data edge012a : ℕ → ℕ → Set where
|
|
|
68 e012a-1 : edge012a 1 2
|
|
|
69 e012a-2 : edge012a 2 3
|
|
|
70 e012a-3 : edge012a 3 4
|
|
|
71 e012a-4 : edge012a 4 5
|
|
|
72 e012a-5 : edge012a 5 1
|
|
|
73
|
|
|
74 graph012a : Graph {Zero} {Zero}
|
|
|
75 graph012a = record { vertex = ℕ ; edge = edge012a }
|
|
|
76
|
|
|
77 data edge012b : ℕ → ℕ → Set where
|
|
|
78 e012b-1 : edge012b 1 2
|
|
|
79 e012b-2 : edge012b 1 3
|
|
|
80 e012b-3 : edge012b 1 4
|
|
|
81 e012b-4 : edge012b 2 3
|
|
|
82 e012b-5 : edge012b 2 4
|
|
|
83 e012b-6 : edge012b 3 4
|
|
|
84
|
|
|
85 graph012b : Graph {Zero} {Zero}
|
|
|
86 graph012b = record { vertex = ℕ ; edge = edge012b }
|
|
|
87
|
|
|
88 data connected { V : Set } ( E : V -> V -> Set ) ( x y : V ) : Set where
|
|
|
89 direct : E x y -> connected E x y
|
|
|
90 indirect : { z : V } -> E x z -> connected {V} E z y -> connected E x y
|
|
|
91
|
|
|
92 open import Data.Empty
|
|
|
93 open import Relation.Nullary
|
|
|
94
|
|
|
95 -- data Dec (P : Set) : Set where
|
|
|
96 -- yes : P → Dec P
|
|
|
97 -- no : ¬ P → Dec P
|
|
|
98
|
|
|
99 reachable : { V : Set } ( E : V -> V -> Set ) ( x y : V ) -> Set
|
|
|
100 reachable {V} E X Y = Dec ( connected {V} E X Y )
|
|
|
101
|
|
|
102 dag : { V : Set } ( E : V -> V -> Set ) -> Set
|
|
|
103 dag {V} E = ∀ (n : V) → ¬ ( connected E n n )
|
|
|
104
|
|
|
105
|
