rw problem

Stream: lean4

[Zhang]

Hi,everyone! The rw tactic keeps failing when I solve the following problem.
Let ${a_n}$ be an arithmetic sequence with common difference $d$, and ${b_n}$ be a geometric sequence with common ratio $q$. Given that the summation of the first $n$ terms of ${a_n+b_n}$ is $S_n = n^2 - n + 2^n - 1$, show that $d + q$ is $4$.
Hint 1: Recall that a sequence is realized as type ℕ → ℝ, a function from natural numbers to real numbers, with indexing starting from $1$.
Hint 2: You are expected to use def to define arithmetic and geometric sequences.
Hint 3: Summation of a sequence can be defined using the ∑ notation.

import Mathlib
open Nat
open Real
open BigOperators

-- Define arithmetic sequence
def a_seq (n : ℕ) (a d : ℕ) : ℕ :=
a + (n - 1) * d

-- Define geometric sequence
def b_seq (n : ℕ) (b q : ℕ) : ℕ :=
b * q^(n - 1)

-- Define sum function S_n
def S_n (n : ℕ) : ℕ :=
n^2 - n + 2^n - 1

theorem sum_arithmetic (n : ℕ) (a d : ℕ) :
∑ i ∈ Finset.range n, (a + i * d) = n * a + (n * (n - 1) * d) / 2 := by
induction' n with k hk
· simp -- Base case: S_0 = 0

rw [Finset.sum_range_succ] -- Expand sum
rw [hk] -- Apply induction hypothesis
rw [add_comm ((k * (k - 1) * d) / 2) (a + k * d)]
rw [← add_assoc (k * a) a (k * d), ← add_mul]
rw [add_comm ((k * d) (k * (k - 1) * d) / 2) ]
have h_div : (k * (k - 1) * d) / 2 + k * d = ((k * (k - 1) + 2 * k) * d) / 2 := by
rw [← Nat.mul_add_div (by norm_num : 0 < 2)]
rw [mul_comm 2 k, ← add_mul]
rw [h_div]
-- Calculate k * (k - 1) + 2k = k * (k - 1 + 2) = k * (k + 1)
rw [Nat.add_sub_cancel]
rw [mul_comm k (k + 1)]
exact rfl

theorem sum_geometric (n : ℕ) (b q : ℕ) (h : q ≠ 1) :
∑ i ∈ Finset.range n, b * q^i = b * (1 - q^n) / (1 - q) :=
by
-- Handle the case when n = 0
cases n with k
· simp -- The case when n = 0 automatically holds (sum of zero terms)

-- Induction: start from n = 1
induction' k with k hk
· simp -- Handle the case when n = 1
rw [Finset.sum_range_succ] -- Split S_(k+1) = S_k + b * q^k
rw [hk] -- Induction hypothesis
rw [mul_sub, mul_one] -- Expand b * (1 - q^k)
rw [add_div (b * (1 - q^k)) (b * q^k) (1 - q)] -- Unify denominators
rw [← mul_add] -- Factor out b
rw [sub_add, add_sub_cancel]
exact rfl

And I'm still cofused about how to prove p+q=4.

[Aaron Liu]

Natural numbers start at 0

[Zhang]

How can I modify the code :working_on_it:

[Aaron Liu]

Can you give a #mwe

[Robin Arnez]

are you confused about this one?

a d k : ℕ
hk : ∑ i ∈ Finset.range k, (a + i * d) = k * a + k * (k - 1) * d / 2
⊢ k * a + k * (k - 1) * d / 2 + (a + k * d) = (k + 1) * a + (k + 1) * (k + 1 - 1) * d / 2

tactic 'rewrite' failed, did not find instance of the pattern in the target expression
  k * (k - 1) * d / 2 + (a + k * d)
a d k : ℕ
hk : ∑ i ∈ Finset.range k, (a + i * d) = k * a + k * (k - 1) * d / 2
⊢ k * a + k * (k - 1) * d / 2 + (a + k * d) = (k + 1) * a + (k + 1) * (k + 1 - 1) * d / 2

in that case, it fails because the goal actually has implicit parentheses, like this:
(k * a + k * (k - 1) * d / 2) + (a + k * d) = (k + 1) * a + (k + 1) * (k + 1 - 1) * d / 2
so you'll need add_assoc to move the parentheses the other way.

[Zhang]

Thank you,I got it.And still confused about this parthave h_div : (k * (k - 1) * d) / 2 + k * d = ((k * (k - 1) + 2 * k) * d) / 2 := by,since rw [← Nat.mul_add_div (by norm_num : 0 < 2)] keeps failing

[Ruben Van de Velde]

I suggest sharing a #mwe that shows the exact error you want help with

[Zhang]

rw [← Nat.mul_div_assoc (k * (k - 1)) (by norm_num : 0 < 2)]
tactic 'rewrite' failed, did not find instance of the pattern in the target expression
k * (k - 1) * (?m.3946 / ?m.3945)
a d k : ℕ
hk : ∑ i ∈ Finset.range k, (a + i * d) = k * a + k * (k - 1) * d / 2
⊢ k * (k - 1) * d / 2 + k * d = k * (k + 1) * d / 2Lean 4

[Aaron Liu]

Your parentheses are the wrong way

[Aaron Liu]

I can't try to debug a solution because you didn't post a #mwe

[Zhang]

import Mathlib

open Nat

open Real

open BigOperators
-- Define arithmetic sequence

def a_seq (n : ℕ) (a d : ℕ) : ℕ :=

a + (n - 1) * d
-- Define geometric sequence

def b_seq (n : ℕ) (b q : ℕ) : ℕ :=

b * q^(n - 1)
-- Define sum function S_n

def S_n (n : ℕ) : ℕ :=

n^2 - n + 2^n - 1

theorem sum_arithmetic (n : ℕ) (a d : ℕ) :

  ∑ i in Finset.range n, (a + i * d) = n * a + (n * (n - 1) * d) / 2 := by

  induction' n with k hk

  · simp -- Base case: S_0 = 0

  rw [Finset.sum_range_succ] -- Expand sum: S_{k+1} = S_k + (a + k * d)

  rw [hk] -- Apply induction hypothesis

  -- Rearranging terms correctly

  rw [add_assoc, add_comm (k * (k - 1) * d / 2) (a + k * d), ← add_assoc]

  have h_div : (k * (k - 1) * d) / 2 + k * d = (k * (k + 1)) * d / 2 := by

    rw [← Nat.mul_div_assoc (k * (k - 1)) (by norm_num : 0 < 2)]

[Kevin Buzzard]

The error is

  Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0))
    (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl false)
has type
  0 < 2 : Prop
but is expected to have type
  ?m.3945 ∣ ?m.3946 : Prop

and indeed you are feeding two arguments to Nat.mul_div_assoc and the second one should be a proof that something divides something, and you have instead fed it a proof that something is less than something. So the error is correct, expected, and telling you what you've done wrong.

[Kevin Buzzard]

If you hover over Nat.mul_div_assoc you are able to see all the explicit inputs and their types.