# Zulip Chat Archive

## 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.

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

@Huỳnh Trần Khanh https://leanprover-community.github.io/extras/well_founded_recursion.html for more info

#### 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:56):

Thanks in advance.

#### 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?

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

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!

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

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: Dec 20 2023 at 11:08 UTC