Recursive definition using some

Stream: new members

[Xavier Roblot]

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]

Your bnd does not hold.

[Reid Barton]

You should start with induction, or pattern matching

[Xavier Roblot]

Martin Dvořák said:

Your bnd does not hold.

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

[Martin Dvořák]

You should start with realizing that 1 < 1 is not true.

[Martin Dvořák]

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]

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]

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]

The same thing you did to define loop

[Reid Barton]

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

[Xavier Roblot]

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]

docs#Exists.some_spec

[Eric Wieser]

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]

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

[Eric Wieser]

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]

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

[Reid Barton]

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

[Reid Barton]

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

[Eric Wieser]

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

[Eric Wieser]

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]

With

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

there aren't any more surprises

[Xavier Roblot]

Yes, that works! Thanks.

[Kyle Miller]

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]

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]

You should write the loop_succ lemma first and then use it to prove your actual goal

[Eric Wieser]

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

[Reid Barton]

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