Zulip Chat Archive

Stream: new members

Topic: semigroup.to_has_mul versus nat.has_mul


view this post on Zulip Moritz Firsching (Feb 17 2021 at 20:50):

Consider the following proof attempt to a simple lemma:

import tactic

lemma factorial_divide (n m : ) (hmn: m  n):
((m.factorial * (n-m).factorial))  (n.factorial) :=
begin
  have chosse_mul:
  (n.choose m)* ((m.factorial * (n-m).factorial)) = (n.factorial) :=
    begin
      simp [nat.choose_eq_factorial_div_factorial hmn],
      -- simp [div_mul_eq_mul_div], why doesn't this work?
      sorry,
    end,
    apply dvd.intro_left ((n.choose m)),
    -- exact choose_mul, why doesn't this work?
  sorry,
end

I'm a bit stumped that e.g. in the after the line apply dvd.intro_left ((n.choose m)), I see the exact same state in the goal and in choose_mul in the lean infoview. When I click on the terms, I can see there is some difference, but how can I actually get control over how the division/multiplication is done when defining choose_mul?

view this post on Zulip Kevin Buzzard (Feb 17 2021 at 20:52):

The second question is easy to answer -- you made a typo :-) chosse -> choose

view this post on Zulip Moritz Firsching (Feb 17 2021 at 20:54):

cool, that explains solves the second "why doesn't this work?"!

view this post on Zulip Kevin Buzzard (Feb 17 2021 at 20:54):

As for the first, #check @div_mul_eq_mul_div shows you that it's a theorem which applies to comm_group_with_zeros, and the naturals are not an example of a comm_group_with_zero.

view this post on Zulip Kevin Buzzard (Feb 17 2021 at 20:56):

In fact there will not be a theorem of the form (a / b) * b = a for naturals, because this is not true in general, e.g. (3 / 2) * 2 = 1 * 2 = 2 :-/

view this post on Zulip Kevin Buzzard (Feb 17 2021 at 20:56):

to prove a / b * b = a for nats you need the assumption that b divides a, which unfortunately is what you're trying to prove :-/

view this post on Zulip Kevin Buzzard (Feb 17 2021 at 20:58):

The result you're trying to prove is already in the library -- it's called nat.factorial_mul_factorial_dvd_factorial, so you can prove it with by library_search. But if you're looking for a proof of your own then maybe this doesn't help.

view this post on Zulip Kevin Buzzard (Feb 17 2021 at 21:00):

There is also nat.choose_mul_factorial_mul_factorial

view this post on Zulip Moritz Firsching (Feb 17 2021 at 21:01):

Thanks I will just check out how those proofs work! (and meanwhile just use them)


Last updated: May 17 2021 at 22:15 UTC