simple algebra

Stream: Is there code for X?

[Mattia Bottoni]

Hi everybody!
I would like to teach my students to do induction with Lean. The goal is not to have an efficient way to prove it in Lean but to be as thorough with the proof as possible. In all three exercises I come quite far, but I always fail to do some simple algebra in Lean to make it understand that the LHS is equal to the RHS. These are the exercises:

import Mathlib.Tactic

variable (n : ℕ)

open Nat
open BigOperators
open Finset

--exercise 3.1
example : (∑ k in range (n+1), k)^2 = ∑ k in range (n+1), k^3 := by
induction' n with d hd
rw [sum_range_one]
rw [sum_range_one]
simp
rw [sum_range_succ]
rw [add_sq]
rw [hd]
rw [succ_eq_add_one]
conv_rhs => rw [sum_range_succ]
rw [add_assoc]
rw [add_left_cancel_iff]
rw [sum_range_id] --Gauss summation formula!
simp
rw [← mul_div (d+1) d 2] --this is where I struggle
--rw [mul_div (d+1) d 2]
--rw [← mul_assoc 2 (d + 1) d / 2]
sorry
done


--exercise 3.2
example : 6 ∣ (n^3 - n) := by
induction' n with d hd
rw [pow_three]
rw [Nat.zero_mul]
rw [Nat.sub_zero]
exact Nat.dvd_zero 6
rw [succ_eq_add_one]
ring_nf
rw [← Nat.sub_sub]
rw [Nat.add_assoc]
rw [Nat.add_assoc]
rw [Nat.add_sub_self_left]
rw [← Nat.add_assoc]
rw [Nat.add_sub_assoc]
rw [← Nat.dvd_add_iff_left hd]
rw [← add_mul]
rw [pow_two]
rw [← mul_one_add] --How can I say that either d or (d+1) must be even?
--by_cases d = 2*k
sorry
rw [Nat.le_self_pow] --I don't know why I get an error message here
done

--exercise 3.3
example (k : ℕ) : (x + y) ^ n = ∑ k in range (n + 1), x^(n - k) * y^k * Nat.choose k n := by
induction' n with d hd
rw [Nat.pow_zero]
rw [Nat.zero_add]
rw [sum_range_one]
rw [Nat.choose_zero_right]
rw [Nat.pow_zero]
rw [Nat.pow_zero]
rw [succ_eq_add_one]
rw [pow_add]
rw [hd]
rw [pow_one]
rw [mul_add]
rw [sum_range_succ] --I want Lean to do this only to the first sum on the lhs
rw [Nat.choose_self]
rw [mul_one]
rw [add_comm]
rw [add_mul]
rw [Nat.sub_self]
rw [Nat.pow_zero]
rw [one_mul]
rw [← pow_one y]
rw [← pow_mul]
rw [one_mul]
rw [← pow_add]
conv_lhs => rw [sum_range_succ'] --and this to the second sum on the lhs
sorry
done

I know that in the first exercises the problem is that /2 is not defined for natural numbers, but I don’t know how to deal with it. In exercise two I would like first to consider d to be even and then (d+1). Then I would just need to multiply the 3 on the RHS with the 2 of the even definition and 6 would divide this term. For the last exercise I am following this proof:

Binomialtheorem.png

But the problem is that when I want to “take out” the last term first sum on the LHS, Lean takes it out in both sums. How can I make it that just the first sum is edited?
Thank you all in advance for your help!

All the best
Matt

[Kevin Buzzard]

Here is how I would solve your first question in Lean. I start by proving intermediate results over $\mathbb{Q}$, where subtraction and division behave normally, and then it's easy to deduce your result using the qify tactic.

import Mathlib.Tactic

variable (n : ℕ)

open Nat
open BigOperators
open Finset

lemma aux1 : ∑ k in range n, (k : ℚ) = (n : ℚ) * (n - 1) / 2 := by
  induction n with
  | zero => simp
  | succ d ih =>
    rw [sum_range_succ, ih, succ_eq_add_one]
    push_cast
    ring

lemma aux2 : ∑ k in range n, (k : ℚ) ^3 = ((n : ℚ) * (n - 1) / 2) ^ 2 := by
  induction n with
  | zero => simp
  | succ d ih =>
    rw [sum_range_succ, ih, succ_eq_add_one]
    push_cast
    ring

-- remark: aux1 and aux2 have exactly the same proof.

example : (∑ k in range (n+1), k)^2 = ∑ k in range (n+1), k^3 := by
  qify
  rw [aux1, aux2]

[Kevin Buzzard]

Your second and third statements have natural subtraction in the statement, so I would like to claim that they do not formally represent the statements which you think they say. The symbol - on natural numbers should not be thought of as what a mathematician means by subtraction, because no mathematician thinks that 2 - 3 = 0 whatever a type theorist says. I don't care about claims of the form "in every case, I can prove that a<=b, so b-a makes sense". I believe that to formally represent the meaning of such statements correctly (in the eyes of mathematicians) you should be coercing into the integers or rationals in the statements, as I have done with my solution to your first question.

[Mattia Bottoni]

Thank you very much for your feedback! I will think about that :)