Function graph is acyclic

Stream: graph theory

[Daniel Weber]

I'm trying to prove the following theorem, but I'm not sure how to formalize the proof in Lean.

lemma IsAcyclic_of_fromRel (f : V → V) (hf : ∀ x n, f^[n] x = x → f x = x) :
    IsAcyclic (SimpleGraph.fromRel (· = f ·)) := by
  generalize h : SimpleGraph.fromRel (· = f ·) = G
  intro a p hp

  sorry

semi-formally, a proof is:
we call the edges in the walk (a, b) up if b = f a, and down if a = f b. Note that a down edge can't be followed by an up edge, as that would violate edges_nodup. This means the walk can be split to some number of up edges followed by some number of down edges. If both numbers are positive then the first and last edges are equal, and otherwise hf implies that the walk must be empty, both of which give a contradiction.

How could I formalize this proof, in particular the part of splitting the cycle to an up walk and a down walk?

[Daniel Weber]

Perhaps I could use docs#List.takeWhile and docs#List.dropWhile on p.darts?

[Shreyas Srinivas]

If you have a cycle starting at x then you have a walk of some length n back to X, and therefore there exists an n f^[n](x) = x. And by hypothesis hf, you have a self loop.

That being said, I don't understand what you mean by "an up edge cannot be followed by a down edge"

[Shreyas Srinivas]

an edge could be both up and down if you have f(a) = b and f(b) = a.

[Kyle Miller]

The lemma seems to be mis-stated. Perhaps you want to add 0 < n as a hypothesis in hf? Right now, hf is equivalent to forall x, f x = x since substituting in n = 0, f^[0] x = x reduces to x = x.

[Daniel Weber]

Yes, I fixed it and managed to prove it on #16009, but it's very long and there are lemmas I need to move to other files