Zulip Chat Archive

Stream: new members

Topic: Tidying up a proof


view this post on Zulip Bhavik Mehta (Nov 19 2019 at 10:53):

Hi all, I've written a proof for a (seemingly) simple statement, but I feel like it could be simplified a lot. Any comments or suggestions appreciated!

lemma sub_sub_assoc {r k n : } (h1 : k  r) (h2 : r  n) : n - r + k = n - (r - k) :=
by omega

lemma fact_pred {r : } (h : r > 0) : nat.fact r = r * nat.fact (r-1) :=
calc nat.fact r = nat.fact (nat.succ (r-1))       : by rw [ nat.pred_eq_sub_one, nat.succ_pred_eq_of_pos h]
        ...     = nat.succ (r-1) * nat.fact (r-1) : nat.fact_succ _
        ...     = r * nat.fact (r-1)              : by rw [ nat.pred_eq_sub_one, nat.succ_pred_eq_of_pos h]

lemma choose_lemma {n r : } (hr1 : 1  r) (hr2 : r  n) : (n - r + 1) * nat.choose n (r-1) = nat.choose n r * r :=
begin
  have: r - 1  n := le_trans (nat.pred_le r) r  n,
  apply nat.eq_of_mul_eq_mul_right (mul_pos (nat.fact_pos (r-1)) (nat.fact_pos (n-r))),
  by calc (n - r + 1) * nat.choose n (r - 1) * (nat.fact (r - 1) * nat.fact (n - r))
        = nat.choose n (r-1) * nat.fact (r-1) * ((n - r + 1) * nat.fact (n - r)) : by rw [mul_assoc, mul_comm]; simp only [mul_assoc]; rw mul_comm _ (n-r+1)
    ... = nat.choose n (r-1) * nat.fact (r-1) * nat.fact (n - r + 1)             : by rw  nat.fact_succ
    ... = nat.choose n (r-1) * nat.fact (r-1) * nat.fact (n - (r - 1))           : by rw sub_sub_assoc hr1 hr2
    ... = nat.fact n                                                             : by rw nat.choose_mul_fact_mul_fact r - 1  n
    ... = nat.choose n r * nat.fact r * nat.fact (n - r)                         : by rw  nat.choose_mul_fact_mul_fact r  n
    ... = nat.choose n r * (r * nat.fact (r - 1)) * nat.fact (n - r)             : by rw fact_pred r  1
    ... = nat.choose n r * r * (nat.fact (r - 1) * nat.fact (n - r))             : by simp only [mul_assoc],
end

theorem main_lemma {A B n r : } (hr1 : 1  r) (hr2 : r  n) : A * r  B * (n - r + 1)  (A : ) / (nat.choose n r)  B / nat.choose n (r-1) :=
begin
  intro k,
  have: r - 1  n := le_trans (nat.pred_le r) r  n,
  have: 0 < nat.choose n (r-1) := nat.choose_pos r - 1  n,
  have: 0 < nat.choose n r := nat.choose_pos r  n,
  rw [div_le_iff', mul_comm, div_mul_eq_mul_div, le_div_iff]; norm_cast, rotate,
    assumption, assumption,
  apply le_of_mul_le_mul_right _,
  exact hr1,
  by calc A * nat.choose n (r - 1) * r = A * r * nat.choose n (r-1) : by rw [nat.mul_assoc, nat.mul_comm _ r,  nat.mul_assoc]
          ...  B * (n - r + 1) * nat.choose n (r-1)                : by apply nat.mul_le_mul_right _ k
          ... = B * nat.choose n r * r                              : by rw [mul_assoc, mul_assoc, choose_lemma hr1 hr2]
end

I don't have need for any of the internal lemmas so feel free to rearrange/remove them, as long as main_lemma looks pretty much the same.
Thanks!

view this post on Zulip Edward Ayers (Nov 19 2019 at 11:16):

You can use ac_refl on the first and last steps of the calc in choose_lemma

view this post on Zulip Bhavik Mehta (Nov 19 2019 at 11:18):

Ooooh nice thanks

view this post on Zulip Mario Carneiro (Nov 19 2019 at 11:29):

I managed the following alternate proof:

theorem div_le_div_iff {α} [linear_ordered_field α] {a b c d : α}
  (hc : 0 < c) (hd : 0 < d) : a / c  b / d  a * d  b * c :=
by rw [le_div_iff hd, div_mul_eq_mul_div, div_le_iff hc]

lemma nat.choose_succ_right_eq (n k) (h : k + 1  n) :
  nat.choose n (k + 1) * (k + 1) = nat.choose n k * (n - k) :=
begin
  have e : n - (k + 1) + 1 = n - k,
  { rw [ nat.sub_add_comm h, nat.add_sub_add_right] },
  have := nat.choose_mul_fact_mul_fact (le_of_lt h),
  rw [ nat.choose_mul_fact_mul_fact h, nat.fact_succ,
     e, nat.fact_succ, nat.succ_eq_add_one, e,
    nat.succ_eq_add_one,
     mul_assoc, nat.mul_right_inj (nat.fact_pos _),
     mul_assoc, mul_right_comm, nat.mul_right_inj (nat.fact_pos _)] at this,
  rw this
end

theorem main_lemma {A B n r : } (hr1 : 1  r) (hr2 : r  n)
  (h : A * r  B * (n - r + 1)) :
  (A : ) / (nat.choose n r)  B / nat.choose n (r-1) :=
begin
  rw [div_le_div_iff]; norm_cast,
  { cases r, cases hr1,
    rw  mul_le_mul_right (nat.succ_pos r),
    rw nat.succ_eq_add_one at *,
    rw [ nat.sub_add_comm hr2, nat.add_sub_add_right] at h,
    rw [nat.add_sub_cancel, mul_assoc B, nat.choose_succ_right_eq _ _ hr2,
      mul_right_comm,  mul_assoc, mul_right_comm B],
    exact nat.mul_le_mul_right _ h },
  { exact nat.choose_pos hr2 },
  { exact nat.choose_pos (le_trans (nat.sub_le _ _) hr2) }
end

view this post on Zulip Kevin Buzzard (Nov 19 2019 at 14:06):

example (n : ℕ) : n > 0 → ¬ (n = 0) := by ?? Which tactic finishes this? Or is it a function? I couldn't find it :-/

view this post on Zulip Kevin Buzzard (Nov 19 2019 at 14:06):

example (n : ℕ) : n > 0 → ¬ (n = 0) := by intros; linarith :D

view this post on Zulip Mario Carneiro (Nov 19 2019 at 14:06):

ne_of_lt or ne_of_gt

view this post on Zulip Kevin Buzzard (Nov 19 2019 at 14:07):

aah I was foolishly looking for ne_zero_of_pos

view this post on Zulip Kevin Buzzard (Nov 19 2019 at 14:43):

I tried multiplying everything out but it was horrible :-(

import data.rat tactic.linarith

open nat

-- this should be in mathlib, right?
theorem div_le_div_iff {α} [linear_ordered_field α] {a b c d : α}
  (hc : 0 < c) (hd : 0 < d) : a / c  b / d  a * d  b * c :=
by rw [le_div_iff hd, div_mul_eq_mul_div, div_le_iff hc]

-- Should this be in data.rat? It doesn't easily follow from nat.choose_eq_fact_div_fact
def rat.choose_eq_fact_div_fact (n k : ) (h : k  n) : (choose n k : ) = fact n / (fact k * fact (n - k)) :=
eq_div_of_mul_eq _ _ (mul_ne_zero (ne_of_gt $ by simp [fact_pos]) (ne_of_gt $ by simp [fact_pos])) $
begin norm_cast, rw mul_assoc, exact choose_mul_fact_mul_fact h end

-- s = r - 1
theorem main_lemma {A B n s : } (hr2 : s + 1  n) (h : A * (s + 1)  B * (n - s)) :
  (A : ) / (nat.choose n (s + 1))  B / nat.choose n s :=
begin
  rw [rat.choose_eq_fact_div_fact, rat.choose_eq_fact_div_fact, div_div_eq_mul_div, div_div_eq_mul_div],
  apply div_le_div_of_le_of_pos,
  norm_cast,
  rw [@nat.sub_add_cancel (n - s) 1, fact_succ, fact_succ, succ_sub, succ_sub_one, nat.sub_sub],
  rw [show A * (succ s * fact s * fact (n - (s + 1))) = A * (s + 1) * (fact s * fact (n - (s + 1))), by ring],
  rw [show B * (fact s * ((n - s) * fact (n - (s + 1)))) = B * (n - s) * (fact s * fact (n - (s + 1))), by ac_refl],
  refine mul_le_mul_right _ h,
  repeat {linarith},
  exact nat.le_sub_left_of_add_le hr2,
  exact nat.le_sub_left_of_add_le hr2,
  norm_cast, apply fact_pos,
end

view this post on Zulip Kevin Buzzard (Nov 19 2019 at 14:45):

This surprised me along the way:

example (B s n : ) : B * (fact s * ((n - s) * fact (n - s - 1))) = B * (n - s) * (fact s * fact (n - s - 1)) :=
begin
--  ac_refl, -- closes goal
  ring, -- does not close goal
  sorry
end

@Mario Carneiro would you have expected ring to work there?

view this post on Zulip Mario Carneiro (Nov 19 2019 at 14:46):

yes

view this post on Zulip Mario Carneiro (Nov 19 2019 at 14:47):

Whenever ring fails, try ring1, which reports a useful error instead of doing a fall back thing

view this post on Zulip Kevin Buzzard (Nov 19 2019 at 14:48):

example (f1 n s: ) : f1 * (n - s)  = (n - s) * f1  := by ring -- fails

view this post on Zulip Kevin Buzzard (Nov 19 2019 at 14:49):

app_builder_exception, more information can be obtained using command `set_option trace.app_builder true`
state:
f1 n s : ℕ
⊢ f1 * (n - s) = (n - s) * f1

is the output from ring1

view this post on Zulip Kevin Buzzard (Nov 19 2019 at 14:49):

[app_builder] failed to create an 'has_neg.neg'-application, there are missing implicit arguments

view this post on Zulip Mario Carneiro (Nov 19 2019 at 14:50):

it thinks the subtraction is ring subtraction, and builds a bad term

view this post on Zulip Kevin Buzzard (Nov 19 2019 at 14:50):

I can generalize my way out of this I guess

view this post on Zulip Kevin Buzzard (Nov 19 2019 at 14:50):

"you don't know this, but n-s is an atom"

view this post on Zulip Kevin Buzzard (Nov 19 2019 at 14:51):

Why does multiplying it all out hurt so much? That's an algorithmic way to solve this problem [I'm now talking about the original q]

view this post on Zulip Kevin Buzzard (Nov 19 2019 at 14:54):

What would the Isabelle proof of this triviality look like? @Sebastien Gouezel do you know?

view this post on Zulip Mario Carneiro (Nov 19 2019 at 14:55):

what do you want to be less painful?

view this post on Zulip Mario Carneiro (Nov 19 2019 at 14:55):

there are several interacting things here

view this post on Zulip Mario Carneiro (Nov 19 2019 at 14:56):

I think the real thing is that the lemma I called nat.choose_succ_right_eq was missing

view this post on Zulip Mario Carneiro (Nov 19 2019 at 14:56):

one of the basic facts about choose is how it changes when you move by one in any direction

view this post on Zulip Mario Carneiro (Nov 19 2019 at 14:57):

div_le_div_iff missing is even more scandalous. I would have expected that in core

view this post on Zulip Mario Carneiro (Nov 19 2019 at 14:58):

-- Should this be in data.rat? It doesn't easily follow from nat.choose_eq_fact_div_fact
def rat.choose_eq_fact_div_fact (n k : ) (h : k  n) : (choose n k : ) = fact n / (fact k * fact (n - k)) :=

It does easily follow from choose_mul_fact_mul_fact though

view this post on Zulip Sebastien Gouezel (Nov 19 2019 at 15:13):

What would the Isabelle proof of this triviality look like? Sebastien Gouezel do you know?

Isabelle automation is order of magnitudes better. So, anything will work. I just tried it:

lemma for_kevin:
  fixes f1 n s::nat
  shows "f1 * (n-s) = (n-s) * f1"
by simp

You can replace by simp with by auto, or by algebra, or by fastforce, or by force. In fact, I just typed try0 and Isabelle suggested all these solutions right away.

view this post on Zulip Mario Carneiro (Nov 19 2019 at 15:14):

I think he's talking about the choose proof

view this post on Zulip Sebastien Gouezel (Nov 19 2019 at 15:15):

Which statement?

view this post on Zulip Mario Carneiro (Nov 19 2019 at 15:16):

Probably main_lemma?

view this post on Zulip Kevin Buzzard (Nov 19 2019 at 15:16):

theorem main_lemma {A B n r : } (hr1 : 1  r) (hr2 : r  n) : A * r  B * (n - r + 1)  (A : ) / (nat.choose n r)  B / nat.choose n (r-1) :=

view this post on Zulip Kevin Buzzard (Nov 19 2019 at 15:17):

I really want this to be easy

view this post on Zulip Mario Carneiro (Nov 19 2019 at 15:17):

I get the sense that kevin's proof is a tactic bash

view this post on Zulip Kevin Buzzard (Nov 19 2019 at 15:17):

My proof is "LOOK. (nr)=n!r!(nr)!\binom{n}{r}=\frac{n!}{r!(n-r)!} AND THE REST IS TRIVIAL"

view this post on Zulip Mario Carneiro (Nov 19 2019 at 15:18):

This sort of proof feels easier in metamath to me

view this post on Zulip Kevin Buzzard (Nov 19 2019 at 15:18):

(assuming fact_succ)

view this post on Zulip Mario Carneiro (Nov 19 2019 at 15:18):

all this business with saturating subtraction isn't a problem

view this post on Zulip Mario Carneiro (Nov 19 2019 at 15:20):

It might help if nat.choose was defined over integers

view this post on Zulip Kevin Buzzard (Nov 19 2019 at 15:26):

-- Should this be in data.rat? It doesn't easily follow from nat.choose_eq_fact_div_fact
def rat.choose_eq_fact_div_fact (n k : ) (h : k  n) : (choose n k : ) = fact n / (fact k * fact (n - k)) :=

It does easily follow from choose_mul_fact_mul_fact though

My proof was an attempt to show this and it was still pretty horrible. What am I missing?

view this post on Zulip Kevin Buzzard (Nov 19 2019 at 15:27):

import data.rat tactic.linarith

open nat

-- this should be in mathlib, right?
theorem div_le_div_iff {α} [linear_ordered_field α] {a b c d : α}
  (hc : 0 < c) (hd : 0 < d) : a / c  b / d  a * d  b * c :=
by rw [le_div_iff hd, div_mul_eq_mul_div, div_le_iff hc]

-- Should this be in data.rat? It doesn't easily follow from nat.choose_eq_fact_div_fact
def rat.choose_eq_fact_div_fact (n k : ) (h : k  n) : (choose n k : ) = fact n / (fact k * fact (n - k)) :=
eq_div_of_mul_eq _ _ (mul_ne_zero (ne_of_gt $ by simp [fact_pos]) (ne_of_gt $ by simp [fact_pos])) $
begin norm_cast, rw mul_assoc, exact choose_mul_fact_mul_fact h end

-- r = s + 1
-- n = t + 1 + s
theorem main_lemma {A B s t : } (h : A * (s + 1)  B * (t + 1)) :
  (A : ) / (nat.choose (t + 1 + s) (s + 1))  B / nat.choose (t + 1 + s) s :=
begin
  rw [rat.choose_eq_fact_div_fact, rat.choose_eq_fact_div_fact, div_div_eq_mul_div, div_div_eq_mul_div],
  apply div_le_div_of_le_of_pos,
  norm_cast,
  rw [nat.add_sub_cancel, add_right_comm, add_assoc, nat.add_sub_cancel, fact_succ, fact_succ],
  convert nat.mul_le_mul_right (fact s * fact t) h using 1,
  repeat {linarith}, repeat {rw succ_eq_add_one; ring},
  norm_cast, apply fact_pos,
end

Using less painful variables s and t I can get it down to this.

view this post on Zulip Kevin Buzzard (Nov 19 2019 at 15:30):

But if Isabelle can just blast through it then this will give me a better understanding of what we are missing in Lean. This proof should be trivial given some hints -- shouldn't it? by schoolkid using [choose_mul_fact_mul_fact, fact_pos, fact_succ]

view this post on Zulip Mario Carneiro (Nov 19 2019 at 15:30):

I think you got it down pretty well.

theorem rat.choose_eq_fact_div_fact (n k : ) (h : k  n) : (choose n k : ) = fact n / (fact k * fact (n - k)) :=
by rw eq_div_iff_mul_eq; norm_cast; [
  rw [ mul_assoc, choose_mul_fact_mul_fact h],
  exact ne_of_gt (mul_pos (fact_pos _) (fact_pos _))]

view this post on Zulip Mario Carneiro (Nov 19 2019 at 15:31):

If you have a sledgehammer then you can make it through this, I think

view this post on Zulip Kevin Buzzard (Nov 19 2019 at 15:31):

because all schoolkids know div_div_eq_mul_div, div_le_div_of_le_of_pos, div_div_eq_mul_div, nat.add_sub_cancel etc

view this post on Zulip Mario Carneiro (Nov 19 2019 at 15:32):

they also know a number of false variations on those :P

view this post on Zulip Kevin Buzzard (Nov 19 2019 at 15:32):

Yeah, it's a pretty powerful tactic. You can prove false with it if you're not careful

view this post on Zulip Kevin Buzzard (Nov 19 2019 at 15:33):

I started my lectures this year with a proof that all triangles were equilateral and it was only once I'd finished that people started complaining; I made the error about 10 lines before that.

view this post on Zulip Kevin Buzzard (Nov 19 2019 at 15:33):

They were happy with the method but uncomfortable with the conclusion

view this post on Zulip Sebastien Gouezel (Nov 19 2019 at 15:43):

Here is an Isabelle proof:

lemma for_kevin2:
  fixes A B n r::nat
  assumes "1 ≤ r" "r ≤ n" "A * r ≤ B * (n-r+1)"
  shows "A / (binomial n r) ≤ B / (binomial n (r-1))"
proof -
  have I: "binomial n r = (fact n)/(fact r * fact (n-r))"
    using assms(2) binomial_fact by blast
  have J : "binomial n (r-1) = (fact n)/(fact (r-1) * fact (n+1-r))"
    using assms(1) assms(2) binomial_fact[of "r-1" n] by force
  have K : "fact r = of_nat r * fact (r-1)"
    using fact_reduce[of r] assms(1) by auto
  have L : "fact (n+1-r) = of_nat (n+1-r) * fact (n-r)"
    using fact_reduce[of "n+1-r"] assms by auto
  show ?thesis unfolding I J K L apply (auto simp add: divide_simps)
    by (metis Suc_diff_le Suc_eq_plus1_left add.commute assms(2) assms(3) of_nat_mono of_nat_mult)
qed

I still had to help it a little bit giving the auxiliary statements I, J, K, L. The last line is needed since my assumption is formulated for integer numbers but the conclusion needs it over rationals (in fact here over the reals, as Isabelle coerced everything to reals when I wrote the division). The point is I didn't write this line, it was found by sledgehammer.

view this post on Zulip Sebastien Gouezel (Nov 19 2019 at 15:46):

I should tell you what binomial_fact and fact_reduce are, by the way. They are preexisting facts in the library, as follows.

lemma fact_reduce: "n > 0 ⟹ fact n = of_nat n * fact (n - 1)"
  by (cases n) auto

lemma binomial_fact:
  assumes kn: "k ≤ n"
  shows "(of_nat (n choose k) :: 'a::field_char_0) = fact n / (fact k * fact (n - k))"

view this post on Zulip Kevin Buzzard (Nov 19 2019 at 15:46):

So I, J, K, L are the things we knew we needed, and the proofs are relatively straightforward using automation, and then you have some proof which kind of looks awful, although it also looks much shorter than the Lean proof, but it was also found using automation. Thanks Sebastien.

view this post on Zulip Kevin Buzzard (Nov 19 2019 at 15:47):

In particular the proof still looks a bit clunky but it was probably much easier for the user to write.

view this post on Zulip Sebastien Gouezel (Nov 19 2019 at 15:50):

When I write an Isabelle proof I write down enough intermediate statements, and then I ask automation to complete the proof of each intermediate statement, and also to combine them all to prove the main result. If it doesn't work, I add more intermediate statements. This is really different from the way I write Lean proofs (and I think the Isabelle way is much smoother!)

view this post on Zulip Kevin Buzzard (Nov 19 2019 at 15:50):

So now we need to turn this into some sort of concrete proposal(s) for improving Lean.

view this post on Zulip Kevin Buzzard (Nov 19 2019 at 15:51):

Occasionally people pop up and say "I want to write Lean automation, what do you guys need?" and if they're not mathematicians I feel like I can't say "Groebner bases"

view this post on Zulip Kevin Buzzard (Nov 19 2019 at 15:53):

but I can't tell my cc from my simp so I don't feel competent enough to answer a computer scientist. Oh, I know we need a sledgehammer but this seems like a highly non-trivial task. I used to know that we needed norm_cast but now we have that. Imagine how much worse the Lean proof would have been a year ago.

view this post on Zulip Sebastien Gouezel (Nov 19 2019 at 15:54):

What we really need is auto (or force). Something that uses the simplifier but also tries some things that have been marked as reasonable in the library, and backtracks if it doesn't work (with some backtracking depth which is not the same for auto, fastforce and force). This is called a tableau prover, I think.

view this post on Zulip Bryan Gin-ge Chen (Nov 19 2019 at 15:54):

Is it like a stronger version of tidy?

view this post on Zulip Kevin Buzzard (Nov 19 2019 at 15:55):

Out of interest, how long does the automation take to (a) prove I,J,K,L, (b) find the two-line incantation at the end and (c) compile the two-line incantation at the end? Are (a) and (c) super-quick and (b) might take a few minutes?

view this post on Zulip Sebastien Gouezel (Nov 19 2019 at 15:57):

What I also dearly miss is simprocs, i.e., simple algorithms that are used by simp to try to simplify things in addition to the lemmas that have been marked as simp. @Johannes Hölzl had given a start to this, in https://github.com/johoelzl/lean-simp-loop, but I think it never made it into production. For instance, if you see ∃a, a = t ∧ p a, you would like to reduce it to p t.

view this post on Zulip Kevin Buzzard (Nov 19 2019 at 15:58):

That's not some lemma in logic.basic which you can just rewrite or something?

view this post on Zulip Kevin Buzzard (Nov 19 2019 at 15:59):

Is it a bad simp lemma?

view this post on Zulip Sebastien Gouezel (Nov 19 2019 at 15:59):

(a) and (c) are instantaneous. (b) takes less than 5 seconds.

view this post on Zulip Sebastien Gouezel (Nov 19 2019 at 16:00):

Johannes also wanted as a simproc to have∃a, p a ∧ ∃b, ∃h : a = f b, q a h transform into ∃b, p (f b) ∧ q (f b) rfl, and also all the possible variations. So, it's rather infinitely many lemmas (and many of them would not fire as simp lemmas, yes).

view this post on Zulip Sebastien Gouezel (Nov 19 2019 at 16:02):

Yes, it's a stronger version of tidy (note that tidy never backtracks). back is supposed to do something like that, but I don't know if @Scott Morrison is planning to do it as a tableau prover, i.e., registering what has already been proved and add progressively new facts, to get something efficient.

view this post on Zulip Bhavik Mehta (Nov 19 2019 at 19:24):

If anyone's interested, I've now got it to this (taking a lot from @Mario Carneiro's version) :

lemma nat.choose_succ_right_eq {n k : } : nat.choose n (k + 1) * (k + 1) = nat.choose n k * (n - k) :=
begin
  have e : (n+1) * nat.choose n k = nat.choose n k * (k+1) + nat.choose n (k+1) * (k+1),
    rw [ nat.right_distrib,  nat.choose_succ_succ, nat.succ_mul_choose_eq],
  rw [ nat.sub_eq_of_eq_add e, mul_comm,  nat.mul_sub_left_distrib],
  simp
end

theorem div_le_div_iff {α} [linear_ordered_field α] {a b c d : α}
  (hc : 0 < c) (hd : 0 < d) : a / c  b / d  a * d  b * c :=
by rw [le_div_iff hd, div_mul_eq_mul_div, div_le_iff hc]

theorem main_lemma {A B n r : } (hr1 : 1  r) (hr2 : r  n)
  (h : A * r  B * (n - r + 1)) :
  (A : ) / (nat.choose n r)  B / nat.choose n (r-1) :=
begin
  rw div_le_div_iff; norm_cast,
  apply le_of_mul_le_mul_right _,
    exact hr1,
  cases r,
    simp,
  rw nat.succ_eq_add_one at *,
  rw [ nat.sub_add_comm hr2, nat.add_sub_add_right] at h,
  rw [nat.add_sub_cancel, mul_assoc B, nat.choose_succ_right_eq, mul_right_comm,  mul_assoc, mul_right_comm B],
  exact nat.mul_le_mul_right _ h,
  apply nat.choose_pos hr2,
  apply nat.choose_pos (le_trans (nat.pred_le _) hr2)
end

In particular a somewhat quicker proof of nat.choose_succ_right_eq, which doesn't need the assumption either

view this post on Zulip Bhavik Mehta (Nov 19 2019 at 19:25):

I don't really like how we do a cases r but it does seem faster

view this post on Zulip Kevin Buzzard (Nov 19 2019 at 19:26):

Your cases r is just my "replace r with s=r-1" right? It's just one less inequality to deal with. If you can start at 0, do.

view this post on Zulip Bhavik Mehta (Nov 19 2019 at 19:30):

It doesn't solve the inequality as far as I can tell - it's just that we state nat.choose_succ_right_eq with lots of + 1s around, so it's easier to unify when we've succed r

view this post on Zulip Bhavik Mehta (Nov 19 2019 at 23:53):

A PR for choose_succ_right_eq and another basic choose fact choose n k = choose n (n-k): https://github.com/leanprover-community/mathlib/pull/1717

view this post on Zulip Johan Commelin (Nov 20 2019 at 08:18):

I see the following line (https://github.com/leanprover-community/mathlib/blob/7ae8b1d6821da5f4018c8c885c88d74e21578a83/src/data/nat/basic.lean#L1086)

lemma succ_mul_choose_eq :  n k, succ n * choose n k = choose (succ n) (succ k) * succ k

Shouldn't that be rewritten to use (n+1) everywhere? I thought succ should be exposed as little as possible.

view this post on Zulip Bhavik Mehta (Nov 21 2019 at 10:17):

div_le_div_iff missing is even more scandalous. I would have expected that in core

PR for this (into algebra/ordered_field): https://github.com/leanprover-community/mathlib/pull/1720

view this post on Zulip Bhavik Mehta (Nov 21 2019 at 10:35):

I see the following line (https://github.com/leanprover-community/mathlib/blob/7ae8b1d6821da5f4018c8c885c88d74e21578a83/src/data/nat/basic.lean#L1086)

lemma succ_mul_choose_eq :  n k, succ n * choose n k = choose (succ n) (succ k) * succ k

Shouldn't that be rewritten to use (n+1) everywhere? I thought succ should be exposed as little as possible.

@Johan Commelin Is this a suggestion for the PR, or a general comment?

view this post on Zulip Johan Commelin (Nov 21 2019 at 10:38):

More of a general comment/question

view this post on Zulip Johan Commelin (Nov 21 2019 at 10:38):

I'm still confused about whether this is intended, or whether mathlib drifted to a style where succ is deprecated


Last updated: May 13 2021 at 18:26 UTC