2 beginner problems with an induction proof

Stream: new members

[rzeta0]

The following defines a recursively defined triangle number function, and then tries to prove a closed form for it.

import Mathlib.Tactic

def T: ℕ → ℚ
  | 0 => 0
  | n + 1 => n + 1 + T n

#eval T 4

example {n: ℕ} : T n = n * (n + 1) / 2 := by
  induction n with
  | zero =>
    calc
      T 0 = 0 := by rw [T]
      _ = 0 * (0 + 1) / 2 := by norm_num
  | succ n ih =>
    calc
      T (n + 1) = n + 1 + T n := by rw [T]
      _ = n + 1 + n * (n + 1) / 2 := by rw [ih]
      _ = (n + 1) * (n + 1 + 1) / 2 := by ring

Question 1: The proof doesn't work with def T: ℕ → ℕ, the last ring fails. Why is this? I assume it is because of the division by 2. Is it good practice to leave it as a rational number, or do people make efforts to "fix it"?

Question 2: Lean is telling me the inductive step is not resolved. Why? The following is the message which I don't know how to interpret - something about upcasting?

⊢ (↑n + 1) * (↑n + 1 + 1) / 2 = ↑(n + 1) * (↑(n + 1) + 1) / 2

[Ilmārs Cīrulis]

Solution with Nat -> Nat definition of T. For me triangle numbers feel more natural this way, but that's subjective, probably.

import Mathlib.Tactic

def T: ℕ → ℕ
  | 0 => 0
  | n + 1 => n + 1 + T n

#eval T 4

example {n: ℕ} : T n = n * (n + 1) / 2 := by
  induction n with
  | zero =>
    calc
      T 0 = 0 := by rw [T]
      _ = 0 * (0 + 1) / 2 := by norm_num
  | succ n ih =>
    calc
      T (n + 1) = n + 1 + T n := by rw [T]
      _ = n + 1 + n * (n + 1) / 2 := by rw [ih]
      _ = (n + 1) * (n + 1 + 1) / 2 := by ring_nf; omega

And no, I don't know why exactly omega works here. :|

[Ilmārs Cīrulis]

import Mathlib.Tactic

def T: ℕ → ℚ
  | 0 => 0
  | n + 1 => n + 1 + T n

#eval T 4

example {n: ℕ} : T n = n * (n + 1) / 2 := by
  induction n with
  | zero =>
    calc
      T 0 = 0 := by rw [T]
      _ = 0 * (0 + 1) / 2 := by norm_num
  | succ n ih =>
    calc
      T (n + 1) = n + 1 + T n := by rw [T]
      _ = n + 1 + n * (n + 1) / 2 := by rw [ih]
      _ = (n + 1) * (n + 1 + 1) / 2 := by ring
    norm_cast

I will have to look up what exactly norm_cast does, but my primitive current understanding is that it "normalizes" coercions or smth like that.

[Ilmārs Cīrulis]

⊢ (↑n + 1) * (↑n + 1 + 1) / 2 = ↑(n + 1) * (↑(n + 1) + 1) / 2 - this means that you still have goal to prove. As one can see, left side isn't equal to right side.

[rzeta0]

I don't understand why Lean thinks the LHS and RHS are different.

[Ilmārs Cīrulis]

For example, (↑n + 1) and ↑(n + 1) are different.
The first is n converted to Q and then with rational number 1 added.
The second is n as natural number with natural number 1 added and then the sum converted to Q.

[rzeta0]

The only thing that comes to mind is to use brackets to get Lean to think of (n+1) as a unit. I tried that and it didn't work.

I also tried things like ((n + 1):ℚ) which also didn't work.

[rzeta0]

But in any case, I feel doing coercions is probably the wrong approach.

[Yaël Dillies]

(↑(n + 1) : ℚ) will do what you expect

[Dan Velleman]

The theorem Nat.cast_succ proves that ↑(n + 1) = (↑n + 1).

[Dan Velleman]

I suspect that you defined T n to be a rational number because your theorem was going to involve division by 2, and division is easier in Q than in N. But by using Q, you were forced to deal with coercions. An alternative would be to state your theorem as 2 * (T n) = n * (n + 1). Now there's no division, so no reason to use Q rather than N.

[rzeta0]

Thanks Ilmārs, Yaël and Dan.

Overall I feel that casting is an ugly "hack" - I will go away and think if there is a better way for what I had hoped would be a nice simple educational example.

If I can get the definition to be ℕ→ℕ that would avoid the casting, but then I need to solve ring failing.

[Dan Velleman]

And once you've proven the theorem in this new form, you could divide both sides by 2 to get the theorem you really wanted.

[rzeta0]

Hi @Dan Velleman - yes, 2*T is the approach I used when I previously defined Triangle as a proposition and that was ok - but I was hoping to avoid it at this later stage of the learning journey.

https://leanfirststeps.blogspot.com/2024/11/19-our-own-definition.html

[rzeta0]

Dan Velleman said:

And once you've proven the theorem in this new form, you could divide both sides by 2 to get the theorem you really wanted.

Interesting - I've never seen this done before.

(except MoPs cancel 2 at h)

[Dan Velleman]

For example, you could do this:

import Mathlib.Tactic

def T: ℕ → ℕ
  | 0 => 0
  | n + 1 => n + 1 + T n

lemma two_T {n: ℕ} : 2 * T n = n * (n + 1) := sorry

example {n : ℕ} : T n = n * (n + 1) / 2 :=
  calc T n
    _ = 2 * T n / 2 := by field_simp
    _ = n * (n + 1) / 2 := by rw [two_T]

Now you can fill in the sorry with an induction proof.

[Zhang Qinchuan]

You can first prove 2 * T n = n * (n + 1) and then divide both side by 2. This is exactly how mathlib handle Gauss' summation formula.

See docs#Finset.sum_range_id_mul_two and docs#Finset.sum_range_id.