Zulip Chat Archive

Stream: new members

Topic: How would you define this sequence?


view this post on Zulip 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)

view this post on Zulip Kenny Lau (Jan 13 2021 at 09:36):

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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Huỳnh Trần Khanh (Jan 14 2021 at 05:56):

Thanks in advance.

view this post on Zulip 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)?

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Yakov Pechersky (Jan 14 2021 at 06:02):

You could use option for differentiating defined and undefined values.

view this post on Zulip Hanting Zhang (Jan 14 2021 at 06:02):

You can also use 37.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Hanting Zhang (Jan 14 2021 at 06:08):

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

view this post on Zulip Huỳnh Trần Khanh (Jan 14 2021 at 06:08):

Gimme a sec.

view this post on Zulip Yakov Pechersky (Jan 14 2021 at 06:09):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Yakov Pechersky (Jan 14 2021 at 06:18):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Huỳnh Trần Khanh (Jan 14 2021 at 06:21):

Thank you, that was really helpful! :heart:

view this post on Zulip 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!

view this post on Zulip Huỳnh Trần Khanh (Jan 14 2021 at 06:23):

I got it now.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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: May 08 2021 at 19:11 UTC