Zulip Chat Archive

Stream: graph theory

Topic: freek 83


Jalex Stark (Aug 15 2020 at 13:21):

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 (Aug 15 2020 at 13:23):

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 (Aug 15 2020 at 13:24):

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

Jalex Stark (Aug 15 2020 at 13:25):

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

Jalex Stark (Aug 24 2020 at 23:25):

#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 (Aug 24 2020 at 23:28):

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

Jalex Stark (Aug 24 2020 at 23:29):

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

Kyle Miller (Aug 24 2020 at 23:29):

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

Aaron Anderson (Aug 24 2020 at 23:30):

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 (Aug 24 2020 at 23:32):

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 (Aug 24 2020 at 23:32):

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 (Aug 24 2020 at 23:34):

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 (Aug 24 2020 at 23:49):

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

Aaron Anderson (Aug 24 2020 at 23:50):

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

Aaron Anderson (Aug 27 2020 at 00:27):

Check out branch#friendship_final

Aaron Anderson (Aug 27 2020 at 00:29):

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

Aaron Anderson (Aug 27 2020 at 00:34):

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

Aaron Anderson (Aug 27 2020 at 00:42):

#3953

Jalex Stark (Aug 27 2020 at 00:53):

Aaron Anderson said:

Check out branch#friendship_final

are we ready to delete the freek_83_friendship_theorem branch?

Aaron Anderson (Aug 27 2020 at 00:56):

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

Aaron Anderson (Aug 27 2020 at 00:57):

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

Jalex Stark (Aug 27 2020 at 01:00):

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 (Aug 27 2020 at 03:18):

You can delete it now.

Aaron Anderson (Aug 27 2020 at 03:19):

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

Kyle Miller (Aug 27 2020 at 06:30):

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 (Aug 27 2020 at 07:18):

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

Aaron Anderson (Aug 27 2020 at 07:18):

Thanks for your help!

Aaron Anderson (Aug 29 2020 at 02:16):

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

Jalex Stark (Aug 29 2020 at 13:56):

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

Aaron Anderson (Aug 29 2020 at 17:23):

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

Aaron Anderson (Aug 29 2020 at 18:56):

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


Last updated: Dec 20 2023 at 11:08 UTC