Zulip Chat Archive
Stream: new members
Topic: question about binomial coefficients
Access (Oct 19 2024 at 14:42):
I want to prove binom n 1 = binom n-1. the code is here
def fact (x : Nat): Nat:=
match x with
| 0 => 1
| n + 1 => (n + 1) * fact n
#eval fact 100
-- Define binomial coefficient using factorial
def binom (n k : Nat) : Nat :=
fact n / ( fact k * fact (n-k) )
-- Import the necessary library for natural numbers (ℕ)
-- Prove that f a * f b = f b * f a using the built-in `mul_comm`
theorem mul_comm_for_functions {f : Nat → Nat} (a b : Nat) : f a * f b = f b * f a :=
Nat.mul_comm (f a) (f b)
theorem functions_one {f : Nat → Nat} (a) : f a * 1 = f a :=
Nat.mul_one (f a)
theorem binom_symmetry (n k : Nat) (h : k ≤ n) : binom n k = binom n (n - k) :=
by
-- Unfold the definition of binom
unfold binom
-- Simplify using commutativity of multiplication (fact k * fact (n - k) = fact (n - k) * fact k)
rw [Nat.mul_comm (fact k) (fact (n - k))]
have : n - (n - k) = k := by
-- Use `Nat.sub_add_eq_add_sub` to show that n - (n - k) = k
exact Nat.sub_sub_self h
rw [this]
theorem binom_zero (n : Nat) (h : n > 0) : binom n 0 = 1 :=
by
-- Unfold the definition of binom
unfold binom
-- Simplify the expression
rw [Nat.sub_zero] -- n - 0 = n
-- Rewrite fact 0 = 1
have fact_0 : fact 0 = 1 := rfl
rw [fact_0] -- Replace fact 0 in the expression
rw [Nat.mul_comm]
rw [functions_one]-- Now it simplifies to fact n / fact n
-- The expression is now fact n / (1 * fact n)
have fact_pos : fact n > 0 := sorry
rw [Nat.div_self] -- Show that fact n / fact n = 1
At last I have laready made the formula to 1=1, but it still cannot be compiled.. Can someone help me? I am new to lean4
Notification Bot (Oct 19 2024 at 15:16):
A message was moved here from #maths > For measures, is MutuallySingular the same as Disjoint? by Kevin Buzzard.
Kevin Buzzard (Oct 19 2024 at 15:20):
I'm not sure I understand the question. At the bottom of your in-progress proof the tactic state is
n : Nat
h : n > 0
fact_0 : fact 0 = 1
fact_pos : fact n > 0
⊢ 0 < fact n
and (abusing the fact that a > b
is defined to mean b < a
) you can close this goal with exact fact_pos
.
Kevin Buzzard (Oct 19 2024 at 15:21):
PS @Access I moved your post to a more appropriate channel.
Kevin Buzzard (Oct 19 2024 at 15:31):
Oh, the issue is perhaps the sorry
in the middle of the proof which I only just spotted! (I'm slightly surprised it didn't come out in red in the code above). This should be proved in a separate lemma if you're going to make all this API yourself (mathlib already has fact and binom with all the API present; you're just seeing here how much work it is to make a new definition actually usable).
theorem fact_pos (n : Nat) : fact n > 0 := by
induction n with
| zero =>
simp [fact]
| succ n ih =>
simp_all [fact]
Access (Oct 19 2024 at 16:42):
Kevin Buzzard said:
Oh, the issue is perhaps the
sorry
in the middle of the proof which I only just spotted! (I'm slightly surprised it didn't come out in red in the code above). This should be proved in a separate lemma if you're going to make all this API yourself (mathlib already has fact and binom with all the API present; you're just seeing here how much work it is to make a new definition actually usable).theorem fact_pos (n : Nat) : fact n > 0 := by induction n with | zero => simp [fact] | succ n ih => simp_all [fact]
but my main problem is that, at the bottom of the line , I have got
rw [Nat.div_self] -- Here I got 1 = 1
But I still not know that is the error about
unsolved goals
n : Nat
h : n > 0
fact_0 : fact 0 = 1
⊢ 0 < fact n
what should I need? Does it have something to do with the fact_pos? thanks
I see , I need to use exact.. but where to use? I still have trouble to unstand the function
Kevin Buzzard (Oct 19 2024 at 23:37):
I cannot see 1 = 1
and I'm wondering if you're misunderstanding Lean's output. If you want to see what's going on then try putting your cursor at the beginning of a line. If you're seeing 1 = 1
then are you sure that this is something Lean is asking you to prove, and not something Lean is printing out because it's trying to be helpful? Can you post a screenshot indicating where your cursor is when you see this 1 = 1
output?
Access (Oct 20 2024 at 03:17):
Kevin Buzzard said:
I cannot see
1 = 1
and I'm wondering if you're misunderstanding Lean's output. If you want to see what's going on then try putting your cursor at the beginning of a line. If you're seeing1 = 1
then are you sure that this is something Lean is asking you to prove, and not something Lean is printing out because it's trying to be helpful? Can you post a screenshot indicating where your cursor is when you see this1 = 1
output?
image.png
Emm, does not it means I get 1=1? Emm, sorry, I am very new one for lean4
Ruben Van de Velde (Oct 20 2024 at 07:13):
Okay, after rewriting with Nat.div_self
, your goal is indeed 1 = 1
(as far as I can tell), but rw
closes this goal for you. Then you have yo prove the second goal, 0 < fact n
Ruben Van de Velde (Oct 20 2024 at 07:14):
You're trying to prove with exact fact_pos
, but fact_pos
is a theorem that takes an explicit argument for the n
in fact n
(or, if you like, a function that eats an n
and spits out a proof of 0 < fact n
. So if you instead write fact_pos n
, I think that'll solve the second goal
Access (Oct 20 2024 at 07:40):
Ruben Van de Velde said:
You're trying to prove with
exact fact_pos
, butfact_pos
is a theorem that takes an explicit argument for then
infact n
(or, if you like, a function that eats ann
and spits out a proof of0 < fact n
. So if you instead writefact_pos n
, I think that'll solve the second goal
Thank you! solved! I am so silly
Last updated: May 02 2025 at 03:31 UTC