Simplification

Stream: new members

[Janitha]

import Mathlib
open Nat

def h : ℕ → Int
  | 0 => 2
  | 1 => 1
  | 2 => 5
  | n + 2 => h (n + 1) + 2 * h n


def g (n : ℕ) : Int := 2^n + (-1)^n

example (n : ℕ) : h n = g n ∧ h (n+1) = g (n+1) := by
  induction n with
  | zero =>
  constructor
  rfl
  rfl
  | succ k ih =>
  constructor
  apply ih.right
  calc
    h (k + 2) = h (k + 1) + 2 * h k := by {unfold h}
               _ = g (k + 1) + 2 * g k := by rw [ih.1, ih.2]
               _ = (2^(k + 1) + (-1)^(k + 1)) + 2 * (2^k + (-1)^k) := by rfl
               _ = 2^(k + 1) + (-1)^(k + 1) + 2 * 2^k + 2 * (-1)^k := by ring
               _ = 2^(k + 2) + (-1)^(k + 2) := by
                 simp only [pow_succ, pow_add, mul_comm]
                 ring


I get an error here: " h (k + 2) = h (k + 1) + 2 * h k := by {unfold h}" . How do I fix this proof?

[Matt Diamond]

the problem is that you've unnecessarily complicated things by explicitly defining the 2 case for h when it already follows from the rest of the definition

without that, rfl works just fine

import Mathlib
open Nat

def h : ℕ → Int
  | 0 => 2
  | 1 => 1
  | n + 2 => h (n + 1) + 2 * h n

def g (n : ℕ) : Int := 2^n + (-1)^n

example (n : ℕ) : h n = g n ∧ h (n+1) = g (n+1) := by
  induction n with
  | zero =>
  constructor
  rfl
  rfl
  | succ k ih =>
  constructor
  apply ih.right
  calc
    h (k + 2) = h (k + 1) + 2 * h k := by rfl
               _ = g (k + 1) + 2 * g k := by rw [ih.1, ih.2]
               _ = (2^(k + 1) + (-1)^(k + 1)) + 2 * (2^k + (-1)^k) := by rfl
               _ = 2^(k + 1) + (-1)^(k + 1) + 2 * 2^k + 2 * (-1)^k := by ring
               _ = 2^(k + 2) + (-1)^(k + 2) := by
                 simp only [pow_succ, pow_add, mul_comm]
                 ring

[Chris Wong]

What Matt said, but also: You can simplify the proof using induction n using Nat.twoStepInduction

[Chris Wong]

docs#Nat.twoStepInduction

[Chris Wong]

induction n using h.induct might work too

[Chris Wong]

import Mathlib
open Nat

def h : ℕ → Int
  | 0 => 2
  | 1 => 1
  | n + 2 => h (n + 1) + 2 * h n

def g (n : ℕ) : Int := 2^n + (-1)^n

example (n : ℕ) : h n = g n := by
  induction n using h.induct with
  | case1 => rfl
  | case2 => rfl
  | case3 k ih' ih =>
    calc
      h (k + 2) = h (k + 1) + 2 * h k := by rfl
                _ = g (k + 1) + 2 * g k := by rw [ih, ih']
                _ = (2^(k + 1) + (-1)^(k + 1)) + 2 * (2^k + (-1)^k) := by rfl
                _ = 2^(k + 1) + (-1)^(k + 1) + 2 * 2^k + 2 * (-1)^k := by ring
                _ = 2^(k + 2) + (-1)^(k + 2) := by ring

[Matt Diamond]

nice

[Chris Wong]

Using the "functional induction" feature described here: https://lean-lang.org/blog/2024-5-17-functional-induction/

[Janitha]

Got it, Thanks Matt and Chris! Could you please tell me, what if I didn't have the case `| 0 => 2 for h but the other three cases

| 1 => 1
| 2 => 5
| n + 2 => h (n + 1) + 2 * h n

and the functions h and g were from positive integers to positive integers? The reason why I defined explicitly for zero was I kept getting an error. I thought I'd prove what was in my code and do something with the restrictions of h and g to positive integers.

[Chris Wong]

Then it would be a type error, because Lean functions must be defined for _every_ value in the domain

[Chris Wong]

There is docs#PNat for positive integers, but I still recommend defining it for zero, because though it's not part of the original problem, it does make the proof easier and more general

[Chris Wong]

You might like to read this to see why such "junk values" are good practice: https://xenaproject.wordpress.com/2020/07/05/division-by-zero-in-type-theory-a-faq/

[Janitha]

I'm stuck at the "sorry." Can someone help? What's a good strategy in general at such steps?

import Mathlib

set_option exponentiation.threshold 5000

example {f : ℕ → ℕ}

(h1 : f 1 = 1) (h2 : ∀ n > 0, f (2 * n) = n * f n) : f (2 ^ 100) = 2 ^ 4950 := by

have h : ∀ n : ℕ, f (2^n) = 2^((n-1) * n / 2) := by

intro n

induction n with

| zero =>
-- Base case: f(2^0) = f(1) = 1

rw [pow_zero]

exact h1

| succ n ih =>

calc

f (2 ^ (n + 1))

= f (2 * 2 ^ n) := by

rw [pow_succ, mul_comm]

_ = (2 ^ n) * f (2 ^ n) := by

apply h2

apply pow_pos

norm_num

_ = (2 ^ n) * (2 ^ ((n - 1) * n / 2)) := by

rw [ih]

_ = 2 ^ (n + ((n - 1) * n / 2)) := by

ring_nf

_ = 2 ^ (((n + 1 - 1) * (n + 1)) / 2) := by

sorry

exact h 100

[Janitha]

I'm having trouble filling the "sorry", please help.

import Mathlib

set_option exponentiation.threshold 5000

example {f : ℕ → ℕ}

(h1 : f 1 = 1) (h2 : ∀ n > 0, f (2 * n) = n * f n) : f (2 ^ 100) = 2 ^ 4950 := by

have h : ∀ n : ℕ, f (2^n) = 2^((n-1) * n / 2) := by

intro n

induction n with

| zero =>
-- Base case: f(2^0) = f(1) = 1

rw [pow_zero]

exact h1

| succ n ih =>

calc

f (2 ^ (n + 1))

= f (2 * 2 ^ n) := by

rw [pow_succ, mul_comm]

_ = (2 ^ n) * f (2 ^ n) := by

apply h2

apply pow_pos

norm_num

_ = (2 ^ n) * (2 ^ ((n - 1) * n / 2)) := by

rw [ih]

_ = 2 ^ (n + ((n - 1) * n / 2)) := by

ring_nf

_ = 2 ^ (((n + 1 - 1) * (n + 1)) / 2) := by

sorry

exact h 100

[Sabbir Rahman]

The problem is that Natural division is floor division in lean, so ring can't really work "across" natural divisions, you can try using theorems like add_mul_div_left which works with natrual division

[Ruben Van de Velde]

Please read #backticks and edit your message

[Ruben Van de Velde]

And can a maintainer merge this with https://leanprover.zulipchat.com/#narrow/channel/113489-new-members/topic/Simplification please, double posting wastes the time of people trying to help you

[Bjørn Kjos-Hanssen]

This works...

      congr
      symm
      nth_rewrite 1 [mul_comm]
      nth_rewrite 2 [mul_comm,add_comm]
      apply Nat.div_eq_of_eq_mul_right
      simp
      rw [mul_add]
      cases n with
      | zero => simp
      | succ n =>
        simp
        have : 2 * ((n + 1) * n / 2) = (n+1) * n := by
          nth_rewrite 1 [mul_comm]
          refine Nat.div_two_mul_two_of_even ?_
          refine Nat.even_mul.mpr ?_
          by_cases H : Even n
          · tauto
          · left
            exact Nat.even_add_one.mpr H
        linarith

[Janitha]

Hi Professor Bjorn. It worked. Thanks!

[Notification Bot]

15 messages were moved here from #lean4 > A proof by induction by Kim Morrison.