Hacky induction - are there alternatives?

Stream: new members

[Alex Brodbelt]

When trying to induct on the odd numbers of the form (n = 2*w +1), I had the issue again that induction step requires me to prove that the assumptions involving n hold rather than succ n which I think is rather impossible to do. A hack someone found was to clear the hypothesis involving n - see clear hn' and clear hn lines, before inducting on w.
But I was wondering if there is a cleaner way of doing this?

On the other hand, I was wondering if there is an easier way of doing computations that involve subtracting natural numbers (see the sorry), is there any tactic that works? simp does not help much, and doing it by hand is rather a lot of effort for what I think it should be. Should I maybe assume prove it for the integers and state that we only consider integers greatar than or equal to zero, so then I can use the ring tactic?

import Mathlib.Data.Nat.Factorization.Basic
import Mathlib.Data.Nat.Prime
import Mathlib.Algebra.BigOperators.Basic
import Mathlib.Algebra.Group.Basic

open Nat

open Finset

open BigOperators

variable {a b x q n : ℕ}

theorem question_5 (nodd : Odd n)(hx : 1 ≤ x)(hn : 2 ≤ n) : x^n + 1 = (x + 1) * (1 + ∑ k in range ((n - 1) / 2), x^(k + 1) * (x - 1)  ) := by
  rcases nodd with ⟨w, hn'⟩
  rw [hn']
  have hw : 1 ≤ w := by
    rw [hn'] at hn
    linarith
  clear hn'
  clear hn
  -- Simplify (2 * w + 1 - 1) / 2 to be w
  rw [Nat.add_sub_assoc, Nat.sub_self, add_zero]
  nth_rewrite 2 [mul_comm 2 w]
  rw [Nat.mul_div_cancel]
  repeat' linarith
  induction' w, hw using Nat.le_induction with w _hw ih
  · simp
    rw [
      ← succ_eq_add_one 2, add_comm, Nat.mul_sub_left_distrib, ← sq, mul_one,
      add_mul, one_mul, mul_add, Nat.mul_sub_left_distrib, add_assoc,
      ← sq, ← Nat.pow_succ', add_comm (x^(succ 2) - x^2), mul_one, ← add_assoc,
      computation_helper_q5, ← Nat.add_sub_assoc, add_assoc, add_comm (x^2), ← add_assoc,
      Nat.add_sub_assoc, Nat.sub_self, add_zero
      ]
    · exact le_refl (x^2)
    · apply pow_le_pow_right hx
      linarith
    · exact hx
    -- Modify LHS
  · rw [mul_add 2, mul_one]
    -- Modify RHS
    rw [Finset.sum_range_succ, ← add_assoc 1, add_comm _ (x ^ (w + 1) * (x - 1)), mul_add (x + 1), ← ih]
    sorry

[Riccardo Brasca]

The result is false, you can see this using slim_check

[Riccardo Brasca]

Anyway to get rid of natural subtraction you can use zify [hx].

[Alex Brodbelt]

Riccardo Brasca said:

The result is false, you can see this using slim_check

You are right! thanks - here is the corrected statement which is proved, but a bit ugly(?). How could I write the induction more cleanly rather than having to clear the hypothesis involving n?

import Mathlib.Data.Nat.Factorization.Basic
import Mathlib.Data.Nat.Prime
import Mathlib.Algebra.BigOperators.Basic
import Mathlib.Algebra.Group.Basic

open Nat

open Finset

open BigOperators

variable {a b x q n : ℕ}

lemma computation_helper_q6 : 2*w + 1 = 1 ↔ w = 0 := by
  constructor
  · intro h
    nth_rewrite 2 [← zero_add 1] at h
    have h₁ : 2*w  = 0 := by rw [add_right_cancel h]
    cases Nat.mul_eq_zero.mp h₁
    case inl h' => contradiction
    case inr h' => exact h'
  · intro h
    rw [h, mul_zero, zero_add]

theorem question_5 (nodd : Odd n)(hx : 1 ≤ x)(hn : 2 ≤ n) : x^n + 1 = (x + 1) * (1 + ∑ k in range ((n - 1) / 2), x^(2*k + 1) * (x - 1)  ) := by
  rcases nodd with ⟨w, hn'⟩
  rw [hn']
  have hx' : 1 ≤ x^2 := by
    rw [← one_mul 1, sq]
    apply mul_le_mul'
    repeat' exact hx
  have hw : 1 ≤ w := by
    rw [hn'] at hn
    linarith
  clear hn'
  clear hn
  -- Simplify (2 * w + 1 - 1) / 2 to be w
  rw [Nat.add_sub_assoc, Nat.sub_self, add_zero]
  nth_rewrite 2 [mul_comm 2 w]
  rw [Nat.mul_div_cancel]
  repeat' linarith
  induction' w, hw using Nat.le_induction with w _hw ih
  · simp
    rw [
      ← succ_eq_add_one 2, add_comm, Nat.mul_sub_left_distrib, ← sq, mul_one,
      add_mul, one_mul, mul_add, Nat.mul_sub_left_distrib, add_assoc,
      ← sq, ← Nat.pow_succ', add_comm (x^(succ 2) - x^2), mul_one, ← add_assoc,
      computation_helper_q5, ← Nat.add_sub_assoc, add_assoc, add_comm (x^2), ← add_assoc,
      Nat.add_sub_assoc, Nat.sub_self, add_zero
      ]
    · exact le_refl (x^2)
    · apply pow_le_pow_right hx
      linarith
    · exact hx
    -- Modify LHS
  · rw [mul_add 2, mul_one]
    -- Modify RHS
    rw [
      Finset.sum_range_succ, ← add_assoc 1, mul_add (x + 1), ← ih,
      mul_comm (x + 1), mul_assoc, ← difference_of_squares, add_assoc _ 1, add_comm 1,
      ← add_assoc]
    nth_rewrite 1 [← mul_one (x^(2*w + 1))]
    rw [
      ← mul_add, ← Nat.add_sub_assoc, add_comm 1, Nat.add_sub_assoc, Nat.sub_self,
      add_zero,← pow_add, add_assoc (2*w) 1 2 ,add_comm 1 2, ← add_assoc
      ]
    · linarith
    · exact hx'

[Riccardo Brasca]

Note that there is a computation_helper_q5 that makes your example not working, but let me try to write a cleaner proof.

[Alex Brodbelt]

Riccardo Brasca said:

Note that there is a computation_helper_q5 that makes your example not working, but let me try to write a cleaner proof.

sorry, I have now added in computation_helper_5

[Riccardo Brasca]

I would prove it like this

import Mathlib.Data.Nat.Factorization.Basic
import Mathlib.Data.Nat.Prime
import Mathlib.Algebra.BigOperators.Basic
import Mathlib.Algebra.Group.Basic

open Nat

open Finset

open BigOperators

variable {a b x q n : ℕ}

theorem question_5 (nodd : Odd n)(hx : 1 ≤ x)(hn : 2 ≤ n) :
    x^n + 1 = (x + 1) * (1 + ∑ k in range ((n - 1) / 2), x^(2*k + 1) * (x - 1)  ) := by
  rcases nodd with ⟨w, rfl⟩
  simp only [add_tsub_cancel_right, zero_lt_two, mul_div_right]
  zify [hx]
  calc _ = ((x : ℤ) + 1) + (∑ i in _, _) * (x ^ 2 - 1) * x := by rw [geom_sum_mul]; ring
  _ = _ := by simp_rw [pow_add, pow_mul, ← Finset.sum_mul]; ring

[Riccardo Brasca]

The point is to use docs#geom_sum_mul

[Riccardo Brasca]

Concerning your previous questions: rcases nodd with ⟨w, rfl⟩ is the same as

rcases nodd with ⟨w, hw⟩
subst hw --this rewrite hw everywhere and discard it

It is a common trick.

[Riccardo Brasca]

Note also the zify [hx] line, that saves you from all the pain of natural subtraction.

[Ruben Van de Velde]

That would be subst hm without the brackets

[Riccardo Brasca]

Ops

[Riccardo Brasca]

I also used quite a lot of _, that is also a standard trick: it means "Lean, please, replace the underscore with the obvious thing". Sometimes it works very well, sometimes no, but it is worth to try.

[Riccardo Brasca]

Wait, hn : 2 ≤ n is not used (the proof works without it). Why isn't the linter complaining?

[Riccardo Brasca]

Ah, rlf touches it

[Riccardo Brasca]

It is again this issue, in some form

[Alex Brodbelt]

Riccardo Brasca said:

I also used quite a lot of _, that is also a standard trick: it means "Lean, please, replace the underscore with the obvious thing". Sometimes it works very well, sometimes no, but it is worth to try.

Sorry, I was a bit busy with assignments and so on - thank you, all of this is very instructive to me! I will keep all of this in mind!