Tidying up a proof

Stream: new members

[Bhavik Mehta]

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!

[Edward Ayers]

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

[Bhavik Mehta]

Ooooh nice thanks

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Mario Carneiro]

ne_of_lt or ne_of_gt

[Kevin Buzzard]

aah I was foolishly looking for ne_zero_of_pos

[Kevin Buzzard]

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

[Kevin Buzzard]

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?

[Mario Carneiro]

yes

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Kevin Buzzard]

I can generalize my way out of this I guess

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

[Kevin Buzzard]

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

[Mario Carneiro]

what do you want to be less painful?

[Mario Carneiro]

there are several interacting things here

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

-- 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

[Sebastien Gouezel]

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.

[Mario Carneiro]

I think he's talking about the choose proof

[Sebastien Gouezel]

Which statement?

[Mario Carneiro]

Probably main_lemma?

[Kevin Buzzard]

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) :=

[Kevin Buzzard]

I really want this to be easy

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Mario Carneiro]

This sort of proof feels easier in metamath to me

[Kevin Buzzard]

(assuming fact_succ)

[Mario Carneiro]

all this business with saturating subtraction isn't a problem

[Mario Carneiro]

It might help if nat.choose was defined over integers

[Kevin Buzzard]

-- 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?

[Kevin Buzzard]

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.

[Kevin Buzzard]

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]

[Mario Carneiro]

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 _))]

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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.

[Kevin Buzzard]

They were happy with the method but uncomfortable with the conclusion

[Sebastien Gouezel]

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.

[Sebastien Gouezel]

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))"

[Kevin Buzzard]

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.

[Kevin Buzzard]

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

[Sebastien Gouezel]

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!)

[Kevin Buzzard]

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

[Kevin Buzzard]

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"

[Kevin Buzzard]

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.

[Sebastien Gouezel]

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.

[Bryan Gin-ge Chen]

Is it like a stronger version of tidy?

[Kevin Buzzard]

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?

[Sebastien Gouezel]

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.

[Kevin Buzzard]

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

[Kevin Buzzard]

Is it a bad simp lemma?

[Sebastien Gouezel]

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

[Sebastien Gouezel]

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).

[Sebastien Gouezel]

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.

[Bhavik Mehta]

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

[Bhavik Mehta]

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

[Kevin Buzzard]

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.

[Bhavik Mehta]

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

[Bhavik Mehta]

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

[Johan Commelin]

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.

[Bhavik Mehta]

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

[Bhavik Mehta]

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?

[Johan Commelin]

More of a general comment/question

[Johan Commelin]

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