## Stream: new members

### Topic: How would you define this sequence?

#### Huỳnh Trần Khanh (Jan 13 2021 at 09:35):

def sequence1 : ℕ → ℝ
| 0 := 6
| n := have n - 1 < n, from sorry,
5 + sequence1 (n - 1)


#### Kenny Lau (Jan 13 2021 at 09:36):

def sequence1 : ℕ → ℝ
| 0 := 6
| (n+1) := 5 + sequence1 n


#### Huỳnh Trần Khanh (Jan 13 2021 at 11:16):

One more question: how does Lean know that this recursion is well founded without me having to supply a proof?

#### Johan Commelin (Jan 13 2021 at 11:50):

It runs an automated check in the background. Usually this works, but if it doesn't there is an option to provide a proof manually.

#### Huỳnh Trần Khanh (Jan 14 2021 at 05:55):

How would you prove that sequence1 n = (some closed form expression)? Through induction right? I tried to rewrite and unfold but the goal then transformed into some Lisp-like gobbledygook and I didn't know how to proceed.

#### Huỳnh Trần Khanh (Jan 14 2021 at 05:59):

Also how would you define the 1-indexed variant of sequence1 (sequence1 1 = 6, sequence1 (n + 1) = 5 + sequence1 n and sequence1 0 is not defined)?

#### Huỳnh Trần Khanh (Jan 14 2021 at 06:00):

Should I just supply a garbage value for sequence1 0, let's say 998244353 and call it a day?

#### Hanting Zhang (Jan 14 2021 at 06:02):

Have you tried the natural number game? To do induction you use induction n with k ih, or cases n.

#### Yakov Pechersky (Jan 14 2021 at 06:02):

You could use option for differentiating defined and undefined values.

#### Hanting Zhang (Jan 14 2021 at 06:02):

You can also use 37.

#### Yakov Pechersky (Jan 14 2021 at 06:02):

Or make sure that all crucial lemmas describing your function take a hypothesis that the input is positive.

#### Huỳnh Trần Khanh (Jan 14 2021 at 06:06):

Yeah induction n with d induction_hypothesis is what I use. How do I "unfold" the function definition so that I can apply the usual tactics such as rw, ring and resolve the goal?

#### Hanting Zhang (Jan 14 2021 at 06:08):

Can you give a MWE of what you're trying to do?

Gimme a sec.

#### Yakov Pechersky (Jan 14 2021 at 06:09):

I'm not sure how you're expressing the idea of "closed form expression" here.

#### Huỳnh Trần Khanh (Jan 14 2021 at 06:15):

Alright so here is my code:

import data.nat.basic
import data.real.basic

def sequence1 : ℕ → ℕ
| 0 := 6
| (n + 1) := 5 + sequence1 n

lemma closed_form { n : ℕ } : sequence1 n = 5 * (n + 1) + 1 := begin
induction n with d hd,
{
have evaluate_right_hand_side : 5 * (0 + 1) + 1 = 6 := begin
ring,
end,

rw evaluate_right_hand_side,

-- I am stuck here
sorry,
},
{
sorry,
}
end


#### Yakov Pechersky (Jan 14 2021 at 06:17):

lemma closed_form {n : ℕ} : sequence1 n = 5 * (n + 1) + 1 :=
begin
induction n with d hd,
{ norm_num [sequence1] },
{ rw [sequence1, hd],
norm_num,
ring }
end


#### Yakov Pechersky (Jan 14 2021 at 06:18):

norm_num deals with numerical calculations for nats, ints, rats, reals, and coercions thereof

#### Yakov Pechersky (Jan 14 2021 at 06:18):

and I give sequence1 to the things it knows about so it can deal with sequence1 0.

#### Hanting Zhang (Jan 14 2021 at 06:19):

When you have

case nat.zero
⊢ 0.sequence1 = 5 * 0 + 6


sequence1 0 is definitionally equal to 6, because you defined it like that, you don't have to unfold it.

#### Yakov Pechersky (Jan 14 2021 at 06:20):

In the inductive case, you have sequence1 d.succ, which rw sequence1 changes to 5 + sequence1 d by the definition of sequence1. Then rw hd uses the inductive hypothesis to change that into whatever statement. norm_num makes it all happy by dealing with the coerced d.succ now, and then finish with ring to combine terms.

#### Huỳnh Trần Khanh (Jan 14 2021 at 06:21):

Thank you, that was really helpful! :heart:

#### Huỳnh Trần Khanh (Jan 14 2021 at 06:23):

Hanting Zhang said:

When you have

case nat.zero
⊢ 0.sequence1 = 5 * 0 + 6


sequence1 0 is definitionally equal to 6, because you defined it like that, you don't have to unfold it.

Thanks! And therefore refl also works for the base case!

I got it now.

#### Huỳnh Trần Khanh (Jan 14 2021 at 08:04):

Now I'm fed up with counting from 0, LOL. How would you prove the same thing, but with the base case being 1 := 6?

import data.nat.basic
import data.real.basic

def sequence1 : ℕ → ℕ
| -- what to put here, 0 := 998244353? but then norm_num would fail to work
-- 998244353 is every competitive programmer's favorite integer
-- see https://codeforces.com/blog/entry/62541
| 1 := 6
| (n + 1) := 5 + sequence1 n

lemma closed_form { n : ℕ } : 1 ≤ n → sequence1 n = 5 * n + 1 := begin
-- nat.le_induction should work right
apply nat.le_induction,
{
norm_num [sequence1],
},
{
intro n,
intro bound,
intro induction_hypothesis,

norm_num [sequence1],
ring,
ring at induction_hypothesis,
rw induction_hypothesis,
}
end


#### Yakov Pechersky (Jan 14 2021 at 08:09):

import data.nat.basic
import data.real.basic

def sequence1 : ℕ → ℕ
| 0 := 0
| 1 := 6
| (n + 1) := 5 + sequence1 n

lemma closed_form {n : ℕ} (hpos : 0 < n) : sequence1 n = 5 * n + 1 :=
begin
cases n,
{ exact absurd hpos (lt_irrefl _) },
{ induction n with n hn,
{ simp [sequence1] },
{ rw [sequence1, hn nat.succ_pos'],
ring } }
end


#### Yakov Pechersky (Jan 14 2021 at 08:16):

What was nice here is expressing the constraint hpos in the more mathlib friendly way, which is 0 < n instead of 1 \le n. Then, one discharges the first case of n = 0 by showing that 0 < 0 leads to a contradiction, easily via lt_irrefl.

Last updated: May 08 2021 at 19:11 UTC