path: root/src/Problem12.agda

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 = {!!}