theorem-proving - 如何在精益中证明反向零是零

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

精益无法从上下文推断右侧空列表的类型。显式传递类型参数：

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