How would you define this sequence?

Stream: new members

[Huỳnh Trần Khanh]

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

[Kenny Lau]

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

[Huỳnh Trần Khanh]

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

[Johan Commelin]

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]

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

[Huỳnh Trần Khanh]

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]

Thanks in advance.

[Huỳnh Trần Khanh]

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]

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

[Hanting Zhang]

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

[Yakov Pechersky]

You could use option for differentiating defined and undefined values.

[Hanting Zhang]

You can also use 37.

[Yakov Pechersky]

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

[Huỳnh Trần Khanh]

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]

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

[Huỳnh Trần Khanh]

Gimme a sec.

[Yakov Pechersky]

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

[Huỳnh Trần Khanh]

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]

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]

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

[Yakov Pechersky]

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

[Hanting Zhang]

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]

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]

Thank you, that was really helpful! :heart:

[Huỳnh Trần Khanh]

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]

I got it now.

[Huỳnh Trần Khanh]

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]

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]

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.