Graph の表現

Agda でやるオートマトンの授業の一環ですが...

　　record Graph　{ v v' : Level } : Set (Suc v ⊔ Suc v' ) where
　　　field
　　　　vertex : Set v
　　　　edge : vertex　→ vertex → Set v'

この edge を data で書くってのが一つ

　　data edge012b :　ℕ → ℕ →　Set where
　　　　e012b-1 : edge012b 1 2
　　　　e012b-2 : edge012b 1 3

これでいいんですけどね。dgree といわれてちょっと困った。一つのノード(vertex)に接続された辺(edge)の数。

数え上げられない。なので、List を使うかと思ったんですが、

　　list012a : List ( ℕ × ℕ )
　　list012a = (1 , 2) ∷ (2 , 3) ∷ (3 , 4) ∷ (4 , 5) ∷ (5 , 1) ∷ []

こんな感じ。 ところが上に合わせようと思うと、なんか残念なことに。結局、

　　conn : List ( ℕ × ℕ ) → ℕ → ℕ → Bool

を書いて、

　　graph012a : Graph {Zero} {Zero}
　　graph012a = record { vertex = ℕ　; edge = λ s t → (conn list012a s t) ≡ true }

とすると良いらしい。

なんですが、すべてのvertexのdgreeの和とかいうと、それなりに複雑になってしまうっぽい。

まあ、さぼって、すべてのvertexのdgreeの和は偶数ってのは証明はできました。