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

docs#Exists.some_spec

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

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