Как доказать обратный ноль ноль в Lean

Question

Я определил функцию реверса в списках, и я пытаюсь доказать тривиальное свойство, что реверс пустого списка пуст. Это должно быть доказуемо по рефлексивности:

def reverse (t : list α) : list α :=
list.rec_on t nil (λ x l r, r ++ [x])

#reduce reverse nil --outputs nil

lemma mylemma: reverse nil = nil := refl

однако, когда я запускаю этот код, я получаю ошибку:

don't know how to synthesize placeholder
context:
⊢ Type

Что это значит?

Answer 1

Lean не может определить тип пустого списка с правой стороны от контекста. Передайте аргумент типа явно:

lemma mylemma: reverse (nil) = @nil α :=
by refl