## Stream: new members

### Topic: Recursion proof

#### Bjørn Kjos-Hanssen (Jul 07 2022 at 23:47):

noncomputable def constant_list : α → ℕ → list α
|z 0 := []
|z (n+1) := z :: (constant_list z n)

theorem ridiculous (z:α) (n:ℕ):
constant_list z (n+1) = z :: (constant_list z n) := sorry


This shouldn't really require a proof but here we are...

does "rfl" work?

#### Yakov Pechersky (Jul 07 2022 at 23:57):

BTW this is docs#list.repeat

#### Bjørn Kjos-Hanssen (Jul 08 2022 at 00:13):

"rfl" does not work... but thanks for mentioning list.repeat

#### Bjørn Kjos-Hanssen (Jul 08 2022 at 00:17):

Hmm, "rfl" works if I use n.succ instead of n+1, and list.repeat... thanks @Yakov Pechersky !

#### Yakov Pechersky (Jul 08 2022 at 00:19):

n+1 doesn't work because you haven't imported anything, and n.succ is the other inductive constructor. n+1 works usually because it's marked as a pattern somewhere. Don't remember where.

#### Patrick Johnson (Jul 08 2022 at 00:20):

rfl doesn't work because you unnecessarily marked constant_list as noncomputable

#### Patrick Johnson (Jul 08 2022 at 00:21):

Remove noncomputable and it will work:

variable {α : Type*}

def constant_list : α → ℕ → list α
|z 0 := []
|z (n+1) := z :: (constant_list z n)

theorem ridiculous (z:α) (n:ℕ):
constant_list z (n+1) = z :: (constant_list z n) := rfl


Last updated: Dec 20 2023 at 11:08 UTC