# Zulip Chat Archive

## Stream: new members

### Topic: Recursive definition using some

#### Xavier Roblot (Feb 17 2023 at 13:00):

Is there a way to unfold a recursive definition using `some`

in its construction. For example, in the following #mwe, is there a way to recover the property used to construct the sequence?

```
import data.nat.basic
lemma double (n : ℕ) : ∃ m : ℕ, 2 * n < m := sorry
noncomputable def loop : ℕ → ℕ
| 0 := 1
| (n+1) := (double (loop n)).some
lemma bnd (n : ℕ) : 2^n < loop (n+1) :=
begin
dsimp [loop], -- fails
sorry,
end
```

#### Martin Dvořák (Feb 17 2023 at 13:01):

Your `bnd`

does not hold.

#### Reid Barton (Feb 17 2023 at 13:02):

You should start with `induction`

, or pattern matching

#### Xavier Roblot (Feb 17 2023 at 13:02):

Martin Dvořák said:

Your

`bnd`

does not hold.

Sure, but I can't even prove that :)

#### Martin Dvořák (Feb 17 2023 at 13:02):

You should start with realizing that `1 < 1`

is not true.

#### Martin Dvořák (Feb 17 2023 at 13:04):

Xavier Roblot said:

Martin Dvořák said:

Your

`bnd`

does not hold.Sure, but I can't even prove that :)

Failing to prove `P`

is not a way to prove `¬P`

is that is your aim.

#### Xavier Roblot (Feb 17 2023 at 13:04):

Martin Dvořák said:

Xavier Roblot said:

Martin Dvořák said:

Your

`bnd`

does not hold.Sure, but I can't even prove that :)

Failing to prove

`P`

is not a way to prove`¬P`

is that is your aim.

Ok, I'll fix the statement... but I think you're missing the point

#### Xavier Roblot (Feb 17 2023 at 13:07):

Reid Barton said:

You should start with

`induction`

, or pattern matching

Induction does not do help much. What do you mean by `pattern matching`

?

#### Reid Barton (Feb 17 2023 at 13:09):

The same thing you did to define `loop`

#### Reid Barton (Feb 17 2023 at 13:12):

Aren't you planning to prove the theorem by induction?

#### Xavier Roblot (Feb 17 2023 at 13:15):

Reid Barton said:

Aren't you planning to prove the theorem by induction?

Well, this is just a toy example, but what I'd you like to be able to do is to recover somehow the fact that `loop n < 2 * loop (n + 1)`

that is the property attached to the element `loop (n+1)`

and I cannot find a way to do that.

#### Reid Barton (Feb 17 2023 at 13:17):

#### Eric Wieser (Feb 17 2023 at 13:20):

I found it pretty hard to get `some_spec`

to work, because I can't prove anything useful abuot `loop (n + 1)`

:

```
import data.nat.basic
lemma double (n : ℕ) : ∃ m : ℕ, 2 * n < m := sorry
noncomputable def loop : ℕ → ℕ
| 0 := 1
| (n+1) := (double (loop n)).some
-- fails
lemma loop_succ (n) : loop (n + 1) = (double (loop n)).some := by rw loop
```

#### Xavier Roblot (Feb 17 2023 at 13:23):

Yes, this is the problem that I have...

#### Eric Wieser (Feb 17 2023 at 13:23):

Ah, this works:

```
lemma loop_succ (n) : loop (n + 1) = (double (loop n)).some :=
begin
rw [loop],
delta Exists.some classical.some classical.indefinite_description,
refl,
end
```

#### Eric Wieser (Feb 17 2023 at 13:25):

This looks like a bug in the equation compiler to me, it should have generated that lemma in the first place

#### Reid Barton (Feb 17 2023 at 13:27):

It looks like a bug in the equation compiler but the lemma should be true by rfl

#### Reid Barton (Feb 17 2023 at 13:27):

seems to be confused by the fact that it's noncomputable

#### Eric Wieser (Feb 17 2023 at 13:28):

It's maybe caused by `@[irreducible] noncomputable def indefinite_description`

#### Eric Wieser (Feb 17 2023 at 13:30):

Some more weirdness:

```
noncomputable def loop : ℕ → ℕ
| 0 := 1
| (n+1) := (double (loop n)).some
lemma loop_succ (n) : loop (n + 1) = (double (loop n)).some :=
begin
rw [loop],
show subtype.val _ = subtype.val _,
dsimp only [classical.indefinite_description],
delta classical.indefinite_description, -- why do I still need this?
refl,
end
```

`dsimp`

refuses to unfold a definition on the LHS but unfolds the same definition on the RHS

#### Reid Barton (Feb 17 2023 at 13:31):

With

```
noncomputable def loop (n : ℕ) : ℕ :=
nat.rec_on n 1 (fun _ l, (double l).some)
```

there aren't any more surprises

#### Xavier Roblot (Feb 17 2023 at 13:39):

Yes, that works! Thanks.

#### Kyle Miller (Feb 17 2023 at 13:41):

I've found that with `noncomputable`

recursive definitions you sometimes need to do `cases`

more times than you'd think to get things to be true by definition:

```
noncomputable def loop : ℕ → ℕ
| 0 := 1
| (n+1) := (double (loop n)).some
lemma loop_succ (n) : loop (n + 1) = (double (loop n)).some :=
by cases n; refl
```

#### Xavier Roblot (Feb 17 2023 at 13:47):

Kyle Miller said:

I've found that with

`noncomputable`

recursive definitions you sometimes need to do`cases`

more times than you'd think to get things to be true by definition:

In my original example, `cases`

is not enough but using `nat.rec_on`

does work

#### Eric Wieser (Feb 17 2023 at 13:50):

You should write the `loop_succ`

lemma first and then use it to prove your actual goal

#### Eric Wieser (Feb 17 2023 at 13:50):

Fighting the equation compiler shouldn't be something you mix with fighting induction and fighting `some_spec`

s

#### Reid Barton (Feb 17 2023 at 13:55):

Though, ideally, the equation compiler wouldn't need to be fought at all, at least in a case like this one

Last updated: Dec 20 2023 at 11:08 UTC