Mathlib and rephrasings

Stream: new members

[Patrick Stevens]

I get the impression that mathlib is happy to have lots of similar rephrasings of things. The specific example I am looking at now is lemma choose_le_middle {r n : ℕ} : nat.choose n r ≤ nat.choose n (n/2), in data.nat.choose, which I need in the form nat.choose (2 * n) r ≤ nat.choose (2 * n) n. Is this the kind of mostly-trivial restatement that would be fine appearing in data.nat.choose immediately next to choose_le_middle?

[Patrick Stevens]

It's not absolutely trivial because the division is "quotient of naturals", so there is going to be at least one contentful line of proof

[Bhavik Mehta]

I think this one is fairly trivial since choose_le_middle r (2 * n) : choose (2 * n) r ≤ choose (2 * n) ((2*n)/2) and I'm fairly sure there's a lemma saying (2*n)/2 = n

[Bhavik Mehta]

(By the way, I think I should've made the arguments of src#choose_le_middle explicit...)

[Patrick Stevens]

Yeah, I am definitely going to make them explicit

[Patrick Stevens]

I think my "contentful" might have been less contentful than yours :P

[Mario Carneiro]

It is probably delicate to draw a sharp line here, but I think that this is the kind of variation that would be okay. Some part of the statement gets more complicated, another part gets simpler, and the statement now uses * instead of /; all of these can affect ease of application in a proof. The sort of lemma I think goes too far is e.g. a + (b + (c + d)) = a + ((b + c) + d), which is a rewrite instance of add_assoc. We have to draw lines like this if we want to "fill out" the library without generating an infinite number of lemmas