diff options
Diffstat (limited to 'src/Problem12.agda')
| -rw-r--r-- | src/Problem12.agda | 459 |
1 files changed, 459 insertions, 0 deletions
diff --git a/src/Problem12.agda b/src/Problem12.agda new file mode 100644 index 0000000..5c147a2 --- /dev/null +++ b/src/Problem12.agda @@ -0,0 +1,459 @@ +module Problem12 where + +open import Axiom.UniquenessOfIdentityProofs using (UIP; module Decidable⇒UIP) +open import Data.Bool hiding (_≟_) +open import Data.Empty using (⊥-elim) +open import Data.Fin hiding (_+_) +import Data.Fin.Properties as Fin +open import Data.List +open import Data.List.Membership.Propositional +open import Data.List.Membership.Propositional.Properties +open import Data.List.Properties +open import Data.List.Relation.Unary.Any using (here; there; satisfied) +open import Data.Nat using (ℕ;zero;suc;_*_; _+_) +open import Data.Nat.Properties hiding (_≟_) +open import Data.Product hiding (map) +open import Data.Sum hiding (map) +open import Function.Base using (_∘′_) +open import Function.Bundles using (Injection; _↣_; _↔_; mk↣; mk↔′) +open import Relation.Binary.PropositionalEquality +open import Relation.Nullary + +-- copied in here because latest stable stdlib doesn't have it?? +_⊎-dec_ : ∀{A B : Set} → Dec A → Dec B → Dec (A ⊎ B) +does (a? ⊎-dec b?) = does a? ∨ does b? +proof (a? ⊎-dec b?) with proof a? +... | ofʸ p = ofʸ (inj₁ p) +... | ofⁿ ¬p with proof b? +... | ofʸ p = ofʸ (inj₂ p) +... | ofⁿ ¬p₁ = ofⁿ (λ { (inj₁ q) → ¬p q; (inj₂ q) → ¬p₁ q }) + +sum-0 : ∀ n → sum (tabulate {n = n} (λ _ → 0)) ≡ 0 +sum-0 zero = refl +sum-0 (suc n) = sum-0 n + +record DisjointPair (A : Set) : Set where + field + from : A + to : A + diff : from ≢ to + +record MultiGraph : Set where + field + #V : ℕ + Vertex = Fin #V + Edge = DisjointPair Vertex + field + E : List Edge + + V : List (Vertex) + V = allFin #V + + VertexUIP : UIP Vertex + VertexUIP = Decidable⇒UIP.≡-irrelevant _≟_ + + Connects : Vertex → Edge → Set + Connects v e = DisjointPair.from e ≡ v ⊎ DisjointPair.to e ≡ v + + connects : (v : Vertex) → (e : Edge) → Dec (Connects v e) + connects v e = (DisjointPair.from e ≟ v) ⊎-dec (DisjointPair.to e ≟ v) + + connects′ : (e : Edge) → (v : Vertex) → Dec (Connects v e) + connects′ e v = connects v e + + degree′ : (E : List Edge) → Vertex → ℕ + degree′ E v = length (filter (connects v) E) + + degree = degree′ E + + open ≡-Reasoning + + degree-split′ : + (e : Edge) (E : List Edge) (v : Vertex) → + degree′ (e ∷ E) v ≡ degree′ (e ∷ []) v + degree′ E v + degree-split′ e E v with does (connects v e) + ... | false = refl + ... | true = refl + + degree-split : + (e : Edge) (E : List Edge) (V : List Vertex) → + sum (map (degree′ (e ∷ E)) V) ≡ sum (map (degree′ (e ∷ [])) V) + sum (map (degree′ E) V) + degree-split e E [] = refl + degree-split e E (v ∷ V) = begin + degree′ (e ∷ E) v + sum (map (degree′ (e ∷ E)) V) ≡⟨ cong₂ _+_ {x = degree′ (e ∷ E) v} {y = degree′ (e ∷ []) v + degree′ E v} (degree-split′ e E v) (degree-split e E V) ⟩ + (degree′ (e ∷ []) v + degree′ E v) + (sum (map (degree′ (e ∷ [])) V) + sum (map (degree′ E) V)) ≡˘⟨ +-assoc (degree′ (e ∷ []) v + degree′ E v) (sum (map (degree′ (e ∷ [])) V)) (sum (map (degree′ E) V)) ⟩ + degree′ (e ∷ []) v + degree′ E v + sum (map (degree′ (e ∷ [])) V) + sum (map (degree′ E) V) ≡⟨ cong (_+ sum (map (degree′ E) V)) (+-assoc (degree′ (e ∷ []) v) (degree′ E v) (sum (map (degree′ (e ∷ [])) V))) ⟩ + degree′ (e ∷ []) v + (degree′ E v + sum (map (degree′ (e ∷ [])) V)) + sum (map (degree′ E) V) ≡⟨ cong (λ ◌ → degree′ (e ∷ []) v + ◌ + sum (map (degree′ E) V)) (+-comm (degree′ E v) (sum (map (degree′ (e ∷ [])) V))) ⟩ + degree′ (e ∷ []) v + (sum (map (degree′ (e ∷ [])) V) + degree′ E v) + sum (map (degree′ E) V) ≡˘⟨ cong (_+ sum (map (degree′ E) V)) (+-assoc (degree′ (e ∷ []) v) (sum (map (degree′ (e ∷ [])) V)) (degree′ E v)) ⟩ + degree′ (e ∷ []) v + sum (map (degree′ (e ∷ [])) V) + degree′ E v + sum (map (degree′ E) V) ≡⟨ +-assoc (degree′ (e ∷ []) v + sum (map (degree′ (e ∷ [])) V)) (degree′ E v) (sum (map (degree′ E) V)) ⟩ + (degree′ (e ∷ []) v + sum (map (degree′ (e ∷ [])) V)) + (degree′ E v + sum (map (degree′ E) V)) ∎ + + + degree-flip : (e : Edge) (V : List Vertex) → sum (map (degree′ (e ∷ [])) V) ≡ length (filter (connects′ e) V) + degree-flip e [] = refl + degree-flip e (v ∷ V) with does (connects v e) + ... | false = degree-flip e V + ... | true = cong suc (degree-flip e V) + + module _ where + degree-[_]′ : (e : Edge) → (∃[ k ] k ∈ filter (connects′ e) V) ↔ Fin 2 + degree-[ e ]′ = mk↔′ from to from-to to-from + where + from : ∃[ k ] k ∈ filter (connects′ e) V → Fin 2 + from (k , prf) with does (DisjointPair.from e ≟ k) + ... | true = zero + ... | false = suc zero + + to : Fin 2 → ∃[ k ] k ∈ filter (connects′ e) V + to zero = DisjointPair.from e , ∈-filter⁺ (connects′ e) (∈-allFin _) (inj₁ refl) + to (suc zero) = DisjointPair.to e , ∈-filter⁺ (connects′ e) (∈-allFin _) (inj₂ refl) + + from-to : (x : Fin 2) → from (to x) ≡ x + from-to zero with DisjointPair.from e ≟ DisjointPair.from e + ... | yes _ = refl + ... | no x≢x = ⊥-elim (x≢x refl) + from-to (suc zero) with DisjointPair.from e ≟ DisjointPair.to e + ... | yes x≡y = ⊥-elim (DisjointPair.diff e x≡y) + ... | no _ = refl + + open Injection using (injective) renaming (f to _⟨$⟩_) + + -- The only use of axiom K + ∈-tabulate-unique : + {n : ℕ} {A : Set} (uip : UIP A) (f : Fin n ↣ A) {x : A} (p q : x ∈ tabulate (f ⟨$⟩_)) → p ≡ q + ∈-tabulate-unique {suc n} uip f (here p) (here q) = cong here (uip p q) + ∈-tabulate-unique {suc n} uip f (here refl) (there q) = ⊥-elim (0≢1+n (cong toℕ (injective f (proj₂ (∈-tabulate⁻ q))))) + ∈-tabulate-unique {suc n} uip f (there p) (here refl) = ⊥-elim (0≢1+n (cong toℕ (injective f (proj₂ (∈-tabulate⁻ p))))) + ∈-tabulate-unique {suc n} uip f (there p) (there q) = cong there (∈-tabulate-unique uip (mk↣ (Fin.suc-injective ∘′ injective f)) p q) + + postulate + filter⁺-filter⁻ : + {A : Set} {P : A → Set} (P? : ∀ x → Dec (P x)) → + {v : A} (xs : List A) (i : v ∈ filter P? xs) → + uncurry (∈-filter⁺ P? {xs = xs}) (∈-filter⁻ P? i) ≡ i + + to-from : (x : ∃[ k ] k ∈ filter (connects′ e) V) → to (from x) ≡ x + to-from (k , prf) with DisjointPair.from e ≟ k + to-from (k , prf) | yes refl with ∈-filter⁻ (connects′ e) {xs = V} prf in filter⁻-eq + ... | k∈allFin , inj₁ p = cong (_ ,_) (begin + ∈-filter⁺ (connects′ e) (∈-allFin _) (inj₁ refl) ≡⟨ cong (λ ◌ → ∈-filter⁺ (connects′ e) ◌ (inj₁ refl)) (∈-tabulate-unique VertexUIP (mk↣ (λ eq → eq)) _ _) ⟩ + ∈-filter⁺ (connects′ e) k∈allFin (inj₁ refl) ≡⟨ cong (∈-filter⁺ (connects′ e) k∈allFin ∘′ inj₁) (VertexUIP refl p) ⟩ + ∈-filter⁺ (connects′ e) k∈allFin (inj₁ p) ≡˘⟨ cong (uncurry (∈-filter⁺ (connects′ e))) filter⁻-eq ⟩ + uncurry (∈-filter⁺ (connects′ e) {xs = V}) (∈-filter⁻ (connects′ e) prf) ≡⟨ filter⁺-filter⁻ (connects′ e) V prf ⟩ + prf ∎) + ... | k∈allFin , inj₂ k≡to = ⊥-elim (DisjointPair.diff e (sym k≡to)) + to-from (k , prf) | no k≢from with ∈-filter⁻ (connects′ e) {xs = V} prf in filter⁻-eq + ... | k∈allFin , inj₁ k≡from = ⊥-elim (k≢from k≡from) + ... | k∈allFin , inj₂ refl = cong (_ ,_) (begin + ∈-filter⁺ (connects′ e) (∈-allFin _) (inj₂ refl) ≡⟨ cong (λ ◌ → ∈-filter⁺ (connects′ e) ◌ (inj₂ refl)) (∈-tabulate-unique VertexUIP (mk↣ (λ eq → eq)) _ _) ⟩ + ∈-filter⁺ (connects′ e) k∈allFin (inj₂ refl) ≡˘⟨ cong (uncurry (∈-filter⁺ (connects′ e))) filter⁻-eq ⟩ + uncurry (∈-filter⁺ (connects′ e) {xs = V}) (∈-filter⁻ (connects′ e) prf) ≡⟨ filter⁺-filter⁻ (connects′ e) V prf ⟩ + prf ∎) + + postulate + degree-[_] : (e : Edge) → sum (map (degree′ (e ∷ [])) V) ≡ 2 + + handshaking′ : (E : List Edge) → sum (map (degree′ E) V) ≡ 2 * length E + handshaking′ [] = begin + sum (map (λ i → 0) V) ≡⟨ cong sum (map-tabulate {n = #V} (λ i → i) (λ _ → 0)) ⟩ + sum (tabulate {n = #V} (λ i → 0)) ≡⟨ sum-0 #V ⟩ + 0 ∎ + handshaking′ (e ∷ E) = begin + sum (map (degree′ (e ∷ E)) V) ≡⟨ degree-split e E V ⟩ + sum (map (degree′ (e ∷ [])) V) + sum (map (degree′ E) V) ≡⟨ cong₂ _+_ degree-[ e ] (handshaking′ E) ⟩ + 2 + 2 * length E ≡˘⟨ *-distribˡ-+ 2 1 (length E) ⟩ + 2 * (1 + length E) ∎ + + handshaking : sum (map degree V) ≡ 2 * length E + handshaking = handshaking′ E + +-- open import Data.Bool using (_∨_) +-- open import Data.Empty using (⊥-elim) +-- open import Data.Fin as Fin hiding (_+_) +-- import Data.Fin.Properties as Fin +-- open import Data.List as List hiding (map) +-- open import Data.List.Properties +-- open import Data.List.Relation.Binary.Pointwise as Pointwise using (Pointwise; []; _∷_) +-- import Data.List.Relation.Binary.Permutation.Setoid as Permutation +-- import Data.List.Relation.Binary.Permutation.Setoid.Properties as Permutation′ +-- open import Data.Nat using (ℕ; zero; suc; s≤s; _*_; _+_) +-- open import Data.Nat.Properties hiding (_≟_) +-- open import Data.Product hiding (map) +-- open import Data.Sum hiding (map) +-- open import Data.Vec as Vec using (Vec; []; _∷_) + +-- open import Function.Base using (_∘′_; _|>_) +-- open import Function.Bundles using (Injection; _↣_; mk↣) + +-- -- open import Relation.Binary.Consequences u +-- open import Relation.Binary.Bundles using (Setoid) +-- open import Relation.Binary.Definitions using (Irreflexive; Trichotomous; tri<; tri≈; tri>) +-- open import Relation.Binary.PropositionalEquality +-- open import Relation.Nullary + +-- -- copied in here because latest stable stdlib doesn't have it?? +-- _⊎-dec_ : ∀{A B : Set} → Dec A → Dec B → Dec (A ⊎ B) +-- does (a? ⊎-dec b?) = does a? ∨ does b? +-- proof (a? ⊎-dec b?) with proof a? +-- ... | ofʸ p = ofʸ (inj₁ p) +-- ... | ofⁿ ¬p with proof b? +-- ... | ofʸ p = ofʸ (inj₂ p) +-- ... | ofⁿ ¬p₁ = ofⁿ (λ { (inj₁ q) → ¬p q; (inj₂ q) → ¬p₁ q }) + +-- infix 6 _⨾_⨾_ + +-- record DisjointPair (A : Set) : Set where +-- constructor _⨾_⨾_ +-- field +-- from : A +-- to : A +-- diff : from ≢ to + +-- data _≐_ {A : Set} : DisjointPair A → DisjointPair A → Set where +-- refl : ∀ {x y diff diff′} → (x ⨾ y ⨾ diff) ≐ (x ⨾ y ⨾ diff′) +-- transpose : ∀ {x y diff diff′} → (x ⨾ y ⨾ diff) ≐ (y ⨾ x ⨾ diff′) + +-- ≐-setoid : (A : Set) → Setoid _ _ +-- ≐-setoid A = record +-- { Carrier = DisjointPair A +-- ; _≈_ = _≐_ +-- ; isEquivalence = record +-- { refl = refl +-- ; sym = (λ { refl → refl ; transpose → transpose }) +-- ; trans = λ +-- { refl refl → refl +-- ; refl transpose → transpose +-- ; transpose refl → transpose +-- ; transpose transpose → refl +-- } +-- } +-- } + +-- -- Variant of DisjointPair for forcing an order + +-- record OrderedPair (A : Set) (_<_ : A → A → Set) : Set where +-- constructor _⨾_⨾_ +-- field +-- from : A +-- to : A +-- ord : from < to + +-- module Pair where +-- open DisjointPair +-- open Injection renaming (f to _⟨$⟩_) + +-- map : {A B : Set} → A ↣ B → DisjointPair A → DisjointPair B +-- map f p .from = f ⟨$⟩ p .from +-- map f p .to = f ⟨$⟩ p .to +-- map f p .diff = p .diff ∘′ injective f + +-- order : +-- {A : Set} {_<_ : A → A → Set} → +-- Trichotomous _≡_ _<_ → DisjointPair A → OrderedPair A _<_ +-- order compare (from ⨾ to ⨾ diff) with compare from to +-- ... | tri< f<t _ _ = from ⨾ to ⨾ f<t +-- ... | tri≈ _ f≡t _ = ⊥-elim (diff f≡t) +-- ... | tri> _ _ f>t = to ⨾ from ⨾ f>t + +-- forget : +-- {A : Set} {_<_ : A → A → Set} → +-- Irreflexive _≡_ _<_ → OrderedPair A _<_ → DisjointPair A +-- forget irrefl (from ⨾ to ⨾ ord) = from ⨾ to ⨾ λ eq → irrefl eq ord + +-- forget∘order : +-- {A : Set} {_<_ : A → A → Set} → +-- (cmp : Trichotomous _≡_ _<_) (irrefl : Irreflexive _≡_ _<_) (p : DisjointPair A) → +-- forget irrefl (order cmp p) ≐ p +-- forget∘order cmp irrefl (from ⨾ to ⨾ diff) with cmp from to +-- ... | tri< f<t _ _ = refl +-- ... | tri≈ _ f≡t _ = ⊥-elim (diff f≡t) +-- ... | tri> _ _ f>t = transpose + +-- -- Multigraphs built inductively + +-- private +-- variable n : ℕ + +-- Vertex : ℕ → Set +-- Vertex = Fin + +-- Edge : ℕ → Set +-- Edge n = DisjointPair (Vertex n) + +-- OEdge : ℕ → Set +-- OEdge n = OrderedPair (Vertex n) _<_ + +-- open module ↭′ n = Permutation (≐-setoid (Vertex n)) using () renaming (_↭_ to [_]_↭_) +-- open module ↭′′ {n} = Permutation (≐-setoid (Vertex n)) hiding (_↭_) +-- module ↭ {n} = Permutation′ (≐-setoid (Vertex n)) + +-- module Graph where +-- data Graph : ℕ → Set where +-- [] : Graph 0 +-- _∷_ : Vec ℕ n → Graph n → Graph (suc n) + +-- -- Empty graph +-- empty : (n : ℕ) → Graph n +-- empty zero = [] +-- empty (suc n) = Vec.replicate 0 ∷ empty n + +-- -- Obtain list of edges + +-- edges′′ : ∀ {k} → Vec ℕ n → Vec (Vertex k) n → List (Edge (suc k)) +-- edges′′ es is = +-- Vec.zipWith (λ n i → replicate n (zero ⨾ suc i ⨾ λ ())) es is |> +-- Vec.toList |> +-- concat + +-- edges′ : Vec ℕ n → List (Edge (suc n)) +-- edges′ es = edges′′ es (Vec.allFin _) + +-- step-edges : List (Edge n) → List (Edge (suc n)) +-- step-edges = List.map (Pair.map (mk↣ Fin.suc-injective)) + +-- edges : Graph n → List (Edge n) +-- edges [] = [] +-- edges (es ∷ g) = edges′ es ++ step-edges (edges g) + +-- -- Degree of a node + +-- degree : Graph n → Vertex n → ℕ +-- degree (es ∷ g) zero = Vec.sum es +-- degree (es ∷ g) (suc i) = Vec.lookup es i + degree g i + +-- -- Easy version of handshaking + +-- Handshake : Graph n → Set +-- Handshake {n} g = sum (List.map (degree g) (allFin n)) ≡ 2 * length (edges g) + +-- handshaking-empty : (n : ℕ) → Handshake (empty n) +-- handshaking-empty zero = refl +-- handshaking-empty (suc n) = {!begin +-- Vec.sum ? + sum (List.map (degree (Vec.replicate 0))) ≡⟨ ? ⟩ +-- ? ∎!} +-- where open ≡-Reasoning +-- -- handshaking : (g : Graph n) → sum (List.map (degree g) (allFin n)) ≡ 2 * length (edges g) +-- -- handshaking [] = refl +-- -- handshaking (es ∷ g) = {!begin +-- -- Vec.sum es + sum (List.map (degree (es ∷ g) ))!} +-- -- where open ≡-Reasoning + +-- -- Add an edge to a graph + +-- infixr 5 _∷ᵉ_ + +-- _∷ᵉ_ : OEdge n → Graph n → Graph n +-- (zero ⨾ suc to ⨾ ord) ∷ᵉ (xs ∷ g) = xs Vec.[ to ]%= suc ∷ g +-- (suc from ⨾ suc to ⨾ s≤s ord) ∷ᵉ (xs ∷ g) = xs ∷ (from ⨾ to ⨾ ord ∷ᵉ g) + +-- -- Construction from edges + +-- private +-- order′ : Edge n → OEdge n +-- order′ = Pair.order Fin.<-cmp + +-- forget′ : OEdge n → Edge n +-- forget′ = Pair.forget Fin.<-irrefl + +-- forget′∘order′ : (e : Edge n) → forget′ (order′ e) ≐ e +-- forget′∘order′ = Pair.forget∘order Fin.<-cmp Fin.<-irrefl + +-- fromEdges : List (Edge n) → Graph n +-- fromEdges es = foldr (λ e g → order′ e ∷ᵉ g) (empty _) es + +-- step-edges-↭ : +-- {es es′ : List (Edge n)} → +-- [ n ] es ↭ es′ → [ suc n ] step-edges es ↭ step-edges es′ +-- step-edges-↭ es↭es′ = +-- ↭.map⁺ (≐-setoid (Vertex (suc _))) (λ { refl → refl ; transpose → transpose }) es↭es′ + +-- edges′′⁻¹-[] : ∀ {k n} (is : Vec (Vertex n) k) → edges′′ (Vec.replicate 0) is ≡ [] +-- edges′′⁻¹-[] [] = refl +-- edges′′⁻¹-[] (i ∷ is) = edges′′⁻¹-[] is + +-- edges′′⁻¹-∷ : ∀ {k n} (es : Vec ℕ k) (is : Vec (Vertex n) k) (j : Fin k) → +-- [ suc n ] +-- edges′′ (es Vec.[ j ]%= suc) is +-- ↭ +-- (zero ⨾ suc (Vec.lookup is j) ⨾ λ ()) ∷ edges′′ es is +-- edges′′⁻¹-∷ (e ∷ es) (i ∷ is) zero = ↭-refl +-- edges′′⁻¹-∷ (e ∷ es) (i ∷ is) (suc j) = begin +-- edges′′ (e ∷ es Vec.[ j ]%= suc) (i ∷ is) ≡⟨⟩ +-- replicate e (zero ⨾ suc i ⨾ λ ()) ++ edges′′ (es Vec.[ j ]%= suc) is ↭⟨ ↭.++⁺ˡ (replicate e (zero ⨾ suc i ⨾ λ ())) (edges′′⁻¹-∷ es is j) ⟩ +-- replicate e (zero ⨾ suc i ⨾ λ ()) ++ (zero ⨾ suc k ⨾ λ ()) ∷ edges′′ es is ↭⟨ ↭.↭-shift (replicate e (zero ⨾ suc i ⨾ λ ())) (edges′′ es is) ⟩ +-- (zero ⨾ suc k ⨾ λ ()) ∷ replicate e (zero ⨾ suc i ⨾ λ ()) ++ edges′′ es is ≡⟨⟩ +-- (zero ⨾ suc k ⨾ λ ()) ∷ edges′′ (e ∷ es) (i ∷ is) ∎ +-- where +-- open PermutationReasoning +-- k = Vec.lookup is j + +-- edges′⁻¹-[] : (n : ℕ) → edges′ {n} (Vec.replicate 0) ≡ [] +-- edges′⁻¹-[] n = edges′′⁻¹-[] (Vec.allFin n) + +-- edges′⁻¹-∷ : +-- (es : Vec ℕ n) (to : Vertex n) → +-- [ suc n ] edges′ (es Vec.[ to ]%= suc) ↭ (zero ⨾ suc to ⨾ λ ()) ∷ edges′ es +-- edges′⁻¹-∷ es to = begin +-- edges′ (es Vec.[ to ]%= suc) ↭⟨ edges′′⁻¹-∷ es (Vec.allFin _) to ⟩ +-- (zero ⨾ suc (Vec.lookup (Vec.allFin _) to) ⨾ λ ()) ∷ edges′ es ≡⟨ cong (λ ◌ → (zero ⨾ suc ◌ ⨾ (λ ())) ∷ edges′ es) (Vec-lookup-tabulate (λ i → i) to) ⟩ +-- (zero ⨾ suc to ⨾ λ ()) ∷ edges′ es ∎ +-- where +-- open PermutationReasoning +-- Vec-lookup-tabulate : +-- {A : Set} (f : Fin n → A) (i : Fin n) → Vec.lookup (Vec.tabulate f) i ≡ f i +-- Vec-lookup-tabulate f zero = refl +-- Vec-lookup-tabulate f (suc i) = Vec-lookup-tabulate (f ∘′ suc) i + +-- edges⁻¹-[] : (n : ℕ) → edges (empty n) ≡ [] +-- edges⁻¹-[] zero = refl +-- edges⁻¹-[] (suc n) = cong₂ (λ ◌ᵃ ◌ᵇ → ◌ᵃ ++ step-edges ◌ᵇ) (edges′⁻¹-[] n) (edges⁻¹-[] n) + +-- edges⁻¹-∷ : (e : OEdge n) (g : Graph n) → [ n ] edges (e ∷ᵉ g) ↭ forget′ e ∷ edges g +-- edges⁻¹-∷ (zero ⨾ suc to ⨾ ord) (xs ∷ g) = ↭.++⁺ʳ (step-edges (edges g)) (begin +-- edges′ (xs Vec.[ to ]%= suc) ↭⟨ edges′⁻¹-∷ xs to ⟩ +-- (zero ⨾ suc to ⨾ _ ∷ edges′ xs) ≋⟨ refl ∷ Pointwise.refl refl ⟩ +-- zero ⨾ suc to ⨾ _ ∷ edges′ xs ∎) +-- where open PermutationReasoning +-- edges⁻¹-∷ (suc from ⨾ suc to ⨾ s≤s ord) (xs ∷ g) = begin +-- edges′ xs ++ step-edges (edges (from ⨾ to ⨾ ord ∷ᵉ g)) ↭⟨ ↭.++⁺ˡ (edges′ xs) (step-edges-↭ (edges⁻¹-∷ (from ⨾ to ⨾ ord) g)) ⟩ +-- edges′ xs ++ step-edges (from ⨾ to ⨾ diff ∷ edges g) ≡⟨⟩ +-- edges′ xs ++ (suc from ⨾ suc to ⨾ _) ∷ step-edges (edges g) ↭⟨ ↭.↭-shift (edges′ xs) (step-edges (edges g)) ⟩ +-- (suc from ⨾ suc to ⨾ _ ∷ edges′ xs ++ step-edges (edges g)) ≋⟨ refl ∷ Pointwise.refl refl ⟩ +-- suc from ⨾ suc to ⨾ _ ∷ edges′ xs ++ step-edges (edges g) ∎ +-- where +-- open PermutationReasoning +-- diff = λ eq → Fin.<-irrefl eq ord + +-- edges⁻¹ : (es : List (Edge n)) → [ n ] edges (fromEdges es) ↭ es +-- edges⁻¹ [] = ↭-reflexive (edges⁻¹-[] _) +-- edges⁻¹ (e ∷ es) = begin +-- edges (order′ e ∷ᵉ fromEdges es) ↭⟨ edges⁻¹-∷ (order′ e) (fromEdges es) ⟩ +-- (forget′ (order′ e) ∷ edges (fromEdges es)) ≋⟨ forget′∘order′ e ∷ Pointwise.refl refl ⟩ +-- e ∷ edges (fromEdges es) <⟨ edges⁻¹ es ⟩ +-- e ∷ es ∎ +-- where open PermutationReasoning + +-- -- Multigraphs as defined by the problem +-- -- I've rearranged the definitions to make things easier to prove + +-- Connects : Vertex n → Edge n → Set +-- Connects v e = DisjointPair.from e ≡ v ⊎ DisjointPair.to e ≡ v + +-- connects : (v : Vertex n) → (e : Edge n) → Dec (Connects v e) +-- connects v e = (DisjointPair.from e ≟ v) ⊎-dec (DisjointPair.to e ≟ v) + +-- degree′ : (E : List (Edge n)) → Vertex n → ℕ +-- degree′ E v = length (filter (connects v) E) + +-- record MultiGraph : Set where +-- field +-- #V : ℕ +-- E : List (Edge #V) + +-- V : List (Vertex #V) +-- V = allFin #V + +-- degree = degree′ E + +-- handshaking : sum (List.map degree V) ≡ 2 * length E +-- handshaking = {!!} |