Recursion proof

Stream: new members

[Bjørn Kjos-Hanssen]

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

[Yakov Pechersky]

does "rfl" work?

[Yakov Pechersky]

BTW this is docs#list.repeat

[Bjørn Kjos-Hanssen]

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

[Bjørn Kjos-Hanssen]

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

[Yakov Pechersky]

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]

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

[Patrick Johnson]

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