konigsberg.lean

import tactic
import combinatorics.quiver
import algebra.big_operators.basic
import data.nat.parity

open_locale big_operators

-- impl notes:
-- we use `psum` as `Prop`-valued quivers are pretty standard - they're just graphs!

-- We use the same universe order as in category theory.
-- See note [category_theory universes]
universes v u

local notation `|` x `|` := finset.card x
local notation `‖` x `‖` := fintype.card x

variable {V : Type u}

inductive upath [quiver.{v} V] (a : V) : V → Sort (max (u + 1) v)
| nil  : upath a
| cons : Π {b c : V}, upath b → psum (b ⟶ c) (c ⟶ b) → upath c

instance [quiver.{v} V] {a : V} : inhabited (upath a a) := ⟨upath.nil⟩

namespace upath

section basic

variables [quiver.{v} V] {a b c : V} (p : upath a b)

-- `has_mem` doesn't like `Sort` so this is "manual"
inductive mem : Π {w x y z : V}, (w ⟶ x) → upath y z → Prop
| inl {a b c} (f : a ⟶ b) : ∀ p : upath c a, mem f $ p.cons $ psum.inl f
| inr {a b c} (f : b ⟶ a) : ∀ p : upath c a, mem f $ p.cons $ psum.inr f
| consl {a b c d x} {f : a ⟶ b} {g : c ⟶ d} {h : upath x c} :
    mem f h → mem f (h.cons $ psum.inl g)
| consr {a b c d x} {f : a ⟶ b} {g : d ⟶ c} {h : upath x c} :
    mem f h → mem f (h.cons $ psum.inr g)

-- I really don't know how to make the eqn compiler work here
def len : ℕ := upath.rec_on p 0 (λ _ _ _ _, (+ 1))

@[simp] lemma len_nil : (upath.nil : upath a a).len = 0 := rfl

@[simp] lemma len_cons (t : psum (b ⟶ c) (c ⟶ b)) : (p.cons t).len = p.len + 1 := rfl

instance [decidable_eq V] [Π a b : V, decidable_eq (a ⟶ b)] : decidable_eq (quiver.total V) :=
by tactic.mk_dec_eq_instance

end basic

section typed

variables [quiver.{v+1} V]
          [fintype V] [Π a b: V, fintype (a ⟶ b)]
          [decidable_eq V] [Π a b : V, decidable_eq (a ⟶ b)]

instance : fintype (quiver.total V) :=
{ elems := finset.univ.bUnion $ λ t : V × V,
           finset.image (λ f : t.fst ⟶ t.snd, ⟨t.fst, t.snd, f⟩) finset.univ,
  complete := λ x, by { rw finset.mem_bUnion,
    refine ⟨⟨x.left, x.right⟩, finset.mem_univ _, _⟩,
    rw finset.mem_image,
    exact ⟨x.hom, finset.mem_univ _, by simp [quiver.total.ext_iff]⟩ } }

def eulerian {x y : V} (p : upath x y) :=
p.len = ‖quiver.total V‖ ∧ ∀ a b, ∀ h : a ⟶ b, mem h p

end typed

end upath

variables [quiver.{v+1} V] [fintype V] [Π a b: V, fintype (a ⟶ b)]

def degree (a : V) := ∑ v : V, (‖a ⟶ v‖ + ‖v ⟶ a‖)

variables [decidable_eq V] [Π a b : V, decidable_eq (a ⟶ b)]

lemma even_degree_of_euler_circuit {a : V} (p : upath a a) (hp : p.eulerian) :
∀ v : V, even (degree v) :=
begin
  -- `by_contra` and `apply`ing without the `@` this was bugged?
  apply @classical.by_contradiction _,
  intro h,
  push_neg at h,
  obtain ⟨v, odd_deg⟩ := h,
  obtain ⟨k, h⟩ := nat.odd_iff_not_even.mpr odd_deg,
  clear odd_deg,
  -- if it helps can assume that `v ≠ a`, by "cyclic shifting" Euler-path
end