Konigsberg Bridges Problem

Stream: new members

[Pierre Guillot]

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 :

koenigsberg.lean

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!

Pierre

[Yaël Dillies]

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

[Kyle Miller]

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

[Pierre Guillot]

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]

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

[Kyle Miller]

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

[Kyle Miller]

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]

(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]

Here are some simplifications for the first material about upair

code

def upair (n m : ℕ) : finset ℕ := {n, m}

lemma mem_upair {x n m : ℕ}:
    x ∈ upair n m ↔ x = n ∨ x=m
:= by simp [upair]

lemma card_single (n : ℕ) : (upair n n).card = 1
:= by simp [upair]

lemma upair_symm {n m : ℕ} : upair n m = upair m n :=
begin
  ext x,
  simp [upair, or_comm],
end

lemma upair_subset {n m : ℕ} (xs : finset ℕ) :
  upair n m ⊆ xs ↔ n ∈ xs ∧ m ∈ xs :=
by simp [upair, finset.insert_subset]

lemma upair_subset_upair {a1 a2 b1 b2 : ℕ} :
  upair a1 a2 ⊆ upair b1 b2 ↔ (a1 = b1 ∨ a1 = b2) ∧ (a2 = b1 ∨ a2 = b2) :=
by simp [upair_subset, mem_upair]

lemma eq_upairs {a1 a2 b1 b2 : ℕ} :
    (upair a1 a2) = (upair b1 b2) ↔ (a1=b1 ∧ a2=b2 ) ∨ (a1=b2 ∧ a2=b1)
:=
begin
  rw le_antisymm_iff,
  simp only [upair_subset_upair, finset.le_eq_subset],
  tauto,
end

[Pierre Guillot]

This is great! Thanks!

[Filippo A. E. Nuccio]

Great job, @Pierre Guillot , congratulations!