Beginner Question on a 'failed "apply"...'

Stream: new members

[Sebastian Ziesche]

I started to read into Lean4. After some browsing here and there, I went through the first 3 chapters of "Mathematics in Lean". Now I tried to apply the learned stuff to some "real" problem. It is about an inequality involving the regularized incomplete beta function. For the start, the integral definition is however not necessary and I just wanted to manage, to write down the theorem I want to prove (I got that with a "sorry" proof without further complaints from VSCode). As a second step, I wanted to apply a well known recursive formula (which you can find on wikipedia and can also easily prove yourself on paper). My current state is the following:

import Mathlib.Tactic
import Mathlib.Util.Delaborators
import Mathlib.Data.Real.Basic

open Nat

set_option warningAsError false

-- definition of the beta function for constraint to the natural numbers
def B (a : ℕ) (b : ℕ) : ℚ := factorial (a-1) * factorial (b-1) / factorial (a + b - 1)

example (k n : ℕ)
                       (I : ℚ → ℕ → ℕ → ℚ)  -- a placeholder for the incomplete regularized beta-function
                       (hrec1: ∀ (q : ℚ) (a b : ℕ), 0 < a → 0 < b → I q a (b+1) = I q a b + q^a * (1-q)^b / b / B a b)  -- the first recursive relation known for I
                       (hrec2: ∀ (q : ℚ) (a b : ℕ), 0 < a → 0 < b → I q (a+1) b = I q a b - q^a * (1-q)^b / a / B a b) -- the second recursive relation known for I
                       (hn : 0 < n-k)
                       (hk : 0 < k) : I ((k+1) / (n+1)) (k+1) (n-k) ≤ I (k / (n+1)) k (n-k+1) := by
  apply hrec2 ((k+1) / (n+1)) k (n-k)

as the first step of the proof, I just want to apply the second known recursion with the proper values but I get the error:
"tactic 'apply' failed, failed to unify
I ((↑k + 1) / (↑n + 1)) (k + 1) (n - k) =
I ((↑k + 1) / (↑n + 1)) k (n - k) -
((↑k + 1) / (↑n + 1)) ^ k * (1 - (↑k + 1) / (↑n + 1)) ^ (n - k) / ↑k / B k (n - k)
with
I ((↑k + 1) / (↑n + 1)) (k + 1) (n - k) ≤ I (↑k / (↑n + 1)) k (n - k + 1)"

so the left-hand-side of both equations looks exactly the same to me, so I don't really understand, why the unification fails. Can somebody explain to me, where I am going wrong?

[Kevin Buzzard]

Do you understand what the apply tactic does? And do you understand what the rw tactic does? The rule of thumb with apply is that even though it sounds like an English word, it turns out that mathematicians "apply" all sorts of ideas in ways which cannot be done with the apply tactic.

[Kevin Buzzard]

Here is what I write about the apply tactic in my undergraduate Lean course (see in particular the "note").

[Kevin Buzzard]

An explanation of why apply doesn't work here

The conclusion of hrec2 ((k+1) / (n+1)) k (n-k) is I ((↑k + 1) / (↑n + 1)) (k + 1) (n - k) = <something>. But your goal is not literally equal to this, it is I ((↑k + 1) / (↑n + 1)) (k + 1) (n - k) ≤ <something else>. So apply is not the appropriate tactic to use here. If you try rw [hrec2 ((k+1) / (n+1)) k (n-k)] then it will change I ((↑k + 1) / (↑n + 1)) (k + 1) (n - k) to the right hand side of the conclusion of hrec2 but it will also create further goals corresponding to the hypotheses of hrec2.

[Sebastian Ziesche]

I definitely have to admit, that I sometimes missed a little more "clear definition" instead of "example" would have been nice in the MIL tut. That combined with me being still quite new, I apparently don't have a too clear understanding of the difference yet.

[Kevin Buzzard]

Well I left some clues and also a spoiler if you just want to see the answer :-) I'm also going to move this thread to #new members . The #lean4 channel is about questions regarding Lean 4 itself; you are using Mathlib and it looks like you are a beginner so the new members channel is perfect for you; please feel free to ask as many beginner questions as you like there.

[Notification Bot]

This topic was moved here from #lean4 > Beginner Question on a 'failed "apply"...' by Kevin Buzzard.

[Kevin Buzzard]

@Sebastian Ziesche just to flag that your question is now here in a different channel.

[Sebastian Ziesche]

thank you for your detailed answer. The description of "apply" was very helpful!
Actually I had tried "rw" too, but as I realized, when I saw your solution, I had a small typo in it ^^ (used hrec1 instead of hrec2).

[Kevin Buzzard]

By the way, if I got it right then you only ever apply the function B to naturals a and b with a>0 and b>0. But in B you have this awkward subtraction a - 1 which is the poorly-behaved natural subtraction (e.g. 0 - 1 = 0) and it's hard to use natural subtraction because results like x - y + y = x are not true (because of this rounding, as naturals can't be negative). You might find your work a lot less painful if you use instead of B the function C defined by $C(x,y)=B(x+1,y+1)$. Then $C$ will not have any natural subtractions in and will thus be easier to work with. Basically I'm suggesting you let x=a-1 and y=b-1 be naturals, and then instead of demanding a>0 and b>0 you just let a=x+1 and b=y+1 which are automatically positive. It's little details like this which can make your life a lot easier in this formalization game.