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

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