MonoidMusician/graph.lean

## graph.lean
-- This work by Nick Scheel is licensed under CC0 1.0
-- https://creativecommons.org/publicdomain/zero/1.0/

-- A basic framework for graph theory on multidigraphs in Lean
-- and a proof that no_watershed_condition is sufficient to
-- establish that a graph has a unique sink for each vertex
--
-- I hope to give some introduction to the syntax of how Lean works here,
-- but I assume some familiarity with functions, pattern matching,
-- type theory, and proofs.
--
-- The most important thing to note is that `begin` and `end` delineate
-- sections of code in "tactic/interactive proof mode" (as opposed to
-- "term mode"). The Lean compiler shows the proof goal and the available
-- assumptions and context, and then shows how it changes after tactics
-- are executed. The best way to see this happen is to download Lean from
-- the following links and open it in VSCode (or emacs) and walk through
-- the steps of a proof to see the changes.
--
-- VSCode: "Typing ctrl-shift-enter opens up a message window which shows you
-- error messages, warnings, output, and goal information when in tactic mode."
-- Emacs: "C-c C-g	show goal in tactic proof (lean-show-goal-at-pos)"
-- (https://leanprover.github.io/reference/using_lean.html)
--
-- Make sure to create a project folder and install mathlib as explained here:
-- https://leanprover.github.io/reference/using_lean.html#using-the-package-manager
--
-- http://leanprover.github.io/
-- https://github.com/leanprover/lean

-- Quick primer on Lean:
--
-- Propositions are types. This means that the mathematical language of Lean is
-- the language of types, which can encode any sensical sentence about math.
-- Types are, of course, also used in the design of computable programming
-- languages, which Lean also is. But "mere" propositions don't contain data
-- to compute on: only the type of a proof matters, really, not its exact details.
--
-- The term language and the type language are the same, which means that values
-- can be mentioned in types, and vice-versa. This is a result of dependent type
-- theory, and it allows encoding interesting propositions, such as about the value
-- of functions: given some (f : ℝ → ℝ), (∀ x : ℝ, x > 0 → f x = 0) is the
-- proposition that, for positive values of `x`, `f x` evaluates to zero. Note that
-- `f` is a fixed value, and `x` is a variable value, both mentioned at the type level.
--
-- ∀ is actually the same thing as Π – they are notation for dependently-typed
-- functions. (f : Π (a : α), β a) is a function that takes an element `a` of type `α`
-- and returns a result that `β a`, with a type that can depend on the value of `a`.
-- Putting this together, if we have `f` as above, and some `v : α`, then `f v : β v`
-- (meaning, the value of `f` applied to `v` has type `β v`).
-- If `β a` does _not_ depend on `a` (that is, if `β` is a constant function, say,
-- β = λ _, γ), then the type of `f` can be written as `α → γ`, the type of a
-- non-dependent function, also familiar as implication from logic.
-- The cool bit about dependent functions, though, is that they are also used to
-- introduce polymorphism, if `α` is chosen to be `Type` (or `Prop`, or `Sort u`
-- most generally). So `(λ _ a, a) : ∀ {α : Type}, α → α` is the polymorphic
-- identity function. Note that function terms are introduced with lambdas:
--    def f : Π (a : α), β a :=
--      λ (a : α), <some value of type `β a` using `a : α` in scope>
--
-- But more typically, top-level definitions will have this alternate syntax:
--    def f (a : α) : β a := <some value of type `β a` using `a : α` in scope>
-- There are subtle differences, but they are basically the same, just note
-- that in this latter form, (a : α) is already in scope without the lambda binder!
--
-- I mention this below, but for completeness, there is existential quantification:
-- (∃ (a : α), p a) : Prop, and dependent products: (Σ' (a : α), p a) : Type.
-- Dependent products give access to the value and the proof, whereas existentials
-- only assert that there is such a value, without giving it explicitly.
-- This is the difference between (non-computable) classical logic and (computable)
-- intuitionistic logic. See https://homotopytypetheory.org/book/ for more.
--
-- Definitional versus propositional equality: there are two varieties of equality:
-- `:=` is the syntax used to declare equalities, most of the time, and
-- `=` is the proposition that two things are equal. The Lean compiler will solve
-- definitional equalities, and this can be turned into a propositional equality
-- using `refl a : a = a` (standing for the reflexivity of equality).
-- For example, `refl 1 : 1 = 1` is the proof that 1 equals itself. Duh!
-- `eq.trans (e1 : a = b) (e2 : b = c) : a = c` is an example where, even though
-- `a`, `b`, and `c` are not known in advance (and thus are not definitionally
-- equal), their propositional equalities can still be combined.

-- Import libraries that this file depends on
import data.fintype data.equiv

-- Just a universe variable (used to avoid Girard's/Russel's paradox).
-- Not so important; see the following for more:
-- https://leanprover.github.io/reference/other_commands.html
-- https://en.wikipedia.org/wiki/Intuitionistic_type_theory#Universe_Types
universe u

-- A few helpful lemmata, explanations skipped
theorem psigma_elim_exists {α : Type} {β : α → Prop} {r : Prop} :
    Exists β → (psigma β → r) → r :=
        λ e f, exists.elim e (λ a b, f (psigma.mk a b))

theorem subtype_elim_exists {α : Type} {β : α → Prop} {r : Prop} :
    Exists β → (subtype β → r) → r :=
        λ e f, exists.elim e (λ a b, f (subtype.mk a b))

lemma list.nodup_tail_of_nodup {α : Type} {l : list α} :
    list.nodup l → list.nodup (list.tail l) :=
    begin
    intro nd,
    cases l,
    exact list.nodup_nil,
    rw list.tail_cons,
    apply list.nodup_of_nodup_cons,
    exact nd,
    end

-- end lemmata

-- First we will need to define the types that characterize a (multi)digraph.

-- An arc connects a starting and ending vertex; this defines the Type for that.
-- in particular, this states that, given a Type (call it V), arcT V is a Type
-- defined as `V × V`, which is an ordered pair consisting of two elements of type V.
def arcT (V : Type) : Type := V × V
def arcT.mk {V : Type} (v1 v2 : V) : arcT V :=
    prod.mk v1 v2

-- Each digraph has a particular type of vertices, type of arcs, and consists of
-- the mapping φ from specific arcs to their starting and ending vertices.
structure digraph
    (V E : Type) : Type :=
        (φ : E → arcT V)

-- `arc G v1 v2` is an arc that goes from v1 to v2 in graph G.
-- V and E are implicit arguments (since they use {}): they can be filled in
-- once we know what the type of G is, since (G : digraph V E) mentions V and E.
def arc
    {V E : Type} (G : digraph V E)
    (v1 v2 : V) :=
        -- this is an edge paired with a proof that the edge connects
        -- the vertices mentioned in the type of the arc
        Σ'(e : E), G.φ e = arcT.mk v1 v2

-- The proposition that an arc exists, without specifying the arc itself.
def has_arc
    {V E : Type} (G : digraph V E)
    (v1 v2 : V) :=
        ∃ (e : E), G.φ e = arcT.mk v1 v2

-- Eliminate the existential has_arc with a non-dependent proof function taking an arc.
def has_arc.elim
    {V E : Type} {G : digraph V E}
    {v1 v2 : V} {r : Prop} :
    has_arc G v1 v2 → (arc G v1 v2 → r) → r :=
        psigma_elim_exists

namespace digraph

-- Get the source of an edge E in a graph G
def source
    {V E : Type} (G : digraph V E)
    (e : E) : V := (G.φ e).1

-- Target of an arc
def target
    {V E : Type} (G : digraph V E)
    (e : E) : V := (G.φ e).2

-- An initial vertex has no edges leading to it in G
def is_initial
    {V E : Type} (G : digraph V E)
    (v : V) : Prop :=
        ¬∃ (e : E), target G e = v

-- A final vertex has no edges leading from it in G
def is_final
    {V E : Type} (G : digraph V E)
    (v : V) : Prop :=
        ¬∃ (e : E), source G e = v

-- Subtype generated by is_initial
-- (that is, a vertex with a proof that it is initial)
def initial
    {V E : Type} (G : digraph V E) :=
        { v : V // is_initial G v }

-- Subtype generated by is_final
def final
    {V E : Type} (G : digraph V E) :=
        { v : V // is_final G v }

-- A walk, as an inductive type, consists of arcs where each next arc leads
-- from the previous arc. This is encoded by matching the vertices at the type
-- level: only an arc from v1 to v2 and a walk from v2 to v3 can produce a walk
-- from v1 to v3.
-- Again, V and E can be figured out from an explicit G.
inductive walk
    {V E : Type} (G : digraph V E) :
    V → V → Type
    | empty {v : V} : walk v v
    | step {v1 v2 v3 : V} : arc G v1 v2 → walk v2 v3 → walk v1 v3

-- This begins a namespace; everything declared in this namespace will be accessed
-- with the prefix `walk.` outside of the namespace, like `walk.length`
namespace walk

-- The edges underlying a walk.
-- This is a function defined by taking some arguments (most notably a walk)
-- and returning a list of elements of type E.
-- Note that G is implicit: it's inferrable from the type of the walk given to edges
def edges
    {V E : Type} {G : digraph V E}
    {v1 v2 : V} :
    walk G v1 v2 → list E :=
    -- this is tactic mode
    begin
    -- `intro` introduces the argument `w : walk G v1 v2`
    intro w,
    -- `induction` takes apart the two cases of `w` (`empty` and `step`)
    -- and adds an induction hypothesis for the nested walk in the `step` case
    induction w,
    -- for the first case, we want to produce an empty list
    -- `exact` just means that we are finishing the goal with a suitable term
    exact list.nil,
    -- for the second case, we `cons`truct a new list by adding the edge
    -- of the arc on the front to the front on the rest of the edges
    -- (note that w_a and w_ih are names automatically generated by `induction w`)
    exact list.cons w_a.1 w_ih,
    end

-- The vertices visited in a walk, including the start and end vertices
-- (which are already mentioned in the type).
def vertices
    {V E : Type} {G : digraph V E}
    {v1 v2 : V} :
    walk G v1 v2 → list V :=
    begin
    -- similar story, but we start with v2 in the empty case
    intro w, induction w,
    exact list.cons v2 list.nil,
    -- and add v1 at each step
    exact list.cons w_v1 w_ih,
    end

-- The length of a walk, i.e. the number of arcs used in it, as a natural number.
def length
    {V E : Type} {G : digraph V E}
    {v1 v2 : V} :
    walk G v1 v2 → ℕ :=
    begin
    intro w,
    induction w,
    exact 0,
    -- Note: nat.succ n = n+1, get used to it ;)
    exact nat.succ w_ih,
    end

-- This is our first lemma; it's like a definition but usually it contains a proof,
-- (in this case: a proof that the length of an empty walk is 0). Conceptually,
-- in type theory, there is no real difference: this is just another
-- dependently-typed function, taking variables V E G and v and returning a result.
@[simp] -- this attribute lets it get picked up by the `simp` tactic
lemma length_empty
    {V E : Type} {G : digraph V E}
    {v : V} :
    -- (empty G : walk G v v) is just a type annotation specifying v
    -- This could be written (empty _ : walk G v v), since G is
    -- inferrable by unification
    length (empty G : walk G v v) = 0 :=
      by refl -- definitional equality holds here

@[simp]
lemma length_step
    {V E : Type} {G : digraph V E}
    {v1 v2 v3 : V}
    (a : arc G v1 v2)
    (w : walk G v2 v3) :
    length (step a w) = length w + 1 :=
      by refl

-- A walk from v1 to v2 can be concatenated with a walk from v2 to v3 by first
-- taking the arcs from the first walk, then taking the arcs from the second.
-- This is a binary function with two arguments, nothing else is new.
def concat
    {V E : Type} {G : digraph V E}
    {v1 v2 v3 : V} :
    walk G v1 v2 → walk G v2 v3 → walk G v1 v3 :=
    begin
    intros w1 w2,
    induction w1,
    exact w2,
    exact step w1_a (w1_ih w2),
    end

-- A proof of a fact that's obvious enough for the equation compiler to solve
@[simp]
lemma concat_empty_left
    {V E : Type} {G : digraph V E}
    {v1 v2 : V}
    (w : walk G v1 v2) :
    concat (empty G) w = w :=
      by refl

-- Again, pretty obvious
lemma concat_step_left
    {V E : Type} {G : digraph V E}
    {v1 v2 v3 v4 : V}
    (a : arc G v1 v2)
    (w1 : walk G v2 v3)
    (w2 : walk G v3 v4) :
    concat (step a w1) w2 = step a (concat w1 w2) :=
      by refl

-- But this one needs to be solved by induction, since there's no special case
-- for an empty walk on the right (one must walk through all of the first walk).
@[simp]
lemma concat_empty_right
    {V E : Type} {G : digraph V E}
    {v1 v2 : V}
    (w : walk G v1 v2) :
    concat w (empty G) = w :=
    begin
    -- luckily it is simple using induction
    induction w,
    refl,
    -- `rw` (or `rewrite`) is a tactic that changes the type of the goal
    -- given particular equalities; in this case, it finishes the goal too.
    rw [concat_step_left, w_ih],
    end

-- Concatenating walks adds their length.
lemma concat_length
    {V E : Type} {G : digraph V E}
    {v1 v2 v3 : V}
    (w1 : walk G v1 v2)
    (w2 : walk G v2 v3) :
    length (concat w1 w2) = length w1 + length w2 :=
    begin
    induction w1,
    -- this is easy enough for the tactic to solve by simplification,
    -- by using these facts (available with the [simp] attribute):
    -- 1. concat (empty G) w2 = w2
    -- 2. length (empty G) = 0
    simp,
    -- provide two additional theorems to help `simp` close the goal:
    simp [concat_step_left, w1_ih],
    end

-- Useful lemmata regarding walk.vertices
-- (still inside the walk namespace!)
namespace vertices

-- Takes an assumption that the walk is empty, making it easier to use
-- when the proof is not obviously `refl`. When it is obvious, use:
--     rw [walk.vertices.empty _ rfl],
@[simp]
def empty
    {V E : Type} {G : digraph V E}
    {v : V}
    (w : walk G v v) :
    (w = walk.empty G) → walk.vertices w = [v] :=
        λ h, eq.substr h rfl

-- Takes an assumption that the walk is nonempty, making it easier to use
-- when the proof is not obviously `refl`. When it is obvious, use:
--     rw [walk.vertices.step _ _ _ rfl],
@[simp]
def step
    {V E : Type} {G : digraph V E}
    {v1 v2 v3 : V}
    (a : arc G v1 v2)
    (w : walk G v2 v3)
    (w' : walk G v1 v3) :
    (w' = walk.step a w) → walk.vertices w' = v1 :: walk.vertices w :=
        λ h, eq.substr h rfl

-- The list of vertices of a walk starts with the starting vertex of the walk.
def starts_with
    {V E : Type} {G : digraph V E}
    {v1 v2 : V}
    (w : walk G v1 v2) :
    walk.vertices w = v1 :: list.tail (walk.vertices w) :=
    begin
    cases w, refl, refl,
    end

-- The list of vertices follow concatenation ... except for the first vertex of
-- the second walk, which would be duplicated by just joining the verticces,
-- since it is the last entry in `walk.vertices w1` already.
def concat
    {V E : Type} {G : digraph V E}
    {v1 v2 v3 : V}
    (w1 : walk G v1 v2)
    (w2 : walk G v2 v3)
    (w3 : walk G v1 v3) :
    (w3 = walk.concat w1 w2) →
        walk.vertices w3 = walk.vertices w1 ++ list.tail (walk.vertices w2) :=
    begin
    intro h, rw h,
    induction w1,
    { simp, exact starts_with w2 },
    rw [concat_step_left w1_a w1_a_1 w2],
    -- simplify right side
    rw [step w1_a w1_a_1 _ rfl],
    -- simplify left side
    rw [step w1_a (concat w1_a_1 w2) _ rfl],
    -- pass through the cons, and apply induction hypothesis
    congr, apply w1_ih _ _ rfl,
    end

end vertices
end walk
-- close out the namespaces; back to the default namespace of this file

-- Back to types, a similar story regarding paths as walks:
-- A path is a walk with a proof that vertices are not repeated.
def path
    {V E : Type} (G : digraph V E) :
    V → V → Type :=
    λ v1 v2, { w : walk G v1 v2 // list.nodup (walk.vertices w) }

-- The proposition that a path between two vertices merely exists.
def has_path
    {V E : Type} (G : digraph V E) :
    V → V → Prop :=
    λ v1 v2, ∃ (w : walk G v1 v2), list.nodup (walk.vertices w)

-- Eliminate the existential has_path via a real path
def has_path.elim
    {V E : Type} {G : digraph V E}
    {v1 v2 : V} {r : Prop} :
    has_path G v1 v2 → (path G v1 v2 → r) → r :=
        subtype_elim_exists

namespace path

-- An empty path is simple to generate; its list of 1 vertex obviously has no
-- duplicates.
def empty
    {V E : Type} (G : digraph V E)
    {v : V} : path G v v :=
    begin
    -- `apply` is sort of like `exact`, but it expects a function that requires more
    -- arguments to reach the proof goal.
    -- In particular, this starts to create a subtype with the value `empty`
    apply subtype.mk (walk.empty G),
    -- but it requires a proof that there are no duplicates in its vertex list:
    simp [walk.vertices.empty, list.nodup_singleton],
    end

-- An arc between distinct vertices gives a path
def from_arc
    {V E : Type} (G : digraph V E)
    {v1 v2 : V} : (v1 ≠ v2) → arc G v1 v2 → path G v1 v2 :=
    begin
    intro h, intro a,
    -- `let` binds a local constant in a way that it can be referred to
    -- in other proof terms
    let w := walk.step a (walk.empty G),
    apply subtype.mk w,
    -- `have` just provides a usuable constant whose definition can't be referred to
    have : walk.vertices w = [v1, v2], refl,
    rw this,
    -- `simp` helps make progress on the goal
    simp [list.nodup_singleton],
    -- the only thing missing is a proof that the vertices are distinct,
    -- which is true by assumption
    exact h -- or we could even use the `assumption` tactic
    end

@[reducible] -- [reducible] makes this definition more transparent
def length
    {V E : Type} {G : digraph V E}
    {v1 v2 : V} :
    path G v1 v2 → ℕ :=
        λ p, walk.length p.1

-- This is a big topic: creating a path from a walk
-- Note that my proofs in this section are ugly, so feel free to skip them
-- (the high-level idea is easy enough to grasp; just know that it's
-- machine-verified ;D)
namespace from_walk

-- A helpful invariant: a walk with just a vertex removed preserves the property
-- of having no duplicates.
def preserves_nodup
    {V E : Type} {G : digraph V E}
    {v v1 v2 : V}
    (w : walk G v1 v2)
    (w' : walk G v v2) :=
        list.nodup (list.tail (walk.vertices w)) →
        list.nodup (list.tail (walk.vertices w'))

-- But it turns out that the desired walk being a subwalk is sufficient
def split_at
    {V E : Type} {G : digraph V E}
    {v1 v2 : V} (w : walk G v1 v2) (v : V) :=
    Σ' (w1 : walk G v1 v) (w2 : walk G v v2),
        w = walk.concat w1 w2

-- This includes the other invariant we want to guarantee (that v does not
-- appear except as the first vertex of w2).
def split_at_without
    {V E : Type} {G : digraph V E}
    {v1 v2 : V} (w : walk G v1 v2) (v : V) :=
    Σ' (w1 : walk G v1 v) (w2 : walk G v v2),
        (v ∉ list.tail (walk.vertices w2)) ∧
        w = walk.concat w1 w2

-- Weaken the latter to the former ...
-- Note: `a_of_b` is convention to indicate a function/lemma with a type like `b → a`
def split_at_of_split_at_without
    {V E : Type} {G : digraph V E}
    {v1 v2 : V} {w : walk G v1 v2} {v : V} :
    split_at_without w v → split_at w v :=
    begin
    intro s, constructor, constructor, exact s.2.2.2
    end

-- And recover the invariant from it
lemma split_at.preserves_nodup
    {V E : Type} {G : digraph V E}
    {v1 v2 : V} {w : walk G v1 v2} {v : V}
    (s : split_at w v) : preserves_nodup w s.2.1 :=
    begin
    cases s with w1 s, cases s with w2 p,
    intro nd, simp,
    rw [walk.vertices.concat _ _ _ p] at nd,
    rw [walk.vertices.starts_with _] at nd,
    simp at nd,
    rw list.nodup_append at nd,
    exact nd.2.1,
    end

def discard_vertex.split_at
    {V E : Type} [decidable_eq V] {G : digraph V E}
    (v : V) {v1 v2 : V} (w : walk G v1 v2) :
    psum (split_at_without w v) (v ∉ list.tail (walk.vertices w)) :=
    begin
    induction w with v0 v1 v2 v3 a w ih,
    right,
    simp [walk.vertices.empty _ rfl],
    simp [walk.vertices.step _ _ _ rfl],
    cases ih, left,
    apply psigma.mk (walk.step a ih.1),
    apply psigma.mk ih.2.1,
    apply and.intro ih.2.2.1,
    rw [walk.concat_step_left _ _ _],
    congr,
    exact ih.2.2.2,
    by_cases h : v = v2,
    left, rw h, rw h at ih,
    have : walk.concat (walk.step a (walk.empty G)) w = walk.step a w,
    {
        simp [walk.concat_step_left _ _ _],
    },
    exact psigma.mk (walk.step a (walk.empty G)) (psigma.mk w (and.intro ih this)),
    right,
    have : walk.vertices w = v2 :: list.tail (walk.vertices w),
        cases w, refl, refl,
    rw this, intro vin, cases vin,
    exact h vin, exact ih vin,
    end

-- Remove any occurrence of a vertex from a walk, by either returning a new walk
-- formed as a subset of the previous walk but starting from the vertex to be
-- removed (along with proofs that the vertex was removed, and that the new walk
-- contains no dupicates if the original did), OR a proof that the vertex
-- does not occur in the original walk.
--
-- This is obviously ugly, but encodes enough information to make from_walk work.
def discard_vertex
    {V E : Type} [decidable_eq V] {G : digraph V E}
    (v : V) {v1 v2 : V} (w : walk G v1 v2) :
    psum
        -- either a new walk
        (Σ' (w' : walk G v v2), -- from v to v2
            -- where v does not occur
            (v ∉ list.tail (walk.vertices w')) ∧
            -- and preserving the no duplicates property
            preserves_nodup w w')
        -- or a proof that the vertex does not occur in the original walk
        (v ∉ list.tail (walk.vertices w)) :=
    begin
    induction w with v0 v1 v2 v3 a w ih,
    right,
    simp [walk.vertices.empty _ rfl],
    simp [walk.vertices.step _ _ _ rfl],
    cases ih, left, apply psigma.mk ih.1, apply and.intro ih.2.1,
    intro ndaw, simp [walk.vertices.step _ _ _ rfl] at ndaw, apply ih.2.2,
    apply list.nodup_tail_of_nodup, exact ndaw,
    by_cases h : v = v2,
    left, rw h, rw h at ih,
    have : preserves_nodup (walk.step a w) w,
    {
        intro ndaw,
        simp [walk.vertices.step _ _ _ rfl] at ndaw,
        apply list.nodup_tail_of_nodup, exact ndaw,
    },
    exact psigma.mk w (and.intro ih this),
    right,
    have : walk.vertices w = v2 :: list.tail (walk.vertices w),
        cases w, refl, refl,
    rw this, intro vin, cases vin,
    exact h vin, exact ih vin,
    end

-- This can obviously be used to discard repeats of the first vertex of a walk.
-- But this is actually unused ...
def discard_vertex.beginning
    {V E : Type} [decidable_eq V] {G : digraph V E}
    {v1 v2 : V} (w : walk G v1 v2) :
    Σ' (w' : walk G v1 v2),
        (v1 ∉ list.tail (walk.vertices w')) ∧
        preserves_nodup w w' :=
    begin
    have := discard_vertex v1 w,
    cases this, exact this,
    exact psigma.mk w (and.intro this id),
    end

-- Using induction on the walk, discard all the vertex repeats to generate a
-- path. This has the effect of removing all cycles in the walk.
def discard_vertex.all.explicit
    {V E : Type} [decidable_eq V] {G : digraph V E}
    {v1 v2 : V} (w : walk G v1 v2) : path G v1 v2 :=
    begin
    -- Induction on a walk considers the base case (empty) and the step case
    induction w with v v1 v2 v3 a w ih,
    -- If the walk is empty, we already know how to generate an empty path; done.
    exact path.empty _,
    -- But if v1 = v2, we discard the arc, and just return the induction
    -- hypothesis (that is, the path generated from the tail), once we have
    -- rewritten v1 as v2.
    by_cases v1_v2 : (v1 = v2), rw v1_v2, exact ih,
    -- Just splits up the induction hypothesis into the walk and the proof.
    cases ih with ih_w ih_nodup,
    -- Now we discard the starting vertex from the induction hypothesis' walk
    have ih_w' := discard_vertex v1 ih_w,
    -- Consider the cases: a new walk, or the same walk
    cases ih_w', cases ih_w' with w' p,
    -- If we obtained a new walk, it is the walk we want to return
    apply subtype.mk w',
    -- Construct a proof that the walk has no duplicates
    rw [walk.vertices.starts_with, list.nodup_cons], constructor,
    -- from the fact that v does not occur in the rest of the vertices
    exact p.1,
    -- and the fact that the ih had no duplicates, so the tail of this has none
    exact (p.2 (list.nodup_tail_of_nodup ih_nodup)),
    -- Otherwise, we should return the walk consisting of this arc and the ih walk
    apply subtype.mk (walk.step a ih_w),
    -- Do some rewrites of the goal ...
    rw [walk.vertices.step _ _ _ rfl, list.nodup_cons], constructor,
    rw [walk.vertices.starts_with, list.mem_cons_iff],
    -- We know that v1 is not the second vertex v2, nor is it in ih_w
    apply not_or v1_v2 ih_w',
    -- And the rest of the ih already had no duplicates, by induction
    exact ih_nodup,
    end

-- This contains the above algorithm but also produces the proof that either
-- the result is the same, or the walk/graph contained a cycle.
--
-- This can be used to prove the equivalence of walks and paths in acyclic
-- digraphs.
def discard_vertex.all.acyc_prf
    {V E : Type} [decidable_eq V] {G : digraph V E}
    {v1 v2 : V} (w : walk G v1 v2) :
        Σ' (p : path G v1 v2),
            p.1 = w ∨ ∃(v : V) (c : walk G v v), c ≠ walk.empty G :=
    begin
    induction w with v v1 v2 v3 a w ih,
    exact psigma.mk (path.empty _) (or.inl rfl),
    by_cases v1_v2 : (v1 = v2),
    apply psigma.mk, right, tactic.swap,
    rw v1_v2, exact ih.1,
    apply exists.intro v2,
    rw v1_v2 at a,
    apply exists.intro (walk.step a (walk.empty _)),
    exact λ h, walk.no_confusion h,
    cases ih with ih prf, cases ih with ih_w ih_nodup,
    have ih_w' := discard_vertex.split_at v1 ih_w,
    cases ih_w',
    have := split_at.preserves_nodup (split_at_of_split_at_without ih_w'),
    cases ih_w' with w1 ih_w', cases ih_w' with w2 p,
    apply psigma.mk (subtype.mk w2
        begin
        rw [walk.vertices.starts_with, list.nodup_cons], constructor,
        exact p.1,
        exact (this (list.nodup_tail_of_nodup ih_nodup)),
        end : path G v1 v3),
    right, apply exists.intro v1,
    apply exists.intro (walk.step a w1),
    exact λ h, walk.no_confusion h,
    apply psigma.mk (subtype.mk (walk.step a ih_w)
        begin
        rw [walk.vertices.step _ _ _ rfl],
        rw [list.nodup_cons], constructor,
        rw [walk.vertices.starts_with],
        rw list.mem_cons_iff,
        apply not_or v1_v2 ih_w',
        exact ih_nodup,
        end : path G v1 v3),
    cases prf,
    left,
    simp at prf,
    simp [prf],
    right,
    exact prf,
    end

-- This defeq will be important
@[reducible]
def discard_vertex.all
    {V E : Type} [decidable_eq V] {G : digraph V E}
    {v1 v2 : V} (w : walk G v1 v2) : path G v1 v2 :=
    (discard_vertex.all.acyc_prf w).1

end from_walk

-- This just references the version inside the from_walk namespace
@[reducible]
def from_walk
    {V E : Type} [decidable_eq V] {G : digraph V E}
    {v1 v2 : V} :
    walk G v1 v2 → path G v1 v2 := from_walk.discard_vertex.all

-- This concatenates the underlying paths then removes cycles to generate
-- the new path.
def concat
    {V E : Type} [decidable_eq V] {G : digraph V E}
    {v1 v2 v3 : V}
    (p1 : path G v1 v2)
    (p2 : path G v2 v3) :
    path G v1 v3 := from_walk (walk.concat p1.1 p2.1)

-- A maximal path is a path going to a final vertex.
def maximal
    {V E : Type} (G : digraph V E)
    (v1 v2 : V) := pprod (path G v1 v2) (is_final G v2)
                    -- (pprod stores a piece of data and a separate proof)

-- Proposition that one exists.
def has_maximal
    {V E : Type} (G : digraph V E)
    (v1 v2 : V) := (has_path G v1 v2) ∧ (is_final G v2) -- regular conjunction

-- Eliminate it following the usual pattern
def has_maximal.elim
    {V E : Type} {G : digraph V E}
    {v1 v2 : V} {r : Prop} :
    has_maximal G v1 v2 → (maximal G v1 v2 → r) → r :=
        λ h f, has_path.elim h.1 (λ p, f (pprod.mk p h.2))

-- Hopefully this makes sense now by just looking at the types!
def maximal.concat
    {V E : Type} [decidable_eq V] {G : digraph V E}
    {v1 v2 v3 : V}
    (p1 : path G v1 v2)
    (p2 : path.maximal G v2 v3) :
    path.maximal G v1 v3 :=
    begin
    constructor,
    exact path.concat p1 p2.1,
    exact p2.2,
    end

def has_maximal.concat
    {V E : Type} [decidable_eq V] {G : digraph V E}
    {v1 v2 v3 : V}
    (p1 : path G v1 v2)
    (p2 : path.has_maximal G v2 v3) :
    path.has_maximal G v1 v3 :=
    flip and.intro p2.2
    begin
    apply exists.elim p2.1, intro w, intro nodup,
    exact subtype.exists_of_subtype (path.concat p1 (subtype.mk w nodup)),
    end

-- If the walk underlying a path is nonempty, produce the path corresponding
-- to its tail.
def vertices.step_back
    {V E : Type} [decidable_eq V] {G : digraph V E}
    {v1 v2 v3 : V}
    (a : arc G v1 v2)
    (w : walk G v2 v3)
    (p : path G v1 v3) :
    (p.1 = walk.step a w) → path G v2 v3 :=
    begin
    intro h, cases p, simp at h,
    apply subtype.mk w,
    rw [walk.vertices.step _ _ _ h] at p_property,
    exact list.nodup_of_nodup_cons p_property,
    end

end path

-- One encoding (fairly direct and easy to use) of the property of an acyclic
-- graph: all walks from a vertex to itself are empty.
def is_acyclic
    {V E : Type} (G : digraph V E) :=
        ∀ (v : V) (w : walk G v v), w = walk.empty G

-- Subtype generated from that (unused).
def acyclic
    {V E : Type} :=
        { G : digraph V E // is_acyclic G }

-- It turns out that in acyclic graphs, from_walk just elaborates the same walk
-- with a proof term.
lemma is_acyclic.from_walk
    {V E : Type} [decidable_eq V] {G : digraph V E}
    {v1 v2 : V}
    (acyc : is_acyclic G)
    (w : walk G v1 v2) :
    (path.from_walk w).val = w :=
    begin
    let fw := path.from_walk.discard_vertex.all.acyc_prf w,
    have : path.from_walk w = fw.1, refl, rw this,
    cases h : fw with p prf,
    simp,
    cases prf,
    exact prf,
    exfalso,
    apply exists.elim prf, intro v, intro prf',
    apply exists.elim prf', intro c, intro prf'',
    exact prf'' (acyc v c)
    end

-- Thus paths and walks are equivalent in acyclic digraphs.
def path.equiv_walk
    {V E : Type} [decidable_eq V] {G : digraph V E}
    {v1 v2 : V} :
    is_acyclic G →
    walk G v1 v2 ≃ path G v1 v2 := λ acyc,
    -- this is an equivalence a ≃ b: a pair of functions a → b and b → a,
    -- with proofs that they are inverses of each other
    equiv.mk path.from_walk subtype.val
        (is_acyclic.from_walk acyc)
        (λ p, subtype.eq (is_acyclic.from_walk acyc p.val))

-- Since the cycle elimination algorithm does nothing in an acyclic graph,
-- lengths are preserved through concatenation
lemma path.acyclic_concat_length
    {V E : Type} [decidable_eq V] {G : digraph V E}
    {v1 v2 v3 : V}
    (p1 : path G v1 v2)
    (p2 : path G v2 v3) :
    is_acyclic G →
    path.length (path.concat p1 p2) = path.length p1 + path.length p2 :=
    begin
    intro acyc,
    show walk.length (path.concat p1 p2).1 = walk.length p1.1 + walk.length p2.1,
    show walk.length (path.from_walk (walk.concat p1.1 p2.1)).1
       = walk.length p1.1 + walk.length p2.1,
    rw [is_acyclic.from_walk acyc _],
    exact walk.concat_length _ _,
    end

-- Okay, done with types! On to the main course:


-- The so-called “no-watershed condition”: for any two vertices with arcs
-- from(!) a common vertex, there is another vertex that has paths from
-- both of those. (Obviously true if {u,v,w} are not distinct.)
-- See section 0.2 in http://www-users.math.umn.edu/~dgrinber/comb2/mt3.pdf
def no_watershed_condition
    {V E : Type} (G : digraph V E) : Prop :=
    Π (u v w : V),
        arc G u v → arc G u w →
        ∃ (t : V), has_path G v t ∧ has_path G w t

-- Having the no-watershed condition in an acyclic graph produces the result
-- that each vertex has a unique sink; that is, a vertex with a maximal path
-- from the other vertex.
namespace unique_sink

-- Inside a namespace/section, we can use the following commands to declare variables
-- used in the definitions/lemmata for this section:
-- implicit and explicit arguments
variables {V E : Type} (G : digraph V E)
variables acyc : is_acyclic G
-- and typeclass arguments! these are variables of a special type that have a
-- canonical value
-- In particular:
-- decidable_eq V gives a function Π(v1 v2 : V), (v1 = v2) ∨ (v1 ≠ v2)
-- that decides whether two vertices are equal, giving a proof either way
-- fintype V asserts that V has finitely many inhabitants, by giving a list
-- of them all (actually a finite set `finset`), and a proof that every
-- element occurs in it: ∀ v : V, v ∈ univ V
variables [decidable_eq V] [decidable_eq E] [fintype V] [fintype E]

-- Now that we have G as a fixed local variable, we can use it in notation!
-- who doesn't love syntactic sugar?!?!? :D
local infix `⟶`:50 := arc G
local infix `~⟶`:50 := walk G -- unused
local infix `*⟶`:50 := path G
local infix `×⟶`:50 := path.maximal G
-- and their propositional equivalents
local infix `⟼`:50 := has_arc G
local infix `*⟼`:50 := has_path G
local infix `×⟼`:50 := path.has_maximal G

-- In finite acyclic graphs, each vertex will have a longest path;
-- if `bounded_by p n` is provided, then the longest path from p is at most n steps.
def bounded_by (p : V) (n : ℕ) := ∀ (q : V) (w : p *⟶ q), path.length w ≤ n

-- This is the proposition used for induction. It limits the results to
-- only pertain to vertices p whose paths away from them have length at most n.
def P (n : ℕ) :=
    ∀ (p : V),
        bounded_by G p n →
        ∃! (q : V), p ×⟼ q

-- Helper: These are logically equivalent via two existing lemmate...
lemma eq_zero_iff_le_zero {n : nat} : n ≤ 0 ↔ n = 0 :=
    iff.intro nat.eq_zero_of_le_zero nat.le_of_eq

-- A walk of length 0 obviously connects the same two vertices.
lemma length0 {v1 v2 : V} (w : v1 ~⟶ v2) :
    walk.length w = 0 → v1 = v2 :=
    begin
    intro h,
    -- obviously the `empty` case is trivial:
    cases w, refl,
    -- but the `step` case is absurd!
    rw [walk.length_step] at h,
    exact absurd h (nat.succ_ne_zero (walk.length w_a_1)),
    end

-- Two maximal paths from the same vertex cannot have one be empty and the other
-- be nonempty.
lemma not_diff_emptiness
    {p q1 q2 : V}
    (w1 : p ×⟶ q1)
    (w2 : p ×⟶ q2) :
    ¬(path.length w1.1 = 0 ∧ path.length w2.1 > 0) :=
    begin
    intro h,
    have pq1 := length0 G w1.1.1 h.1,
    have q1_final := w1.2,
    rw [← pq1] at q1_final,
    apply q1_final,
    let w := w2.1.1,
    cases hw : w,
    apply flip absurd (ne_of_gt h.2),
    show walk.length w = 0,
    rw hw, exact walk.length_empty,
    apply exists.intro a.1,
    have x : (arcT.mk p v2).1 = p, refl,
    rw [← a.2] at x,
    exact x,
    end

-- ... basically the same as above, but more explicit.
lemma same_emptiness
    {p q1 q2 : V}
    (w1 : p ×⟶ q1)
    (w2 : p ×⟶ q2) :
    (path.length w1.1 = 0 ∧ path.length w2.1 = 0) ∨
    (path.length w1.1 > 0 ∧ path.length w2.1 > 0) :=
    begin
    cases h1 : path.length w1.1,
    left, constructor, refl,
    cases h2 : path.length w2.1, refl,
    apply flip absurd (not_diff_emptiness G w1 w2),
    constructor, exact h1,
    have := nat.zero_lt_succ n,
    rw [← h2] at this,
    exact this,
    right, constructor, exact nat.zero_lt_succ n,
    cases h2 : path.length w2.1,
    apply flip absurd (not_diff_emptiness G w2 w1),
    constructor, exact h2,
    have := nat.zero_lt_succ n,
    rw [← h1] at this,
    exact this,
    exact nat.zero_lt_succ n_1,
    end

-- A proof that each path has finite length, bounded above by the number of vertices
lemma finite {p q : V} (w : p *⟶ q) : path.length w + 1 ≤ fintype.card V :=
    begin
    cases w with w nodup,
    -- this should really be a separate lemma, but it's easy enough to prove inline...
    have : walk.length w + 1 = list.length (walk.vertices w),
    {
        induction w,
        refl, simp [walk.vertices.step _ _ _ rfl],
        rw add_comm, apply w_ih,
        rw [walk.vertices.step _ _ _ rfl] at nodup,
        exact list.nodup_of_nodup_cons nodup,
    },
    rw this,
    -- now we don't need the fact that it is a list of vertices anymore
    -- so replace it with a generic `l : list V` in the hypothesis and goal:
    generalize_hyp h : walk.vertices w = l at nodup, rw h,
    -- make a finite set from the list
    let fs : finset V := finset.mk (quotient.mk l) nodup,
    -- with the same size
    have : list.length l = finset.card fs :=
    by symmetry; apply quot.lift_beta list.length multiset.card._proof_1,
    rw this,
    -- it must be smaller or the same size, since it is a subset
    exact finset.card_le_of_subset (finset.subset_univ _),
    end

-- A vertex is either final or it has an arc leading from it to some other vertex.
-- Relies on [fintype E]
def any_arc_from (p : V) :
    (∃ (v : V), p ⟼ v) ∨ is_final G p :=
    begin
    let elems : finset E := finset.univ,
    -- Prove that these are equivalent
    -- instead of proving each direction separately, we use bijections at each step
    have : (p ∈ multiset.map (source G) elems.val) ↔ (∃(e : E), source G e = p),
        symmetry,
        rw multiset.mem_map,
        apply exists_congr,
        intro e,
        symmetry,
        apply and_iff_right,
        exact finset.mem_univ e,
    -- this is a decidable proposition, so we can determine whether it is true or false
    by_cases h : p ∈ multiset.map (source G) elems.val,
    {
        rw this at h,
        left,
        apply exists.elim h, intro e, intro he,
        apply exists.intro (target G e),
        apply exists.intro e,
        apply prod.eq_iff_fst_eq_snd_eq.2, constructor,
        show (G.φ e).1 = p, exact he,
        show (G.φ e).2 = target G e, refl,
    },
    {
        rw this at h,
        right, exact h,
    },
    end

-- tactic mode doesn't know to include this variable
-- we will use it in the remaining proofs
include acyc

-- If all paths leading out of a vertex have length 0, it must be a sink
def is_final_of_bounded_by_zero (v : V) :
    bounded_by G v 0 → is_final G v :=
    begin
    intros len,
    have := any_arc_from G v,
    cases this,
    {
        exfalso,
        apply exists.elim this, intros v1 ha,
        apply has_arc.elim ha, intro a,
        let p : v *⟶ v1 := path.from_walk (walk.step a (walk.empty _)),
        have len0 := len _ p,
        rw [eq_zero_iff_le_zero] at len0,
        suffices : path.length p = 1, cc,
        have : p.1 = walk.step a (walk.empty _),
            from is_acyclic.from_walk acyc _,
        unfold path.length, rw this, refl
    },
    exact this,
    end

-- Helper for induction: giving a path from v1 to v2 with length no less
-- than m and the fact that all paths from v1 are at most length n+m, means
-- that a path from v2 to v3 must have length at most n.
lemma reduce_length
    {v1 v2 v3 : V}
    {n m : ℕ}
    (w : v1 *⟶ v2)
    (p : v2 *⟶ v3)
    (lw : path.length w ≥ m)
    (mh : bounded_by G v1 (n+m)) :
    path.length p ≤ n :=
    begin
    let wp : v1 *⟶ v3 := path.concat w p,
    have lwp : path.length wp = path.length w + path.length p,
        from path.acyclic_concat_length w p acyc,
    -- rewrite lw at lwp,
    apply @nat.le_of_add_le_add_left (path.length w) _ _,
    rw [← lwp, add_comm],
    transitivity,
    apply mh v3,
    exact nat.add_le_add_left lw _,
    end

-- All vertices have a sink.
-- This is a smaller proof following the style of the larger proof.
-- We prove it by induction for all vertices that are bounded by n,
-- then we pick a sufficiently large n to cover all vertices.
lemma find_sink.bounded (n : ℕ) (v1 : V) :
    bounded_by G v1 n →
    ∃ (s : V), v1 ×⟼ s :=
    begin
    intros len,
    induction n with n ih generalizing v1,
    {
        apply exists.intro v1,
        apply and.intro (subtype.exists_of_subtype (path.empty G)),
        apply is_final_of_bounded_by_zero, assumption, assumption,
    },
    have := any_arc_from G v1,
    cases this,
    {
        apply exists.elim this, intros v2 ha,
        apply has_arc.elim ha, intro a,
        let p : v1 *⟶ v2 := path.from_walk (walk.step a (walk.empty _)),
        have := ih v2
            begin
            have : path.length p = 1,
                have : p.1 = walk.step a (walk.empty _),
                    from is_acyclic.from_walk acyc _,
                unfold path.length, rw this, refl,
            intros v' p',
            apply reduce_length G acyc p,
            exact ge_of_eq this,
            exact len,
            end,
        apply exists.elim this, intros s hm,
        apply exists.intro s,
        exact path.has_maximal.concat p hm
    },
    {
        apply exists.intro v1,
        apply and.intro (subtype.exists_of_subtype (path.empty G)),
        assumption,
    },
    end

-- Using `finite`, we pick a sufficient n to bound all vertices
lemma find_sink
    (v1 : V) :
    ∃ (s : V), v1 ×⟼ s :=
        find_sink.bounded G acyc _ v1
            begin
            unfold bounded_by, intros,
            rw ← nat.pred_succ (path.length w),
            apply nat.pred_le_pred,
            apply unique_sink.finite G
            end

-- Final vertices are their own sink
lemma P_final (p : V) : is_final G p → ∃!(q : V), p ×⟼ q :=
    begin
    intro final, apply exists_unique.intro p,
    constructor, exact subtype.exists_of_subtype (path.empty G), exact final,
    intro sink, intro has_max, apply subtype_elim_exists has_max.1,
    intro p, cases p, cases p_val, refl, exfalso,
    apply final,
    apply exists.intro p_val_a.1,
    show (G.φ p_val_a.1).1 = p,
    rw p_val_a.2, refl
    end

-- The base case, basically applies only to sinks, which are their own
-- sink, obviously.
lemma P0 : P G 0 :=
    λ p len, P_final _ acyc p (is_final_of_bounded_by_zero _ acyc p len)

-- The whole proof together.
--
-- Big picture idea:
-- For any vertex p with bounded_by G p n, try to find an arc leading out of it, call
-- its target v (≠ p). The unique sink can be obtained by applying induction to v.
-- But to establish that it is also unique for p, we take any otherSink
-- with a maximal path from p, take the first new vertex visited by that path v2
-- and we can apply the watershed condition to an arc p v and an arc p v2 to get t with
-- a path v t and a path v2 t. But by using this, the sinks from v, t, and v2 must
-- all be the same since we can extend the maximal path from t to be from v or v2.
-- This is essentially the statement that connected vertices share the same sink...
-- (Obviously the computer requires more details to formalize this and accept
-- it as rigorous, but they are explained below.)
theorem Pn : no_watershed_condition G → ∀ (n : ℕ), P G n :=
    begin
    -- introduce the watershed condition as a variable in scope
    intro watershed,
    -- this is the variable for induction, named n' since n will be in scope
    intro n,
    -- regular induction on natural numbers (just a special case of induction in DTT)
    induction n with n ih,
    -- base case, already proved as P0 above
    exact P0 G acyc,
    -- this is the vertex of interest
    intro p,
    -- and the proof that maximal paths from p have length at most n+1
    intro len,
    -- try to obtain an arc from p
    have aa := any_arc_from G p,
    -- this splits it up into the two cases, replacing aa with the result of each case
    -- (what follows is mostly the proof of the first case, the second takes one line)
    cases aa,
    apply exists.elim aa,
    -- obtain the vertex it goes to, and the proof that there is an arc
    intro v, assume ha : p ⟼ v,
    -- obtain some actual arc from p to v
    apply has_arc.elim ha, assume a : p ⟶ v,
    -- a funny proof by contradiction that p ≠ v since it is in an acyclic graph
    -- TODO: factor this out
    by_cases (p = v),
    {
        let a' : p ⟶ v := a,
        rw h at a',
        have := acyc _ (walk.step a' (walk.empty G)),
        exfalso,
        exact walk.no_confusion this,
    },
    -- using that we can make a path from the arc ...
    let start : p *⟶ v := path.from_arc G h a,
    -- ... of length 1 (duh!)
    have len1 : path.length start = 1, refl,
    -- Now we can apply the induction hypothesis onto v, since `start`
    -- guarantees that the length will go down by 1.
    have exu := ih v
        begin
        intro v', intro p',
        apply reduce_length G acyc start p' (ge_of_eq len1) len,
        end,
    -- Now we unpack the existentials ...
    apply exists_unique.elim exu, simp,
    -- ... to obtain the sink, the existence of a maximal path from v to that
    -- sink, and the proof that that sink is unique
    intro sink, intro has_maxPathToSink, intro uniq,
    -- so we know that this is the sink we want, just need to prove it has a
    -- maximal path ...
    apply exists_unique.intro sink,
    apply subtype_elim_exists has_maxPathToSink.1,
    assume pathToSink : v *⟶ sink,
    constructor,
    apply subtype.exists_of_subtype,
    apply path.concat start pathToSink,
    exact has_maxPathToSink.2,
    -- ... and that it is unique. Oh boy.
    -- Given otherSink and a max path from p to otherSink, prove that they are
    -- the same sink.
    intro otherSink, intro has_maxPathToOtherSink,
    show otherSink = sink,
    apply path.has_maximal.elim has_maxPathToOtherSink,
    assume maxPathToOtherSink : p ×⟶ otherSink,
    -- Argue that the maximal path is nonempty.
    cases hp : maxPathToOtherSink.1.1,
    {
        exfalso, apply maxPathToOtherSink.2, apply exists.intro a.1,
        show (G.φ a.1).1 = p,
        exact (prod.eq_iff_fst_eq_snd_eq.1 (a.2)).1,
    },
    -- Now we have hp : (maxPathToOtherSink.fst).val = walk.step a_1 a_2
    -- so a_1 is an arc from p to some v2
    -- Apply the watershed condition with a : walk p v, a_1 : walk p v2
    have water1 := watershed p v v2 a a_1,
    -- so there is some t with paths from v to t and from v2 to t
    apply exists.elim water1, intro t, simp,
    intro has_vt, intro has_v2t,
    apply subtype_elim_exists has_vt, intro vt,
    apply subtype_elim_exists has_v2t, intro v2t,
    -- now we have another path like starting, but from p to t, via v.
    let startt : p *⟶ t := path.concat start vt,
    -- Induction again!
    have exu2 := ih t
        begin
        intro v', intro p',
        -- startt has length at least 1, since start has length 1, and
        -- vt may have length greater than 1, and since it is acyclic.
        have len_ge1 : path.length startt ≥ 1,
            have : path.length startt = path.length start + path.length vt,
                from path.acyclic_concat_length start vt acyc,
            rw len1 at this,
            transitivity,
            exact le_of_eq (eq.symm this),
            rw [add_comm],
            exact nat.succ_le_succ (nat.zero_le (path.length vt)),
        apply reduce_length G acyc startt p' len_ge1 len,
        end,
    apply exists_unique.elim exu2, simp,
    -- Oh here is anotherSink! the unique sink from t
    intro anotherSink, intro has_maxPathToAnotherSink, intro uniq2,
    -- but anotherSink = sink, since any maxpath can be extended along vt
    have := uniq _ (path.has_maximal.concat vt has_maxPathToAnotherSink),
    -- again argue that an arc connects distinct vertices
    by_cases (p = v2),
    {
        let a' : p ⟶ v2 := a_1,
        rw h at a',
        have := acyc _ (walk.step a' (walk.empty G)),
        exfalso, exact walk.no_confusion this,
    },
    -- So there's a path from p to v2 just using the arc a_1.
    let startv2 : p *⟶ v2 := path.from_arc G h a_1,
    -- Induction yet again! last time I promise
    have exuv2 := ih v2
        begin
        intro v', intro p',
        apply reduce_length G acyc startv2 p',
        exact ge_of_eq (rfl : path.length startv2 = 1),
        exact len,
        end,
    apply exists_unique.elim exuv2, simp,
    -- finalSink is the unique sink from v2
    intro finalSink, intro has_maxPathToFinalSink, intro uniqv2,
    -- but finalSink = otherSink, due to the maxpath a_2 from v2 to otherSink
    have := uniqv2 otherSink
        begin
        -- construct the maxpath
        constructor,
        -- we can demonstrate the exact path, but we just need its existence,
        apply subtype.exists_of_subtype,
        -- hp : (maxPathToOtherSink.fst).val = walk.step a_1 a_2
        -- means that just the walk a_2 creates a path too
        exact path.vertices.step_back _ _ maxPathToOtherSink.1 hp,
        -- and is maximal since otherSink is still final
        exact maxPathToOtherSink.2,
        end,
    -- and finalSink = anotherSink, by extending maxpaths along v2t
    have := uniqv2 anotherSink
                (path.has_maximal.concat v2t has_maxPathToAnotherSink),
    -- so the congruence closure calculates that otherSink = sink via
    -- the equalities in scope
    cc,
    -- Oh yeah, and if aa had no arcs, then its a final vertex and we're done.
    exact P_final G acyc p aa,
    end

end unique_sink

-- It turns out that we can pick a sufficient n such that Pn holds for all p
theorem unique_sink
    {V E : Type} {G : digraph V E}
    [decidable_eq V] [decidable_eq E] [fintype V] [fintype E] :
    is_acyclic G → no_watershed_condition G →
    ∀ (p : V), ∃! (q : V), path.has_maximal G p q :=
        λ acyc watershed p, unique_sink.Pn G acyc watershed _ p
            begin
            unfold unique_sink.bounded_by, intros,
            rw ← nat.pred_succ (path.length w),
            apply nat.pred_le_pred,
            apply unique_sink.finite G
            end


end digraph