potential PR's

Stream: PR reviews

[Jeremy Avigad]

I don't know if this is a good place to propose potential PR's before working on them. If not, let me know. In any case, I have three to suggest.

(1) Silvia de Toffoli recently asked me to show her the clearest, most intuitive formalization of the mutilated checkerboard problem I could. This is what I came up with: https://gist.github.com/avigad/1080e327ad6806884c9c5091f5c449bd. Is this worth putting in mathlib? @Floris van Doorn recently formalized the Littlewood problem on cubes, which is much more impressive. I couldn't find that in the library, but did I miss it? If not, we could create a 'combinatorics' folder for both of these.

(2) On finset, we use bind s f or s.bind f for the union of f x as x ranges over s. This would scare any mathematician away. By analogy to the version on set, we could call it bUnion s f for 'bounded union'. How do people feel about that change? I can also look into introducing the bounded union notation, but I worry that it will conflict with the set theory notation in a bad way.

(On finset we also use the notation filter s p for the set of x in s satisfying p. There is a generic typeclass sep that handles that on set, but, alas, we cannot use that for finset because the finset version requires a typeclass instance for decidable equality. So I would be inclined to stick with filter.)

(3) The library has an empty pending folder. Does that serve a purpose any more? If not, shall we delete it?

[Mario Carneiro]

I believe it's done pending and is now fully pent

[Jeremy Avigad]

O.k., I PR'ed (3).

[Simon Hudon]

(2) we can introduce a synonym but this is a useful entry to have in the API. When you're trying to build a monad or even just use finset as a monad, you shouldn't have to wonder what bind is called. It's called bind.

[Floris van Doorn]

About (1). We discussed what to do with the cubing the cube problem here (including the replies below):
https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/cubing.20a.20cube/near/166786363

I think the consensus was that it was good to have a folder in mathlib, but outside src/with these kind of projects.

[Floris van Doorn]

But my formalization is indeed not yet in mathlib.

[Floris van Doorn]

I don't have a strong opinion on (2), but it would be nice to have notation for it.
For the parenthesized part of (2): would it be reasonably to add a sep typeclass for finset that uses classical.prop_decidable? (That is possible, right?) Just don't use the notation if you don't want to be fully classical.

[Jeremy Avigad]

Sounds good. At this stage, I prefer not to take the lead on structural decisions for mathlib, since the younger generation will (hopefully) be dealing with them longer than I will. If anyone creates such a folder, I'd be glad to add it, but I also don't mind leaving it as a gist.

I am also writing some notes for Silvia. It has to do with exactly the issue discussed on the last thread. Fenner Tanswell used the mutilated checkerboard problem in a paper (based on a formalization by Larry Paulson in Isabelle and another one in Mizar), and Silvia wants to respond to it. It seems that the philosophical community is looking to draw conclusions on the relationship between mathematics and formalization, and at least we can make sure the data is accurate from an ITP perspective.