freek 83

Stream: graph theory

[Jalex Stark]

I started down the "PR graph theory to lean" path when Aaron came to me with a mostly-error-free proof of the "friendship theorem" which characterizes graphs with the property "every pair of distinct vertices has a unique common neighbor". We used some algebraic stuff in our proof, which has since been sliced up and PRed, except for the coupld of most specialized lemmas.

[Jalex Stark]

The branch is here
https://github.com/leanprover-community/mathlib/tree/freek_83_friendship_theorem
(the code is in the archive / 100-theorems folder)

[Jalex Stark]

It needs quite a bit more polishing. It may also be a good testbed for changes to the API.

[Jalex Stark]

There's a nontrivial counting argument there, with some machinery that maybe one could profitably re-use elsewhere.

[Jalex Stark]

#3458 was born from this project, and now it's approved. I think @Aaron Anderson plans to slice off the rest of branch#freek_83_friendship_theorem into PRs; possibly the PRs don't need to depend on each other very much.

[Aaron Anderson]

One of those PRs has already been PR'd, the one on adjacency matrices #3672

[Jalex Stark]

sorry I don't see a PR on #3672. did you mean to say "approved"?

[Kyle Miller]

To save you a little work: mul_val is now known as mul_apply in the newest mathlib

[Aaron Anderson]

Jalex Stark said:

sorry I don't see a PR on #3672. did you mean to say "approved"?

I just mean that I've created the PR.

[Jalex Stark]

got it. a PR is just a branch of mathlib + a request to merge that branch into master. Someone who doesn't have push access to branches of mathlib could hypothetically open a pull request to merge stuff into an open PR, the same way that you can push stuff to the PR branch.

[Jalex Stark]

and this PRing a PR is not just hypothetical, sometime this summer a new contributor opened a PR on a PR, thinking it was a PR to master, then we ended up in a state where both PRs were reviewed and marked as approved, but neither of them got merged into master

[Kyle Miller]

I was surprised GitHub does PRs based on a branch rather than a commit. It makes some sense, because it makes it easier to incorporate code review changes, but, still, it causes problems like what you describe.

[Aaron Anderson]

IIRC the remaining work breaks into (adjacency matrix PR) and (friendship proof + like 2 linear algebra lemmas PR)

[Aaron Anderson]

maybe that second one is too big, but I don't remember any sensible ways to break it up

[Aaron Anderson]

Check out branch#friendship_final

[Aaron Anderson]

I've placed the prerequisites around the library. Feel free to give me comments here, or edit or golf.

[Aaron Anderson]

I'm going to PR all the prereqs not in the one archive file separately first

[Aaron Anderson]

#3953

[Jalex Stark]

Aaron Anderson said:

Check out branch#friendship_final

are we ready to delete the freek_83_friendship_theorem branch?

[Aaron Anderson]

I think there’s extra stuff on there, like a slightly different approach to adjacency matrix generalization.

[Aaron Anderson]

I should double-check that everything I want is backed up and get back to you tonight.

[Jalex Stark]

No rush. Now that I think of it, I have an old mathlib branch (I had worked just a bit on freek 73 before Bhavik PRed it) to garbage-collect.

[Aaron Anderson]

You can delete it now.

[Aaron Anderson]

branch#friendship_final builds, although it'll stay unlinted until I merge the prereqs branch back in

[Kyle Miller]

Aaron Anderson said:

Feel free to give me comments here, or edit or golf.

I've pushed a few commits for the friendship lemma. It changes some definitions, splits off a lemma or two, and adds some documentation. (If any of the changes aren't welcome, feel free to revert.)

[Aaron Anderson]

That all looks good to me, but I should probably review it again tomorrow.

[Aaron Anderson]

Thanks for your help!

[Aaron Anderson]

The prereqs PR hasn't been merged yet, but it's far enough along that I'm comfortable creating #3970

[Jalex Stark]

ah, the diff looks very beefy, but that's just because it has the diff from the unmerged prereqs PR

[Aaron Anderson]

#3953 is on the merge queue, and when it merges, there should only be one file in the diff

[Aaron Anderson]

It merged, there is now only one file in the diff