question about binomial coefficients

Stream: new members

[Access]

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]

A message was moved here from #maths > For measures, is MutuallySingular the same as Disjoint? by Kevin Buzzard.

[Kevin Buzzard]

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]

PS @Access I moved your post to a more appropriate channel.

[Kevin Buzzard]

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]

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]

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]

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

image.png
Emm, does not it means I get 1=1? Emm, sorry, I am very new one for lean4

[Ruben Van de Velde]

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]

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]

Ruben Van de Velde said:

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

Thank you! solved! I am so silly