multigraph_defs.lean

import data.sym2
import data.fintype.basic
import algebra.big_operators
import tactic

open_locale big_operators

universes u v

structure link (V : Type u) (E : Type v) :=
(fst : V) (via : E) (snd : V)

namespace link
variables {V : Type u} {E : Type v}

@[simps] def rev (x : link V E) : link V E := ⟨x.snd, x.via, x.fst⟩

/-- Are the two links for the same edge? -/
def same_edge (x y : link V E) : Prop := x = y ∨ x = y.rev

def is_loop (x : link V E) : Prop := x.fst = x.snd

instance [decidable_eq V] (x : link V E) : decidable x.is_loop :=
by { unfold is_loop, apply_instance }

end link

/-
Chou, C.-T.
Melham, T. F. & Camilleri, J. (Eds.)
A formal theory of undirected graphs in higher-order logic 
Higher Order Logic Theorem Proving and Its Applications, Springer Berlin Heidelberg, 1994, 144-157
https://doi.org/10.1007/3-540-58450-1_40

Finiteness: can say [fintype V], [fintype E], and [∀ v, fintype (G.darts_at v)]
-/
structure multigraph₁ (V : Type u) (E : Type v) :=
(links : set (link V E))
(link_rev : link.rev '' links ⊆ links)
(has_edges : link.via '' links = set.univ)
(efficient : ∀ {x y : link V E}, x ∈ links → y ∈ links → x.via = y.via → link.same_edge x y)

namespace multigraph₁
variables {V : Type u} {E : Type v}

/-- The set of links that start at a given vertex. -/
def links_at (G : multigraph₁ V E) (v : V) : set (link V E) := {x | x ∈ G.links ∧ x.fst = v}

/-- The set of vertices neighboring a vertex. -/
def neighbor_set (G : multigraph₁ V E) (v : V) : set V := link.snd '' G.links_at v

/-- The set of incident edges at a vertex. -/
def incidence_set (G : multigraph₁ V E) (v : V) : set E := link.via '' G.links_at v

lemma has_edges' (G : multigraph₁ V E) (e : E) : ∃ (x : link V E), x ∈ G.links ∧ x.via = e :=
begin
  have h : e ∈ set.univ := set.mem_univ _,
  rw ←G.has_edges at h,
  exact h,
end

/-- The halves of each edge.  Loop edges have two halves, hence `side`. -/
structure darts_at [decidable_eq V] (G : multigraph₁ V E) (v : V) :=
(x : link V E)
(hx : x ∈ G.links_at v)
(side : if x.is_loop then bool else unit)

def degree [decidable_eq V] (G : multigraph₁ V E) (v : V) [fintype (G.darts_at v)] : ℕ :=
fintype.card (G.darts_at v)

instance [decidable_eq E] (G : multigraph₁ V E) (v : V) :
  decidable_eq (G.incidence_set v) :=
by { rintros ⟨e₁, he₁⟩ ⟨e₂, he₂⟩, apply_instance, }

instance [decidable_eq V] [decidable_eq E] (G : multigraph₁ V E) (v : V) [fintype (G.darts_at v)] :
  fintype (G.incidence_set v) :=
begin
  let f : G.darts_at v → G.incidence_set v := λ d, ⟨d.x.via, d.x, d.hx, rfl⟩,
  have h : function.surjective f,
  { rintro ⟨e, x, hx, rfl⟩,
    let d : G.darts_at v,
    { use [x, hx],
      split_ifs,
      { exact tt, },
      { exact (), }, },
    use d, },
  exact fintype.of_surjective f h,
end

end multigraph₁


/-- Finiteness: can say [fintype V], [fintype E], and [∀ v, fintype (G.darts_at v)]
-/
structure multigraph₂ (V : Type u) (E : Type v) :=
(ends : E → sym2 V)

namespace multigraph₂
variables {V : Type u} {E : Type v}

/-- The set of vertices neighboring a vertex. -/
def neighbor_set (G : multigraph₂ V E) (v : V) : set V := {w : V | ⟦(v, w)⟧ ∈ G.ends '' set.univ}

/-- The set of incident edges at a vertex. -/
def incidence_set (G : multigraph₂ V E) (v : V) : set E := {e : E | v ∈ G.ends e}

def is_loop (G : multigraph₂ V E) (e : E) : Prop := (G.ends e).is_diag

/-- The halves of each edge.  Loop edges have two halves, hence `side`.
(A different version of `multigraph₁.darts_at`.) -/
@[derive decidable_eq]
inductive darts_at (G : multigraph₂ V E) (v : V)
| standard (e : E) (hi : e ∈ G.incidence_set v) (hs : ¬G.is_loop e) : darts_at
| loop (e : E) (hi : e ∈ G.incidence_set v) (hl : G.is_loop e) (side : bool) : darts_at

def degree (G : multigraph₂ V E) (v : V) [fintype (G.darts_at v)] : ℕ := fintype.card (G.darts_at v)

instance [decidable_eq V] (G : multigraph₂ V E) (v : V) (e : E) : decidable (e ∈ G.incidence_set v) :=
by { dunfold incidence_set, apply_instance }

instance [decidable_eq V] (G : multigraph₂ V E) (e : E) : decidable (G.is_loop e) :=
by { dunfold is_loop, apply_instance }

instance [decidable_eq V] [decidable_eq E] (G : multigraph₂ V E)
  [fintype E] (v : V) : fintype (G.darts_at v) :=
begin
  let es := (finset.univ : finset E).filter (λ e, v ∈ G.ends e),
  let f : E → finset (G.darts_at v),
  { intro e,
    by_cases hi : e ∈ G.incidence_set v,
    by_cases hl : G.is_loop e,
    exact {darts_at.loop e hi hl ff, darts_at.loop e hi hl tt},
    exact {darts_at.standard e hi hl},
    exact ∅, },
  use finset.univ.bind f,
  rintro (⟨e, hi, hl⟩|⟨e, hi, hl, side⟩);
    rw finset.mem_bind;
    use e;
    simp only [finset.mem_univ, true_and];
    simp [f, hi, hl],
  cases side; simp,
end

end multigraph₂

/-- A multigraph is a collection of "darts" (oriented edges) along with a
fixed-point free involution on darts, a surjective map to edges, and a map to vertices.
The map `via : dart → E` is the quotient map by the involution.

Finiteness: [fintype V], [fintype E], and [∀ v, fintype (G.darts_at v)]
-/
structure multigraph₃ (V : Type u) (E : Type v) :=
(dart : Type v)
(rev : dart → dart)
(rev_invol : function.involutive rev)
(rev_ne : ∀ (d : dart), rev d ≠ d)
(via : dart → E)
(via_rev : ∀ (d : dart), via (rev d) = via d)
(fst : dart → V)
(has_edges: function.surjective via)
(is_quo: ∀ {d d' : dart}, via d = via d' → d = d' ∨ d = rev d')

namespace multigraph₃
variables {V : Type u} {E : Type v}

/-- The vertex opposite the dart. -/
def snd (G : multigraph₃ V E) (d : G.dart) : V := G.fst (G.rev d)

@[simp] lemma rev_rev (G : multigraph₃ V E) (d : G.dart) : G.rev (G.rev d) = d :=
G.rev_invol d

def darts_at (G : multigraph₃ V E) (v : V) : set G.dart := {d | G.fst d = v}

/-- The set of vertices neighboring a vertex. -/
def neighbor_set (G : multigraph₃ V E) (v : V) : set V := G.snd '' G.darts_at v

/-- The set of incident edges at a vertex. -/
def incidence_set (G : multigraph₃ V E) (v : V) : set E := G.via '' G.darts_at v

def is_loop (G : multigraph₃ V E) (e : E) : Prop :=
∃ (d : G.dart), G.via d = e ∧ G.fst d = G.snd d

def degree (G : multigraph₃ V E) (v : V) [fintype (G.darts_at v)] : ℕ := fintype.card (G.darts_at v)

/-- A function with this class has an associated computation for the preimages. -/
class finite_preimages {α : Type u} {β : Type v} (f : α → β) :=
(preimage : β → finset α)
(is_preimage : ∀ (b : β) (a : α), f a = b ↔ a ∈ preimage b)

noncomputable
instance (G : multigraph₃ V E) : finite_preimages G.via :=
begin
  classical,
  fsplit,
  { exact λ e, let d := classical.some (G.has_edges e) in {d, G.rev d}, },
  { intros e d,
    have hd := classical.some_spec (G.has_edges e),
    split,
    { rintro rfl,
      cases G.is_quo hd with h h; simp [h], },
    { simp, rintro (rfl|rfl),
      exact hd,
      rw G.via_rev,
      exact hd, }, },
end

noncomputable
instance (G : multigraph₃ V E) [fintype E] : fintype G.dart :=
begin
  classical,
  haveI : finite_preimages G.via := infer_instance,
  use finset.univ.bind (finite_preimages.preimage G.via),
  intro d,
  rw finset.mem_bind,
  use G.via d,
  simp only [finset.mem_univ, true_and],
  rw ←finite_preimages.is_preimage,
end

noncomputable
instance finite_darts_at_from_edges (G : multigraph₃ V E)
  [fintype E] (v : V) : fintype (G.darts_at v) :=
by { dunfold darts_at, apply_instance }

instance finite_darts_at_from_darts [decidable_eq V] (G : multigraph₃ V E)
  [fintype G.dart] (v : V) : fintype (G.darts_at v) :=
by { dunfold darts_at, apply_instance }

end multigraph₃


/--
Like multigraph₃, but make darts more important than edges.

A multigraph is a collection of darts (half edges) with maps to V, and the darts are
put together into edges via an involution.

Downside: definition of multigraph with labeled edges needs to be something like
having a labeling function `f : D → L` such that `f (G.rev d) = f d`.

finiteness: with [fintype V], [fintype D], and [∀ v, fintype (G.darts_at v)]
-/
structure multigraph₄ (V : Type u) (D : Type v) :=
(rev : D → D)
(rev_invol : function.involutive rev)
(rev_ne : ∀ (d : D), rev d ≠ d)
(fst : D → V)

namespace multigraph₄
variables {V : Type u} {D : Type v}

def snd (G : multigraph₄ V D) (d : D) : V := G.fst (G.rev d)

@[simp] lemma rev_rev (G : multigraph₄ V D) (d : D) : G.rev (G.rev d) = d :=
G.rev_invol d

def same_edge (G : multigraph₄ V D) (d d' : D) : Prop := d = d' ∨ d = G.rev d'

def edge_setoid (G : multigraph₄ V D) : setoid D :=
{ r := G.same_edge,
  iseqv := begin
    fsplit,
    { intro x, exact or.inl rfl, },
    fsplit,
    { rintros x y (rfl|rfl); simp [same_edge], },
    { rintros x y z (rfl|rfl) (rfl|rfl); simp [same_edge], },
  end }

def edge (G : multigraph₄ V D) : Type v := quotient G.edge_setoid

def via (G : multigraph₄ V D) (d : D) : G.edge := @quotient.mk _ G.edge_setoid d

def darts_at (G : multigraph₄ V D) (v : V) : set D := {d | G.fst d = v}

/-- The set of vertices neighboring a vertex. -/
def neighbor_set (G : multigraph₄ V D) (v : V) : set V := G.snd '' G.darts_at v

/-- The set of incident edges at a vertex. -/
def incidence_set (G : multigraph₄ V D) (v : V) : set G.edge := G.via '' G.darts_at v

def dart_of_loop (G : multigraph₄ V D) (d : D) : Prop := G.fst d = G.snd d
def is_loop (G : multigraph₄ V D) (e : G.edge) : Prop := ∃ (d : D), G.via d = e ∧ G.dart_of_loop d

def degree (G : multigraph₄ V D) (v : V) [fintype (G.darts_at v)] : ℕ := fintype.card (G.darts_at v)


end multigraph₄


/--
Similar to what is in hedetniemi.  It is in some sense dual to multigraph₄.

finiteness: [fintype V] and [∀ v w, fintype (edges v w)], but having finitely many edges is more awkward,
as is local finiteness

it's less clear how to have labeled edges.

Note: rev could be asserting equalities, but then would need to figure out to do loop edges
(which are essentially handled with rev_ne)
-/
structure multigraph₅ (V : Type u) :=
(edges : V → V → Type v)
(rev : Π {v w : V}, edges v w ≃ edges w v)
(rev_rev : ∀ {v w : V} (e : edges v w), rev (rev e) = e)
(rev_ne : ∀ {v : V} (e : edges v v), rev e ≠ e)

namespace multigraph₅
variables {V : Type u}

/-- The set of vertices neighboring a vertex. -/
def neighbor_set (G : multigraph₅ V) (v : V) : set V := {w | nonempty (G.edges v w)}

/-- A dart is a vertex along with an incident edge. -/
def darts_at (G : multigraph₅ V) (v : V) : Type (max u v) := Σ (w : V), G.edges v w

structure link (G : multigraph₅ V) :=
(fst snd : V)
(via : G.edges fst snd)

namespace link
variables {G : multigraph₅ V}

@[simps]
def rev (x : G.link) : G.link :=
{ fst := x.snd,
  snd := x.fst,
  via := G.rev x.via }

@[simp] lemma rev_rev (x : G.link) : x.rev.rev = x :=
by { cases x with fst snd via, simp [rev, G.rev_rev] }

@[simps]
def rev_setoid : setoid G.link :=
{ r := λ x y, x = y ∨ x = y.rev,
  iseqv := begin
    fsplit,
    { intro x, simp, },
    fsplit,
    { rintros x y (rfl|rfl); simp, },
    { rintros x y z (rfl|rfl) (rfl|rfl); simp, },
  end }

end link

/-- The set of all edges, which are links modulo `rev`. -/
def E (G : multigraph₅ V) : Type (max u v) := @quotient G.link link.rev_setoid

/-- The edge in `E` associated to an edge in one of the edge sets. -/
def via (G : multigraph₅ V) {v w : V} (e : G.edges v w) : G.E :=
@quotient.mk G.link link.rev_setoid (link.mk v w e)

/-- The set of incident edges at a vertex. -/
def incidence_set (G : multigraph₅ V) (v : V) : set G.E :=
{e' : G.E | ∃ (w : V) (e : G.edges v w), G.via e = e'}

/-- degree seems to need finiteness of `V` -- though there are probably clever ways of
indicating local finiteness -/
def degree (G : multigraph₅ V) (v : V) [fintype V] [∀ w, fintype (G.edges v w)] : ℕ :=
∑ (w : V), fintype.card (G.edges v w)

end multigraph₅


@[derive decidable_eq]
inductive inc_type
| none
| standard
| loop

def inc_type.val : inc_type → ℕ
| inc_type.none := 0
| inc_type.standard := 1
| inc_type.loop := 2

/--
Suggestion by Peter Nelson.  I needed a `finset` to formalize it (so that the `sum` property could
be a sum), but the `sum` property can surely be rewritten without `ends` and `ends_prop`.
(`ends` is determined by `sum` and `inc`).

Finiteness: [fintype V], [fintype E], [∀ v, fintype (G.incidence_set v)]
-/
structure multigraph₆ (V : Type u) (E : Type v) :=
(inc : V → E → inc_type)
(ends : E → finset V)
(ends_prop : ∀ v e, inc v e ≠ inc_type.none ↔ v ∈ ends e)
(sum : ∀ e, (∑ v in ends e, (inc v e).val) = 2)
-- or:
--(sum : ∀ e, (ends e).sum (λ v, (inc v e).val) = 2)

namespace multigraph₆
variables {V : Type u} {E : Type v}

def is_incident (G : multigraph₆ V E) (v : V) (e : E) : Prop := G.inc v e ≠ inc_type.none

/-- The set of incident edges at a vertex. -/
def incidence_set (G : multigraph₆ V E) (v : V) : set E := {e | G.is_incident v e}

/-- Check that `w` is opposite `v` through `e`. -/
def is_opp (G : multigraph₆ V E) (v : V) (e : E) (w : V) : Prop :=
match G.inc v e with
| inc_type.none := false
| inc_type.loop := v = w
| inc_type.standard := G.inc v e = inc_type.standard ∧ v ≠ w
end

/-- The set of vertices neighboring a vertex. -/
def neighbor_set (G : multigraph₆ V E) (v : V) : set V :=
{w | ∃ e, G.is_opp v e w }

def is_loop (G : multigraph₆ V E) (e : E) : Prop :=
∃ v, G.inc v e = inc_type.loop

def degree (G : multigraph₆ V E) (v : V) [fintype (G.incidence_set v)] :=
∑ e in (G.incidence_set v).to_finset, (G.inc v e).val
-- or:
--(G.incidence_set v).to_finset.sum (λ e, (G.inc v e).val)

end multigraph₆