|
138
|
1 module dag where
|
|
|
2
|
|
|
3 -- f0
|
|
|
4 -- -----→
|
|
|
5 -- t0 t1
|
|
|
6 -- -----→
|
|
|
7 -- f1
|
|
|
8
|
|
|
9
|
|
330
|
10 data TwoObject : Set where -- vertex
|
|
|
11 t0 : TwoObject
|
|
|
12 t1 : TwoObject
|
|
138
|
13
|
|
|
14
|
|
330
|
15 data TwoArrow : TwoObject → TwoObject → Set where -- edge
|
|
|
16 f0 : TwoArrow t0 t1
|
|
|
17 f1 : TwoArrow t0 t1
|
|
138
|
18
|
|
|
19
|
|
|
20 -- r0
|
|
|
21 -- -----→
|
|
|
22 -- t0 t1
|
|
|
23 -- ←-----
|
|
|
24 -- r1
|
|
|
25
|
|
|
26 data Circle : TwoObject → TwoObject → Set where
|
|
330
|
27 r0 : Circle t0 t1
|
|
|
28 r1 : Circle t1 t0
|
|
138
|
29
|
|
330
|
30 --
|
|
|
31 -- Definition of ⊥ and ¬ in agda
|
|
|
32 --
|
|
138
|
33
|
|
330
|
34 data ⊥ : Set where -- data with no consutructor
|
|
138
|
35
|
|
330
|
36 ⊥-elim : {A : Set } → ⊥ → A -- function with no possible input
|
|
|
37 ⊥-elim () -- no constructor
|
|
|
38
|
|
|
39 ¬_ : Set → Set -- A won't happen (This is a type, not an imlemetation )
|
|
138
|
40 ¬ A = A → ⊥
|
|
|
41
|
|
|
42 data Bool : Set where
|
|
330
|
43 true : Bool
|
|
|
44 false : Bool
|
|
138
|
45
|
|
141
|
46 data connected { V : Set } ( E : V → V → Set ) ( x y : V ) : Set where
|
|
330
|
47 direct : E x y → connected E x y
|
|
141
|
48 indirect : { z : V } → E x z → connected {V} E z y → connected E x y
|
|
138
|
49
|
|
330
|
50 -- this is similar to the List
|
|
|
51 data List ( A : Set ) : Set where
|
|
|
52 nil : List A
|
|
|
53 cons : A → List A → List A
|
|
|
54
|
|
138
|
55 lemma1 : connected TwoArrow t0 t1
|
|
141
|
56 lemma1 = {!!}
|
|
138
|
57
|
|
|
58 lemma2 : ¬ ( connected TwoArrow t1 t0 )
|
|
141
|
59 lemma2 = {!!}
|
|
138
|
60
|
|
|
61 -- lemma2 (direct ())
|
|
|
62 -- lemma2 (indirect () (direct _))
|
|
|
63 -- lemma2 (indirect () (indirect _ _ ))
|
|
|
64
|
|
|
65 lemma3 : connected Circle t0 t0
|
|
330
|
66 lemma3 = ?
|
|
|
67
|
|
|
68 -- decidabity
|
|
138
|
69
|
|
|
70 data Dec (P : Set) : Set where
|
|
|
71 yes : P → Dec P
|
|
|
72 no : ¬ P → Dec P
|
|
|
73
|
|
330
|
74 reachable : { V : Set } ( E : V → V → Set ) ( x y : V ) → Set
|
|
138
|
75 reachable {V} E x y = Dec ( connected {V} E x y )
|
|
|
76
|
|
330
|
77 dag : { V : Set } ( E : V → V → Set ) → Set
|
|
138
|
78 dag {V} E = ∀ (n : V) → ¬ ( connected E n n )
|
|
|
79
|
|
330
|
80 -- dag {V} E = ∀ (n : V) → connected E n n → ⊥
|
|
|
81
|
|
138
|
82 lemma4 : dag TwoArrow
|
|
330
|
83 lemma4 = ?
|
|
138
|
84
|
|
|
85 lemma5 : ¬ ( dag Circle )
|
|
330
|
86 lemma5 x = ?
|
|
138
|
87
|
|
330
|
88 -- record Finite ( A : Set ) : Set where
|
|
|
89 -- field
|
|
|
90 -- a : ?
|
|
|
91 --
|
|
|
92 -- record FiniteE {A : Set} ( E : A → A → Set ) : Set where
|
|
|
93 -- field
|
|
|
94 -- a : ?
|
|
|
95 --
|
|
|
96 -- lemma6 : ( V : Set ) ( E : V → V → Set ) → Finite V → FiniteE E → ( x y : V ) → reachable E x y
|
|
|
97 -- lemma6 = ?
|
|
|
98 --
|
|
|
99 --
|
