Zulip Chat Archive

Stream: new members

Topic: Konigsberg Bridges Problem

Pierre Guillot (Jul 31 2022 at 21:26):

Hi everyone!

I'm still learning Lean, and I would like your opinion on a proof that I've produced this week. I've read here that the Koenigsberg Brigdges problem, solved by Euler, was one of the 100 problems proposed by Wiedijk which has not been formalized in Lean. So i've done that as an exercise. The formal statement is :

theorem eulerian_even_degree {Γ : graph} (p : path Γ) (euler : eulerian p)
    (v : ) (notfirst : v  p.vertex 0) (notlast : v  p.vertex p.len) :
    even (degree Γ v)

In other words, if there's a eulerian path on a graph (a path visiting each edge just once), then the degree of each vertex is even, with two exceptions at most. (In fact, one can prove that there are 0 or 2 exceptions.) The graph in the original problem was not like that, so it does not have a eulerian path.

I have attached the file, it's about 700 lines with lots of comments :


I'm very interested in your comments about the mistakes I make, the things that I ought to know, and so on. (I'm less interested in suggestions for improvements of the code when they're too specific to the question at hand, I don't care about Koenigsberg's bridges all that much...)

One thing I can point out: there's an inconsistency in the online documentation. If you read here you see the following signature:

 theorem finset.card_disj_union {α : Type u_1} (s t : finset α) (h :  (a : α), a  s  a  t) :
(s.disj_union t h).card = s.card + t.card

But with the version of Lean which I'm using -- that is, on gitpod -- it is rather :

finset.card_disjoint_union :
   {α : Type u_1} {s t : finset α} [_inst_1 : decidable_eq α], disjoint s t  (s  t).card = s.card + t.card

(I've wasted a lot of time with that...)

Thanks in advance!


Yaël Dillies (Jul 31 2022 at 21:27):

cc @Kyle Miller, who opened a PR for this recently!

Kyle Miller (Jul 31 2022 at 21:29):

Regarding card_disj_union, beware that there is both docs#finset.card_disj_union and docs#finset.card_disjoint_union

Pierre Guillot (Jul 31 2022 at 21:33):

Oh my, I didn't even realize that I've gone from "disj" to "disjoint"... pff... sorry... and thanks for the explanation!

I keep reading "PR", does that mean "peer review" or something?

and how do I cc someone? (I really am a beginner...)

Kyle Miller (Jul 31 2022 at 21:34):

#15279 is the PR ("pull request" -- git terminology)

Kyle Miller (Jul 31 2022 at 21:34):

That specifically has that the Konigsberg graph does not have an Eulerian walk

Kyle Miller (Jul 31 2022 at 21:35):

Here's the analogue of the theorem you proved: docs#simple_graph.walk.is_eulerian.card_odd_degree. Edit: I mean this one: docs#simple_graph.walk.is_eulerian.even_degree_iff

Kyle Miller (Jul 31 2022 at 21:36):

(Zulip hint: you can click the '...' on a message and do "View source" to see how someone typed something. You can cc someone with @, like @Pierre Guillot. There's also the "?" below the message editing box with a guide.)

Kyle Miller (Jul 31 2022 at 22:27):

Here are some simplifications for the first material about upair


Pierre Guillot (Aug 01 2022 at 07:16):

This is great! Thanks!

Filippo A. E. Nuccio (Aug 01 2022 at 07:45):

Great job, @Pierre Guillot , congratulations!

Last updated: Dec 20 2023 at 11:08 UTC