Search code examples
theorem-provingformal-verificationlean

How to prove reverse nil is nil in Lean

I have defined a reverse function on lists, and I am trying to prove the trivial property that reverse of an empty list is empty. It should be provable by reflexivity: 

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

however, when I run this code, I get an error:

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

What does this mean?

Solution

  • Lean cannot infer the type of the empty list on the right-hand side from context. Pass the type argument explicitly:

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